Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ 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.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ 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 $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -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 $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

The Role of Participation in Innovation Contests: Multiple Rewards Are Optimal Exactly When Entry Is Costly, the Budget Is Large and a Failed Contest Is CostlyResearch Paper

Why reward design depends on entry

An innovation contest asks people outside a firm to submit solutions and promises payments according to the rank of their submissions. The firm would like a strong best submission, but a potential solver must decide whether entering is worth a fixed cost before knowing who else will enter. Paying only the winner can encourage effort while leaving the contest with no entries. Paying several ranks can make entry more attractive while spreading the reward budget across more people. Stouras, Hutchison-Krupat and Chao study that tradeoff in a model where the firm values the best solution and pays a penalty if the contest receives none (accepted SSRN version, Sections 3–5.1).

The question is operational: given a budget and entry cost, how many ranks should receive a positive reward? The paper's Theorem 2 describes regimes in which a winner-take-all allocation is optimal and regimes in which the optimum pays several ranks. Its supporting results connect the equilibrium entry threshold to the number of entrants and identify allocations that maximize participation (Theorems 1–2, pp. 10–12).

Contest and ability model

There are $n$ potential solvers, with $n\ge2$ . Their abilities $A_i$ are independent draws from a common distribution on $[0,1]$ with CDF $F$ and continuous, strictly positive density $f$ . A solver who exerts effort $e\ge0$ produces performance $x=ae$ when their ability is $a$ . The marginal cost of effort is one. Entry also costs $c_p$ , so performance $x$ costs $x/a+c_p$ for a solver with $a>0$ (model setup, pp. 6–7).

An allocation $r$ lists rank rewards $r_1\ge\cdots\ge r_n\ge0$ with $\sum_{j=1}^n r_j\le B$ , where $B$ is the firm's budget. Rank one is the best submission. A rank beyond the number of entrants receives no payment. The number $m(r)$ of rewards is the count of strictly positive entries in that list, including tied positive payments at different ranks.

Given $r$ , the paper's symmetric equilibrium has an ability threshold $a_{\min}(r,c_p)$ : a solver enters precisely when $a\ge a_{\min}$ . The expected rank reward $R_r(a)$ determines that threshold, and the paper gives an integral expression for the resulting equilibrium performance $x_r^*(a)$ (Proposition 1, p. 8). Both quantities depend on the entire announced allocation. The independent ability profile has the product law of the density on $[0,1]$ . If $N$ is the number entering, the failure probability is $\Pr(N=0)$ .

The firm's objective is equation (6), with failure cost $c_f\ge0$ :

\Pi(r;c_p,c_f)=\mathbb E\!\left[\max_{1\le i\le n}\{x_r^*(A_i)\mathbf 1_{\{A_i\ge a_{\min}(r,c_p)\}}\}\right]-c_f\Pr_r(N=0).

Every allocation comparison recalculates $a_{\min}$ , $x^*$ , and the failure probability. An optimal allocation maximizes this objective over every feasible $r$ , including allocations that spend less than the budget.

Formalization targets

The main target is Theorem 2, including existence of an optimum. For $c_p=0$ , every positive budget and nonnegative failure cost have an optimum, and every optimum pays exactly one rank. For $c_p>0$ , the corrected statement asserts thresholds $\widehat c_p>c_p$ and, for each budget $c_p<B<n c_p$ , a threshold $\widehat c_f>0$ such that every optimum satisfies

B<\widehat c_p\ \text{or}\ c_f<\widehat c_f\quad\Longrightarrow\quad m(r^*)=1,

\widehat c_p<B\ \text{and}\ \widehat c_f<c_f\quad\Longrightarrow\quad 2\le m(r^*)\le m_p^*(B).

Here $m_p^*(B)$ is the largest number of equal awards that maximizes participation. The same two thresholds govern both clauses. Equality at a threshold is left open because allocations can tie there. The bound $B<n c_p$ is the paper's constrained-budget regime, stated in its discussion and used in its threshold proof (Theorem 1 and its discussion, p. 10; proof of Proposition 1, p. 23). At $n=2$ , this regime may have no multi-reward case; the conditional statement retains the paper's population range.

The milestone results include the rank-probability identity (EC.3), the binomial law for the number of entrants (Proposition 2), the equal-award participation optimum (Theorem 1), attainment of the firm's maximum, and the claim that winner take all maximizes the first, performance term of $\Pi$ (Electronic Companion and proofs, pp. ec1, 9–10, 28).

What the result supplies

The theorem separates the firm's two aims in a precise way: a positive entry cost and a sufficiently consequential failure can justify paying more than the top rank, while the participation-maximizing number $m_p^*$ bounds how far the firm should spread rewards. The result is a statement about all optimal feasible allocations, not merely a comparison of a few equal-split choices. It also identifies the number of entrants through a binomial law, so the failure event has an explicit probability (Proposition 2, p. 9).

The paper presents these results and their arguments, but this mission's statements still require Lean proofs. A complete formalization would connect the rank and participation formulas to the objective evaluated on independent ability profiles, and establish existence and the design regimes. The order-statistic definitions and product-measure treatment of the ability population can be reused in other contest models.

Mathematical difficulty

The obvious thought is to maximize performance and participation separately, then compare their best allocations. That does not settle the firm's problem because changing a reward changes the entry threshold and the performance schedule at the same time. In particular, the performance term under partial entry cannot be replaced by its guaranteed-entry counterpart: entrants are selected by ability, and the selection threshold moves with the allocation. The printed proof of Theorem 2 cites a guaranteed-entry result at this point, leaving a substantive partial-entry comparison for the mission (proof of Theorem 2, pp. 27–28; Theorem EC.2, p. ec5).

Formalization scope

Lean uses natural-number ranks $1,\ldots,n$ , real abilities and rewards, and the density-based measure on $[0,1]$ whose finite product gives independent solver abilities. The order-statistic CDF is a binomial sum; its empty-range value is zero. The participation threshold is the least $a\in[0,1]$ for which expected rank reward reaches $c_p$ , with value one when that set is empty. The submission schedule is equation (4), and the firm's objective is the expectation in equation (6), not its later reduced integral form. A finite maximum over the $n$ solvers represents the best submission. Only positive rewards count toward $m(r)$ ; the unused rank-zero coordinate and rewards above rank $n$ are fixed at zero. At ability zero, division by ability is avoided in the submitted definitions.

The source's proof introduces an additional constraint that $\Pi\ge0$ , even though Theorem 2 does not require it and a large failure cost can make it impossible. The mission keeps the original feasible set with $\sum r_j\le B$ and no sign restriction on $\Pi$ . This prevents a formally easy but vacuous optimum claim. The strict performance milestone is labelled as a strengthening of the printed maximization claim. Contributions that establish the equilibrium characterization, measure identities, continuity and attainment, or a rigorous partial-entry performance comparison are within scope.

Selected references

Konstantinos I. Stouras, Jeremy Hutchison-Krupat and Raul O. Chao, The Role of Participation in Innovation Contests, accepted version forthcoming in Management Science, 2021, SSRN 2924224.

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

Strong Algorithms for the Ordinal Matroid Secretary Problem: Every Algorithm with Forbidden Sets of Size k Is α(k) Probability-CompetitiveResearch Paper

Motivation

The secretary problem asks an online decision maker to pick the best of $n$ candidates who arrive in uniformly random order, deciding irrevocably on each one at arrival. Its matroid generalization, the matroid secretary problem (MSP) of Babaioff, Immorlica and Kleinberg (SODA 2007), asks the algorithm to select an independent set of a matroid whose elements arrive in random order. The MSP models online hiring under combinatorial constraints, posted-price mechanisms for matroid-constrained markets and online bipartite matching, and the conjecture that it admits an $O(1)$ -competitive algorithm for every matroid is still open.

Soto, Turkieltaub and Verdugo (arXiv:1802.01997; Mathematics of Operations Research, 2021) study the ordinal version, in which the algorithm only compares revealed elements and never sees weights, and introduce the strongest of several competitiveness notions, probability-competitiveness: every element of the optimum must be selected with probability at least $1/\alpha$ . Their central tool is the forbidden sets technique, summarized in a single statement, the Key Lemma, which turns a combinatorial property of an algorithm into a constant competitive ratio. Every constant-ratio algorithm of the paper for a specific matroid class (transversal matroids and gammoids, graphic and hypergraphic matroids, $k$ -framed matroids, laminar matroids, semiplanar gammoids) is obtained by verifying the hypothesis of this lemma.

Timeline. Dynkin (1963) and Lindley (1961) solve the classical problem with ratio $e$ . Babaioff et al. (2007) pose the MSP. Korula and Pál (ICALP 2009) and Kesselheim, Radke, Tönnis and Vöcking (ESA 2013) analyze random-order algorithms through the reverse arrival sequence, the device the Key Lemma abstracts. Soto, Turkieltaub and Verdugo (SODA 2018, MOR 2021) state the Key Lemma and use it to improve the best known ratios for almost all studied matroid classes.

Setting

Let $\mathcal M$ be a matroid on a finite ground set $R$ with $|R| = n$ , and let $\succ$ be a total order on $R$ , the value order. The span of $Q \subseteq R$ is the set of elements whose addition does not increase the rank of $Q$ . For $Q \subseteq R$ , the greedy optimum $\mathrm{OPT}(Q)$ is the base of $Q$ obtained by scanning $Q$ in decreasing value order and keeping each element that keeps the set independent; equivalently

\mathrm{OPT}(Q) = \{ r \in Q : r \notin \mathrm{span}(\{q \in Q : q \succ r\}) \}, \qquad \mathrm{OPT} = \mathrm{OPT}(R).

The elements arrive in a uniformly random order $r_1, r_2, \dots, r_n$ , and $R_t = \{r_1, \dots, r_t\}$ . An algorithm draws a sample size $s \sim \mathrm{Bin}(n, p)$ for a fixed sampling probability $p$ , observes the arrivals, and returns a set $\mathrm{ALG}$ . It has forbidden sets of size $k$ (Definition 7) if

its output is always independent;
it never accepts one of the first $s$ arrivals;
there is a rule assigning to every triple $(X, Y, r^*)$ with $r^* \in \mathrm{OPT}(Y)$ and $X \subseteq Y - r^*$ a set $\mathcal F(X, Y, r^*) \subseteq X$ of at most $k$ forbidden elements, such that for every time $t \ge s+1$ : if $r_t \in \mathrm{OPT}(R_t)$ and no $r_j$ with $s + 1 \le j \le t - 1$ lies in $\mathcal F(R_j, R_t, r_t)$ , then $r_t$ is selected.

The algorithm is $\alpha$ probability-competitive if $\Pr(r \in \mathrm{ALG}) \ge 1/\alpha$ for every $r \in \mathrm{OPT}$ , the probability being over $s$ and the arrival order.

Formalization targets

Goal: Lemma 1 (Key Lemma)

With

(p(k), \alpha(k)) = \begin{cases} (1/e,\ e) & k = 1,\\ (k^{-1/(k-1)},\ k^{k/(k-1)}) & k \ge 2,\end{cases}

every algorithm with forbidden sets of size $k \ge 1$ , run with sampling probability $p = p(k)$ , satisfies

\Pr(r^* \in \mathrm{ALG}) \ \ge\ \frac{1}{\alpha(k)} \qquad \text{for every } r^* \in \mathrm{OPT}.

Milestones

Lemma 4: $\mathrm{OPT} \cap Q \subseteq \mathrm{OPT}(Q)$ for every $Q \subseteq R$ .
Per-scenario bound (proof of Lemma 1): conditioned on $s$ , on $r_t = r^*$ and on $R_t = Y$ , the probability that $r^*$ is selected is at least $\prod_{j=s+1}^{t-1} ((j-k)/j)_+$ .
Display (5): $\Pr(r^* \in \mathrm{ALG}) \ge \mathbb E_{s \sim \mathrm{Bin}(n,p)} \frac1n \sum_{t=s+1}^n \prod_{j=s+1}^{t-1} (1 - k/j)_+$ .
Game bound: the right-hand side of (5) is at least $\int_p^1 (p/\tau)^k\, d\tau$ .
Integral: $\int_p^1 (p/\tau)^k\, d\tau$ equals $-p\ln p$ for $k = 1$ and $(p - p^k)/(k-1)$ for $k \ge 2$ .
Optimizing $p$ : these bounds are maximized over $p \in (0,1]$ at $p(k)$ , with value $1/\alpha(k)$ .

Significance

The Key Lemma separates the analysis of a random-order algorithm into a structural part (exhibit forbidden sets of size $k$ ) and a probabilistic part (the lemma itself), so the probabilistic part is done once. Its consequences in the paper include an $e$ probability-competitive algorithm for transversal matroids (the first guarantee in the probability notion for Kesselheim et al.'s matching algorithm), ratio $4$ for graphic matroids, $3\sqrt3$ for laminar matroids and $k^{k/(k-1)}$ for $k$ -framed matroids. Because probability-competitiveness implies the ordinal, utility and intersection notions, each of these also bounds the weighted problem.

The result is proved in the paper; nothing here is open. To our knowledge no part of it is formalized in Lean. A formal Key Lemma makes every forbidden-sets analysis a purely combinatorial obligation (Definition 7 for a concrete algorithm), and it fixes a precise probability model for the random-order MSP that later formalizations of the paper's algorithms, or of the classical secretary rule, can reuse.

Difficulty

The obvious argument, "each earlier arrival is forbidden with probability at most $k/j$ , so multiply", fails as stated: the forbidden set $\mathcal F(R_j, R_t, r_t)$ depends on the random set $R_j$ , so the events " $r_j$ is not forbidden" are not independent in the forward direction. The proof needs the reverse arrival sequence: conditioned on $R_t$ , the arrivals $r_{t-1}, r_{t-2}, \dots$ are revealed backwards, each uniform in the current prefix and independent of what was revealed after it. Making this conditioning precise over a finite uniform permutation space is the main formal work. The second difficulty is analytic: the expectation in (5) over $s \sim \mathrm{Bin}(n,p)$ has no closed form, and the paper bounds it by a continuous-time coupling with uniform arrival times rather than by direct summation.

Formalization scope

All objects live in one definitions file, namespace OrdinalMSP.Forbidden.

The ground set is a Fintype R with DecidableEq R and a LinearOrder R; the value order $r \succ q$ is q < r. The matroid is a Mathlib Matroid R with ground set Set.univ, and the span is Matroid.closure.
$\mathrm{OPT}(Q)$ is defined by the span characterization above (opt M Q), which is the greedy output.
An arrival order is σ : Fin n ≃ R; σ i arrives at time $i+1$ . Times in milestone statements are the paper's 1-based ones.
An algorithm is any map from (arrival order, sample size) to a finite set. Online-ness is not required, which is a generalization the proof allows; randomness beyond the sample size is not modelled.
The forbidden-set rule is fixed before the run, independent of the order and of $s$ , and is constrained exactly on the printed domain.
$\Pr(r \in \mathrm{ALG})$ is the exact finite sum $\sum_{s=0}^n \binom ns p^s (1-p)^{n-s} \cdot \#\{\sigma : r \in \mathrm{ALG}(\sigma,s)\}/n!$ in $\mathbb R$ , not a measure-theoretic probability.
$e$ is Real.exp 1; the powers are Real.rpow; $p(k)$ and $\alpha(k)$ branch on $k = 1$ before dividing by $k - 1$ .

Definition 7 is satisfiable (the rule "accept every element after the sample" in a free matroid satisfies it with empty forbidden sets), so the goal is not vacuous; a formalization that strengthens Definition 7, for instance by requiring the selection condition for times $t \le s$ , or that fixes $s = \lfloor pn \rfloor$ instead of drawing it from $\mathrm{Bin}(n,p)$ , would prove a different statement and is ruled out. The auxiliary game of the paper is a proof device and is not formalized; its milestone is a real-number inequality.

Needed infrastructure: counting over Fin n ≃ R conditioned on a prefix set (the reverse arrival sequence), binomial sums, interval integrals of $\tau^{-k}$ , and calculus on $p \mapsto -p\ln p$ and $p \mapsto (p - p^k)/(k-1)$ . The reverse-arrival counting lemmas are reusable for any random-order secretary analysis. Contributions of alternative proofs of the game bound (for example by direct summation) are welcome.

Selected references

J. A. Soto, A. Turkieltaub, V. Verdugo, Strong Algorithms for the Ordinal Matroid Secretary Problem, Mathematics of Operations Research, 2021; preprint arXiv:1802.01997v1, 2018. https://arxiv.org/abs/1802.01997
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, Proc. SODA 2007, pp. 434–443.
N. Korula, M. Pál, Algorithms for secretary problems on graphs and hypergraphs, Proc. ICALP 2009, LNCS 5556, pp. 508–520.
T. Kesselheim, K. Radke, A. Tönnis, B. Vöcking, An optimal online algorithm for weighted bipartite matching and extensions to combinatorial auctions, Proc. ESA 2013, LNCS 8125, pp. 589–600.
E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Mathematics Doklady 4:627–629, 1963.
D. V. Lindley, Dynamic programming and decision theory, Applied Statistics 10(1):39–51, 1961.

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

The Beneficial Effects of Ad Blockers: Both Platforms Allowing Ad Blockers Is an Equilibrium That Beats a World Without Ad Blockers for Low β and High γ/βResearch Paper

Why ad blockers matter to platforms

Ad blockers remove advertising from web pages, and with it the revenue that pays for free content. By the time of this paper a large share of desktop users ran one, and publishers had three responses at hand: tolerate ad blockers, block access to users who run one (an adblock wall), or move behind a paywall. The common view was that ad blockers can only hurt ad-funded platforms.

Despotakis, Ravi and Srinivasan (SSRN 3083119, version of November 28, 2017; published in Management Science in 2020, doi:10.1287/mnsc.2020.3653) model this choice as competition between two platforms and show that ad blockers can raise platform revenue. The mechanism is a segmentation effect: users who would install an ad blocker are typically the most ad-averse, and competition over them pushes ad intensities down for everyone. Letting them block ads takes them out of the ad market, so competition for the remaining users is softer. This mission formalizes the paper's first main result, Proposition 1, together with the case analysis of its proof.

Setting

Two platforms sit at the endpoints $0$ and $1$ of a Hotelling line. Users are spread uniformly on $[0,1]$ ; a user at position $x$ gets intrinsic value $1-x$ from platform 1 and $x$ from platform 2, plus a common value $m$ large enough that every user joins exactly one platform (full coverage). There are two user segments:

non-adblock users, of mass $\lambda$ and ad sensitivity $\beta$ ;
adblock users, of mass $\mu$ and ad sensitivity $\gamma$ , who block ads whenever a platform allows it.

The price sensitivity of all users is $1$ . Each platform $i$ chooses a plan:

Ban: ad blockers are banned, everyone sees ads of intensity $a_i \ge 0$ , and the platform earns $a_i$ per user;
Allow: ad blockers are allowed; non-adblock users see ads of intensity $a_i \ge 0$ and the platform earns $a_i$ per such user, while adblock users see nothing and generate no revenue;
Fee: no ads, a subscription fee $p_i \ge 0$ paid by every user.

At platform 1 a non-adblock user suffers disutility $\beta a_1$ under Ban and Allow and $p_1$ under Fee; an adblock user suffers $\gamma a_1$ under Ban, $0$ under Allow and $p_1$ under Fee. Platform 2 is symmetric. Within a segment, platform 1's share is the length of the set of users who prefer it,

s(d_1, d_2) = \max\Big\{0, \min\Big\{1, \tfrac{1 + d_2 - d_1}{2}\Big\}\Big\},

where $d_1, d_2$ are the two disutilities, and the revenue $r_i$ is the sum over the segments of mass × share × payment per user.

The game has two stages. Platforms first choose plans $(s_1, s_2)$ ; then they choose decision values $(d_1, d_2)$ , and a stage-2 equilibrium is a pure Nash equilibrium of the resulting revenue game over $d_i \ge 0$ . A plan profile with its decision values is an equilibrium if the decision values form a stage-2 equilibrium and, after any unilateral change of plan by either platform, the new subgame has a stage-2 equilibrium in which the deviator earns no more.

The benchmark is the world without ad blockers: plans are Ads (identical to Ban: everyone sees ads, the adblock-prone segment keeps sensitivity $\gamma$ ) and Fee.

Formalization targets

Goal: Proposition 1

For $\lambda, \mu, \beta, \gamma > 0$ :

\beta \le \frac{\lambda(3\lambda+4\mu)^2}{(\lambda+\mu)(3\lambda+2\mu)^2} \quad\text{and}\quad \frac{\lambda+\mu\,\gamma/\beta}{(3\lambda+4\mu\,\gamma/\beta)^2} \le \frac{\lambda}{(3\lambda+2\mu)^2},

then (Allow, Allow) with $a_1 = a_2 = 1/\beta$ is an equilibrium, each platform earning $\lambda/(2\beta)$ ; 2. if $\gamma/\beta \ge 2 + \mu/\lambda$ and $\beta \le \lambda/(\lambda+\mu)$ , then the same holds and $\lambda/(2\beta)$ is at least each platform's revenue in every symmetric stage-2 equilibrium of the benchmark subgames (Ads, Ads) and (Fee, Fee).

Milestones

The milestones follow the numbered cases of the appendix proof: the share formula (case 1), the benchmark subgames (Ads, Ads) and (Fee, Fee) (cases 1–2), the on-path subgame (Allow, Allow) (case 5), the deviation subgames (Ban, Allow) and (Fee, Allow) (cases 8–9), and the three algebraic facts of p. 44 that turn revenue comparisons into conditions on $\beta$ and $\gamma/\beta$ .

Significance

Proposition 1 is the paper's answer to whether ad blockers must hurt publishers: in a region of parameters both platforms prefer to let ad blockers in, and both earn more than without ad blockers. It underlies the paper's welfare result (Proposition 2) and the extensions with an intermediate segment, whitelisting and content investment, which all build on the same equilibrium.

The result is proved on paper by first-order conditions of interior solutions. It is not formalized anywhere. A machine-checked version has to deal with what the first-order derivation leaves out: corner responses where a platform abandons a segment, global rather than local optimality of each response, and uniqueness where it is needed. Two of the paper's intermediate claims fail as printed in parts of the parameter region (see Difficulty), and one threshold on p. 44 contains a typo; the formal statements here are the corrected versions, so a completed proof also certifies the corrected thresholds.

Difficulty

The obvious argument solves the first-order system $\partial r_1/\partial d_1 = \partial r_2/\partial d_2 = 0$ in every subgame. That gives candidate points, not equilibria. With clipped shares the revenue of a platform is only piecewise quadratic in its decision, and a platform can do better by moving to a corner, for example by raising its ad intensity until it serves no adblock user at all.

This happens in exactly the region where Proposition 1 matters. In the (Ban, Allow) deviation subgame the interior point printed in the paper is not a stage-2 equilibrium for large $\gamma/\beta$ : at $(\lambda,\mu,\beta,\gamma) = (1,2,1/10,1)$ the Ban platform earns about $0.75$ there but about $2.97$ by serving only non-adblock users. The proof must therefore find the right stage-2 equilibrium regime by regime and check every unilateral deviation globally over $[0,\infty)$ . Similarly, the benchmark (Ads, Ads) point is not an equilibrium for large $\gamma/\beta$ , which is why the benchmark comparison quantifies over actual equilibria.

Formalization scope

All parameters and decision values are real numbers; $\lambda, \mu, \beta, \gamma > 0$ are hypotheses of the goal; each milestone assumes positivity of the parameters it uses, and decision values range over $[0,\infty)$ .
Market shares are clipped to $[0,1]$ . A formalization with the unclipped share $(1 + d_2 - d_1)/2$ is ruled out: it turns every revenue into a global quadratic, makes every printed first-order point an equilibrium, and trivializes the corner analysis that the result actually requires.
The intrinsic value $m$ cancels under full coverage and appears only in the share milestone, which identifies the clipped share with the Lebesgue measure of the users preferring platform 1.
Platform 2's revenue is platform 1's with the roles exchanged.
The equilibrium notion requires a stage-2 equilibrium on the path and, after each unilateral plan deviation, some stage-2 equilibrium leaving the deviator no better off; play after joint deviations is unconstrained.
The benchmark is the main game with plans restricted to Ban (= Ads) and Fee. Its comparison is with every symmetric stage-2 equilibrium; when (Ads, Ads) has none, that clause is vacuous, while (Fee, Fee) always has the unique equilibrium $p_1 = p_2 = 1$ .
"Better off" is the weak inequality, as in the paper's conditions.

The development needs only real analysis of piecewise quadratic functions and Lebesgue measure of intervals. The model definitions (Hotelling share with full coverage, pure Nash equilibrium over nonnegative reals) are reusable for other duopoly models. Proofs of individual milestones are welcome independently; the goal follows from them by the case analysis described above.

Selected references

A. Despotakis, R. Ravi, K. Srinivasan, The Beneficial Effects of Ad Blockers, SSRN working paper 3083119, version of November 28, 2017. https://ssrn.com/abstract=3083119
A. Despotakis, R. Ravi, K. Srinivasan, The Beneficial Effects of Ad Blockers, Management Science, 2020. https://doi.org/10.1287/mnsc.2020.3653
H. Hotelling, Stability in Competition, The Economic Journal 39(153), 41–57, 1929. https://doi.org/10.2307/2224214

12 thms3 active usersReviewed

Completed

Combinatorics Machine Learning Operations Research·Captain: mikedeng1

Private Sequential Learning: The Query Complexity of an (ϵ, δ, L)-Private Learner Lies Between max{log(1/ϵ), log(δ/ϵ) + 2L − 4} and log(1/(Lϵ)) + 2LResearch Paper

Motivation

A learner wants to locate an unknown number, the true value $v^* \in [0,1)$ , by asking threshold questions of a database: each query $q$ is answered by the single bit $\mathbb I(v^* \ge q)$ . Bisection finds $v^*$ to within $\epsilon/2$ with $\lceil \log_2(1/\epsilon) \rceil$ queries, and no strategy does better (Waeber, Frazier and Henderson, 2013). Bisection, however, reveals everything: each query is a function of the previous answers, so anyone who sees the queries can reconstruct the answers and hence $v^*$ .

Tsitsiklis, Xu and Xu study a learner whose queries, but not the answers, are watched by an adversary. Their motivating examples (pp. 2–3) are a firm testing prices whose surveys a competitor can observe, a consumer browsing products on a platform that sees what is browsed, and an optimizer whose test points are visible to the database it queries. The question is how many queries the learner needs if she must find $v^*$ accurately while keeping the adversary uncertain about it.

The model is from the authors' COLT 2018 extended abstract and Z. Xu's master's thesis (MIT, 2017); the journal version appeared in Operations Research (2021). This mission formalizes arXiv version 3 (26 Feb 2020), and all page and theorem numbers refer to it.

Setting

The learner submits $N$ queries one at a time. A random seed $Y$ , uniform on $\{1, \dots, \bar Y\}$ , lets her randomize. A learner strategy $\phi$ of length $N$ consists of query maps $\phi_k$ and an estimation map $\phi^E$ (§2.1, p. 8): the $k$ -th query is $q_k = \phi_k(r_1, \dots, r_{k-1}, Y) \in [0,1)$ , where $r_i = \mathbb I(v^* \ge q_i)$ are the responses so far, and the estimate is $\hat x = \phi^E(r_1, \dots, r_N, Y) \in [0,1)$ . The class $\Phi_N$ consists of the strategies of length $N$ that submit pairwise distinct queries. Write $\bar q(x,y)$ for the queries and $\hat x(x,y)$ for the estimate when $v^* = x$ and $Y = y$ .

The adversary knows $\phi$ and sees $\bar q$ . The set of query sequences that can occur when $v^* = x$ is $\mathcal Q(x) = \{\bar q(x,y) : y\}$ (eq. (1)), and the adversary's information set is

\mathcal I(\bar q) = \{x \in [0,1) : \bar q \in \mathcal Q(x)\} \qquad \text{(Definition 3.1, p. 9).}

Its size is measured by the $\delta$ -cover number $C_\delta(E)$ , the least number of closed intervals of length at most $\delta$ whose union contains $E$ (Definition 3.2, p. 10). A strategy is $(\epsilon, \delta, L)$ -private (Definition 3.3, p. 10) if

it is accurate: $|\hat x(x,y) - x| \le \epsilon/2$ for every $x \in [0,1)$ and every seed $y$ ; and
it is private: $C_\delta(\mathcal I(\bar q)) \ge L$ for every $x \in [0,1)$ and every $\bar q \in \mathcal Q(x)$ .

The query complexity is $N^*(\epsilon, \delta, L) = \min\{N : \Phi_N \text{ contains an } (\epsilon,\delta,L)\text{-private strategy}\}$ (eq. (5), p. 11). All logarithms are base 2 and are rounded up (footnote 1, p. 4).

Formalization targets

Goal: Theorem 4.1 (p. 12)

For $\epsilon > 0$ , $\delta > 0$ and an integer $L \ge 2$ with $2\epsilon < \delta \le 1/L$ ,

\max\left\{ \left\lceil \log_2 \tfrac1\epsilon \right\rceil,\ \left\lceil \log_2 \tfrac\delta\epsilon \right\rceil + 2L - 4 \right\} \le N^*(\epsilon,\delta,L) \le \left\lceil \log_2 \tfrac{1}{L\epsilon} \right\rceil + 2L.

Upper bound (§6)

The Opportunistic Bisection (OB) strategy first places $L$ "guesses" $[i/L, i/L+\epsilon)$ with $2L$ fixed queries, and then runs a bisection of $\lceil \log_2(1/(\epsilon L)) \rceil$ steps in one of the gaps. The bisection is truthful if no guess caught $v^*$ , and driven by the seed otherwise. The milestones are: OB is accurate; the union of guesses $\mathcal G$ has $C_\delta(\mathcal G) \ge L$ (Claim 6.3); $\mathcal G \subseteq \mathcal I(\bar q)$ for every observable $\bar q$ (Claim 6.4); the cover number is monotone; and OB is $(\epsilon,\delta,L)$ -private (Proposition 6.2).

Lower bound (§7)

For an accurate strategy, the final interval between consecutive sorted queries (with $q_0 = 0$ , $q_{N+1} = 1$ ) has length at most $\epsilon$ (§7.1), so $\mathcal I(\bar q) \subseteq \bar{\mathcal I}(\bar q)$ , the union of special intervals (display (20)). Lemma 7.1 puts $\lceil \log_2(\delta/\epsilon) \rceil$ queries in $(0,\delta)$ for some true value, and accuracy alone gives $N \ge \lceil \log_2(1/\epsilon) \rceil$ . A covering bound gives $C_\delta(\bar{\mathcal I}(\bar q)) \le (K+3)/2$ , with $K$ the number of special queries in $[\delta, 1]$ (p. 21). Together these give $N \ge \lceil \log_2(\delta/\epsilon) \rceil + 2L - 4$ for every private strategy.

Corollary 4.2 (the case $\delta = 1/L$ ) is Theorem 4.1 specialized and is not posed separately.

Significance

The result. The theorem gives the cost of privacy in this model up to an additive constant. At $\delta = 1/L$ the two bounds differ by at most 4 (Corollary 4.2), and the extra cost over plain bisection is at most an additive $2L$ . That is much less than the non-adaptive $\epsilon$ -dense strategy, which is always private but needs about $1/\epsilon$ queries (§5). The lower bound also shows that the $2L$ obfuscating queries cannot be shared with the queries that locate $v^*$ (§7, p. 19).

Formalizing it. The result is proved on paper, but Lemma 7.1 is given only an intuitive argument: the paper calls its proof "fairly standard" and omits it (p. 20). The covering step on p. 21 is argued component by component, with an exceptional component straddling $\delta$ . A formal development supplies both and checks the bookkeeping behind the constants $-4$ , $+3$ and $2L - 3$ . To our knowledge, no machine-checked proof of this theorem or of the bisection lower bound in this form exists.

Difficulty

The upper bound is a construction. Its delicate point is Claim 6.4. For every point $g$ of every guess one must exhibit a seed under which $g$ produces exactly the observed queries, and that seed differs according to whether the observed run was truthful or fictitious.

The lower bound is harder. Counting queries is not enough by itself, because the obvious argument conflates query values with query indices. Lemma 7.1 counts indices along a single run (a fixed true value and seed). The covering bound counts distinct values in $[\delta,1]$ , one of which may be the artificial point $1$ . The natural first idea, a direct counting bound on $N^*$ , is unavailable: $N^*$ is a minimum, so a lower bound must be proved for every private strategy of every length. Only the goal speaks about $N^*$ , where the upper bound shows the set being minimized is nonempty.

Formalization scope

Everything lives in the namespace PrivSeqLearn.QueryComplexity, built on Mathlib with no measure theory in any statement. Conventions:

The seed space is Fin Ybar with 0 < Ybar. "Positive probability" is read as "for some seed" and "probability one" as "for every seed", which is exact for a uniform seed on a finite set.
Response histories are List Bool, and the response to $q$ at true value $x$ is decide (q ≤ x). Queries are 0-indexed (Fin N).
$\Phi_N$ (InPhi) requires query values on every history of length $< N$ and estimate values on every history of length $N$ to lie in $[0,1)$ , and the queries to be pairwise distinct for every $x \in [0,1)$ and seed.
Covers are Fin L-indexed families of closed intervals Set.Icc. $C_\delta$ and $N^*$ are sInf over $\mathbb N$ , which equals the minimum when the set is nonempty.
Every logarithm term is ⌈Real.logb 2 ·⌉ computed in $\mathbb Z$ , so $2L - 4$ never truncates. In the regime, all log arguments exceed 1.
The OB seed is $\{0, \dots, L \cdot 2^M - 1\}$ , decoded as the gap $\tilde{\mathcal J}$ and the bits $Z_1, \dots, Z_M$ . The OB estimate, specified in the paper only inside the proof of Proposition 6.2, is the guess mid-point or the mid-point of the final bisection interval.
Disclosed deviations from the page:
- Lemma 7.1 assumes $\delta \le 1$ .
- The lower-bound milestones do not assume distinct queries, which is a strengthening.
- The OB-only milestones use $2\epsilon < 1/L$ in place of $2\epsilon < \delta \le 1/L$ .
- Cover-number monotonicity assumes a bounded superset.

Trivializing encodings are ruled out:

an empty seed space is excluded by 0 < Ybar;
information sets range over $[0,1)$ only;
privacy is required for every true value and every observable query sequence;
OB is the constructed strategy, not "some strategy".

Contributions are welcome on any milestone. The bisection lower bounds (Lemma 7.1 and the $\log_2(1/\epsilon)$ bound) and the interval-covering facts are reusable beyond this mission.

Selected references

J. N. Tsitsiklis, K. Xu, Z. Xu, Private Sequential Learning, arXiv:1805.02136v3, 2020; Operations Research, 2021. https://arxiv.org/abs/1805.02136
R. Waeber, P. I. Frazier, S. G. Henderson, Bisection search with noisy responses, SIAM Journal on Control and Optimization 51(3):2261–2279, 2013. https://doi.org/10.1137/120861898
M. Horstein, Sequential transmission using noiseless feedback, IEEE Transactions on Information Theory 9(3):136–143, 1963. https://doi.org/10.1109/TIT.1963.1057832
Z. Xu, Private sequential search and optimization, Master's thesis, MIT, 2017. http://hdl.handle.net/1721.1/112054

15 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

On the Fair Division of a Random Object: The Bottom-Heavy Rule Dominates Every Other Symmetric Almost Prior-Independent Rule for Bads Satisfying Fair ShareResearch Paper

Motivation

Many allocation problems divide an object whose value to the participants is uncertain at the time the division rule is designed: computing time on a shared cluster, a recurring chore, the cost of a service used jointly. If the rule must be fixed before the realizations are known, and must treat everyone fairly in expectation, the designer faces a tradeoff between ex ante fairness and ex post efficiency. Bogomolnaia, Moulin and Sandomirskiy (arXiv:1903.10361, published in Management Science, 2022) study this tradeoff for a single divisible object, in the setting of online and repeated fair division (Moulin 2019).

The paper characterizes the most efficient fair rules that need almost no knowledge of the underlying distribution. For a good the efficient fair rules form a one-parameter family; for a bad (a chore, a cost) there is a single most efficient fair rule, the Bottom-Heavy rule. This mission formalizes the bads result, Theorem 17 of the paper.

Setting

There are $n\ge2$ agents $N=\{1,\dots,n\}$ and one divisible bad. A profile $x\in\mathbb R^N_+$ lists the agents' disutilities for the whole bad; zero disutilities are allowed. Write $x_N=\sum_i x_i$ , $\bar x=x_N/n$ and $e^N=(1,\dots,1)$ . The disutility profile is random, with distribution $\mu$ on $\mathbb R^N_+$ ; the coordinates may be correlated. A problem is normalized if $\mathbb E_\mu X_i=1$ for every $i$ .

A division rule maps each realized profile $x$ to a lottery $\varphi(x)\in\Delta(N)$ ; agent $i$ bears the fraction $\varphi_i(x)$ of the bad. A rule is almost prior-independent (API) if it is a single measurable map, used for every distribution once disutilities are normalized by their means. It is symmetric if permuting agents permutes shares. It satisfies Fair Share if in every normalized problem each agent's expected disutility is at most $1/n$ of her expected disutility for the whole bad:

\mathbb E_\mu\big(\varphi_i(X)\,X_i\big)\le\frac1n .

The social cost of $\varphi$ at $x$ is $\sum_i\varphi_i(x)x_i$ , and $\varphi$ dominates $\psi$ if its social cost is at most that of $\psi$ at every profile and strictly lower at some profile.

For $\theta\in[0,1]$ , let $\psi^\theta_i(x)=\frac1n+\frac{\theta}{n-1}\big(\frac{\bar x}{x_i}-1\big)$ (with $1/0=+\infty$ ). The Bottom-Heavy rule $\varphi^\theta$ orders agents by disutility, gives the full $\psi^\theta_i(x)$ to the longest prefix of low-disutility agents that fits into the simplex, splits the remainder equally among the next class of tied agents, and gives nothing to the others. The canonical rule is $\varphi^1$ , whose prefix shares are $x_{N\setminus\{i\}}/(n(n-1)x_i)$ .

Formalization targets

Goal: Theorem 17 (p. 16)

For every $n\ge2$ , $\varphi^1$ is a symmetric API rule satisfying Fair Share, and for every symmetric API rule $\varphi$ satisfying Fair Share with $\varphi\ne\varphi^1$ somewhere on $\mathbb R^N_+$ ,

\sum_i\varphi^1_i(x)x_i\le\sum_i\varphi_i(x)x_i\ \ \forall x\in\mathbb R^N_+,\quad\text{with strict inequality for some }x .

Milestones

Proof of Proposition 14 (p. 25). Fair Share gives a supporting vector $\alpha$ with $\varphi_1(x)x_1\le\alpha\cdot(x-e^N)+\frac1n$ on $\mathbb R^N_+$ , and then $\delta\ge0$ with $\varphi_i(x)\le\frac1n+\delta\big(\frac{\bar x}{x_i}-1\big)$ .
Proposition 14 (p. 15). A symmetric API rule satisfies Fair Share iff for some $\theta\in[0,1]$

\varphi_i(x)\le\min\Big\{\frac1n+\frac{\theta}{n-1}\Big(\frac{\bar x}{x_i}-1\Big),1\Big\}\quad\forall i,\ x\in\mathbb R^N_+ .\tag{9}

Step 1 (p. 25). $\psi^\theta_i\ge0$ and $\sum_i\psi^\theta_i\ge1$ , strictly off the diagonal for $\theta\ne0$ ; with a helper stating that $\varphi^\theta$ is a symmetric API rule satisfying (9).
Remark after Definition 15 (p. 16). The shares $\varphi^1_i(x)$ are anti-monotonic to the $x_i$ .
Step 2 (p. 25). For $\theta=0$ , (9) forces Equal Split on profiles with positive coordinates; for $\theta\in(0,1]$ , a symmetric API rule satisfying (9) equals $\varphi^\theta$ or is dominated by it.
Step 3 (p. 26). $\varphi^{\theta^+}$ dominates $\varphi^{\theta^-}$ for $1\ge\theta^+>\theta^->0$ .

Significance

Theorem 17 says that, for a bad, the efficiency cost of ex ante fairness without knowledge of the prior is resolved by a single explicit rule: no fair API rule is ever cheaper ex post, at any realization, than the Bottom-Heavy rule. This is the basis of the paper's worst-case and asymptotic comparisons for bads (competitive ratio and price of fairness, §5–6), and it contrasts with goods, where the undominated fair rules form a family. Proposition 14 is of independent use: it turns a condition on all priors (Fair Share) into a pointwise inequality on the rule.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the model (normalized random objects, API rules, Fair Share, ex post domination) and a path of eight milestones to the main theorem. The formalization also makes precise two points the printed proof leaves implicit: the convention $1/0=+\infty$ at $\theta=0$ and at zero disutilities, and the case $\theta=0$ of the final domination argument, which Step 3 does not cover.

Difficulty

The "only if" direction of Proposition 14 is the analytic core. Fair Share is a statement about expectations under every normalized distribution, and has to be turned into a bound on the rule at each profile. Testing Fair Share on finitely supported normalized laws shows that $f(x)=\varphi_1(x)x_1$ agrees with its concave majorant at $e^N$ ; extracting a supporting affine function there and pinning down its coefficients needs the symmetry of the rule and the boundary profiles $x=e^{\{i\}}$ . Mathlib has supporting-hyperplane and separation theorems but no concavification operator.

The domination steps are exchange arguments around the threshold $\tilde t$ that defines the Bottom-Heavy rule. Step 3 compares two thresholds as $\theta$ varies; it is proved on profiles with distinct coordinates, and ties need a separate argument (the paper invokes continuity of the total disutility, while the rule itself is discontinuous there). The natural first idea, that $\varphi^1$ minimizes cost among rules satisfying (9) for $\theta=1$ , does not suffice: a fair rule may satisfy (9) only for a smaller $\theta$ , so the comparison across the whole family is needed, and the case $\theta=0$ (Equal Split) requires the anti-monotonicity of $\varphi^1$ and Chebyshev's sum inequality.

Formalization scope

Agents are Fin n (0-based; the paper's agent 1 is agent 0), and $n\ge2$ throughout. Profiles are vectors x : Fin n → ℝ; $\mathbb R^N_+$ is 0 ≤ x and includes zero coordinates. A distribution is a measure on Fin n → ℝ, normalized meaning probability, carried by the orthant, integrable coordinates with mean $1$ . An API rule is a measurable map (Fin n → ℝ) → (Fin n → ℝ) that is simplex-valued on the orthant; values off the orthant never matter. Fair Share quantifies over all normalized laws, not only finitely supported ones. Domination is for a bad: lower social cost, weakly everywhere on the orthant and strictly somewhere.

The convention $1/0=+\infty$ is explicit: the bound (9) is $1$ whenever $x_i=0$ , for every $\theta$ ; in $\varphi^\theta$ with $\theta>0$ , agents with zero disutility split the bad equally (at $x=0$ this is $e^N/n$ ). The threshold $\tilde t$ is encoded at the level of values (prefix masses $\sum_{j:x_j\le v}\psi^\theta_j$ ) rather than by sorting. Two printed claims are posed in corrected form and disclosed in the statements: the case $\theta=0$ of Step 2 holds only on profiles with all coordinates positive, and "α ≥ 0" in the proof of Proposition 14 is $\beta\ge0$ .

A trivializing formalization is ruled out: the goal asserts that $\varphi^1$ is itself a symmetric API rule satisfying Fair Share (so a mis-encoded $\varphi^1$ , such as the cost-minimizing utilitarian rule, cannot pass), "other" means differing at some profile of the orthant, and domination includes a strict inequality.

A complete development needs: integrals of bounded measurable functions against probability measures on Fin n → ℝ; a supporting-hyperplane or concave-envelope argument for Proposition 14; finite-sum manipulations over filtered Finsets and Chebyshev's sum inequality for the domination steps; measurability of piecewise-defined maps. The model layer (normalized random objects, API rules, Fair Share, domination) is reusable for the goods half of the paper. Proofs of any milestone, and sanity checks of the definitions (Example 16 for $n=2$ ), are welcome.

Selected references

A. Bogomolnaia, H. Moulin, F. Sandomirskiy, On the Fair Division of a Random Object, arXiv:1903.10361v4, 2021; Management Science 68(2), 2022. https://arxiv.org/abs/1903.10361
H. Moulin, Fair Division in the Internet Age, Annual Review of Economics 11, 2019. https://doi.org/10.1146/annurev-economics-080218-025559
R. Laraki, On the Regularity of the Convexification Operator on a Compact Set, Journal of Convex Analysis 11(1), 2004.
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

11 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

A simple formula for the average gate fidelity of a quantum dynamical operationResearch Paper

Motivation

A simple formula for the average gate fidelity of a quantum dynamical operation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $d$ be a positive integer and let $\mathcal E$ be a trace-preserving quantum operation on a $d$ -dimensional quantum system $Q$ . Define its average fidelity by $\overline F(\mathcal E)=\int \langle\psi|\mathcal E(|\psi\rangle\langle\psi|)|\psi\rangle\,d\psi$ , where $d\psi$ is the uniform Haar probability measure on normalized pure states. Let $R$ be a $d$ -dimensional reference system, let $|\phi_d\rangle=d^{-1/2}\sum_{j=0}^{d-1}|j\rangle_R|j\rangle_Q$ , and define $F_e(\mathcal E)=\langle\phi_d|(\mathrm{id}_R\otimes\mathcal E)(|\phi_d\rangle\langle\phi_d|)|\phi_d\rangle$ . Then

\overline F(\mathcal E)=\frac{d F_e(\mathcal E)+1}{d+1}.

This identity converts entanglement fidelity into the average probability of preserving a uniformly distributed pure state.

Formalization Note The frozen channel predicate supplies complete positivity, trace preservation and linearity through a normalized Kraus representation. The Haar state measure is the image of normalized full-unitary Haar measure applied to a fixed unit vector; channel integrability is established in the imported definition module. Entanglement fidelity is an overlap probability, independent of the choice of maximally entangled state.

Target

Equation (3); proof on PDF pages 1–2

\overline F(\mathcal E)=\frac{d F_e(\mathcal E)+1}{d+1}.

This identity converts entanglement fidelity into the average probability of preserving a uniformly distributed pure state.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

A simple formula for the average gate fidelity of a quantum dynamical operation, arXiv:quant-ph/0205035v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Additional independently reviewed proof targets

Unnumbered claim following Eq. (2): unit average gate fidelity iff perfect implementation

Let $d>0$ , let $\mathcal E$ be a completely positive trace-preserving map on $d$ -dimensional matrices, and let $U$ be a unitary target. Let $\overline F(\mathcal E,U)$ denote the normalized Haar average of $\langle\psi|U^\dagger\mathcal E(|\psi\rangle\langle\psi|)U|\psi\rangle$ . Then

\overline F(\mathcal E,U)=1\quad\Longleftrightarrow\quad\mathcal E(X)=UXU^\dagger\text{ for every matrix }X.

Thus unit overlap fidelity characterizes exact implementation of the target channel, including its action on all density inputs.

Twirled channel: channel property, fidelity invariance, and unitary covariance; Eqs. (6), (8), (10)

Let $d>0$ and let $\mathcal E$ be a completely positive trace-preserving map. Define its normalized unitary Haar twirl by $\mathcal E_T(X)=\int U^\dagger\mathcal E(UXU^\dagger)U\,dU$ . Then $\mathcal E_T$ is completely positive and trace preserving, and

\overline F(\mathcal E_T)=\overline F(\mathcal E),\qquad F_e(\mathcal E_T)=F_e(\mathcal E),\qquad V\mathcal E_T(\rho)V^\dagger=\mathcal E_T(V\rho V^\dagger)

for every density matrix $\rho$ and unitary $V$ . Here $\overline F$ is the normalized pure-state Haar overlap average, and $F_e$ is the normalized maximally entangled overlap with identity action on the reference register.

These properties allow the fidelity calculation to be reduced to a unitarily covariant channel.

Unnumbered central proof result: the twirl is depolarizing

Let $d>0$ and let $\mathcal E$ be a completely positive trace-preserving map. Its normalized unitary Haar twirl $\mathcal E_T(X)=\int U^\dagger\mathcal E(UXU^\dagger)U\,dU$ has a real parameter $p$ , independent of the density input, such that

\mathcal E_T(\rho)=\frac p d I+(1-p)\rho\qquad\text{for every density matrix }\rho.

No additional interval constraint on $p$ is imposed. This identifies the twirl as a depolarizing channel.

Eq. (16): entanglement fidelity in an orthogonal unitary operator basis

Let $d>0$ and let $\mathcal E$ be a completely positive trace-preserving map. Let $(U_j)_{j=1}^{d^2}$ be a complex operator basis consisting of unitaries with $\operatorname{tr}(U_j^\dagger U_k)=d\delta_{jk}$ . With $F_e$ the overlap of the normalized maximally entangled state before and after applying $\mathcal E$ to its system register,

F_e(\mathcal E)=\frac{1}{d^3}\sum_{j=1}^{d^2}\operatorname{Re}\operatorname{tr}(U_j^\dagger\mathcal E(U_j)).

This expresses entanglement fidelity using the channel action on an operator basis.

Eq. (17): the paper's general qudit average gate fidelity formula

Let $d>0$ , let $\mathcal E$ be a completely positive trace-preserving map, and let $U$ be a unitary target. Let $(U_j)_{j=1}^{d^2}$ be a complex operator basis of unitaries satisfying $\operatorname{tr}(U_j^\dagger U_k)=d\delta_{jk}$ . The normalized Haar average gate overlap is

\overline F(\mathcal E,U)=\frac{\sum_{j=1}^{d^2}\operatorname{Re}\operatorname{tr}(U U_j^\dagger U^\dagger\mathcal E(U_j))+d^2}{d^2(d+1)}.

The target inverse conjugates the channel output. This is the paper's general qudit formula, with no unitality assumption.

Eq. (18): qubit Pauli specialization

Let $\mathcal E$ be a completely positive trace-preserving map on a qubit, let $U$ be a unitary target, and let $\sigma_1=X$ , $\sigma_2=Y$ , $\sigma_3=Z$ be the Pauli matrices, with $Y=\begin{pmatrix}0&-i\\i&0\end{pmatrix}$ . Then the normalized Haar gate overlap satisfies

\overline F(\mathcal E,U)=\frac12+\frac1{12}\sum_{j=1}^{3}\operatorname{Re}\operatorname{tr}(U\sigma_jU^\dagger\mathcal E(\sigma_j)).

This specializes the general operator-basis formula to three nonidentity Pauli operators; trace preservation suffices.

Eq. (19): average gate fidelity from a preparable state operator basis

Let $d>0$ , let $\mathcal E$ be a completely positive trace-preserving map, and let $U$ be a unitary target. Let $(U_j)_{j=1}^{d^2}$ be a complex operator basis of unitaries with $\operatorname{tr}(U_j^\dagger U_k)=d\delta_{jk}$ . Let $(\rho_k)_{k=1}^{d^2}$ be a complex operator basis whose elements are density matrices. Define the unique complex coordinates $\alpha_{jk}$ by $U_j=\sum_k\alpha_{jk}\rho_k$ . Then

\overline F(\mathcal E,U)=\frac{\sum_{j,k}\operatorname{Re}\!\left[\alpha_{jk}\operatorname{tr}(U U_j^\dagger U^\dagger\mathcal E(\rho_k))\right]+d^2}{d^2(d+1)}.

This gives an exact algebraic determination from the outputs on the state basis. It asserts no finite-shot accuracy or sample-cost guarantee.

These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.

10 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+2·Captain: mikedeng1

Distributionally Robust Inverse Covariance Estimation: The Wasserstein Shrinkage Estimator: Without Sparsity Information the Robust Estimator Is a Closed-Form Shrinkage of the Sample EigenvaluesResearch Paper

Motivation

The precision matrix $X=\Sigma^{-1}$ of a Gaussian random vector $\xi\in\mathbb R^p$ encodes its conditional independence structure: $X_{ij}=0$ exactly when $\xi_i$ and $\xi_j$ are independent given the other coordinates. Estimating it is a basic step in Gaussian graphical models, portfolio selection and linear discriminant analysis. The textbook estimator, the inverse of the sample covariance matrix $\widehat\Sigma$ , fails when the number $n$ of samples is smaller than the dimension $p$ : then $\widehat\Sigma$ is singular and the maximum likelihood problem $\min_{X\succ0}\{-\log\det X+\langle\widehat\Sigma,X\rangle\}$ has no solution. Even for $n>p$ the inverse sample covariance is badly conditioned.

Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1805.07194, Operations Research 2022) replace the nominal distribution $\mathcal N(0,\widehat\Sigma)$ in the likelihood by the worst case over all normal distributions within a type-2 Wasserstein distance $\rho$ of it, and show that the resulting robust problem has a closed-form solution. The solution keeps the eigenvectors of $\widehat\Sigma$ and maps its eigenvalues through an explicit nonlinear shrinkage, and it is invertible for every sample size. Shrinkage estimators of this kind had been proposed earlier for statistical reasons (Ledoit and Wolf, doi:10.1016/S0047-259X(03)00096-4); here the shrinkage follows from the robust model rather than being imposed.

Setting

Fix a dimension $p\ge1$ . Write $\mathbb S^p_+$ and $\mathbb S^p_{++}$ for the positive semidefinite and positive definite symmetric $p\times p$ matrices, and $\langle A,B\rangle=\operatorname{Tr}[A^\top B]$ for the trace inner product. For distributions $\mathbb P_1,\mathbb P_2$ on $\mathbb R^p$ the type-2 Wasserstein distance is

\mathbb W(\mathbb P_1,\mathbb P_2)=\inf_\Pi\Big(\int\|\xi_1-\xi_2\|^2\,\Pi(d\xi_1,d\xi_2)\Big)^{1/2},

the infimum over couplings $\Pi$ with marginals $\mathbb P_1$ , $\mathbb P_2$ (Definition 1.1).

Given a sample covariance matrix $\widehat\Sigma\in\mathbb S^p_+$ (possibly singular) and a radius $\rho>0$ , the ambiguity set is

\mathcal P^0_\rho=\big\{\mathbb Q=\mathcal N(0,S):\ S\in\mathbb S^p_+,\ \mathbb W(\mathbb Q,\mathcal N(0,\widehat\Sigma))\le\rho\big\},

the centred normal distributions, degenerate ones included, within distance $\rho$ of the nominal one. The worst-case expectation is $g(\widehat\Sigma,X)=\sup_{\mathbb Q\in\mathcal P^0_\rho}\mathbb E^{\mathbb Q}[\langle\xi\xi^\top,X\rangle]$ (7), and the robust estimation problem (5) is

\mathcal J(\widehat\Sigma)=\inf_{X\in\mathcal X}\Big\{-\log\det X+g(\widehat\Sigma,X)\Big\},

where $\mathcal X\subseteq\mathbb S^p_{++}$ is the set of admissible precision matrices; without structural information $\mathcal X=\mathbb S^p_{++}$ .

The paper reformulates (5) through the metric $\mathbb W_S(\Sigma_1,\Sigma_2)=\sqrt{\operatorname{Tr}[\Sigma_1]+\operatorname{Tr}[\Sigma_2]-2\operatorname{Tr}[\sqrt{\sqrt{\Sigma_2}\Sigma_1\sqrt{\Sigma_2}}]}$ on $\mathbb S^p_+$ (Definition 2.3), the scalar program (8)

\inf_{\gamma:\ \gamma I\succ X}\ \gamma\big(\rho^2-\operatorname{Tr}[\widehat\Sigma]\big)+\gamma^2\big\langle(\gamma I-X)^{-1},\widehat\Sigma\big\rangle,

and the joint convex program (6), which minimizes $-\log\det X$ plus the objective of (8) over $\gamma I\succ X\succ0$ , $X\in\mathcal X$ .

Formalization targets

Goal: Theorem 3.1 (p. 12)

Let $\rho>0$ , $\mathcal X=\mathbb S^p_{++}$ , and $\widehat\Sigma=\sum_{i=1}^p\lambda_iv_iv_i^\top$ with orthonormal $v_i$ . Then the equation

\Big(\rho^2-\tfrac12\sum_{i=1}^p\lambda_i\Big)\gamma-p+\tfrac12\sum_{i=1}^p\sqrt{\lambda_i^2\gamma^2+4\lambda_i\gamma}=0\tag{16b}

has a unique positive solution $\gamma^\star$ , and the unique minimizer of (5) is

X^\star=\sum_{i=1}^px^\star_iv_iv_i^\top,\qquad x^\star_i=\gamma^\star\Big[1-\tfrac12\Big(\sqrt{\lambda_i^2(\gamma^\star)^2+4\lambda_i\gamma^\star}-\lambda_i\gamma^\star\Big)\Big].\tag{16a}

Milestones

The worst case over $\mathcal P^0_\rho$ equals $\sup\{\langle S,X\rangle: S\in\mathbb S^p_+,\ \mathbb W_S(S,\widehat\Sigma)\le\rho\}$ (proof of Proposition 2.8, p. 8).
Lemma 2.7 (p. 7): partial infima of functions continuous in $\varepsilon$ are upper semicontinuous; under uniform calmness from below they are lower semicontinuous.
Proposition 2.8 (p. 7): for $\widehat\Sigma\succeq0$ , $X\succ0$ , $g(\widehat\Sigma,X)$ equals the value of (8), and $g$ is continuous on $\mathbb S^p_+\times\mathbb S^p_{++}$ .
Theorem 2.6 (p. 7): for every $\mathcal X\subseteq\mathbb S^p_{++}$ , $\mathcal J(\widehat\Sigma)$ equals the value of (6), and $\mathcal J$ is continuous on $\mathbb S^p_+$ .
Equation (16b) has a unique root in $[0,\infty)$ , and it is positive (p. 12).
Identity (17), $(\gamma^\star)^2x^\star_i\lambda_i=(\gamma^\star-x^\star_i)^2$ (p. 12), and $\rho^2(\gamma^\star)^2=\sum_ix^\star_i$ (p. 13).
For $\widehat\Sigma\succ0$ , $(X^\star,\gamma^\star)$ is feasible and optimal in (6) (p. 12).

Significance

The result. Theorem 3.1 gives the robust estimator in closed form up to an eigendecomposition and a scalar root, so it costs no more than the sample covariance itself. It shows that the estimator commutes with $\widehat\Sigma$ , is positive definite for every $\rho>0$ even when $\widehat\Sigma$ is singular, and depends on the data only through the eigenvalues; the paper's later sensitivity results (Proposition 3.5) and the numerical comparisons with Ledoit–Wolf shrinkage and the graphical lasso rest on this formula. Theorem 2.6 shows more generally, for sparsity-constrained $\mathcal X$ , that the robust problem is a convex program although the ambiguity set is not convex.

Formalizing it. The results are proved on paper; none is machine-checked. The formalization exercises a measure-level definition of the robust problem, with the ambiguity set defined through the coupling Wasserstein distance, and connects it to matrix analysis: the Gelbrich formula for Gaussians, a semidefinite duality, continuity of optimal value functions, and a first-order optimality argument for a matrix-fractional objective. Each milestone is reusable for other Gaussian–Wasserstein robust models, of which the platform already has several (Kalman filtering, minimax mean-square-error estimation).

Difficulty

The obvious argument is to plug $X^\star$ into the first-order conditions of (6). This works only when $\widehat\Sigma\succ0$ : for singular $\widehat\Sigma$ , every zero eigenvalue gives $x^\star_i=\gamma^\star$ , so $\gamma^\star I-X^\star$ is singular and $(X^\star,\gamma^\star)$ is not even feasible in (6). The singular case, which is the case of interest ( $p>n$ ), therefore needs continuity of the optimal value $\mathcal J$ and of the worst-case expectation $g$ in $\widehat\Sigma$ , which is the content of Theorem 2.6 and Proposition 2.8. Those in turn require the reduction from distributions to covariance matrices (the Gelbrich formula, which holds for degenerate normals and is an optimal-transport theorem in its own right), a Lagrangian duality with a Lyapunov-equation inner problem, and a priori eigenvalue bounds on near-optimal $X$ that vary continuously with $\widehat\Sigma$ . Sufficiency of the first-order conditions also needs joint convexity of $\gamma^2\langle(\gamma I-X)^{-1},\widehat\Sigma\rangle$ , which the paper cites.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p) and matrices are Matrix (Fin p) (Fin p) ℝ with the entrywise topology. $\mathcal N(0,S)$ is Mathlib's multivariateGaussian 0 S, which allows singular $S$ . The Wasserstein distance is the published coupling distance WassersteinDRO.Gelbrich.wassersteinDistance 2, valued in $[0,\infty]$ ; the radius enters through ENNReal.ofReal ρ. The square root is the published psdSqrt, and $\langle\cdot,\cdot\rangle$ the published WassMMSE.Sandwich.frob. The worst-case expectation, $\mathcal J$ , and the values of (6) and (8) are suprema and infima in EReal. Every distribution in $\mathcal P^0_\rho$ is Gaussian, so the integrand $\langle\xi\xi^\top,X\rangle$ is integrable. Every matrix inverse sits under the constraint $\gamma I\succ X$ inside the infimum. "Unique minimizer" is stated as IsMinOn over all positive definite $X$ together with equality of every positive definite minimizer to $X^\star$ . The eigendecomposition is an arbitrary orthonormal one, not a basis chosen by the library.

One hypothesis is added: $p\ge1$ , because for $p=0$ (16b) has no positive solution. Definition 2.1 prints the normal density without the factor $\tfrac12$ in the exponent; the standard normal distribution is used.

The goal is stated for the measure-level problem (5). Stating it on the matrix program (6) would be a different and, for singular $\widehat\Sigma$ , false theorem. Replacing $\mathcal P^0_\rho$ by the covariance ball or by all distributions, or computing suprema as real sSup (which returns $0$ on unbounded sets), would trivialize or change the statement.

The mission concerns the zero-mean problem (5) with $\mathcal X=\mathbb S^p_{++}$ for the goal; Theorem 2.6 is posed for general $\mathcal X\subseteq\mathbb S^p_{++}$ . Out of scope: Theorem 2.10 (the unknown-mean problem (4)), Corollary 2.9, Lemma 3.3, Proposition 3.5, the algorithm of §4, the extremal distributions of §5 (Theorem 5.1) and the experiments of §6. The Gelbrich formula (Proposition 2.2) is not posed here; it is Open on the platform as WassKF.Reform.proposition_2_2. The Open theorem WassMMSE.Sandwich.proposition_A_4_i, a covariance-level duality behind Proposition 2.8, is included for reuse. Welcome contributions: the Gelbrich formula for possibly degenerate centred normals, second moments of multivariateGaussian, continuity of optimal value functions (Berge's maximum theorem), and convexity of the matrix-fractional function.

Selected references

V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Distributionally Robust Inverse Covariance Estimation: The Wasserstein Shrinkage Estimator, Operations Research 70(1), 2022; read as arXiv:1805.07194v1, 2018. https://arxiv.org/abs/1805.07194
C. R. Givens, R. M. Shortt, A class of Wasserstein metrics for probability distributions, Michigan Mathematical Journal 31(2), 1984. https://doi.org/10.1307/mmj/1029003026
O. Ledoit, M. Wolf, A well-conditioned estimator for large-dimensional covariance matrices, Journal of Multivariate Analysis 88(2), 2004. https://doi.org/10.1016/S0047-259X(03)00096-4
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441

14 thms3 active usersReviewed

Completed

Algorithmic Game Theory Machine Learning Mechanism Design+1·Captain: mikedeng1

Dynamic Incentive-Aware Learning: Robust Pricing in Contextual Auctions: Against Utility-Maximizing Buyers the CORP Policy Has Regret O(Nd(log(Td) log T + log²T / log²(1/γ)))Research Paper

Motivation

Display advertising is sold one impression at a time, mostly through second-price auctions with reserve prices. A reserve tailored to each buyer and to the features of the impression can raise the seller's revenue considerably, but the right reserve depends on the buyers' valuations, which the seller does not know and must learn from past auctions. The buyers participate in the same exchange day after day and know that their bids feed the seller's learning, so a patient buyer may bid untruthfully today to obtain lower reserves tomorrow. Learning reserve prices from strategic buyers is therefore a joint problem of statistics and incentives.

Golrezaei, Javanmard and Mirrokni (arXiv:2002.11137, Operations Research 69(1), 2021) study this problem in a contextual model and propose the policy CORP (Contextual Robust Pricing). Earlier work on learning against strategic buyers considered a single buyer facing posted prices, without contexts: Amin, Rostamizadeh and Syed (NeurIPS 2013) introduced the discounted strategic buyer, and contextual and revenue-optimization variants followed (Amin, Rostamizadeh and Syed, NeurIPS 2014; Mohri and Muñoz Medina, NeurIPS 2015). Personalized reserves in second-price auctions were studied by Paes Leme, Pál and Vassilvitskii (2016). The present paper treats many buyers, personalized reserves, contexts in $\mathbb R^d$ and censored observations (the seller sees who won, not the valuations).

Setting

In every period $t=1,2,\dots$ the seller observes a feature vector $x_t\in\mathbb R^d$ , drawn i.i.d. from a law $\mathcal D$ supported in the unit ball. Each of $N$ buyers has the valuation

v_{it}=\langle x_t,\beta_i\rangle+z_{it},

where $\beta_i\in\mathbb R^d$ is an unknown preference vector with $\|\beta_i\|\le B_p$ and the noises $z_{it}$ are i.i.d. with a known density $f$ on $[-B_n,B_n]$ , mean zero, and distribution function $F$ . Assumption 1 asks $F$ and $1-F$ to be log-concave on $[-B_n,B_n]$ .

Each period runs a lazy second-price auction with personalized reserves $r_{it}$ : the highest bidder $i^\star$ gets the item if $b_{i^\star t}\ge r_{i^\star t}$ and pays $\max\{r_{i^\star t},\max_{j\neq i^\star}b_{jt}\}$ ; nobody else pays. The benchmark knows the $\beta_i$ and sets $r^\star_i(x)=\arg\max_y y\,(1-F(y-\langle x,\beta_i\rangle))$ (4); its expected revenue against truthful buyers is $\mathrm{rev}^\star_t$ (5).

CORP works in episodes $E_k=\{\ell_k,\dots,\ell_{k+1}-1\}$ with $\ell_k=2^{k-1}$ . At the start of episode $k$ it computes, for each buyer, a maximum-likelihood estimate $\hat\beta_{ik}$ over $\|\beta\|\le B_p$ from the censored outcomes of episode $k-1$ (8)–(9). In each period of episode $k$ , with probability $1/\ell_k$ it explores: one uniformly chosen buyer is offered the item at a price uniform on $[0,B_p+B_n]$ . Otherwise it exploits with reserves $r_{it}=\arg\max_y y\,(1-F(y-\langle x_t,\hat\beta_{ik}\rangle))$ (10).

Buyer $i$ 's bid may depend on his own history of valuations, bids, allocations and payments, on $x_t$ , on $v_{it}$ and on private randomness. His utility is $\sum_t\gamma^t\,\mathbb E[v_{it}q_{it}-p_{it}]$ with a discount factor $\gamma\in(0,1)$ , and buyers are utility-maximizing. The regret after $T$ periods is $\sum_{t=1}^T(\mathrm{rev}^\star_t-\mathrm{rev}_t)$ , worst case over $\beta$ and $\mathcal D$ (7).

Formalization targets

Goal: Theorem 4.1 (p. 23)

There is $C$ , depending only on $B_p,B_n,M,f,c_{\min},c_{\max}$ , such that for all $N,d\ge1$ , $T\ge2$ , $\gamma\in(0,1)$ , all admissible $\mathcal D,\beta$ and all utility-maximizing buyers,

\mathrm{Regret}(T)\le C\,N d\Big(\log(Td)\log T+\frac{\log^2T}{\log^2(1/\gamma)}\Big).

Milestones, in the order the proof uses them

Proposition 3.1 (p. 15): the reserves (4) are revenue-optimal against truthful buyers.
Lemma 1 (p. 56): the conditional revenue $W_{it}$ is flat at $r^\star_{it}$ and has a bounded second derivative.
Lemma 2 (p. 56): $|r^\star_{it}-r_{it}|\le|\langle x_t,\beta_i-\hat\beta_{ik}\rangle|$ .
Lemma 3 (p. 57): the second-highest bid and the competing bid move by at most the shading and overbidding.
Proposition 9.2 (p. 53): per episode, a utility-maximizing buyer lies $O(\log(\ell/\delta)+\log(\ell N)/\log(1/\gamma))$ times, and his total shading and overbidding are $O(\log(\ell N)/\log(1/\gamma))$ , with high probability.
Corollary 18.2 (p. 88): the vector Freedman inequality.

Significance

If true, Theorem 4.1 says that a seller can learn personalized, contextual reserves from censored data at a cost logarithmic in $T$ and linear in $Nd$ , even when buyers manipulate their bids. The strategic term vanishes as buyers become impatient. The episodic delay between a bid and its effect on reserves, together with the random exploration prices, is what makes untruthful bidding unprofitable. The lemmas are of independent use. Proposition 3.1 and Lemma 2 concern the monopoly price under log-concave noise. Lemma 3 is a deterministic fact about second-price auctions. Corollary 18.2 is a vector concentration inequality.

Status. None of these results is machine-checked anywhere known to us. The paper's printed proof has gaps. Proposition 9.1 (p. 52), which bounds the estimation error of the MLE by the number of lies, fails as printed. With uniform noise a single lie per episode keeps the estimate a constant distance from $\beta_i$ . Its supporting Lemma 5 uses a constant $u_F$ that is infinite for every compactly supported $F$ (p. 71). Its curvature bound (89) also fails when a likelihood term leaves the support of $f$ . Lemma 6 (p. 76) conditions on an event the exploration lottery itself moves. A proof of Theorem 4.1, or a counterexample to it, would settle the question. The goal is stated as the paper states it, and is neither asserted nor denied here.

Difficulty

The natural route is the paper's. First bound the estimation error of the censored MLE in terms of the number of lies. Then bound the number of lies by comparing a lie's discounted future gain with its immediate loss under the exploration lottery. Finally sum over episodes.

The first step is where it breaks. With noise supported on $[-B_n,B_n]$ , an observation whose threshold falls outside the support carries no curvature. Its likelihood term is constant or $+\infty$ , so the minimizer of (9) is in general a set, not a point. A minimizer at the wrong end of that set can keep the reserve below the benchmark for many episodes, even with truthful buyers. Any proof must say which minimizer CORP takes, or show that all of them work. The second step must handle buyers who react to one another through their histories; the paper's proof holds the other buyers' bids fixed. The concentration steps need a vector martingale inequality and a covariance concentration bound, neither of which is in Mathlib.

Formalization scope

Lean represents features as EuclideanSpace ℝ (Fin d) and buyers as Fin N. Periods are indexed from $0$ internally (Lean's $n$ is the paper's $t=n+1$ ), and episodes likewise (Lean's $e$ is the paper's $k=e+1$ , so $\ell_k=2^e$ ). Period $1$ always explores. The per-period randomness consists of the features, the noises, the exploration coin, the chosen buyer, the exploration price and the buyers' seeds. It is independent across periods, under Measure.infinitePi, and the play is defined by recursion over periods. The likelihood (9) takes values in $[0,+\infty]$ with $-\log 0=+\infty$ ; a real-valued Real.log would make impossible observations free and change the estimator. The estimator (8) and the reserve rule (10) are arbitrary measurable selections of the argmin and argmax, quantified universally. No tie-break or uniqueness is added. The same reserve rule defines the benchmark (4).

Standing assumptions and added hypotheses.

The noise density is continuous on $[-B_n,B_n]$ , with mass one and mean zero, and Assumption 1 holds.
$\|x\|\le1$ almost surely, and $c_{\min}/d\,\|u\|^2<\mathbb E\langle x,u\rangle^2\le c_{\max}/d\,\|u\|^2$ ; the proof uses these eigenvalue bounds (pp. 57, 72–73).
Bids are at most $M$ (p. 14) and pairwise distinct almost surely (p. 20).
Strategies and selections are measurable, $N,d\ge1$ and $T\ge2$ .
Utility-maximizing is pinned as the inequality the proof uses on p. 77: no buyer gains by switching to truthful bidding from the start of any episode on. Every best-response profile satisfies it, and the all-truthful profile does too.
Exploration is a posted price to the chosen buyer.
Lemma 1 adds $f\in C^1(\mathbb R)$ , which its proof uses.
Lemma 2 adds that both indices exceed $-B_n$ ; without that, the argmax is unbounded.
Lemma 3's (45) adds that another buyer wins; as printed it fails when nobody wins.
Corollary 18.2 adds $u_0=0$ .

Ruled out. The constant $C$ comes before every instance, horizon, selection and strategy, so a bound depending on $T$ or on the instance does not count. The policy is CORP as defined, not any reserve-setting rule. The rationality hypothesis is satisfiable.

Infrastructure. A complete development needs the following.

Measurability of the recursive play.
The monopoly price under log-concavity (Proposition 3.1, Lemma 2).
Censored-likelihood estimation with compactly supported noise.
A vector Freedman inequality (Corollary 18.2, reusable).
Covariance concentration for bounded vectors.

Contributions on any milestone are welcome. So is a formal counterexample to the goal in the model as stated, for example with one truthful buyer, uniform noise and the smallest minimizer of (9).

Out of scope. CORP-II and SCORP (Theorems 5.1–5.3, Propositions 11.1–11.2) and the extensions of Appendix 8 are not part of this mission. Proposition 9.1, Lemma 5, Lemma 6 and Theorem 18.1 are not posed (see Significance).

Selected references

N. Golrezaei, A. Javanmard, V. Mirrokni, Dynamic Incentive-Aware Learning: Robust Pricing in Contextual Auctions, Operations Research 69(1), 2021; read as arXiv:2002.11137v1. https://arxiv.org/abs/2002.11137
K. Amin, A. Rostamizadeh, U. Syed, Learning Prices for Repeated Auctions with Strategic Buyers, NeurIPS 2013. https://papers.nips.cc/paper/2013/hash/1e6e0a04d20f50967c64dac2d639a577-Abstract.html
R. Paes Leme, M. Pál, S. Vassilvitskii, A Field Guide to Personalized Reserve Prices, WWW 2016. https://doi.org/10.1145/2872427.2883071
J. A. Tropp, Freedman's inequality for matrix martingales, Electronic Communications in Probability 16, 2011. https://doi.org/10.1214/ECP.v16-1624
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

10 thms3 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Bayesian Sequential Learning for Clinical Trials of Multiple Correlated Medical Interventions: The cPDE Allocation Policy Is Asymptotically ConsistentResearch Paper

Motivation

A clinical trial that compares several treatments for the same condition must decide, patient by patient, which treatment the next patient receives. When the treatments are related (doses of one drug, drugs of one class), an outcome observed on one arm is informative about the others, and a good allocation rule should exploit that correlation. Chick, Gans and Yapar (SSRN 3184758, version of August 31, 2020; later in Management Science) model this as Bayesian sequential sampling with a correlated Gaussian prior and propose the cPDE allocation policy, which samples the arm with the largest value of an adaptive-lookahead optimal-stopping index. Their one theorem, Theorem 1, says that cPDE is asymptotically consistent: run forever, it learns every arm's mean and identifies the best arm.

Consistency is the minimal guarantee asked of an allocation heuristic: a rule that can stop sampling an arm whose value is still uncertain may settle on the wrong treatment forever. The argument follows the consistency proof of Xie, Frazier and Chick (Operations Research 64(2):542–559, 2016; "XFC") for one-step knowledge-gradient (cKG) policies, extended to an index whose lookahead is itself an optimal stopping time.

Setting

There are $M\ge2$ arms. Arm $i$ has unknown mean $\theta_i$ ; an observation of arm $i$ is $Y\mid\theta_i\sim N(\theta_i,\lambda_i)$ with known $\lambda_i>0$ , independent across observations. The prior is $\theta\sim N(\mu^0,\Sigma^0)$ with $\Sigma^0$ positive definite, and sampling arm $i$ costs $c_i>0$ . After $t$ observations the belief is $(\mu^t,\Sigma^t)$ ; one observation $y$ of arm $i$ updates it by Bayes' rule (8):

\mu'=\mu+\frac{y-\mu_i}{\lambda_i+\Sigma_{i,i}}\Sigma e_i,\qquad \Sigma'=\Sigma-\frac{\Sigma e_ie_i^\top\Sigma}{\lambda_i+\Sigma_{i,i}}.

From a belief $(\mu,\Sigma)$ , imagine sampling arm $i$ alone. The predictive change $Z^\tau_i=\mu^{t+\tau}_i-\mu^t_i$ after $\tau$ samples is a centred Gaussian with variance $\lambda_i\tau/(n_i(n_i+\tau))$ , $n_i=\lambda_i/\Sigma_{i,i}$ ((9)–(10)). The cPDE allocation index is (EC.8):

\nu^*_i(\mu,\Sigma)=\sup_{T_i\ge1}\mathbb E\Big[-T_i+\frac1{c_i}\max_j\Big\{\mu_j+\frac{\Sigma_{i,j}}{\Sigma_{i,i}}Z^{T_i}_i\Big\}\Big]-\frac1{c_i}\max_j\mu_j,

the supremum over stopping times of the sampling of arm $i$ . The one-step index $\nu^{cKG_1}_i$ is the same expression with $T_i\equiv1$ ((EC.6)). The cPDE policy allocates observation $t+1$ to an arm maximizing $\nu^*_i(\mu^t,\Sigma^t)$ ; the trial never stops.

Formalization targets

Goal: Theorem 1 (p. 13)

For each arm $i$ , almost surely,

\Sigma^T_{i,i}\to0,\qquad \nu^*_i(\mu^T,\Sigma^T)\to-1,\qquad \mu^T_i\to\theta_i\ \text{(also in }L^2),

and almost surely $\theta$ has a unique maximizer which, for all large $T$ , is also the unique maximizer of $\mu^T$ .

Milestones

Prop. 3 (p. 12): $Z^\tau_i$ is a uniformly integrable martingale and $\mathbb E[Z^{T}_i]=0$ for a.s. finite stopping times.
Lemma EC.1, first inequality (p. ec3): $\nu^{cKG_1}_i\le\nu^*_i$ .
Lemma EC.3 (p. ec6): if $\liminf_T\nu^{cKG_1}_i(\mu^T,\Sigma^T)=-1$ for all $i$ , then every $\Sigma^T_{i,i}\to0$ .
Lemma EC.4 (p. ec7): an arm sampled infinitely often has $\Sigma^T_{i,i}\to0$ , and $\Sigma^T_{i,i}\to0$ forces $\nu^*_i(\mu^T,\Sigma^T)\to-1$ .
Lemma EC.5 (p. ec7): if $\liminf_T\nu^*_i(\mu^T,\Sigma^T)=-1$ for all $i$ , then every $\Sigma^T_{i,i}\to0$ .

Significance

Theorem 1 is the only theoretical guarantee the paper gives for cPDE; the rest of the paper is computational (bounds, comparators, experiments). It also covers, through the same sandwich argument, the cheaper variants cPDELower and cPDEUpper (Corollary 1), which are not part of this mission. A consistent policy cannot lock onto a wrong treatment, which is the property a trial designer needs before comparing finite-horizon performance.

The result is proved on paper but has no machine-checked proof. Formalizing it requires a correlated-Gaussian Bayesian learning model, optimal stopping indices defined as suprema over stopping times, and the XFC consistency argument, none of which exist in Lean. The paper's proof also routes Lemma EC.4 through an upper bound that is false as printed (see below), so a checked proof replaces that step with a correct one.

Difficulty

The obvious route bounds $\nu^*_i$ above by a one-step index with a fixed lookahead $\bar\tau$ , as the paper's Lemma EC.1 does. That bound fails: $\bar\tau$ of (EC.11) changes under a change of currency while every index is invariant. For $M=2$ , $\mu=(0,10^{-3})$ , $\Sigma=\mathrm{diag}(10^{-6},10^{-6})$ , $\lambda=(10^{-4},10^{-4})$ , $c=(10^{-7},10^{-7})$ , the formula gives $\bar\tau=1$ and $\nu^{cKG_1:1}_1\approx-1$ , while the lookahead $T\equiv242$ already yields a value above $240$ . Any upper bound on $\nu^*_i$ must instead be uniform over stopping times of unbounded length, and showing that it tends to $-1$ needs $(\Sigma^T_{i,j})^2/\Sigma^T_{i,i}\to0$ along posterior covariances, not only $\Sigma^T_{i,i}\to0$ .

The second difficulty is the "finitely sampled arms" half of the argument (Lemmas EC.3, EC.5): an arm whose variance stays positive must keep a one-step value of sampling bounded away from zero, even while correlated arms are learned. This uses almost sure convergence of the posterior means and the structure of the piecewise linear terminal reward.

Formalization scope

Arms are Fin M (0-based) and time $t$ counts observations, $t=0$ being the prior. The trial lives on the canonical space $\theta\in\mathbb R^M$ times an array of standard normal noises $\varepsilon_{i,k}$ , with law multivariateGaussian µ0 Σ0 times an infinite product of gaussianReal 0 1; the $k$ -th sample of arm $i$ is $\theta_i+\sqrt{\lambda_i}\,\varepsilon_{i,k}$ . The index $\nu^*_i$ is built on its own auxiliary space (a prior draw of $\theta_i-\mu_i$ and i.i.d. noise), not as a conditional expectation on the trial space.

Committed conventions, each a disclosed reading of the page:

$\nu^*_i$ is (EC.8). The printed definition (15) omits $-\frac1{c_i}\max_j\mu_j$ ; with (15) Theorem 1 ii) would be false.
The supremum in (EC.8) is a real sSup over stopping times of the auxiliary filtration with $1\le T_i\le N$ for some $N$ ; this has the paper's value and keeps every expectation finite.
Ties in the cPDE argmax go to the least index (the paper: randomly). Every arm is eligible at every time ( $\mathcal M_t=\mathcal M$ ), so Assumption 1 iii) is trivial.
Theorem 1 ii) and Lemmas EC.4–EC.5 are read with $(\mu^T,\Sigma^T)$ . Theorem 1 iv) is uniqueness of the maximizer of $\theta$ plus eventual agreement of the unique maximizer of $\mu^T$ . The $L^2$ claim is MemLp plus eLpNorm → 0.
"liminf $=-1$ " in Lemmas EC.3, EC.5 is "for every $\varepsilon>0$ , the index is below $-1+\varepsilon$ infinitely often"; since both indices are $\ge-1$ this is the printed hypothesis. Lemma EC.4 is stated for every sample path.

Trivializing formalizations are ruled out: $\nu^*_i$ is defined from $(\mu,\Sigma,\lambda_i,c_i)$ , not a parameter, a fixed-lookahead index or a supremum over non-adapted times; the policy is defined, not assumed; $\mu^t$ and $\Sigma^t$ both come from (8); the $L^2$ part does not use an integral that is $0$ for non-integrable functions; iv) asserts uniqueness; and the false upper bound of Lemma EC.1 is not posed or used.

A complete development needs Gaussian conditioning for the update (8) (that $\mu^t=\mathbb E[\theta\mid\mathcal F_t]$ ), the closed form $\Sigma^t=(\Sigma_0^{-1}+\mathrm{diag}(n^t_k/\lambda_k))^{-1}$ , optional stopping for uniformly integrable martingales, measurability of the index, and the XFC argument. The Gaussian-update and optional-stopping parts are reusable for other Bayesian ranking-and-selection results; contributions of those as separate lemmas are welcome.

Selected references

S. E. Chick, N. Gans, Ö. Yapar, Bayesian Sequential Learning for Clinical Trials of Multiple Correlated Medical Interventions, SSRN 3184758 (INSEAD Working Paper 2020/40/TOM/ACGRE), version of August 31, 2020. https://ssrn.com/abstract=3184758
J. Xie, P. I. Frazier, S. E. Chick, Bayesian Optimization via Simulation with Pairwise Sampling and Correlated Prior Beliefs, Operations Research 64(2):542–559, 2016.
P. I. Frazier, W. B. Powell, S. Dayanik, The Knowledge-Gradient Policy for Correlated Normal Beliefs, INFORMS Journal on Computing 21(4):599–613, 2009.
S. E. Chick, P. I. Frazier, Sequential Sampling for Selection with Economics of Selection Procedures, Management Science 58(3):550–569, 2012.
D. Williams, Probability with Martingales, Cambridge University Press, 1991.

11 thms3 active usersReviewed

Completed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Static Pricing: Universal Guarantees for Reusable Resources: Some Static Price Guarantees 15/19 of the Profit Rate, Market Share and Service Level of an Optimal Dynamic Pricing PolicyResearch Paper

Motivation

Many services rent out a fixed stock of units that come back after use: hotel rooms, rental cars, cloud servers, hospital beds, parking spaces. Such reusable resources differ from perishable inventory because a unit sold now returns to the stock later, so the provider's pricing problem is a queueing control problem rather than a stock-depletion problem. A provider can change its price with the number of free units (dynamic pricing), or post one price and keep it (static pricing). Static prices are simpler to run, and easier to explain to customers, but they forgo the gains of reacting to congestion. How much a single price can lose is the question.

For perishable inventory, Gallego and van Ryzin (1994) showed that under a concave revenue rate a static price loses a vanishing fraction in large systems and at most a fraction $1/e$ in every regime. For reusable resources the evidence for static pricing was numerical or asymptotic: Paschalidis and Tsitsiklis (2000) reported numerical results for multi-class systems, and Gans and Savin (2007) showed near-optimality of static pricing in rental systems whose offered load and capacity are both large. Besbes, Elmachtoub and Sun (arXiv:1905.00731) gave a guarantee that does not depend on the scale of the system: a constant fraction $15/19 \approx 78.9\%$ that holds for every capacity, service rate, demand curve and weighting of the provider's objectives.

Setting

A provider owns $C \ge 1$ identical units. Customers arrive as a Poisson process of rate $\Lambda > 0$ , and at price $p$ a customer buys with probability $\bar F(p)$ ; the effective arrival rate is $\lambda(p) = \Lambda \bar F(p)$ . Prices and rates are in one-to-one correspondence, so the provider chooses a rate $\lambda \in [0,\Lambda]$ and charges $p(\lambda)$ . A buyer holds one unit for an exponential time of mean $1/\mu$ , pays $p(\lambda)$ , and costs the provider $c > 0$ . A customer who finds every unit busy is lost.

A stationary policy is a vector of rates $\lambda_1, \dots, \lambda_C \in [0,\Lambda]$ , with $\lambda_i$ used while $i$ units are free; a static policy uses one rate $l$ in every state. The number of free units is a birth–death process with steady-state probabilities

\mathbb P_i(\pi) = \frac{\frac{C!}{(C-i)!}\prod_{j=i+1}^{C}\frac{\lambda_j}{\mu}}{\sum_{k=0}^{C}\frac{C!}{(C-k)!}\prod_{j=k+1}^{C}\frac{\lambda_j}{\mu}}, \qquad i = 0, \dots, C .

The profit rate, market share and service level of the policy are

\mathcal P^\pi = \sum_{i=1}^{C}\lambda_i(p(\lambda_i)-c)\,\mathbb P_i(\pi),\qquad \mathcal{MS}^\pi = \sum_{i=1}^{C}\lambda_i\,\mathbb P_i(\pi),\qquad \mathcal{SL}^\pi = 1-\mathbb P_0(\pi),

and the provider maximizes $\alpha_1\mathcal P^\pi+\alpha_2\mathcal{MS}^\pi+\alpha_3\mathcal{SL}^\pi$ for weights $\alpha_i \ge 0$ summing to $1$ . The instance class $\Omega$ requires the profit rate $\lambda(p(\lambda)-c)$ to be concave in $\lambda$ .

For a policy $\lambda$ , the static rate $\tilde\lambda = \sum_{i\ge1}\lambda_i\mathbb P_i/\sum_{i\ge1}\mathbb P_i$ is its average rate over the states with a free unit. The proof works in the variables $z_i = \prod_{j=i}^{C}\lambda_j/\mu$ (with $z_{C+1} = 1$ ), $a_i = C!/(C-i)!$ , $x = \sum_{k=1}^{C}a_kz_{k+1}$ and $y = \sum_{k=2}^{C}a_kz_k$ , in which the ratio of service levels of $\tilde\lambda$ and $\lambda$ becomes a rational function $R(z_1,\dots,z_C)$ , and in a truncation $\tilde R \le R$ used for $C \ge 4$ .

Formalization targets

Goal: Theorem 1 (p. 11)

For every instance of $\Omega$ and every optimal stationary policy $\pi^*$ there is a static rate $l \in [0,\Lambda]$ with

\mathcal{MS}^{l} \ge \tfrac{15}{19}\,\mathcal{MS}^{\pi^*},\qquad \mathcal{SL}^{l} \ge \tfrac{15}{19}\,\mathcal{SL}^{\pi^*},\qquad \mathcal P^{l} \ge \tfrac{15}{19}\,\mathcal P^{\pi^*}\ \text{ if } \mathcal P^{\pi^*} \ge 0 .

One price serves all three objectives at once, whatever the weights.

Milestones

Lemma 1 (p. 11): optimal rates are non-decreasing in the number of free units on the states the optimal policy reaches, and $\lambda^*_C$ is at most the myopic rate $\bar\lambda$ .
(11), (12) (pp. 12–13): for the static rate $\tilde\lambda$ of any policy, the market-share ratio equals the service-level ratio and the profit ratio is at least it.
Step 2 (p. 13): the service-level ratio equals $R(z_1,\dots,z_C)$ .
Step 2a (p. 14): $R \ge 4/5$ for $C = 2$ and $R \ge 15/19$ for $C = 3$ .
Step 2b (p. 14): $\tilde R \le R$ for $C \ge 4$ .
Lemmas 2–4 (p. 15): $\partial\tilde R/\partial z_1 \ge 0$ when $y \ge a_1z_1$ ; $\tilde R(0,z_2,\dots,z_C) \ge 104/131$ ; $\tilde R \ge 6/7$ when $y \le a_1z_1$ .
Combination (p. 15): $R \ge \tilde R \ge \min\{104/131, 6/7\} \ge 15/19$ for $C \ge 4$ .

Significance

The theorem bounds the value of dynamic pricing for reusable resources by a universal constant: dynamic pricing can improve each objective by at most a factor $19/15$ , so a provider can adopt a single price at a known, bounded cost. Since the same price works for all weights, the optimal static price also earns at least $15/19$ of the optimal weighted objective. Section 3.2 of the paper shows that the constructed static rate $\tilde\lambda$ attains exactly $15/19$ in a limit, so the analysis of that rate cannot be improved.

The result is proved in the paper (arXiv v3, 2020; Operations Research, 2022). No part of it has a machine-checked proof. Formalizing it checks a proof whose second half is a case analysis of high-degree rational functions spread over ten pages of an e-companion, and produces closed-form, reusable statements about the stationary distribution of finite birth–death chains with state-dependent rates.

Difficulty

Step 1 is algebra and one application of Jensen's inequality. The difficulty is in bounding $R$ for every $C$ . For $C \le 3$ the bound is coefficient matching between two explicit polynomials. For $C \ge 4$ the numerator and denominator of $R$ have degree growing with $C$ , and no term-by-term comparison works uniformly; the paper's lemmas each cover a regime of $y/z_1$ and require bookkeeping that is uniform in $C$ .

A second difficulty is Lemma 1. It is a statement about the average-reward optimal policy of a controlled birth–death chain, proved in the paper by value iteration. In the formal statement optimality is a maximization over the closed-form objective, so a proof must either develop the average-reward optimality equation for this chain or argue directly on the closed form. The goal itself quantifies over every optimal policy, including any that is not monotone; the paper's combination step assumes the monotone structure that Lemma 1 provides only on reached states, so a complete proof of the goal must handle this gap.

Formalization scope

The model is posed over stationary state-dependent pricing policies with the closed-form steady state of §2.3; the paper's reduction from general non-anticipating policies to stationary ones, and the long-run averages (1)–(2), are taken as the model and not re-proved. A policy is a function lam : ℕ → ℝ read at the states $1,\dots,C$ with rates in $[0,\Lambda]$ ; optimality is IsMaxOn of the weighted objective over this set, and existence of an optimal policy is not assumed. Standing assumptions (the structure Standing): $C \ge 1$ ; $\mu,\Lambda,c > 0$ ; $\alpha_i \ge 0$ with $\alpha_1+\alpha_2+\alpha_3 = 1$ ; $\lambda(p(\lambda)-c)$ concave on $[0,\Lambda]$ ; $p$ strictly decreasing on $(0,\Lambda]$ .

Added hypotheses, each disclosed in its item: Theorem 1's profit bound is conditional on $\mathcal P^{\pi^*} \ge 0$ (the profit ratio is meaningless otherwise); Lemma 1 assumes $\alpha_1 > 0$ and strict concavity, and restricts monotonicity to states of positive probability (the printed version is false without these). Lemma 2 and the combination step are stated for every nonnegative $z$ , as printed. Identities (11), (12) and the $R$ identity are stated for every stationary policy, since their derivations use no optimality.

The objectives are the closed forms above, not free functions constrained by hypotheses; ratios are cross-multiplied so that no objective is divided by a possibly zero quantity; $z_{C+1} = 1$ is built into the definitions so that $R$ and $\tilde R$ never divide by zero for $z \ge 0$ ; the derivative in Lemma 2 is asserted with HasDerivAt, not deriv. Every constant ( $15/19$ , $4/5$ , $104/131$ , $6/7$ ) appears as stated.

Needed beyond Mathlib's finite sums and products, Nat.descFactorial, ConcaveOn and HasDerivAt: nothing. Theorem 2 (the 95.5% guarantee for two units and linear demand), its Lemmas 5–6, the tightness example of §3.2 and the numerical experiments are out of scope. Proofs of any milestone, and alternative proofs of the bound on $R$ , are welcome.

Selected references

O. Besbes, A. N. Elmachtoub, Y. Sun, Static Pricing: Universal Guarantees for Reusable Resources, arXiv:1905.00731v3, 2020; Operations Research, 2022. https://arxiv.org/abs/1905.00731
I. Ch. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842141
G. Gallego, G. van Ryzin, Optimal dynamic pricing of inventories with stochastic demand over finite horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
N. Gans, S. Savin, Pricing and capacity rationing for rentals with uncertain durations, Management Science 53(3) 390–407, 2007 (cited on p. 11 for the monotonicity of optimal prices in a discounted setting).

13 thms3 active usersReviewed

Completed

Functional Analysis·Captain: Yuxuan Xu

Sharp diagonal Hlawka constant: formalize cutoff 21Research Paper

Motivation

A norm measures the size of a vector. The triangle inequality says that adding two vectors cannot increase their size beyond the sum of their sizes. The Hlawka constant problem asks for a quantitative comparison between the deficit in a three-vector triangle inequality and the sum of the deficits in the three two-vector inequalities. For operator norms, the comparison constant must work in every matrix dimension. Audenaert and Kittaneh state this question in Section 8.2, Problem 7 of Problems and Conjectures in Matrix and Operator Inequalities.

This mission concerns the diagonal, or commuting, case. For a complex diagonal matrix, its Schatten p-norm equals the coordinate p-norm of its diagonal. An exact answer in this setting identifies a concrete extremal family while preserving the requirement that the constant work in every finite dimension. It does not settle the sharp constant for arbitrary noncommuting matrices.

The foundation mission formalizes the cyclic formula for real exponents at least 256. The accepted cutoff-32 theorem, recorded on 16 October 2026, lowers that threshold. The present source is Yuxuan Xu's AI-assisted research preprint, which supplies a computer-assisted argument extending the formula to all real exponents at least 21. The preprint has not undergone independent analytic review. Its new interval has numerical verification reports but no Lean proof.

Setting

For a real exponent p greater than one and a finite complex vector x, define the coordinate p-norm by

N_p(x)=\left(\sum_i |x_i|^p\right)^{1/p}.

For three vectors x, y, and z in the same dimension, set

S=N_p(x)+N_p(y)+N_p(z),\qquad T=N_p(x+y+z),

P=N_p(x+y)+N_p(x+z)+N_p(y+z),\qquad G=2S-P.

The quantity S minus T is the triple deficit. The quantity G is the sum of the three pair deficits and is nonnegative by the triangle inequality. A real number C is a uniform Hlawka constant when

S-T\le C G

for all triples and all finite complex dimensions. No equal-norm or nonzero-vector restriction is part of this property.

The candidate sharp constant is specified by an explicit scalar formula. For a real parameter t in the closed interval from one half to two, let

A_p(t)=(t^p+2)^{1/p},\qquad B_p(t)=(2|1-t|^p+2^p)^{1/p},

R_p(t)=\frac{3A_p(t)-3^{1/p}|2-t|}{6A_p(t)-3B_p(t)},\qquad K_p=\sup_{1/2\le t\le2}R_p(t).

The ratio comes from the cyclic triple (-t,1,1), (1,-t,1), and (1,1,-t). In the exponent range of the mission its denominator is positive, and continuity makes the supremum an attained maximum. The mission imports the campaign's existing definitions of these quantities.

Formalization targets

The goal is Theorem 1.1 of the source preprint, in the campaign's exact statement format:

\forall p\in\mathbb R,\quad 21\le p\ \Longrightarrow\ K_p=\min\{C\in\mathbb R:\ \forall n\in\mathbb N,\ S-T\le C G\text{ on }\mathbb C^n\}.

Here the minimum notation includes both admissibility and leastness; existence of an admissible constant is part of the conclusion. The theorem does not assume that certificate validation, localization, or convexity already holds. It does not assert that 21 is the smallest possible exponent threshold.

Four supporting targets follow the source's two finite windows. Equation (7) and Table 1 give, on each full real interval, the scalar inequalities

cp<K_p\le p/2,\qquad E_p(q)<K_p,\qquad E_p(q)=\frac{1-q}{2\left(1-((1+q^p)/2)^{1/p}\right)}.

Window I is [21,26], with c=273/625 and q=1011/2500. Window II is [26,32], with c=443/1000 and q=197/500. Two further targets are the unconditional real three-dimensional Hlawka inequalities on these respective windows, as concluded in Section 7 of the source. The previously proved tail for p at least 32 is included as a referenced theorem, preserving its published identity and attribution.

Significance

The proposed result would extend the known formalized range of the exact diagonal constant from p at least 32 to p at least 21. It would give one constant simultaneously for all complex dimensions and for all real exponents in that range, rather than separate statements at selected integer exponents. The cyclic witnesses also explain the obstruction to decreasing the constant itself.

Formalizing this source means closing the gap between its analytic argument and its finite computations. The release replay report records exact rational linear-dual replay and directed interval checks. Those reports support the paper's computer-assisted claim; they are not kernel-checked proofs of the mission's open statements. A completed mission must establish those statements in the platform's ordinary proof system.

Difficulty

The least constant is defined through a special three-dimensional family, but admissibility quantifies over arbitrary triples in arbitrary dimensions. Unequal singleton norms and degenerate triples are included. Arguments that verify only the cyclic family establish a lower bound and leave the main admissibility assertion unresolved.

The source also requires inequalities uniform in a continuously varying real exponent. Pointwise numerical optimization and dense sampling cannot establish such interval statements. Its localized convexity estimates retain norm bounds and linear coordinate-sum constraints; each retained constraint must genuinely follow from the preceding localization argument, and the averaging domain must remain convex. In particular, retaining a norm-sum equality as if it defined a convex domain would not justify the required averaging step. These issues are part of the formalization target, not additional assumptions supplied to solvers.

Formalization scope

The environment is Mathlib commit 0df444a360eaa60ab8c11dca51a86af692955474, using Lean v4.33.1. The goal uses Fin n → ℂ, real p, the existing lpNorm, cyclicConstant, and HasHlawkaConstant, and IsLeast over real constants. Natural-number dimensions include zero. In dimension zero all coordinate norms vanish, so the inequality is harmless; triples containing zero vectors remain included in positive dimensions. All quantities must retain their foundation definitions.

The four new milestone declarations use the same scalar and coordinate definitions, including the existing scalarEnvelope. They introduce no replacement norm and no axiom saying that an external Python execution is correct. The source package contains exact certificates, two arithmetic implementations, and explicit remainder estimates for its rational interval backend. Those implementations share the mathematical model and are not independent end-to-end proofs. Independent analytic review remains pending.

Contributions may reuse the existing dimension reduction, complex transfer, cyclic sharpness, and cutoff-32 results when their hypotheses match the target range. Formalization of the new scalar bounds, exact linear-dual implications, interval arithmetic soundness, and real three-dimensional admissibility is welcome. Proof details and the proposed dependency order are available in the source paper and the milestone descriptions. The declarations uploaded with this proposal are statements to prove, with the standard by sorry placeholders; compiling them checks well-formedness only.

Selected references

Yuxuan Xu (徐宇轩), School of Computer Science, Wuhan University, A computer-assisted sharp diagonal Hlawka inequality for real exponents p ≥ 21, research preprint, v1 (2026). PDF, LaTeX, certificates and code. AI assistance is disclosed in the paper.
K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv:1201.5232v3 (2012), Section 8.2, Problem 7. Source.
D.-Ş. Marinescu and C. P. Niculescu, A survey of the Hornich–Hlawka inequality, arXiv:2407.03278 (2024). Source.
Ezzeri Esa / savarin and contributors, Dimension-independent Hlawka constants for Schatten norms, Lean source repository (2026). Repository.
Prove2Me contributors, including @bwdaugherty, Sharp diagonal Hlawka constant: cutoff 32 (2026). Accepted theorem, campaign. Exact source identifiers and hashes are preserved in the paper repository's provenance record.

11 thms3 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: marwahaha

Sands–Sauer–Woodrow: monochromatic paths in two-coloured tournamentsResearch Paper

Motivation

A tournament is a directed graph in which every two distinct vertices are joined by exactly one arc — the model of a round-robin competition, and the setting of Ramsey theory's oldest questions.

In 1982 Sands, Sauer and Woodrow asked: if the arcs of a tournament are coloured with two colours, must some vertex be reachable from every other vertex along a monochromatic path, one whose arcs all carry the same colour? They answered yes [SSW82, Corollary 2, p. 273], through a theorem on arbitrary digraphs [SSW82, Theorem 1, pp. 271–273]. That theorem is also the two-colour case of kernel theory: kernels are independent dominating sets, they exist in digraphs whose arcs split into two transitive classes, and the stable-marriage theorem is a special case [Ch26, §1].

The tournament statement is the settled case of a question of Erdős that remains open: with three colours, must either a rainbow directed triangle occur, or a vertex reach every other vertex monochromatically [SSW82, PROBLEM, p. 275]? The platform already carries that open problem as the mission "Monochromatic reachability or rainbow triangles" (OPG1808.root_problem). This mission is the two-colour theory beside it, not a duplicate: it collects the results that are known and that any attack on the three-colour question builds on.

Timeline. Sands–Sauer–Woodrow (1982) prove Theorem 1, deduce the two-colour tournament statement, exhibit a three-coloured tournament with no vertex reaching all others, and ask whether three colours force a rainbow triangle or such a vertex [SSW82]. Shen Minggang (1988) proves the theorem for any number of colours when no triangle carries three distinct colours [Mi88]. Galeana-Sánchez and Rojas-Monroy (2005) give a six-vertex four-coloured tournament with neither, so three colours is the last case of the rainbow formulation [GR05]. Bousquet, Lochet and Thomassé (2017) show that a k-coloured tournament has a dominating set of size $O(\ln 2k \cdot k^{k+2})$ built from monochromatic paths — bounded, but not the single vertex of the two-colour case [BLT17]. Chancelier (2026) gives the first machine-checked proof of the general theorem, in Rocq, and records that no Lean formalization exists [Ch26].

Setting

Fix a vertex type $V$ . A digraph is a relation $D : V \to V \to \mathrm{Prop}$ , written $x \to y$ ; an arc colouring assigns each ordered pair a colour in $\mathrm{Fin}\,3$ ; a colouring uses at most two colours when every arc has colour $0$ or colour $1$ . A tournament is a loopless digraph in which every two distinct vertices are joined by exactly one arc.

A monochromatic path from $x$ to $y$ has distinct vertices, consecutive ones joined by an arc, all those arcs of one colour; write $x \rightsquigarrow y$ when one exists, and say that $x$ monochromatically reaches $y$ . A set $S$ is monochromatically independent when no two distinct members are connected by a monochromatic path in either direction — this is not graph independence: in a tournament a single arc joins any two vertices, so such a set has at most one element. A digraph has no monochromatic infinite outward path when no injective $x : \mathbb{N} \to V$ has all arcs $x_n \to x_{n+1}$ of one colour.

Formalization targets

Goal — the two-coloured tournament theorem (SSW Corollary 2)

$D$ a tournament on a nonempty finite vertex type, its arcs coloured with at most two colours:

\exists v,\ \forall x,\ x \neq v \Rightarrow x \rightsquigarrow v .

Milestone — the two-coloured digraph theorem (SSW Theorem 1)

$D$ any digraph on any vertex type, arcs coloured with at most two colours, with no monochromatic infinite outward path:

\exists S,\ S \text{ monochromatically independent} \ \wedge\ \forall x,\ x \notin S \Rightarrow \exists s \in S,\ x \rightsquigarrow s .

Milestone — the source form of the goal

The goal in the orientation of the platform's existing definition, the distinguished vertex reaching the others:

\exists s,\ \forall t,\ s \rightsquigarrow t .

Milestone — the blocked three-coloured theorem (SSW Theorem 3)

$T$ a tournament whose arcs carry three colours and whose vertices are partitioned into blocks, two vertices of different blocks always joined by a red arc and two of the same block by a blue or a green arc; then some vertex is monochromatically reached by every other.

Significance

The result. The goal settles the two-colour case of Erdős's question in the sharp form that one vertex suffices, and it is the base of the known theory: the paper's own block-coloured three-colour theorem is proved from it by iteration, and the kernel and stable-matching corollaries of the general theorem make it standard digraph theory. Without it the three-colour question has no settled case to compare against.

Formalizing it. No Lean formalization of these statements is recorded, for the corollary or for the general theorem [Ch26]; the machine-checked development that exists is in Rocq, for the general theorem, and is the first for the infinite case. This mission produces, in Lean, a classical theorem the platform does not have, together with the definitions it rests on: monochromatic reachability and monochromatic independence over an arbitrary vertex type. Status is stated per target: the goal is a theorem of the source paper, not an open question; the three-colour problem beside it remains open.

Difficulty

The first idea — take a longest monochromatic path and read off its end — does not close the argument. It gives monochromatic reachability only for the vertices on the path; for a vertex outside it, one knows only that the arcs from the path to that vertex cannot continue the path's colour, which yields no path back to the path's end. The source instead takes a maximal element, under a relation mixing the two colours, of a family of monochromatically independent sets — $S \preceq T$ when every $s \in S$ has $s \in T$ , or a blue path to some $t \in T$ with no red path back — and shows by a minimal-counterexample argument on red reachability that a maximal element is the required set. Over an arbitrary vertex type the family needs Zorn's lemma, and the no-infinite-outward-path hypothesis, not finiteness, is what bounds the argument. A second trap is definitional: because independence here is monochromatic, the tournament case collapses to one vertex; a formalization using graph independence would state a different and false theorem.

Formalization scope

Reuses the platform module opg1808_colored_tournaments: Digraph V := V → V → Prop, ArcColoring V := V → V → Fin 3, IsTournament, and MonochromaticallyReaches, the reflexive-transitive closure of one colour's arcs. A new definition supplies monochromatic independence; prose and statements use the same notation.
Colours are three-valued even when two occur, matching that module; the two-colour hypothesis says every arc has colour $0$ or colour $1$ . Relabelling two used colours into $\{0,1\}$ preserves which paths are monochromatic, so nothing is lost.
The source allows loops and multiple edges; the formalization uses a simple relation. Multiple edges are irrelevant, since reachability depends only on the presence of an arc, and loops are excluded by IsTournament. For the general digraph target loops change nothing, as the source's paths have distinct vertices.
The source's paths have distinct vertices while MonochromaticallyReaches uses walks; the two agree for reachability, and independence is stated through walks, so no distinctness hypothesis is needed.
The goal is stated on [Fintype V] [Nonempty V]; nonemptiness is required, the target being false on an empty vertex type. The general target is stated on an arbitrary type, and its hypothesis is vacuous in the finite case, which is the entry point for the goal.
The platform's IsMonochromaticSource is the reversed orientation of the goal; the goal follows the source paper, which orients paths towards the distinguished vertex.

Needed: the reused module, a definition of monochromatic independence, reachability lemmas for two colour classes, and for the general target Zorn's lemma and infinite outward paths. The reachability and independence layer is reusable by any later mission on coloured digraphs, including the three-colour problem beside this one. Contributions to any target are welcome.

Selected references

B. Sands, N. Sauer, R. Woodrow, On monochromatic paths in edge-coloured digraphs, J. Combin. Theory Ser. B 33 (1982), no. 3, 271–275. Theorem 1 (pp. 271–273), Corollary 2 (p. 273), Theorem 3 (pp. 274–275), PROBLEM (p. 275). https://doi.org/10.1016/0095-8956(82)90047-8
S. Minggang, On monochromatic paths in m-coloured tournaments, J. Combin. Theory Ser. B 45 (1988), 108–111. https://doi.org/10.1016/0095-8956(88)90062-2
H. Galeana-Sánchez, R. Rojas-Monroy, Monochromatic paths and at most 2-colored arc sets in edge-coloured tournaments, Graphs Combin. 21 (2005), 307–317. https://doi.org/10.1007/s00373-005-0627-y
M. Melcher, K. B. Reid, Monochromatic sinks in nearly transitive arc-colored tournaments, Discrete Math. 310 (2010), 2697–2704. https://doi.org/10.1016/j.disc.2010.05.017
N. Bousquet, W. Lochet, S. Thomassé, A proof of the Erdős–Sands–Sauer–Woodrow conjecture, arXiv:1703.08123 (2017). https://arxiv.org/abs/1703.08123
J.-P. Chancelier, A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect, arXiv:2604.21376 (2026). https://arxiv.org/abs/2604.21376
Open Problem Garden, Monochromatic reachability or rainbow triangles. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles

6 thms3 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics CII: Multiple-Life Survival, Joint-and-Survivor Annuities and Contingent AssurancesTextbook

Multiple-Life Survival, Joint-and-Survivor Annuities and Contingent Assurances

Motivation

A multiple-life contract has payments depending on the survival of more than one individual. A joint-life pension might stop at the first death, while a last-survivor annuity continues until both lives have died. A retirement pension may continue in a smaller amount to a surviving spouse, and a policy may instead pay one capital sum on the first or second death. These arrangements arise in pension schemes, life insurance and the valuation of dependent beneficiaries. They have different claim events, beneficiaries and settlement dates. The distinction matters in actual valuation, especially when both deaths occur between scheduled pension dates.

The basic mathematical objects are laid out in Promislow's Fundamentals of Actuarial Mathematics, third edition (2015, Chapter 10), and Dickson, Hardy and Waters' Actuarial Mathematics for Life Contingent Risks, third edition (2020, Chapter 10). Both discuss joint and last-survivor states. The latter also treats dependent future lifetimes and common shocks. The mission develops event-consistent formulas from a shared joint mortality law, rather than selecting unrelated survival probabilities for different contract components.

Setting

Let two future lifetimes be represented by death-time states $K_x$ and $K_y$ on a finite grid with right-censoring horizon $h$ . For $i<h$ , state $K_x=i$ means the first life dies in the interval after anniversary $i$ and its death benefit is payable at tick $i+1$ under the annual settlement convention. The terminal state $K_x=h$ means that this death has not been observed before the horizon. The same convention applies to the second life. More finely spaced ticks can represent payment and death dates within a year, so ordering is retained when the two deaths fall in different subannual intervals.

The joint probability mass function is $p_{ij}=\Pr(K_x=i,K_y=j)$ , with $p_{ij}\geq0$ and $\sum_{i=0}^{h}\sum_{j=0}^{h}p_{ij}=1$ . It determines both one-life margins and their dependence. In particular, the probability that both lives are alive at tick $t$ is $\sum_{i,j}p_{ij}\mathbf{1}_{\{t\leq i\}}\mathbf{1}_{\{t\leq j\}}$ . Products of the two marginal survival probabilities are valid only under an explicit independence assumption.

At a scheduled payment anniversary there are four disjoint in-force states: both alive, member only, spouse only and neither alive. The joint-life status is the both-alive state. The last-survivor status consists of all states except neither alive. The reversionary spouse status is specifically member dead and spouse alive. A reversionary pension starts once member death makes the spouse entitled and pays only when the spouse is alive at the relevant instalment date. This is contractually distinct from an unqualified joint-and-survivor pension, whose original member and survivor amounts may follow a different schedule.

Write $d_t$ for a discount factor taking a payment at tick $t$ to commencement, and $b_t$ for its gross benefit amount. A member pension may pay $b_t$ while the member is alive and $\rho b_t$ when the member is dead but the spouse remains alive. The ratio $\rho$ is the spouse continuation factor. Unless stated otherwise, the status is tested at each scheduled payment date, so a spouse who dies before the first eligible instalment receives no instalment. Death lump sums use the tick immediately after their death-year state and are distinct from these scheduled pension payments.

Formalization targets

Joint-law occupation states

The first group constructs the joint law, marginal survivals and four exclusive occupation states. Their probability sums and event identities must agree without assuming independent lives. Strict order events $K_x<K_y$ and $K_y<K_x$ are accompanied by the tie event $K_x=K_y$ ; both terminal states are right-censored and must not cause a fictitious death claim. Equal grid times are treated as genuine ties in the grid model. Physical simultaneous death in continuous time requires a separate law assigning it positive mass.

Annuity and reversionary values

The second group gives realised annuity cashflows and expected present values for joint-life, last-survivor, member-only and reversionary spouse statuses. A key identity for identical payment dates and discounting is

a_{\text{last}}=a_x+a_y-a_{xy},\qquad a_{y\mid x}=a_y-a_{xy}.

The first term values any surviving life, and the second values the spouse-only reversion. These identities are valid under general dependence because all terms come from the same joint distribution. For a member pension with a separately contractual spouse continuation of $\rho$ , its expected value is

V=a_x+\rho a_{y\mid x} =(1-\rho)a_x+\rho a_{\text{last}}.

This formula presumes the member payment and spouse payment are evaluated at the same dates with no overlapping guarantee or independent payment entitlement. Guarantee cashflows require separate contractual events.

Order-sensitive death claims

The third group models a unit claim on the first death, a unit claim on the second death, the member dying first, the spouse dying first and simultaneous-grid death. It also models a later death of the survivor and pure endowments contingent on joint or last-survivor survival. Payment at death and payment on a pension anniversary can differ even when the same person eventually receives a benefit. Both deaths within a year are represented with a sufficiently fine tick grid; annual year-end states alone do not identify their physical order.

Integrated capstone

The capstone values a combined pension and assurance from the realised cashflow across all death-time pairs. It then reconciles the expected value independently against single-life, reversionary and last-survivor annuity factors, together with the disjoint first- and second-death assurance values. The event partition is incorporated in the total cashflow rather than appended as an unrelated identity.

Significance

The identities provide actuarially auditable bridges between benefits administered by member and spouse status and factors calculated by conventional life-contingency methods. In Dickson, Hardy and Waters (2020, Chapter 11), pension mathematics supplies further context. They can be used to check spouse continuation calculations in defined benefit pension administration, premium valuations of first- and second-death assurances, and mortality stress tests where lives in a household may be dependent. A dependent joint law can change the joint annuity and first-death insurance values while preserving each single-life margin.

The formalisation keeps payment timing, benefit entitlement, event order and valuation date visible in the mathematics. In the published sources the classical factor relations are known results, while the present finite-grid cashflow definitions and their combined capstone are original derived formulations. Each proposed theorem remains an open formal target until independently verified by Prove2Me's authoritative remote Lean compiler and, separately, proved.

Difficulty

Marginal survivals do not determine joint survival or within-year death order. A spouse may become entitled before the first payable instalment, and may die between those events. Death settlement, grid ties and terminal censoring therefore require careful treatment. The capstone reconciles expected realised cashflows with independently calculated factors, preserving the same joint law, dates and entitlement rules in both valuations.

Formalization scope

The Lean kernel uses finite double sums over one right-censored joint law. Due, arrears, subannual, deferred and guaranteed member/spouse cashflows are defined. Death timing is represented on an integer grid; periods can be made subannual by changing the tick size. Scheduled pension payments are due at their specified ticks. Lump sums are settled at the following death tick. Discount factors and benefit amounts are parameterised as schedules; no particular flat interest rate is built into the definitions.

In the guarantee kernel, $g$ is an absolute expiry tick and $a$ starts the payment window. Guaranteed member payments do not require survival to $a$ : they model an already vested obligation, not a pension conditional on reaching retirement. A guarantee lasting $G$ periods from $a$ would expire at $a+G$ and require a separate retirement-eligibility condition. UK defined benefit death-in-deferment and dependant entitlements are scheme-specific and outside this kernel.

The main decomposition identities do not need independence, and explicit independent/dependent finite counterexamples are staged for remote theorem proofs. Equal-tick ties are explicit. A smooth continuous-time law, arbitrary within-tick death times, integrals for immediate death settlement, changing spouse eligibility and other pension guarantee arrangements require further declarations and remote verification before the complete mission can be released. The finite model does not imply those continuous-time results. Annuity-certain or single-life results from other unpublished owner Drafts are not assumed to be importable.

Formal contributors must preserve the same probability law and the same discount and settlement conventions across all components of any identity. A vacuous statement established by assuming its intended conclusion, using inconsistent marginals or suppressing the tie event does not meet the mission's mathematical contract.

Selected references

S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, Chapter 10, Sections 10.2–10.8, publisher-linked contents.
D. C. M. Dickson, M. R. Hardy and H. R. Waters, Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020, Chapter 10, book DOI.

159 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Cross-licensing in a Supply Chain with Asymmetric Manufacturers II: Every Innovation Equilibrium Is a Downstream Duopoly, Boundary or InteriorResearch Paper

Motivation

In industries built on a key component sold by one dominant supplier, such as smartphone chipsets, the supplier's contract terms shape how much its downstream customers innovate. Some suppliers require their customers to cross-license their own patents to each other as a condition of buying the component, so that each manufacturer's innovation also improves its rival's product. Wang, Huang and Lee (SSRN 3053682; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2019.0477) ask when a supplier facing two manufacturers of unequal innovation ability benefits from imposing cross-licensing. Their answer runs through the equilibrium of the manufacturers' innovation game, which is the subject of this mission: Proposition 2 describes how much each manufacturer innovates and shows that the supplier never ends up selling to a single manufacturer.

Setting

A supplier sells a component at wholesale price $r \ge 0$ to manufacturers $M_1$ and $M_2$ . Manufacturer $M_i$ chooses a quality improvement $T_i \ge 0$ at cost $k_iT_i^2$ . With cross-licensing of effectiveness $\beta \in [0, 1]$ , the quality improvement of $M_i$ is $T_i + \beta T_j$ ( $j \ne i$ ), and its inverse demand is $p_i = 1 + T_i + \beta T_j - q_i - q_j$ . The standing assumptions are

0 \le \beta \le 1, \qquad \tfrac{49}{144} < k_2 < k_1,

so $M_2$ is the superior manufacturer. The game has three stages.

Quantities. Given $(T_1, T_2)$ and $r$ , each $M_i$ chooses $q_i \ge 0$ to maximize $\Pi_i = (1 + T_i + \beta T_j - q_i - q_j - r)q_i$ (display (1)). The equilibrium quantities, display (2), are a duopoly when $r$ is low and a monopoly of the manufacturer with the higher quality when $r$ is higher.
Price. The supplier chooses $r \ge 0$ to maximize $r(q_1 + q_2)$ . Its price $r^*(T_1, T_2)$ is the least maximizer. Lemma 1 computes it: the supplier induces a duopoly exactly when $\beta \ge \sqrt3 - 1$ or $T_2 \le \hat T_2(T_1\mid\beta)$ , where

\hat T_2(T_1\mid\beta) = \frac{2 - \sqrt3 + T_1(1 - \beta(\sqrt3 - 1))}{\sqrt3 - 1 - \beta}.

Innovation. Each $M_i$ chooses $T_i \ge 0$ to maximize $\Pi^*_i(T_1, T_2\mid\beta) - k_iT_i^2$ , where $\Pi^*_i$ is its Cournot profit at the supplier's price. An innovation equilibrium is a pure Nash equilibrium of this game.

The proof of Proposition 2 defines two candidate profiles in closed form: the interior candidate $T^I = (T^I_1, T^I_2)$ , which solves both manufacturers' first-order conditions, and the boundary candidate $T^B = (T^B_1, T^B_2)$ , where $M_2$ invests exactly up to $\hat T_2$ . A threshold $\hat k_2(k_1\mid\beta)$ separates them, and $T^*(\beta) = T^B$ if $k_2 < \hat k_2(k_1\mid\beta)$ , $T^*(\beta) = T^I$ otherwise.

Formalization targets

Goal: Proposition 2 (p. 12)

Under the standing assumptions:

every innovation equilibrium is a duopoly, meaning both manufacturers sell a positive quantity at the supplier's price;
$T^*(\beta)$ is an innovation equilibrium and a duopoly;
if $k_2 < \hat k_2(k_1\mid\beta)$ , then $\beta < \sqrt3 - 1$ and $M_2$ is on the boundary:

T^*_2 = \hat T_2(T^*_1\mid\beta);

if $k_2 \ge \hat k_2(k_1\mid\beta)$ , then $T^*(\beta) = T^I$ and both duopoly first-order conditions hold at $T^*(\beta)$ .

Milestones

display (2): the Cournot quantities are the unique equilibrium of the quantity game;
Lemma 1: the supplier's price, the regime, its optimal profit, and the gross profits $\Pi^*_1, \Pi^*_2$ ;
monopoly infeasibility at $T_1 = 0$ , from the proof (p. A.1): $M_2$ 's monopoly optimum $1/(16k_2 - 1)$ lies below $\hat T_2(0\mid\beta)$ ;
$T^I$ is the unique solution of the two first-order conditions (p. A.1);
$T^B_2 = \hat T_2(T^B_1\mid\beta)$ , and $T^B_1$ is $M_1$ 's best response to $T^B_2$ (p. A.1);
$\hat k_2$ is where $T^I_2 = T^B_2$ , and above it $T^I$ lies in the duopoly region (p. A.2);
$\hat k_2(k_1\mid\beta)$ is strictly decreasing in $\beta$ with $\hat k_2(k_1\mid 1) = 0$ (p. A.2), so the boundary region shrinks to empty as $\beta$ grows.

Significance

Proposition 2 is the paper's equilibrium characterization. Proposition 3 is its instance $\beta = 0$ (no cross-licensing), and Proposition 4 compares the supplier's equilibrium profits with and without cross-licensing on the closed forms $T^B$ , $T^I$ and $\hat k_2$ established here. The economic content is that, under cross-licensing, the supplier always ends up selling to both manufacturers. When the superior manufacturer's cost advantage is large it caps its own innovation exactly where the supplier stops preferring a monopoly.

The paper's proof states the closed forms and asserts the checks ("one can obtain", "we verify"). This mission produces a machine-checked version: a complete definition of the three-stage game, with the supplier's price defined as an optimization rather than by its solution, and the equilibrium claims stated against that game. To our knowledge no part of this result has been formalized before.

Difficulty

The innovation payoff of the superior manufacturer is discontinuous. When $T_2$ moves just above $\hat T_2(T_1\mid\beta)$ , the supplier switches from a duopoly price to a monopoly price, and $M_2$ 's gross profit jumps down. A first-order argument therefore does not show that $T^*$ is an equilibrium. One must also show that $M_2$ never gains by moving into the monopoly region, and that $M_1$ never gains by deviating above $T_2$ , where $M_1$ itself becomes the potential monopolist. The boundary candidate is an equilibrium only because the supplier breaks its indifference at the boundary toward the duopoly.

Part 1 quantifies over every equilibrium, not only $T^*$ . The paper checks monopoly infeasibility only at $T_1 = 0$ , so the general case needs its own argument. The equilibrium is not unique: for some parameters a mirrored profile with $M_1$ at its own boundary is also an equilibrium. Uniqueness is therefore not claimed. The remaining steps are polynomial and rational inequalities in $(k_1, k_2, \beta)$ involving $\sqrt3$ .

Formalization scope

Parameters $\beta, k_1, k_2$ are real numbers. The standing assumptions $0 \le \beta \le 1$ and $49/144 < k_2 < k_1$ are bundled as Standing β k1 k2.
Quantities and innovation levels range over $\mathbb R_{\ge 0}$ (NNReal). Equilibria use the published two-player predicate CompetingChains.Cournot.IsPureNash.
Wholesale prices range over $[0, \infty)$ . The paper leaves this implicit, so it is a disclosed addition.
Display (2) is encoded in symmetric form, with the manufacturer of larger quality as the possible monopolist. The paper prints it for $T_2 \ge T_1$ , but deviations in the innovation game reach $T_1 > T_2$ .
The supplier's price is the least maximizer of $r(q_1 + q_2)$ over $r \ge 0$ . This is the tie-break Lemma 1 uses at $T_2 = \hat T_2$ .
First-order conditions are stated as derivatives (HasDerivAt … 0) of Lemma 1's duopoly polynomials, because the game payoff is not differentiable at the boundary.
All closed forms are transcribed as printed, with $\sqrt3$ as Real.sqrt 3. Every denominator is proved nonzero in its regime, never assumed.

Two trivializing formalizations are ruled out. Equilibria are never defined by first-order conditions or by the closed forms, and the supplier's price is never defined by Lemma 1's case rule. Both are theorems here.

The source is the authors' SSRN manuscript (abstract 3053682, version of 2023-04-27); its proofs are in the appendix, pp. A.1–A.9. The paper's equivalent threshold $\hat\beta(k_1, k_2)$ is not formalized. Proofs of any milestone are welcome. Lemma 1 and display (2) are self-contained, and the closed-form milestones need only real-algebraic inequalities with $\sqrt3$ .

Selected references

J. Wang, T. Huang, H. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN 3053682, version of 2023-04-27. https://ssrn.com/abstract=3053682
J. Wang, T. Huang, H. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2019.0477

11 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes II: Consortium Price, No Cure No Pay: Subsidize Only Patients When the Price Is High, Only the Manufacturer When LowResearch Paper

Motivation

A rare disease affects few patients, so a drug for it has a small market and its research and development (R&D) cost is spread over few sales. Governments respond with two kinds of subsidy: cost subsidies that pay part of the manufacturer's R&D bill (orphan drug programmes), and price subsidies that pay part of what each patient is charged. At the same time two practices change how drugs are priced and paid for. In some markets an independent consortium negotiates the price instead of the manufacturer, and some manufacturers offer outcome-based payment ("No Cure No Pay", as in a programme of Bristol-Myers Squibb), under which the patient pays only if the drug works.

W. Olsder, T. Martagan and C. S. Tang ask how a government with a fixed budget should divide it between the manufacturer and the patients under each pricing and payment regime. This mission formalizes their analysis of the regime with a consortium price and outcome-based payment, Setting (2B) of the paper, where the answer depends on the price: for a high price only patients should be subsidized, and for a low price only the manufacturer. The source is the SSRN working paper 3481150 (version of 2019-11-13); the article later appeared in Management Science (2023) with possibly different numbering, which is not used here.

Setting

The market has size one. A patient's valuation $V$ of an efficacious drug is uniform on $[0,1]$ . The model has three positive primitives: the R&D cost scale $k$ , the government's budget $B$ , and the unit price $p$ , which the consortium fixes and which lies in $(0,1)$ .

A subsidy policy is a pair $(\alpha,\beta)$ with $\alpha\in[0,1)$ and $\beta\in[0,1)$ . The government pays the share $\alpha$ of the R&D cost and the share $\beta$ of the unit price.
The manufacturer chooses a target efficacy $e>0$ , the probability that the drug works, at R&D cost $ke^2$ . Under outcome-based payment it is paid $p$ per patient only when the drug works, and the demand is $1-(1-\beta)p$ . Its profit, the bracket of the paper's (9), is

\pi_m(e)=e\,p\,[1-(1-\beta)p]-(1-\alpha)ke^2 .

A best response to $(\alpha,\beta)$ is a maximizer of $\pi_m$ over $e>0$ .

At efficacy $e$ the patient welfare (7) and the government spending, the left-hand side of the budget constraint in (10), are

W=\tfrac12\,e\,(1-(1-\beta)p)^2,\qquad M=\alpha k e^2+e\,\beta p\,[1-(1-\beta)p].

A policy is optimal when it has a best response at which $M\le B$ and its welfare there is at least the welfare of every other policy at each of that policy's best responses with $M\le B$ .
$\alpha_{\max}$ is the largest $\alpha\in[0,1)$ for which the policy $(\alpha,0)$ is affordable at the manufacturer's best response.

The Lean development names these objects IsPolicy, profit, BR, welfare, spend, IsOptimal and IsAlphaMax, in the namespace RareDisease.ExogOutcome.

Formalization targets

Goal: Proposition 3, parts 1 and 3

For $k>0$ , $B>0$ , $0<p<1$ and $\alpha_{\max}$ as above:

At every optimal policy the budget constraint binds: $M=B$ at the best response.
If

p\ \ge\ \frac{2}{5-\alpha_{\max}}\quad\text{and}\quad B<\frac{p^2}{2k},

then there is a $\beta_1$ such that $(0,\beta_1)$ is optimal and every optimal policy equals $(0,\beta_1)$ . Only patients are subsidized. 3. If

p\ \le\ \frac{2(1-\alpha_{\max})}{5},

then $(\alpha_{\max},0)$ is optimal, every optimal policy equals it, and

\alpha_{\max}=\frac{8Bk+p^4-2p^3+p^2-(p-p^2)\sqrt{16Bk+p^4-2p^3+p^2}}{8Bk}.

Only the manufacturer is subsidized.

The thresholds are the printed ones. They are not the sharpest possible (see Formalization scope), but they are what the paper states.

Milestones

In attack order: the best response (19), $e^*=p(1-(1-\beta)p)/(2(1-\alpha)k)$ ; the reduced problem (20), giving welfare and spending at the best response; the fact that both expressions of (20) are increasing in $\alpha$ and in $\beta$ ; and the marginal-rate identity from the proof of Proposition 3 (Appendix C, p. 37), whose sign is that of $(5-\alpha)p-2(1-\alpha)$ .

Significance

The result splits the decision between subsidizing patients and subsidizing the manufacturer by a single comparison of the consortium's price with thresholds that depend only on the budget and the cost scale. For a policy maker the consequence is concrete. A high negotiated price already gives the manufacturer enough incentive to develop an efficacious drug, so every unit of budget should lower what patients pay. A low price leaves the manufacturer short of incentive, so every unit should go to R&D. Splitting the budget is never optimal in either regime.

The formalization adds three things. First, it checks a statement whose printed form has errors. Part 2 of the proposition, "subsidize both" for intermediate prices, is false as printed: $B=0.05$ , $k=0.3$ , $p=0.2$ lies in the printed middle range, yet the unique optimum is manufacturer-only. The printed closed form for the patient subsidy in part 1 does not satisfy the binding budget constraint. Second, the proof in the paper is a marginal argument along the binding curve, and its extremal step takes a maximum over $\alpha$ at the wrong end; the parts posed here stay true because their thresholds are stronger than needed, which a machine-checked proof makes explicit. Third, the game is stated as a game: the government's problem is posed over the manufacturer's best-response set, not over the reduced formulas, so the reduction (19)–(20) is itself a theorem. None of these results has a machine-checked proof yet.

Difficulty

The reduced problem (20) is a two-variable optimization with a nonlinear constraint, and its feasible region has no simple shape. The obvious first idea is to solve the first-order conditions of the Lagrangian, but the optimum of parts 1 and 3 is on the boundary of the policy square ( $\alpha=0$ or $\beta=0$ ), so stationarity says nothing there. What has to be shown instead is a global sign property along the whole binding curve: trading manufacturer subsidy for patient subsidy changes welfare per unit of spending with the sign of $(5-\alpha)p-2(1-\alpha)$ , and this sign must be controlled for every $\alpha$ the curve passes through. That requires knowing that the curve stays in $\alpha\le\alpha_{\max}$ , which comes from the monotonicity of spending. Two existence and uniqueness questions also arise. In part 1 a patient-only policy must exhaust the budget with $\beta<1$ , which is where $B<p^2/(2k)$ enters. In both parts no other policy may tie the optimum.

Formalization scope

All quantities are real numbers. The standing assumptions $k>0$ , $B>0$ and $0<p<1$ are hypotheses of every theorem. The paper uses them without stating them: with $p\ge1$ and $\beta=0$ the demand $1-p$ is not positive and the manufacturer has no best response with $e>0$ ; the closed form of $\alpha_{\max}$ divides by $8Bk$ . As in the paper, the efficacy $e$ ranges over all positive reals and is not bounded by $1$ . Policies satisfy $\alpha,\beta\in[0,1)$ , a half-open interval.

The added hypothesis $B<p^2/(2k)$ in part 1 is necessary. With $\alpha=0$ the spending tends to $p^2/(2k)$ as $\beta\uparrow1$ , so for larger budgets no patient-only policy exhausts the budget. The thresholds $2/(5-\alpha_{\max})$ and $2(1-\alpha_{\max})/5$ are posed as printed; replacing them by the sharper values $2/5$ and $2(1-\alpha_{\max})/(5-\alpha_{\max})$ would be a different theorem. Part 2 and the printed closed form of part 1 are not posed, because both are false as printed.

The formalization cannot be trivialized by defining the government's problem through the reduced forms (20), because welfare and spending in IsOptimal are evaluated at members of the best-response set BR. "Optimal" means attained and compared against every policy at every best response, not a supremum. $\alpha_{\max}$ is defined as the greatest affordable manufacturer-only subsidy, not by its closed form, which is part of the goal.

A complete development needs only real analysis from Mathlib: maximization of a concave quadratic, monotonicity of rational functions, one-variable derivatives for the marginal-rate milestone, and Real.sqrt for the closed form. Proofs of any milestone are welcome.

Selected references

W. Olsder, T. Martagan, C. S. Tang, Improving Access to Rare Disease Treatments: Optimal Subsidies, Pricing, and Payment, SSRN working paper 3481150, version of 2019-11-13. https://ssrn.com/abstract=3481150
W. Olsder, T. Martagan, C. S. Tang, Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4634

7 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

A Theory of Liquidity in Private Equity I: Without a Secondary Market, Two Capital-Share Thresholds Characterize Equilibrium, and Liquid LPs Earn Strictly More When Both Fund Types ExistResearch Paper

Why liquidity can explain persistent private equity returns

Private equity funds are organized as limited partnerships. Limited partners (LPs: pension funds, endowments, insurers) commit capital, and a general partner (GP) manages the fund and calls the committed capital over several years. A well-documented empirical regularity is that some LPs earn persistently higher returns than others, and that fund returns persist across a GP's successive funds (Kaplan and Schoar, 2005; Lerner, Schoar and Wongsunwai, 2007). The usual explanation is differences in skill.

Maurin, Robinson and Strömberg propose a different channel. Because capital is called gradually, an LP hit by a liquidity shock may default on the remaining commitment. GPs who raise money from LPs that tolerate illiquidity can invest efficiently. GPs who raise money from LPs that do not must call capital early to protect themselves against default, which distorts investment. When illiquidity-tolerant capital is scarce, GPs compete for it and pay its owners a premium. This mission formalizes the paper's main equilibrium result without a secondary market: that premium exists exactly when both kinds of funds are raised.

Setting

An investment pays $R$ per unit on success and $0$ on failure. It succeeds with probability $p$ if the GP exerts effort and with probability $q<p$ if the GP shirks, in which case the GP enjoys a private benefit $B$ per unit invested. Each GP has wealth $A$ and runs one fund of total size $I>A$ . A share $x\in[0,1]$ of the fund is invested in period 0 and the rest, $1-x$ , in period 1; both investments succeed or fail independently.

A fee schedule $f$ pays the GP a fee per unit of investment that depends on which investments succeeded. It must satisfy limited liability, $0\le f\le$ the fund's cash flow, and incentive compatibility: effort on both investments must be at least as profitable for the GP as shirking on either or both. Write $\bar f$ for the expected fee under effort. LPs who receive the promised expected return $\bar R$ per unit contributed supply $I-A$ , which ties the fund size to the fee through

(pR-\bar f)\,I=\bar R\,(I-A).\qquad(3)

LPs consume in periods 1 and 2. With probability $\lambda\in(0,1)$ an aggregate liquidity shock hits in period 1. After the shock an LP discounts period-2 consumption by $\delta\in(0,1)$ . There are two types, $L$ and $H$ , with $\delta_L<\delta_H$ , holding the shares $1-\mu_H$ and $\mu_H$ of the LPs' total capital $K$ . Without a secondary market an LP honours the second capital call only if the claim is worth at least its cost:

1-x\le\delta\,\bar R.\qquad(4)

A GP chooses $(x,I,f)$ to maximize the profit $\Pi_{GP}=\bar f I$ subject to (3) and (4). LPs invest in private equity when its value $(1-\lambda)\bar R+\lambda\delta\bar R$ exceeds the value $1$ of cash. An equilibrium (Definition 2) consists of the fractions $\alpha_L,\alpha_H$ of GPs raising each fund type, the returns $\bar R^*_{PE,L},\bar R^*_{PE,H}$ , and optimal contracts such that GPs raise only profit-maximizing fund types and each primary market clears.

The key quantities are the LPs' break-even return $1+r(\lambda,\delta)=1/(1-\lambda(1-\delta))$ , the minimal safe early call $\hat x(\lambda,\delta)=1-\delta/(1-\lambda(1-\delta))$ , and the tolerance threshold $\hat\delta(\lambda)=1-p/(p+(1-\lambda)q)$ . The Lean development uses the namespace PELiquidity.Primary, with grossReturn, xHat, deltaHat, xLow, xBar, IsFeasibleContract, IsOptimalContract, IsCapitalSupply and IsEquilibrium.

Formalization targets

Goal: Proposition 2

There are thresholds

0<\underline\mu_H<\bar\mu_H<1

such that for every $\mu_H\in(0,1)$ an equilibrium exists, and every equilibrium satisfies the following:

if $\mu_H<\underline\mu_H$ , both fund types are raised and $\bar R^*_{PE,H}>\bar R^*_{PE,L}=1+r(\lambda,\delta_L)$ ;
if $\mu_H\ge\underline\mu_H$ , then $\alpha^*_L=0$ ;
$\bar R^*_{PE,H}$ is strictly decreasing in $\mu_H$ on $[\underline\mu_H,\bar\mu_H]$ ;
if $\mu_H\ge\bar\mu_H$ , then $\bar R^*_{PE,H}=1+r(\lambda,\delta_H)$ .

The thresholds are existential, as in the paper. A variant pinning $\bar\mu_H$ by (C.3) is a welcome strengthening.

Milestones

(11): the break-even return $1+r(\lambda,\delta)$ , decreasing in $\delta$ .
Lemma 1 with (12): $\Pi_{GP}=pRI-\bar R(I-A)$ , so an optimal contract minimizes $\bar f$ .
Lemma 2: the minimal incentive-compatible fee is (15), minimized exactly on $x\in[q/(p+q),p/(p+q)]$ .
Proposition 1: under (4) the optimal early call is $[\max\{\underline x,\hat x\},\bar x]$ if $\delta\ge\hat\delta(\lambda)$ , and $\hat x(\lambda,\delta)$ with a strictly higher fee if $\delta<\hat\delta(\lambda)$ .
(C.4): when only H-funds are raised above the H-LPs' break-even rate, $\mu_HK=I_H-A=(pR-\bar f_H)A/(\bar R_H-(pR-\bar f_H))$ ; for fixed fee, the contribution decreases with $\bar R_H$ .
(18): the indifference rate $\bar R^{max}_{PE,H}\in(1+r(\lambda,\delta_L),pR)$ .
Lemma C.1: $\alpha^*_L>0$ implies $\bar R^*_{PE,L}=1+r(\lambda,\delta_L)$ .

Significance

The result shows that heterogeneous liquidity needs alone, without any difference in skill, produce a cross-section of LP returns: when capital from liquidity-tolerant LPs is scarce, those LPs earn strictly more than other LPs investing in otherwise identical funds. When it is abundant, they earn only their fair liquidity premium. This separates a liquidity explanation of return persistence from a skill explanation, and it is the benchmark against which the paper's second main result, the effect of a secondary market (Proposition 3, a separate mission), is measured.

The paper proves the result by hand. No part of it has a machine-checked proof. A formalization would check the three-case equilibrium argument, including uniqueness, which the paper treats briefly. It would also fix the readings of Definition 2 that the printed statement leaves open (see below) and record the hypotheses the proofs use without stating. The fee-design lemma (Lemma 2) is a small linear program of independent interest for moral-hazard models with several projects.

Difficulty

The equilibrium statements quantify over every equilibrium, and an equilibrium includes an optimal contract for each fund type, optimal against all fee schedules, call shares and fund sizes. The obvious approach, substituting the closed-form fee (15) and the optimal call (17) into the profit function, does not suffice. Uniqueness requires showing that no other combination of returns, fund fractions and contracts clears both markets. That includes returns at which a fund type is not raised. It also includes returns above the break-even rate, where the no-default constraint loosens and the fee falls. Ruling these out needs the GP's optimal profit to be decreasing in the promised return even when the no-default constraint binds. The boundary at $\underline\mu_H$ , where the $H$ -market just clears with every GP raising an $H$ -fund, has to be placed correctly.

Formalization scope

Parameters. The parameter structure records $0<q<p\le 1$ $0 < q < p \leq 1$ , $B,A,K>0$ $B, A, K > 0$ , $\lambda,\delta_L,\delta_H\in(0,1)$ $λ, δ_{L}, δ_{H} \in (0, 1)$ , and Assumptions 1, 2, 3 and 6 as printed. Two hypotheses are added and disclosed:
- Assumption 5 is required strictly for $\delta_L$ , $1+r(\lambda,\delta_L)<pR$ . With equality the GP's profit does not depend on the fee, and the strict ranking of returns fails.
- $B\le p(p-q)R$ makes limited liability compatible with incentive compatibility at every call share. The paper's Claim A.1 assumes the stronger $R\ge B/(p-q)^2$ .
Fee schedules are indexed by the four success outcomes rather than the four cash-flow values. These differ only at $x=1/2$ , and the minimal fee is the same.
Equation (3) is stated multiplied out with $I>A$ , never as a quotient. A return at which the GP's profit is unbounded therefore admits no optimal contract and cannot be an equilibrium price. Contract optimality is global over $(x,I,f)$ .
Definition 2 is read with $\alpha_L+\alpha_H=1$ , which the proof uses. GP fund choice is read as "a raised fund type is profit-maximizing", the only-if direction of the printed biconditional. The literal biconditional admits no equilibrium at $\mu_H=\underline\mu_H$ .
Two printed boundaries are corrected. Proposition 2 i) is stated for $\mu_H<\underline\mu_H$ , which resolves the overlap of its two cases as the proof does. "Decreasing" is read as strict.
Out of scope. Assumption 4 and capital-call relief (Appendix C.1) are not formalized, since the no-default constraint (4) is imposed directly. The GP takes $\bar R$ as given, so raising the promised return (C.2) is not modelled. Appendix A's alternative contracts and the "no fund" option are also out of scope.
Trivializations ruled out. The goal asserts existence of an equilibrium for every $\mu_H\in(0,1)$ , so its "every equilibrium" clauses are not vacuous. The strict chain $0<\underline\mu_H<\bar\mu_H<1$ excludes degenerate thresholds.

Everything is built from Mathlib's real numbers and finite sums. The fee-schedule linear program (Lemma 2), the contract problem (Proposition 1) and the equilibrium predicate are reusable for the secondary-market mission of the same paper. Proofs of any milestone, and the pinned-threshold variant of the goal, are welcome.

Selected references

V. Maurin, D. T. Robinson and P. Strömberg, A Theory of Liquidity in Private Equity, working paper, draft of December 2020; published in Management Science 69(10), 2023. https://doi.org/10.1287/mnsc.2022.4612
S. N. Kaplan and A. Schoar, Private Equity Performance: Returns, Persistence, and Capital Flows, Journal of Finance 60(4), 1791–1823, 2005. https://doi.org/10.1111/j.1540-6261.2005.00775.x
J. Lerner, A. Schoar and W. Wongsunwai, Smart Institutions, Foolish Choices: The Limited Partner Performance Puzzle, Journal of Finance 62(2), 731–764, 2007. https://doi.org/10.1111/j.1540-6261.2007.01220.x

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Precommitments in Two-Sided Market Competition 2: Commission Precommitment Beats No Commitment When γ ≥ β or γ ≪ β, and Loses to It When γ Is Just Below βResearch Paper

Motivation

Many service platforms set a price paid by customers and a wage paid to the providers who serve them. A platform may instead announce how much of each transaction's price it will pass to providers, then choose prices after both platforms have announced their shares. These are different games: a price change in the second game changes both customer demand and provider pay. Hu and Liu's study of precommitments in two-sided competition asks which timing gives platforms a more favorable equilibrium. This mission isolates their comparison between a commission precommitment and no commitment, Proposition 3(b) of the submitted manuscript. The authors' Online Appendix, included in that manuscript, contains the proofs.

The comparison is useful where a platform must choose a contract with providers before it can adjust customer prices. It is not enough to know that either side of the market is competitive: the answer changes as demand-side and supply-side competition intensities move relative to each other. The mission makes the claimed parameter regions precise and ties them to equilibria of the two games.

Setting

There are two platforms, indexed by $i=1,2$ , with rival $j\ne i$ . Platform $i$ posts a consumer price $p_i$ and a provider wage $w_i$ . Fix a potential market size $\Omega>0$ . The demand substitution factor $\gamma\in[0,1)$ measures how a rival's price raises demand for platform $i$ . The supply substitution factor $\beta\in[0,1)$ measures how a rival's wage draws providers away. The paper uses the positive part $[x]^+=\max\{x,0\}$ :

d_i(p)=[\Omega-p_i+\gamma p_j]^+,\qquad s_i(w)=[w_i-\beta w_j]^+.

The number of completed matches is $z_i=\min\{d_i(p),s_i(w)\}$ . Profit is $\pi_i=(p_i-w_i)z_i$ . Unmatched consumers or providers generate no revenue. Keeping the positive parts matters when a platform chooses a price or wage that leaves one side of the market empty.

In mode P, both platforms choose their prices and wages simultaneously, and each can change its own price and wage together while its rival's choices stay fixed. In mode C, each platform first commits to a pay-out ratio $\alpha_i\in(0,1)$ . The provider then receives $w_i=\alpha_i p_i$ per match and the platform keeps $1-\alpha_i$ of its price. After observing both ratios, the platforms choose prices. Their profit in this second stage is

\pi_i(\alpha,p)=(1-\alpha_i)p_i\min\{d_i(p),s_i(\alpha p)\}.

A subgame-perfect equilibrium in mode C specifies a price equilibrium after every admissible pair of ratios and an initial pair of ratios that resists unilateral deviation when prices are chosen again. The mission compares symmetric commission equilibria to the positive-profit equilibrium of mode P. In the paper's platform preference ranking, $X\succeq Y$ means that mode $X$ gives each platform a weakly higher price and profit, and a weakly lower wage and matching quantity, than mode $Y$ .

Formalization targets

No commitment and commission outcomes

Lemma 1 gives the simultaneous price-and-wage outcome. Writing $D=4-3\beta-3\gamma+2\beta\gamma$ , its price, wage, matching quantity, and profit are

p_P^*=\frac{3-2\beta}{D}\Omega,\quad w_P^*=\frac{\Omega}{D},\quad z_P^*=\frac{1-\beta}{D}\Omega,\quad \pi_P^*=\frac{2(1-\beta)^2}{D^2}\Omega^2.

Lemma F.2 says that second-stage commission prices equate demand and supply. Lemma 4 characterizes the symmetric commission equilibrium by the radical $\alpha^*$ in equation (7), its price $p_C^*=\Omega/[1-\gamma+(1-\beta)\alpha^*]$ , and its profit in equation (9). These are the three milestones. The radical is transcribed exactly in the Lean definition associated with equation (7).

Proposition 3(b)

The goal compares the two equilibrium outcomes using all four components of the platform preference ranking:

\gamma\geq\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\ll\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\leq\beta\text{ and sufficiently close to }\beta\ \Longrightarrow\ P\succeq C.

The two informal proximity phrases are expressed by the existence of positive thresholds, with the threshold allowed to depend on $\beta$ . At $\gamma=\beta$ , both rankings can hold because the outcomes coincide. The goal also asserts that the equilibria being compared exist for every admissible parameter pair.

Significance

The result identifies when committing to a provider share yields a platform outcome that is preferable to choosing price and wage together. Its four-way comparison is stronger than a profit-only ranking: the associated prices, wages, and match counts all move in specified directions. It makes clear that the relative competition intensities on the two sides determine whether the timing of the provider contract helps or hurts platforms. Without the comparison, the closed-form equilibrium results for modes P and C would not say which contract timing platforms prefer.

The result is proved in the cited manuscript, with derivations in Online Appendix §F; it is not an open mathematical conjecture. The remaining work in this mission is a machine-checked Lean proof of the equilibrium statements and the parameter-region comparison. The development will also provide a reusable formal model of simultaneous and two-stage decisions in a two-sided market. No existing machine-checked proof of this particular comparison is identified in the local Prove2Me index.

Difficulty

A change in a commission ratio changes the wage at any given price, while the subsequent price decision changes both demand and the wage again. That coupling makes the comparison more delicate than ordering two prices by inspection. The commission equilibrium ratio contains a square root, and the ranking must establish the directions of four outcome quantities in several parameter regions. The apparent shortcut of comparing profits alone would leave three of Definition 1's required inequalities unresolved. The positive-part demand and supply functions also admit zero-match equilibria that complicate an unqualified uniqueness statement.

Formalization scope

The Lean development uses real-valued prices and wages, two platforms indexed by Fin 2, and all unilateral deviations in the stated strategy sets. Market size is positive, both substitution factors lie in $[0,1)$ , and pay-out ratios lie in $(0,1)$ . The paper does not spell out the strategy sets; these choices preserve the derivations in §3 and Appendix §F. The no-commitment uniqueness statement is restricted to equilibria where both platforms profit, because the literal unrestricted claim has zero-profit counterexamples. A second-stage strategy in mode C selects an equilibrium with positive profits for both platforms whenever one exists. This condition prevents off-path zero-profit punishments from making the printed symmetric SPE claim false.

The goal quantifies over equilibria derived from the demand, supply, match, and profit functions. It does not define an outcome to equal the paper's closed form, and it asserts equilibrium existence so that its universal comparisons have content. The radical for $\alpha^*$ is a named expression; Lemma 4, rather than its definition, establishes its equilibrium role. A full proof needs reasoning about unilateral deviations, positive-part functions, equilibrium existence and uniqueness, the radical expression, and real inequalities. The general Nash condition and the paper's market primitives are intended for reuse in other two-player platform games. Contributions addressing these foundations and any of the three cited milestones are within scope. Wage- and price-precommitment modes are outside this mission.

Selected references

Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript with Online Appendix associated with the 2023 publication, SSRN 3734828. Manuscript.
Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, Manufacturing & Service Operations Management 25(2), 704–718, 2023. DOI.

7 thms3 active usersReviewed

Completed

Markov Chain Operations Research Reinforcement Learning·Captain: mikedeng1

Nonstationary Reinforcement Learning: The Blessing of (More) Optimism III: Under Uniform One-Step Reachability ζ, the Un-widened Confidence Region Contains an MDP of Diameter at Most 1/ζResearch Paper

Motivation

Reinforcement learning in a changing environment has a difficulty that is absent from a fixed Markov decision process: transition data gathered earlier may describe a different system from the one the decision maker currently faces. A learning algorithm therefore estimates transitions from a recent window of observations. The estimate comes with a confidence region, a set of transition laws consistent with the data at a chosen statistical radius. In the general nonstationary setting studied by Cheung, Simchi-Levi and Zhu, their algorithm widens this region to ensure that it can contain a model whose states remain readily reachable. Such a model is needed for the paper's dynamic regret analysis. Section 7 isolates a structural condition under which widening is unnecessary: every destination is reachable from every state with a uniformly positive one-step probability under a suitable action. Cheung, Simchi-Levi and Zhu, §7.

This mission formalizes Proposition 4 of that paper, the precise claim that the original, unwidened transition region contains a model with a controlled diameter. It is one of three separate missions for the paper. The result supports the paper's no-widening variant of its learning algorithm; it is not a claim that every model in the confidence region has small diameter. Cheung, Simchi-Levi and Zhu, Proposition 4.

Setting

There are finitely many states $\mathcal S$ and, for each state $s$ , a nonempty finite set $\mathcal A_s$ of permitted actions. At each time $t\in[T]$ , the system has a reward $r_t(s,a)\in[0,1]$ and a probability distribution $p_t(\cdot\mid s,a)$ for the next state. The distribution may change with $t$ . A trajectory records the observed state $s_q$ , chosen action $a_q$ , and successor state $s_{q+1}$ at each time $q$ . These are the model primitives in §2.2. Cheung, Simchi-Levi and Zhu, pp. 6–7.

An episode begins at $\tau(m)$ and uses a window of length $W$ . At time $t$ in that episode, $N_t(s,a)$ counts how often the pair $(s,a)$ appears between $(\tau(m)-W)\vee1$ and $t-1$ ; $N_t^+(s,a)=\max\{1,N_t(s,a)\}$ . The empirical row $\hat p_t(\cdot\mid s,a)$ counts observed successors and divides by $N_t^+(s,a)$ . The corresponding average true row $\bar p_t$ averages the time-varying transition probabilities over the same visits. Both are zero vectors when there are no visits. Cheung, Simchi-Levi and Zhu, equations (3) and (5).

Write $SA=\sum_s|\mathcal A_s|$ , so this is the number of allowed state-action pairs. At confidence level $\delta$ , the transition radius is $\operatorname{rad}_{p,t}(s,a)=2\sqrt{2S\log(SAT/\delta)/N_t^+(s,a)}$ . The region $H_{p,t}(s,a;\eta)$ consists of probability vectors within $\ell_1$ distance $\operatorname{rad}_{p,t}(s,a)+\eta$ of $\hat p_t$ . Here $\eta=0$ means no widening. The estimation event $E_p$ bounds the $\ell_1$ distance between $\bar p_t$ and $\hat p_t$ by that radius for each allowed pair. Cheung, Simchi-Levi and Zhu, pp. 12, 14.

For a stationary transition model and policy $\pi$ , the hitting time $\Lambda(s'\mid\pi,s)$ counts transitions until the first arrival at $s'$ after starting at $s$ . This includes the first return time when $s=s'$ . Its diameter is $D=\max_{s,s'}\min_\pi\mathbb E[\Lambda(s'\mid\pi,s)]$ . Infinite expectations are possible in the definition. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization targets

Goal: Proposition 4

Assumption 2 supplies $\zeta>0$ and an allowed action $a_{(s,s')}$ for every ordered pair of states, fixed across time, such that $p_t(s'\mid s,a_{(s,s')})\ge\zeta$ for all $t\in[T]$ . Conditional on $E_p$ , Proposition 4 says that for every time in the horizon there exists a transition model $p$ whose every allowed row belongs to $H_{p,t}(s,a;0)$ and whose diameter obeys

D(\mathcal S,\mathcal A,p)\le\bar D:=\frac1\zeta.

The target is existential: the region need only contain one such model at each time. The milestone list follows the two cases in the proof of Lemma 13, the lemma's model existence claim, and the expected hitting-time bound in the proof of Proposition 4. Cheung, Simchi-Levi and Zhu, pp. 21, 49–50.

Significance

Proposition 4 identifies a condition under which the algorithm can use $\eta=0$ while retaining a uniform diameter guarantee for at least one plausible transition model. The paper uses this to analyze a no-widening version of its dynamic regret bound, and later applies that viewpoint to inventory control. Without a bounded-diameter model in the region, the diameter-dependent regret argument does not apply in the same form. Cheung, Simchi-Levi and Zhu, §7.

The proposition and its appendix proof are known results of the paper. This mission asks for a machine-checked account of the exact confidence region, its pathwise estimation event, Lemma 13, and the diameter claim. A general finite MDP with probability-valued transition rows is already available as the published FiniteMDPLearning definition; the paper-specific window estimators and its return-time diameter still need formal proofs. The paper's headline Theorems 1–4 are not posed here because their displayed bounds hide constants in $\widetilde O(\cdot)$ notation. Cheung, Simchi-Levi and Zhu, p. 6 and Theorems 1–4.

Difficulty

The obvious idea that the true transition law belongs to the confidence region can fail under drift: the region is centered on recent observations, while the law at the current time may differ from the laws that generated those observations. Even the average true row has a special case. At an unvisited pair, equation (5) sets it to the zero vector, which is not a probability distribution and therefore is not a member of the simplex-valued confidence region. The existence claim must cover visited and unvisited pairs while preserving one-step reachability for all targets under a single transition law. Cheung, Simchi-Levi and Zhu, pp. 12, 49–50.

The diameter also uses the paper's first-arrival-after-start convention. A library travel time that is zero when source equals target misses the return-time cases and would weaken the stated conclusion. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization scope

States and actions are Fin S and Fin A; permitted actions are state-dependent finite sets. Extra MDP rows for disallowed actions are never consulted. The finite MDP type supplies valid probability rows and bounded rewards. Hitting times and the diameter use extended nonnegative reals, so infinite values are represented without a default real value. The diameter ranges over allowed deterministic stationary policies and over all ordered state pairs, including equal pairs. Time is zero-based in Lean: paper time $t\in[T]$ is index $t-1<T$ , and the paper's window becomes the half-open interval [τm-W,t). The paper's $N^+$ is at least one, so its estimators never divide by zero. A result at arbitrary $t$ with $\tau_m\le t<T$ covers every episode time without assuming any additional episode schedule property.

The Lean statement makes two domain conditions explicit: $S>1$ and $0<\delta<1$ . These ensure the paper's claim that the radius at an unvisited pair is at least one; it can fail when $S=1$ and the confidence level is close to one. Assumption 2 is required for every time in the horizon, with $\zeta>0$ . The event $E_p$ is the $\ell_1$ estimation inequality at the selected time. The paper writes it as membership of $\bar p_t$ in a simplex-valued region for every pair, but that literal wording is false at an unvisited pair because $\bar p_t=0$ there. At visited pairs, the inequality and membership agree. This convention is disclosed in the definition item and keeps the theorem meaningful on ordinary early trajectories.

The region is centered at the exact empirical $\hat p_t$ , uses $\eta=0$ , and constrains every allowed row of the constructed model. The diameter uses its full extended-real value, and $\zeta$ is strictly positive; dropping any of these clauses would change the claim. Reusable contributions include finite-state hitting-time estimates and windowed transition estimation identities. Proofs of the four milestones and the goal, as well as small lemmas connecting the published MDP measure to successive transition rows, are welcome.

Selected references

W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. arXiv
T. Jaksch, R. Ortner and P. Auer, Near-optimal Regret Bounds for Reinforcement Learning, Journal of Machine Learning Research 11, 2010. JMLR

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance III: Partial-Collaboration Equilibria: KKT Utilities and Free-Riding EffortsResearch Paper

Motivation

After a sudden-onset disaster, humanitarian organizations (HOs) raise most of their response budget from private donors within days. Donors increasingly earmark their gifts, restricting them to a region, a program or a type of expense. Earmarking makes an appeal more attractive to a donor but lowers the share of each dollar that the HO can deploy immediately. Aflaki and Pedraza-Martinez (SSRN 3705595, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202) model how HOs set earmarking and fundraising effort under three institutional arrangements: competition, full collaboration (a coalition that fundraises and decides as one), and partial collaboration, in which HOs pool the cost of reaching donors on a common platform while each donor still chooses which HO to give to. Joint appeals such as the UK's Disasters Emergency Committee are of the last kind.

This mission formalizes the paper's equilibrium result for partial collaboration (Proposition 4): equilibria exist, equilibrium earmarking is determined by first-order conditions that do not involve the efforts, and only the HOs with the largest required funding relative to their unit performance pay for the platform, while the others free-ride.

Setting

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$ . HO $i$ chooses a base utility $s_i \in [a_i, b_i]$ , the attractiveness to donors that its earmarking level induces, and an effort $x_i \in [0, 1]$ , the fraction of donors it pays to contact, at cost $C_i(x_i)$ . Its unit performance $\delta_i(s_i) \in (0, 1]$ is the fraction of each donated dollar usable now, and $B_i > 0$ is its required funding. The mean donation is normalized to $1$ .

Pooled effort reaches $\bar x = \min\left(\sum_{i \in I} x_i, 1\right)$ donors. A contacted donor gives to HO $i$ with the multinomial-logit probability

\theta^p_i(s) = \frac{e^{s_i}}{1 + \sum_{j \in I} e^{s_j}},

the $1$ being the option of not donating, so HO $i$ expects donations $\bar x\,\theta^p_i(s)$ and achieves total performance $\delta_i(s_i)\,\bar x\,\theta^p_i(s)$ , of which only $\min(\cdot, B_i)$ is useful. HO $i$ is lexicographic (problem (10)): given the other HOs' strategies, it first minimizes its funding gap $\left(B_i - \delta_i(s_i)\bar x\theta^p_i(s)\right)^+$ over $[a_i, b_i] \times [0,1]$ ; among the gap minimizers it maximizes its utility $\min\left(\delta_i(s_i)\bar x\theta^p_i(s), B_i\right) - C_i(x_i)$ ; and an HO that is still indifferent picks a strategy maximizing its unconstrained total performance $\delta_i(s_i)\bar x\theta^p_i(s)$ . A Nash equilibrium is a profile $(s, x)$ in the product of the boxes at which every HO's strategy is such a best response. Finally,

\alpha^p_i(s) = \min\left(\frac{B_i}{\delta_i(s_i)\,\theta^p_i(s)}, 1\right)

is the reach HO $i$ needs to close its own gap.

Formalization targets

Goal: Proposition 4

A pure Nash equilibrium exists. For every profile $(s, x)$ in the box, labelled so that $\alpha^p_1(s) \ge \dots \ge \alpha^p_n(s)$ , with $\bar k = \#\{i : \alpha^p_i(s) = \alpha^p_1(s)\}$ : $(s, x)$ is an equilibrium if and only if (i) for every $i$ there are $\lambda^p_{i1}, \lambda^p_{i2} \ge 0$ with

\frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\partial \theta^p_i(s)/\partial s_i}{\theta^p_i(s)} + \lambda^p_{i1} - \lambda^p_{i2} = 0, \quad \lambda^p_{i1}(a_i - s_i) = 0, \quad \lambda^p_{i2}(s_i - b_i) = 0, \tag{11}

and (ii) $\sum_{i=1}^{\bar k} x_i = \alpha^p_1(s)$ and $x_{\bar k+1} = \dots = x_n = 0$ .

Milestones

(S11): $(s, x)$ is an equilibrium iff each $s_i$ maximizes $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ on $[a_i, b_i]$ and $x_i = \left(\alpha^p_i(s) - \sum_{j \ne i} x_j\right)^+$ .
Log-concavity: $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ is log-concave on $[a_i, b_i]$ .
Total effort: every solution of $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ with $\alpha$ sorted decreasingly has $\sum_i x_i \ge \alpha_1$ .
Effort system: for $1 \ge \alpha_1 \ge \dots \ge \alpha_n \ge 0$ and $x \in [0,1]^n$ , that system holds iff $\sum_{i \le \bar k} x_i = \alpha_1$ and $x_i = 0$ for $i > \bar k$ .

Significance

The proposition separates the two decisions. Equilibrium earmarking solves each HO's own first-order condition (11) and does not depend on anyone's effort, because the pooled reach multiplies every HO's donations by the same factor. Equilibrium effort is a pure coordination outcome: the platform is funded exactly up to the largest required reach $\alpha^p_1$ , and only the HOs attaining it contribute. The paper uses these facts to compare earmarking and performance across the three arrangements (its Propositions 5 and 7), and the free-riding structure is what drives the comparison of partial collaboration with competition.

The result is proved in the paper's Online Supplement (pp. S13–S14). No machine-checked version exists. The mission asks for a Lean proof of the proposition as stated, with the equilibrium defined from the HOs' lexicographic problem rather than from its characterization; the effort-system milestones are self-contained statements about a piecewise-linear fixed-point system and are reusable for other pooled-contribution games.

Difficulty

The obvious argument, "each HO maximizes $\delta_i\theta^p_i$ , and the rest is bookkeeping", skips the case analysis behind (S11). Whether HO $i$ 's gap can be closed depends on the others' efforts. When the others' pooled effort already covers HO $i$ 's requirement, HO $i$ 's gap and utility no longer depend on its base utility. Only the third, tie-breaking level of the best response then pins $s_i$ down, and without it (11) is false. The existence part needs a fixed point of the base-utility best-response map on $\prod_i [a_i, b_i]$ ; when HO $i$ 's best response is not unique, that map is not even a function. In part (ii), the effort system $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ is not a contraction, and the paper's proof by successive elimination of indices is informal.

Formalization scope

HOs are Fin n with 0-based indices, so $\alpha^p_1$ is the value at index 0, and [NeZero n] is assumed. Strategies are in base-utility coordinates: $\delta_i : \mathbb R \to \mathbb R$ is a primitive function of $s_i$ , as in the paper's problem (10). The earmarking coordinates are not modelled. All definitions live in one Setting structure with a Standing predicate, which every theorem assumes:

$a_i \le b_i$ and $B_i > 0$ ;
$C_i$ is nonnegative and strictly increasing on $[0,1]$ ;
on an open interval containing $[a_i, b_i]$ , $\delta_i$ is positive, differentiable and concave;
$\delta_i \le 1$ on $[a_i, b_i]$ .

$B_i > 0$ is implicit in the paper; with all $B_i = 0$ every base utility is an equilibrium strategy. Concavity of $\delta_i$ is used by the paper's proof. The HO problem (10) is printed with decision $(s_i, \bar x)$ and cost $C^p(\bar x)$ . It is encoded with HO $i$ 's own effort $x_i$ and own cost $C_i(x_i)$ , the reading used by the paper's proof and by part (ii). The paper's "without loss of generality" ordering is the hypothesis that $\alpha^p(s)$ is antitone in the index, and $\bar k$ is the number of entries tied with the first; this gives $\bar k = n$ when all tie. Partial derivatives are Mathlib deriv of $t \mapsto \theta^p_i(s \text{ with } s_i := t)$ . Every function differentiated is differentiable at the point by Standing. The pure-algebra milestones 3–4 use no game objects.

The equilibrium must not be defined by (S11) or (11); that would make the goal a tautology. The Setting defines it as the three-level lexicographic best response over the full strategy box, and (S11) is a milestone to be proved. A sorry-free check that the standing hypotheses hold for the paper's numerical primitives ( $\delta_i(s) = 1 - s/4$ , $C_i(x) = x/10$ , $[a_i, b_i] = [0,1]$ , $B = (0.2, 0.3)$ ) accompanies the draft.

A full development needs: KKT conditions for a differentiable concave function on a compact interval (including the degenerate interval $a_i = b_i$ ); log-concavity of the logistic share; a continuous-maximum (Berge-type) argument and Brouwer's fixed-point theorem on a product of intervals; and the algebra of the effort system. Contributions of the interval-KKT lemma and of the effort-system lemmas are welcome as separate theorems.

The source is the authors' SSRN version (abstract 3705595, dated December 2022); all proofs are in its Online Supplement, Section S3.

Selected references

A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202

6 thms3 active usersReviewed

Completed

Analysis Economics Operations Research+1·Captain: mikedeng1

The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization III: Whether Utility Rises with Session Length Is Decided by Span Versus MoreishnessResearch Paper

Motivation

Platforms that rank content by engagement (time spent, items consumed) implicitly assume revealed preference: a user who stays longer is a user who is better off. Kleinberg, Mullainathan and Raghavan (arXiv:2202.11776, Management Science 2023, doi:10.1287/mnsc.2022.03683) model a user with inconsistent preferences, a forward-looking system 2 and an impulsive system 1, and show that engagement and utility can come apart. Because utility cannot be read off behavioural data, platforms also run post-session surveys. Section 5.1 of the paper asks what such surveys can reveal: if a survey gives an estimate of the utility $S$ of a session, does $\mathbb E[S\mid T=t]$ rise or fall with the session length $t$ , and what does that say about the content? Theorem 5.1 answers this in terms of two content parameters, the span $q$ and the moreishness $p$ .

Setting

A session proceeds in two phases (§2.1, pp. 5–7).

Span. After each item, system 2 remains interested with probability $q$ . The number of items it enjoys, $T_q$ , has the geometric law on $\{1,2,\dots\}$ : $\Pr[T_q=\tau]=q^{\tau-1}(1-q)$ .
Moreishness. Once system 2 is done, system 1 keeps the user on: with probability $p$ at each step, the first one included, it consumes one more item. With $T_p:=T-T_q+1$ , $\Pr[T_p=k]=p^{k-1}(1-p)$ for $k\ge1$ .
$T_q$ and $T_p$ are independent, and the session length is $T=T_q+T_p-1\in\{1,2,\dots\}$ . For $1\le\tau\le t$ ,

\Pr[T_q=\tau\cap T_p=t-\tau+1]=q^{\tau-1}(1-q)\,p^{t-\tau}(1-p).

Utility. Each item system 2 enjoys has value of mean $\bar v$ ; every step costs the outside option $W$ . The paper's equations (8)–(9) give

\mathbb E[S\mid T=t]=\bar v\,\mathbb E[T_q\mid T=t]-Wt,\qquad \mathbb E[T_q\mid T=t]=\frac{\sum_{\tau=1}^{t}\tau\Pr[T_q=\tau\cap T_p=t-\tau+1]}{\sum_{\tau'=1}^{t}\Pr[T_q=\tau'\cap T_p=t-\tau'+1]}.

The Lean development names these objects geomLaw (the law $g_r(k)=r^{k-1}(1-r)$ , $k\ge1$ ), jointMass, condMeanTq (9) and condUtility (8), all in the namespace EngagementOpt.Survey. Write $f(t)=\mathbb E[S\mid T=t]$ and

\varphi(x)=\frac{x+1}{x}\left(1-\frac{\ln(x+1)}{x}\right)

(phi), the function of the paper's (11) and Lemma D.1.

Formalization targets

Goal: Theorem 5.1 (p. 19)

Assume $0<p<1$ , $0<q<1$ , $\bar v\ge0$ and $W>0$ . For integer session lengths $t\ge1$ :

$q=p$ : $\;\bigl(\forall t\ge1,\ f(t)<f(t+1)\bigr)\iff \bar v>2W$ .
$q>p$ : (a) if $\bar v>2W$ then $f(t)<f(t+1)$ for all $t\ge1$ ; (b) if $\bar v>W$ there is $t^*$ with $f(t)<f(t+1)$ for all $t>t^*$ .
$q<p$ : (a) if $\bar v<2W$ then $f(t+1)<f(t)$ for all $t\ge1$ ; (b) there is $t^*$ with $f(t+1)<f(t)$ for all $t>t^*$ .

The goal is the conjunction of the five claims.

Milestones, in proof order

(9) with $p=q$ (p. 20): $\mathbb E[T_q\mid T_q+T_p=t+1]=\frac{t+1}{2}$ .
(10) (p. 21): $f(t)=\bar v\frac{t+1}{2}-Wt$ if $p=q$ , and $f(t)=\bar v\bigl(\frac{t\beta^t}{\beta^t-1}-\frac1{\beta-1}\bigr)-Wt$ with $\beta=q/p$ if $p\ne q$ .
(11) (p. 21): extending (10) to real $s>0$ , its derivative at $t$ is $\bar v\,\varphi(\beta^t-1)-W$ .
Proof of Lemma D.1 (pp. 40–41): $\varphi(x)\to\frac12$ as $x\to0$ ; $(x+2)\ln(x+1)-2x$ is $\ge0$ for $x>0$ and $\le0$ on $(-1,0)$ .
Lemma D.1 (p. 40): $\varphi(x)\ge\frac12$ for $x>0$ and $\varphi(x)\le\frac12$ for $-1<x<0$ .
Proof of Theorem 5.1 (p. 22): $\varphi(x)\to1$ as $x\to\infty$ and $\varphi(x)\to0$ as $x\to-1^+$ .

Significance

The theorem describes how span and moreishness affect the relation between survey utility and session length. When $q>p$ and $\bar v>W$ , utility eventually increases; when $q<p$ , it eventually decreases. In the symmetric case $q=p$ , the sign is decided by $\bar v$ against $2W$ alone. These are conditional predictions for survey data, rather than a converse that identifies $q$ and $p$ from the sign by itself.

The result is proved in the paper; it has no machine-checked proof. Formalizing it checks the Bayes computation (9)–(10), including an arithmetico-geometric sum and a printed exponent slip on p. 20 ( $p^{t+1}$ for $p^{t-1}$ , harmless because it cancels), and the real-analytic Lemma D.1. It also makes explicit one hypothesis the printed theorem omits (below).

Difficulty

The closed form (10) needs the sum $\sum_{\tau=1}^t\tau\beta^{\tau}$ and care with $\beta^t-1$ in denominators. The main obstacle is that monotonicity is a statement about integer $t$ , while the natural tool, the derivative $\varphi(\beta^t-1)$ of the real extension, lives on real $t$ ; the integer statement must be recovered from bounds on $\varphi$ over whole intervals, not at single points. Lemma D.1 is a two-level sign analysis of a function with a removable singularity at $0$ , and the two limits at $\infty$ and at $-1^+$ are of L'Hôpital type. The obvious argument for 2(b), " $\varphi\to1>W/\bar v$ ", silently uses $\bar v>W$ ; without it, since $\varphi<1$ on $(0,\infty)$ , the claim fails.

Formalization scope

Explicit discrete model. (8) and (9) are taken as the definitions of $\mathbb E[S\mid T=t]$ and $\mathbb E[T_q\mid T=t]$ ; no measure-theoretic conditioning is involved. Independence of $T_q$ and $T_p$ is the product form of jointMass.
Integer time in the goal. $t\in\mathbb N$ , $t\ge1$ (the support of $T$ ). "Increases with $t$ " is $f(t)<f(t+1)$ , strictly; "for $t>t^*$ " is $\exists t_0\in\mathbb N,\ \forall t>t_0$ . Real $t$ and the real power $\beta^t$ appear only in the milestone (11).
Hypotheses. $0<p<1$ and $0<q<1$ are the paper's standing assumptions; they exclude the degenerate $p=q=0$ , where $T=1$ almost surely and Lean's $x/0=0$ would make claim 1 false. The paper's parameter space has $\bar v\ge0$ (p. 15). $W>0$ is implicit (§2.1 normalizes $W=1$ ). $\bar v>W$ in 2(b) is added: the proof uses it on p. 22 ("since $\bar v>W$ by assumption") and 2(b) is false without it.
Domain of $\varphi$ . Every statement about $\varphi$ restricts $x$ to $x>0$ , $-1<x<0$ , a punctured neighbourhood of $0$ , the right neighbourhood of $-1$ , or $x\to\infty$ , so the junk values at $x=0$ and $x\le-1$ never enter.
Ruled out. Stating the goal for real $t$ , dropping $p,q>0$ , or reading 1 as a one-way implication all give a different theorem.
Infrastructure. Mathlib's Real.log, Real.rpow, HasDerivAt, Filter.Tendsto and finite sums suffice. The inequality $\ln(1+x)\ge 2x/(x+2)$ for $x\ge0$ is in Mathlib (Real.le_log_one_add_of_nonneg). Contributions of any milestone, of alternative discrete proofs of monotonicity that avoid the real extension, and of the full goal are welcome.

Selected references

J. Kleinberg, S. Mullainathan, M. Raghavan, The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization, Management Science, 2023. arXiv:2202.11776v3 (cited version): https://arxiv.org/abs/2202.11776 ; https://doi.org/10.1287/mnsc.2022.03683
G. S. Becker, K. M. Murphy, A Theory of Rational Addiction, Journal of Political Economy 96(4), 1988. https://doi.org/10.1086/261558

14 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Frontiers in Operations: Battery as a Service: Flexible Electric Vehicle Battery Leasing: Win-Win-Win of Flexible Leasing for a Large High-Capacity Range and Battery Cost near a(1−ρ)/2Research Paper

Motivation

Electric-vehicle makers such as NIO sell cars without the battery and lease the battery separately, a business model called Battery as a Service (BaaS). The leased battery can be swapped at a station in minutes, so a customer is not tied to one battery size: a driver who leases a small battery for the daily commute can rent a large one for a long holiday trip, and a driver who leases a large battery can downgrade for a while and pay less. Shi and Hu (M&SOM 2024, doi:10.1287/msom.2022.0587) ask whether such flexible battery leasing is good for all three parties at once: the manufacturer (profit), the customers (total cost) and the environment (total battery capacity that has to be produced). A business-model innovation of this kind is adopted only if it improves profit; it is defensible publicly only if it does not raise customer cost or the number of batteries in circulation. The paper's answer is a "win-win-win" region of parameters, and that result is the goal of this mission.

Setting

A manufacturer serves a unit mass of customers with two batteries. The low-capacity battery has range $r_l=0$ , lease rate $p_l=0$ and acquisition cost $c_l=0$ (normalizations). The high-capacity battery has range $r_h$ , lease rate $p_h$ and incremental acquisition cost $c_h$ . Driving a distance beyond the battery's range costs the customer the shortfall: a need $x$ served by range $r$ costs $(x-r)^+$ plus the lease rate.

Each customer has a regular need $d\sim\mathcal U[0,1]$ , known when choosing a primary battery, and a peak need $D\sim\mathcal U[0,a]$ with $a>1$ , independent of $d$ and learned later. A fraction $\rho$ of the time is regular usage, $1-\rho$ peak usage. The standing assumptions are $a>1$ , $a/(2+a)<\rho<1$ , $0<r_h\le a$ and $0\le c_h\le(1-\rho)a$ .

Simple leasing. The manufacturer sets $p_h$ ; each customer leases low capacity iff $\rho d+(1-\rho)\mathbb E[D]\le p_h+\rho(d-r_h)^++(1-\rho)\mathbb E[(D-r_h)^+]$ . With $\tau^b$ the low-capacity volume, the profit is $\Pi^b=(1-\tau^b)(p_h-c_h)$ , the total customer cost $CT^b$ is the integral over $d$ of the cost each customer bears, and the total battery capacity is $BT^b=(1-\tau^b)r_h$ .

Flexible leasing. A two-period game. The manufacturer sets $p_h$ ; customers choose primary batteries anticipating the peak period; the manufacturer then sets an upgrade rate $\bar p_h$ and a downgrade rate $\bar p_l$ ; customers learn $D$ and choose whether to swap according to Table 1 of the paper (a low lessee pays $(D-r_h)^++\bar p_h$ after upgrading, a high lessee pays $D+\bar p_l$ after downgrading). Upgrades $U$ in excess of downgrades $V$ must be met by buying $Q_h=[U-V]^+$ extra high-capacity batteries. The peak-period objective is (1): $(1-\tau)p_h+V(\bar p_l-p_h)+U\bar p_h-c_hQ_h/(1-\rho)$ , and the total profit is (2): $\Pi^f=\rho(1-\tau)p_h+(1-\rho)\cdot(1)-(1-\tau)c_h$ . A flexible equilibrium is a lease rate $p_h$ with optimal peak rates, a lease volume $\tau$ that customers rationally expect, and a profit no other lease rate and continuation can beat. $CT^f$ is the total expected cost of the customers' choices, and $BT^f=(1-\tau+Q_h)r_h$ .

Formalization targets

Write $c_0=a(1-\rho)/2$ ; by Proposition 2 this is the cost at which the manufacturer stops buying extra batteries.

Goal: Proposition 6 (win-win-win)

For $a>1$ , $a/(2+a)<\rho<1$ :

if $\rho<7a/(8+7a)$ , there is $\delta>0$ such that for each $c_h\in(c_0-\delta,c_0)$ there is $R<a$ such that for all $r_h\in(R,a]$ , a benchmark optimum and a flexible equilibrium exist, and every pair of them satisfies

Q^f_h>0,\qquad \Pi^b<\Pi^f,\qquad CT^f<CT^b,\qquad BT^f<BT^b;

there is $\delta>0$ such that for each $c_h\in(c_0,c_0+\delta)$ there is $R<a$ such that for all $r_h\in(R,a]$ , the same holds with $Q^f_h=0$ .

Milestones

Lemma 1 and Proposition 1 (the benchmark), Lemma 2 (peak volumes), Lemma 3 (optimal peak rates), Lemma 4 (flexible lease volume), Proposition 2 in its first case (the flexible equilibrium for $c_h<c_0$ ), Proposition 4 near the corner $(r_h,c_h)=(a,c_0)$ (customer cost), and Proposition 5 in its first bullet (capacity is smaller iff $\rho<7a/(8+7a)$ and $c_h\le T(r_h)$ for an explicit $T$ ).

Significance

The result identifies conditions under which a pricing innovation helps the firm, its customers and the environment at the same time: a battery cost near $a(1-\rho)/2$ and a high-capacity range close to the largest peak need. Flexible leasing reallocates high-capacity batteries from customers who do not need them in the peak period to customers who do, so fewer batteries have to be produced. But the manufacturer prices the up/downgrade options to extract the efficiency gain and may buy extra batteries, so lower customer cost and lower capacity are not automatic. Proposition 6 states where all three improvements coexist.

The paper proves its results by calculus on closed forms. Nothing here is machine-checked yet. A formalization adds three things. First, it derives the closed forms from the model itself (customer choices from Table 1, volumes as measures of customer sets, equilibria as maximizers), where the paper states them. Second, it settles which reading of "sufficiently close" and "sufficiently large" is true. Third, it records the regimes in which the intermediate lemmas hold, which the printed statements leave implicit.

Difficulty

The closed forms of Lemmas 1–4 are routine integrals of piecewise-linear functions. The difficulty is global optimality and the corner analysis.

Equilibrium is global. A flexible equilibrium must beat every lease rate together with every rationally expected continuation, including continuations in the regime where the manufacturer buys no extra batteries and at lease rates where customers all lease one type. A first-order condition on one regime does not establish this.
The $Q^f_h=0$ side is not the printed one. For $c_h$ just above $c_0$ the equilibrium is a kink regime that the paper does not describe. The paper's second-case formulas in Proposition 2 are not the equilibrium there, so the goal's second branch cannot be obtained from them.
Order of limits. At the corner $(r_h,c_h)=(a,c_0)$ the two capacities coincide. Profit and customer cost are strictly better under flexible leasing there, but capacity is only weakly better. The capacity comparison holds only when $r_h$ approaches $a$ after $c_h$ is fixed.

Formalization scope

The model is the paper's base model of §3–§4: flexible leasing introduced into an existing BaaS program with independent regular and peak needs. The extensions of §5 (correlated needs, range choice, launching with flexible leasing) and the numerical calibration (§4.1, Figures 2–5) are out of scope.

Representation. All parameters are real numbers. Expectations over $D\sim\mathcal U[0,a]$ are interval integrals divided by $a$ ; volumes of customers are Lebesgue measures of subsets of $[0,1]$ . Every volume, expected cost and equilibrium is defined from the model; the paper's closed forms are theorems, never definitions. Customers lease low when indifferent, upgrade on $\le$ and downgrade on $>$ , following the proofs. The lease rate ranges over all of $\mathbb R$ ; the paper's remark "we require $p_h<\min(1,r_h)$ " is not imposed, because the benchmark optimum can exceed 1. The peak rates range over the set $\bar p_h\le a$ , $p_h-a\le\bar p_l\le p_h$ that the paper requires (p. 13). An equilibrium is optimal against every continuation at every lease rate.

Readings and added hypotheses.

Proposition 6 is posed as " $c_h$ sufficiently close to $c_0$ , then $r_h$ sufficiently large". A single neighbourhood of $(a,c_0)$ in both variables is false on both sides. On the $Q^f_h>0$ side, Proposition 5's threshold $T(r_h)$ equals $c_0$ at $r_h=a$ and is below it for $r_h<a$ . The point $c_h=c_0$ is excluded.
Each branch of the goal asserts existence of a benchmark optimum and a flexible equilibrium, so it is not vacuous. A goal of the form "every equilibrium is win-win-win" without existence would be trivially true where no equilibrium exists, and is ruled out.
Lemma 2's interior cases hold with $r_h$ in place of $a$ (and $\bar p_h\ge0$ ). The statement also gives the missing outer cases for rates below zero or beyond $r_h$ , covering every real rate.
Lemma 3 is posed in the regime $\tau>c_h/(a(1-\rho))$ , the only one in which its acquisition quantity is nonnegative. Its rates are assumed to lie below $r_h$ .
Lemmas 1, 4 and Propositions 1, 2, 5 carry the proofs' interior conditions as explicit parameter inequalities: the indifferent customer lies below $r_h$ , and Proposition 1's range for $c_h$ holds.
Proposition 5(i) is the $\le$ form, as in its proof. Proposition 4 is posed in its corner-neighbourhood clauses only.
Proposition 2's second case, Proposition 3 and the remaining clauses of Propositions 4–5 are not posed: the second case of Proposition 2 is false on part of its range, and Proposition 3's threshold is garbled in the manuscript.

What a complete development needs. Lebesgue measure of intervals, interval integrals of piecewise-linear functions, and maximization of concave quadratics with a kink. It also needs the kink-regime equilibrium on the $Q^f_h=0$ side and continuity arguments at the corner. Lemmas 1–4 are reusable for any variant of the model, and proofs of the milestones in any order are welcome.

Selected references

L. Shi and B. Hu, Battery as a Service: Flexible Electric Vehicle Battery Leasing, Manufacturing & Service Operations Management, Frontiers in Operations, 2024. Read as the authors' manuscript of 13 January 2024. https://doi.org/10.1287/msom.2022.0587

10 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Tokenomics: When Tokens Beat Equity IV: Under Moral Hazard Every Equity-Financeable Venture Is Token-Financeable and Every Token-Financeable One Is Debt-Financeable, Both StrictlyResearch Paper

Motivation

Start-ups that build a platform or a digital service increasingly raise their set-up capital by pre-selling tokens: claims on the future output of the service, redeemable once it exists. Between 2017 and 2019 such token offerings raised billions of dollars, and corporate finance asked whether a token is anything more than a disguised equity or debt claim. K. Malinova and A. Park (Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023; Management Science 2023) answer this in a stylized monopoly model. Without frictions, a well-designed token contract is equivalent to equity and to debt: all three leave the entrepreneur the project's full NPV (missions I–III of this series). With moral hazard, when the entrepreneur can influence demand through effort that investors cannot observe, the three instruments separate.

The question goes back to M. C. Jensen and W. H. Meckling (Theory of the firm, J. Financial Economics 3, 1976), who showed that outside equity dilutes the owner's incentive to exert effort, while debt, which leaves the owner the full upside above the repayment, dilutes it less. This mission formalizes where tokens sit in that ranking: strictly between debt and equity.

Setting

An entrepreneur needs a set-up cost $C_0>0$ and then produces a quantity $q$ at marginal cost $c>0$ against the linear inverse demand $p(q)=x-q$ . The demand intercept $x$ is uniformly distributed on $(0,\theta)$ , and the expectation of a payoff $g$ is $\mathbb E_\theta[g]=\frac1\theta\int_0^\theta g(x)\,dx$ . Facing the realized $x$ , a monopolist produces $q^m(x)=\max\{(x-c)/2,0\}$ and earns $\pi^m(x)=\max\{x-c,0\}^2/4$ ; the project's NPV is $\mathrm{NPV}(\theta)=\mathbb E_\theta[\pi^m]-C_0$ .

Moral hazard. With effort the intercept is uniform on $(0,\theta_h)$ , without effort on $(0,\theta_l)$ , with $c<\theta_l<\theta_h$ . Effort costs the entrepreneur $C_e$ in value. It is chosen after the financing contract is signed and cannot be contracted upon. The project has positive NPV only with effort ( $\mathrm{NPV}_l\le0<\mathrm{NPV}_h$ ) and $\mathrm{NPV}_h>C_e$ . Investors break even under effort, so every contract term is fixed by $\theta_h$ ; a project can be financed by an instrument when the break-even terms make effort the entrepreneur's best choice.

Equity. Investors take the share $\alpha_s=C_0/\mathbb E_{\theta_h}[\pi^m]$ (17); the incentive constraint is $(1-\alpha_s)\mathbb E_{\theta_h}[\pi^m]-C_e\ge(1-\alpha_s)\mathbb E_{\theta_l}[\pi^m]$ (18).
Debt. A face value $D\ge0$ with $\mathbb E_{\theta_h}[\min\{\pi^m,D\}]=C_0$ (21); the entrepreneur keeps $\max\{\pi^m-D,0\}$ , and the incentive constraint (22) compares its expectations under $\theta_h$ (minus $C_e$ ) and $\theta_l$ .
Optimal tokens. The entrepreneur pre-sells $t$ tokens and gives token-holders the share $\alpha_t=t/(t+c)$ of all tokens issued later. At demand $x$ and output $q>t$ she earns $\pi^e_t(x,q)=(1-\alpha_t)(q-t)(x-q)-c(q-t)$ , and $0$ when $q\le t$ . The pre-sale solves the break-even condition (16) at $\theta_h$ ,

\frac{c}{c+t}\,\frac{2}{3\theta_h}\Big(\frac{\theta_h-c}{2}-t\Big)^3=\mathrm{NPV}_h ,\qquad 0<t<\frac{\theta_h-c}{2},

and the incentive constraint (27) compares $\mathbb E[\pi^e_t(x,q^m(x))]$ under $\theta_h$ (minus $C_e$ ) and $\theta_l$ .

Write $\lambda=(\theta_l-c)/(\theta_h-c)$ (19), $\delta=2\sqrt D/(\theta_h-c)$ (23) and $\tau=2t/(\theta_h-c)$ (28).

Formalization targets

Goal: Proposition 8

Writing $\mathcal E,\mathcal T,\mathcal D$ for the sets of parameters $(c,C_0,C_e,\theta_l,\theta_h)$ satisfying the standing assumptions at which equity, optimal tokens and debt can finance the project,

\mathcal E\subsetneq\mathcal T\subsetneq\mathcal D .

The two inclusions are universal statements; strictness is posed as the existence of separating parameter values.

Milestones

The break-even terms exist and are unique; the token entrepreneur's expected profit is the left side of (26), and $0$ under $\theta_l$ when $\theta_l\le c+2t$ .
Proposition 5: equity finances the project iff $\mathrm{NPV}_h-C_e\ge\lambda^3\frac{\theta_h}{\theta_l}\mathrm{NPV}_h$ (20).
(48) and Proposition 6: $\mathrm{NPV}_h=\frac{(\theta_h-c)^3}{12\theta_h}(1-3\delta^2+2\delta^3)$ ; debt always induces effort when $\lambda\le\delta$ , and otherwise iff

\mathrm{NPV}_h-C_e\ge\frac{(\lambda-\delta)^2}{(1-\delta)^2}\,\frac{\lambda+2\delta}{1+2\delta}\,\frac{\theta_h}{\theta_l}\,\mathrm{NPV}_h .

Proposition 7: tokens always induce effort when $\lambda\le\tau$ , and otherwise iff $\mathrm{NPV}_h-C_e\ge\frac{(\lambda-\tau)^3}{(1-\tau)^3}\frac{\theta_h}{\theta_l}\mathrm{NPV}_h$ (29).
Lemmas 4–5 and Corollaries 2–3: equity's constraint is the strongest.
Lemma 6 ( $0<\tau<\delta^2<\delta<1$ ) and Lemma 7 (for $\delta<\lambda<1$ , $\lambda^3>\frac{(\lambda-\tau)^3}{(1-\tau)^3}>\frac{(\lambda-\delta)^2(\lambda+2\delta)}{(1-\delta)^2(1+2\delta)}$ ).
Appendix B: with $C_0=110$ , $c=10$ , $\theta_l=50$ , $C_e=25$ , the case $\theta_h=60$ is financed by debt and tokens but not by equity, and $\theta_h=57$ by debt only.

Significance

The result places a new instrument in the classical ranking of financing by incentive strength. Under the optimal token contract the entrepreneur earns only from tokens issued beyond the pre-sale, so, like a debtor, she earns nothing in low-demand states; this makes effort more attractive than under equity. Because the break-even pre-sale is smaller in normalized terms than the break-even debt ( $\tau<\delta^2$ ), tokens still leave more of the low-demand upside to the entrepreneur than debt does, and debt remains strictly better. The separating instances show that neither inclusion is an artefact of the model's parametrization.

The paper proves the result by hand in Appendix A and illustrates it numerically in Appendix B; none of it has been machine-checked. The mission produces a checked version of the whole chain, including the two points where the printed statements need repair (Lemmas 6 and 7, see below), and a verified treatment of the two Appendix B instances, whose contract terms are roots of cubic equations rather than the rounded values printed.

Difficulty

Each step is elementary real analysis, and there are many of them. Three require care.

Token versus debt. Comparing (24) and (29) for arbitrary $\tau<\delta<\lambda$ fails: the second inequality of Lemma 7 is false, for example, at $\delta=0.5$ , $\tau=0.49$ , $\lambda=0.8$ . It holds only for the actual contract terms, which are tied to each other through the two break-even conditions, so the comparison cannot be made on the incentive constraints alone.
The two regimes of each incentive constraint. When $\theta_l\le c+2\sqrt D$ (or $\le c+2t$ ), the printed right-hand sides of (22) and (27) have reversed integration ranges; the no-effort profit is $0$ there and the constraint holds trivially. Each inclusion must handle both regimes and their interaction across instruments.
The separating instances. $D$ and $t$ at $\theta_h\in\{57,60\}$ are roots of cubics and are only known to a few digits; the margins are small (equity at $\theta_h=60$ fails by $38.61$ against $39.08$ ), so the roots must be bracketed tightly and the uniqueness of the break-even terms is needed to rule out other contracts.

Formalization scope

All objects are real functions of real parameters: the shared model (expect, pim, qm, npv, the debt and token payoffs, condition (16)) in TokenFinance.Debt, the financeability predicates and every theorem in TokenFinance.MoralHazard; there is no probability layer. Expectations are expect θ g, the interval integral over $[0,\theta]$ divided by $\theta$ , and every expectation in a definition is of a realized payoff: the closed forms (20), (24), (26), (29), (48) are theorems. This rules out the trivializing formalization in which the incentive constraints are written as their closed forms, which would turn Propositions 5–8 into algebra. Debt and token payoffs carry positive parts, so the paper's case split ("the moral hazard problem does not arise") is a theorem, not a definition.

Conventions committed to:

The standing assumptions are $0<c<\theta_l<\theta_h$ , $C_0>0$ , $\mathrm{NPV}_l\le0<\mathrm{NPV}_h$ and $C_e<\mathrm{NPV}_h$ . Positive marginal cost is the paper's ("with a positive marginal cost", p. 22). $\mathrm{NPV}_h>0$ is written out, reading "positive expected NPV only if the entrepreneur exerts effort" together with "exceeds $C_e$ "; without it a negative $C_e$ would put a project with $\mathrm{NPV}_h\le0$ in $\mathcal E$ but not in $\mathcal T$ . No sign is imposed on $C_e$ .
Financeability is existential in the contract terms (equity's share is determined by (17)); the token break-even is condition (16) as printed, which the proof of Proposition 3 derives from the token-holders' break-even (35).
Propositions 5–7 are posed as equivalences: (20), (24), (29) are rearrangements of (18), (22), (27).
Lemmas 4–5 add $0<\delta$ , $0<\tau$ , which their proofs assume (at $0$ they are equalities). Lemma 6 is posed as $0<\tau<\delta^2<\delta<1$ , what its proof establishes; the printed " $\delta<\lambda$ " is not a property of the terms, since Proposition 6 treats $\lambda\le\delta$ . Lemma 7 carries the contract terms as hypotheses.
Out of scope: the secondary token market and redemption mechanics, bankruptcy costs, consumer welfare, and the institutional discussion of §I and §V.

Needed infrastructure: interval integrals of piecewise polynomials, the intermediate value theorem and strict monotonicity for the break-even terms, and polynomial inequalities. A lemma computing $\mathbb E_\theta$ of truncated quadratics is reusable across all four missions of the series. Proofs of any milestone, and of the Appendix B root bracketing, are welcome.

Selected references

K. Malinova, A. Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023; published in Management Science, 2023. https://ssrn.com/abstract=3286825, doi:10.1287/mnsc.2023.4882
M. C. Jensen, W. H. Meckling, Theory of the firm: Managerial behavior, agency costs and ownership structure, Journal of Financial Economics 3(4), 1976, 305–360. https://doi.org/10.1016/0304-405X(76)90026-X

19 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Tokenomics: When Tokens Beat Equity III: The Break-Even Token Pre-Sale Strictly Increases in the Set-Up Cost and the Marginal Cost and Strictly Decreases in Expected DemandResearch Paper

Motivation

Firms can raise money before production by selling claims on future output. In the model of Malinova and Park, these claims are tokens: a buyer prepays for a quantity of the good, and the final contract also gives token holders a share of tokens issued after demand becomes known. The firm must choose how many tokens to pre-sell. A larger pre-sale brings in more finance but changes the allocation of later sales revenue. The paper identifies contract terms that preserve the firm's monopoly output choice and determines the pre-sale quantity by investors' break-even condition (Proposition 3, p. 24). Proposition 4 asks how that quantity responds when financing need, production cost, or expected demand changes. These comparative statics make the contract's financing response explicit rather than leaving the break-even equation as an isolated root.

Setting

An entrepreneur pays a set-up cost $C_0>0$ to launch production and then incurs a marginal cost $c>0$ per unit. After financing, a demand intercept $x$ is drawn uniformly from $(0,\theta)$ , where $c<\theta$ . At output $q$ , the inverse demand price is $x-q$ . Without financing distortions, the monopoly quantity is $q^m(x)=\max\{(x-c)/2,0\}$ and its profit is $\pi^m(x)=\max\{x-c,0\}^2/4$ . For a realized payoff $g(x)$ , expectation means the average $E_\theta[g]=\theta^{-1}\int_0^\theta g(x)\,dx$ . The venture's net present value is $E_\theta[\pi^m]-C_0$ , equal in this domain to $(\theta-c)^3/(12\theta)-C_0$ (equation (3), p. 14).

Under the optimal token contract of Proposition 3, investors buy $t$ tokens at time zero, and token holders receive the fraction $\alpha_t=t/(t+c)$ of new tokens issued when output exceeds the pre-sale. A refund rule applies when output falls below the pre-sale. The resulting positive break-even pre-sale size is determined by equation (16):

\frac{c}{c+t}\frac{2}{3\theta}\left(\frac{\theta-c}{2}-t\right)^3 =\frac{(\theta-c)^3}{12\theta}-C_0.

For a positive-NPV venture, this equation has one positive root, in $(0,(\theta-c)/2)$ (Appendix A, pp. 40–41). The mission treats the root as a solution of the equation, so statements about the optimal quantity apply to every value satisfying it.

Formalization targets

The comparative-statics goal

Proposition 4, p. 25, asserts three strict directions. If $t(c,C_0,\theta)$ denotes the unique positive root of (16), then, while both endpoint ventures have positive NPV,

C_0<C_0'\ \Longrightarrow\ t(c,C_0,\theta)<t(c,C_0',\theta),

c<c'\ \Longrightarrow\ t(c,C_0,\theta)<t(c',C_0,\theta),

\theta<\theta'\ \Longrightarrow\ t(c,C_0,\theta')<t(c,C_0,\theta).

Thus a larger set-up cost or marginal cost requires more pre-sold tokens, while a higher demand level requires fewer. The Lean goal compares arbitrary positive roots directly. It places the NPV condition at the higher cost in the second comparison and at the lower demand level in the third; these are the restrictive endpoints. The first comparison places it at the higher set-up cost.

Source milestones

The milestone list follows the Appendix A proof: existence and uniqueness of the root of (41); the negative $t$ derivative (42); the positive $c$ derivative (45); the negative $\theta$ derivative (46); and the derivative in $t$ of the expression in (46), equation (47). These are source claims, with their displayed constants retained. Equation (42) and equation (45) contain printing errors in the SSRN copy; the formal statements use the actual derivatives and the milestone quotes retain the printed text.

Significance

Proposition 3 establishes that the chosen token contract can finance a positive-NPV venture while keeping the efficient monopoly output. Proposition 4 then describes the contract's response to the model's three principal parameters. Its strict inequalities distinguish an actual response from a weak monotonicity claim that could allow the pre-sale to remain unchanged. The demand comparative static is economically specific: a higher $\theta$ raises the demand intercept on average, but the quantity of tokens needed to finance the same set-up cost falls.

The paper proves these results analytically. This mission seeks machine-checked proofs of the root comparison and its stated derivative milestones. A completed development would provide reusable results about parameter-dependent roots of rational functions, especially when the root is specified by a break-even condition rather than by an explicit formula. The current Lean files are compiled statements with proof placeholders; compilation does not establish the mathematical results.

Difficulty

Equation (16) is cubic in a quantity that also occurs in a denominator, so the root does not offer a convenient closed expression for direct comparison. The endpoint restrictions matter: the meaningful root lies strictly between zero and $(\theta-c)/2$ , and derivatives that have the desired sign in that interval need not keep the same sign outside it. In particular, the $t$ derivative in (42) reaches zero at the upper boundary. The demand derivative in (46) also vanishes at $t=0$ , making its strict sign in the interior a separate claim. A literal transcription of two printed derivatives would give incorrect equalities even though their intended sign conclusions survive. The formal development therefore needs both careful domain control and the corrected expressions.

Formalization scope

The namespace TokenFinance.Statics represents all quantities as real functions. Uniform expectation is the interval integral divided by $\theta$ . Monopoly output and profit use max to encode zero production below cost. The common Setting definition file also records the equity and debt payoffs and the token contract's case split, following the series-wide model. The break-even condition is exactly the closed-form equation (16), while NPV remains the integral of realized monopoly profit minus $C_0$ . The goal assumes the paper's standing $c>0$ , $C_0>0$ , $c<\theta$ , and positive NPV, written as $C_0<(\theta-c)^3/(12\theta)$ using equation (3). Derivative statements state their own regions and nonzero-denominator conditions. The token size is quantified over positive roots rather than chosen by an arbitrary selection function.

The root cannot be defined to have the claimed monotonicity, and the derivative signs cannot be inserted as hypotheses of the goal. The missing work includes real-variable derivative calculations, root existence and uniqueness on the economic interval, and the strict parameter comparisons. The secondary token market, redemption mechanics beyond the contract payoffs, bankruptcy costs, consumer welfare, and the paper's institutional discussion are outside this mission's scope.

Selected references

Katya Malinova and Andreas Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023, pp. 14, 24–25, 40–42. SSRN preprint.
Katya Malinova and Andreas Park, Tokenomics: When Tokens Beat Equity, Management Science, 2023. DOI:10.1287/mnsc.2023.4882. The mission's equation and page references follow the SSRN version above.

7 thms3 active usersReviewed