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.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 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≤ 1.9202796Open frontier

4 provers on it7 of 8 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.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 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≤ 1.9202796Open frontier

4 provers on it7 of 8 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

Economics Operations Research Optimization·Captain: mikedeng1

What Is the Impact of Nonrandomness on Random Choice Models?: Revenue-Ordered Assortments Are Optimal When One Product's Utility Is DeterministicResearch Paper

Motivation

Retailers choose which products to show a customer, and the customer chooses at most one of them. The assortment problem asks for the offer set that maximizes expected revenue, given a model of how customers choose. Under the multinomial logit (MNL) model every alternative, the no-purchase option included, carries an independent Gumbel noise term of the same scale, and Talluri and van Ryzin (2004) showed that the optimal set is then a revenue-ordered assortment: the $n$ most expensive products, for some $n$ . This structure turns an exponential search over subsets into a comparison of $N$ candidates, and it is the reason MNL-based assortment optimization is used in practice.

Equal randomness for all alternatives is a strong assumption. A product a consumer has bought many times, or a well-advertised one, is known; its utility carries little or no noise. Wang (SSRN 3579781; published in Manufacturing & Service Operations Management, 2021) studies the extreme case in which exactly one alternative has a deterministic utility. The choice probabilities for that case go back to Besanko, Perry and Spady (1990) and are no longer MNL once that alternative is offered. The paper asks what this does to the standard operations problems. Its answer for assortment planning splits in two: if the deterministic alternative is a product, revenue-ordered assortments remain optimal (Theorem 5); if it is the no-purchase option, the feasibility version of the assortment problem is NP-complete (Theorem 6). This mission formalizes the first half.

Setting

Let $\mathcal N=\{1,\dots,N\}$ be the products and $0$ the no-purchase option, always available. Utilities are $U_i=u_i+\xi_i$ for $i\in\mathcal N\setminus\{i'\}$ and $U_0=u_0+\xi_0$ , with the $\xi$ 's independent Gumbel of scale $\mu>0$ and mean zero; one product $i'$ has deterministic utility $U_{i'}=u_{i'}$ . Product $i$ has price $p_i$ . Write

$a_i=\exp(u_i/\mu)$ and $a_0=\exp(u_0/\mu)$ for the attraction values;
$\Lambda=\exp(-u_{i'}/\mu-\gamma)$ , with $\gamma$ the Euler–Mascheroni constant;
$\Psi(S^+/\{i'\})=a_0+\sum_{j\in S\setminus\{i'\}}a_j$ for an offer set $S\subseteq\mathcal N$ .

If $i'\notin S$ the choice probabilities are MNL: $q_i(S)=a_i/(a_0+\sum_{j\in S}a_j)$ . If $i'\in S$ , with $\Psi=\Psi(S^+/\{i'\})$ , they are given by model (1):

q_i(S)=\frac{a_i}{\Psi}\bigl[1-e^{-\Lambda\Psi}\bigr]\ (i\in S\setminus\{i'\}),\qquad q_{i'}(S)=e^{-\Lambda\Psi},

and $q_0(S)=1-\sum_{i\in S}q_i(S)$ . The expected revenue (12) is $R(S)=\sum_{i\in S}p_iq_i(S)$ , which on the page reads

R(S)=\begin{cases}\dfrac{\sum_{i\in S}p_ia_i}{a_0+\sum_{j\in S}a_j}, & i'\notin S,\\[1.5ex]\dfrac{\sum_{i\in S\setminus\{i'\}}p_ia_i}{\Psi}\bigl[1-e^{-\Lambda\Psi}\bigr]+p_{i'}e^{-\Lambda\Psi}, & i'\in S.\end{cases}

The assortment problem (13) is $\max_{S\subseteq\mathcal N}R(S)$ . When the products, $i'$ included, are labelled so that $p_1\ge p_2\ge\dots\ge p_N$ , the sets $S_n=\{1,\dots,n\}$ are the revenue-ordered assortments.

In Lean the products are Fin N, and attr, attr0, Lam, Psi, choiceProb, revenue12 and roSet N n are $a_i$ , $a_0$ , $\Lambda$ , $\Psi$ , $q_i(S)$ , $R(S)$ and $S_n$ .

Formalization targets

Goal: Theorem 5 (p. 14)

For $\mu>0$ and prices $p_1\ge\dots\ge p_N\ge0$ ,

\exists\,n\in\{1,\dots,N\}:\qquad R(S)\le R(S_n)\quad\text{for all }S\subseteq\mathcal N .

The statement fixes no constants; it asserts only the structure of an optimal set.

Milestones

Lemma 1 (p. 28). For any regular choice model in which each $q_i(S)$ , $i\in S$ , is a nonnegative convex function of $q_0(S)$ , and prices $p_1\ge\dots\ge p_N$ , some $S_n$ , $n\in\{0,\dots,N\}$ , maximizes $R(S)=\sum_{i\in S}p_iq_i(S)$ .
$q_0$ is increasing and concave in $q_{i'}$ (p. 29). With $a_0=1$ , $q_0=h_\Lambda(q_{i'})$ where $h_\Lambda(y)=\Lambda(1-y)/(-\log y)$ , increasing and concave on $(0,1)$ .
$q_{i'}$ is increasing and convex in $q_0$ (p. 29). The inverse of $h_\Lambda$ is increasing and convex on the range of $h_\Lambda$ .
The model satisfies Lemma 1 (pp. 14, 29). The model above is regular, each $q_i$ is a nonnegative convex function of $q_0$ , and (12) equals $\sum_{i\in S}p_iq_i(S)$ .

Significance

Theorem 5 says that a deterministic product utility, which destroys the MNL form of the choice probabilities, does not destroy the nested structure of the optimal assortment. The problem therefore stays solvable by checking $N$ sets, in contrast with the companion case of a deterministic no-purchase utility, whose feasibility version is NP-complete. Lemma 1 is a criterion of independent use: any regular choice model whose choice probabilities are convex functions of the no-purchase probability has a revenue-ordered optimal assortment, and the MNL model is the case of linear functions.

The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The mission produces a checked version of the convex-in- $q_0$ criterion on top of the platform's published regular-choice-model definitions, and a checked treatment of model (1), which is also the model of truncated utilities (Corollary 2 of the paper).

Difficulty

The classical MNL argument uses the fact that $R(S)$ is a ratio of sums linear in the attraction values, so optimality reduces to a threshold on prices. Model (1) is not of that form once $i'$ is offered: $q_{i'}=e^{-\Lambda\Psi}$ and the other probabilities carry the factor $(1-e^{-\Lambda\Psi})/\Psi$ , so a direct exchange argument on the revenue fails. The work lies in the analytic step: expressing $q_{i'}$ as a function of $q_0$ only through the implicit relation $q_0=\Lambda(1-q_{i'})/(-\log q_{i'})$ , and establishing that this function is convex, which requires sign control of a second derivative involving $\log$ near both ends of $(0,1)$ . A formal proof must also check regularity of the model, which the printed proof uses but does not verify.

Formalization scope

The model is encoded as in the Setting: products Fin N (the label $k$ is index $k-1$ ), the deterministic product as a parameter ip, and the no-purchase option outside Fin N. $R$ is the two-branch revenue (12), written literally, not the MNL revenue, and optimality is over all subsets of $\mathcal N$ ; the MNL special case alone is not the goal. Committed conventions:

$\mu>0$ (implicit on p. 5) and the Euler–Mascheroni constant Real.eulerMascheroniConstant in $\Lambda$ ; $a_{i'}$ plays no role;
$p_1\ge\dots\ge p_N$ is Antitone p, and $S_n$ is the set of the first $n$ indices (ties in prices do not change $S_n$ );
the goal adds $p_i\ge0$ : with all prices negative, $\emptyset$ is the unique optimum and no $S_n$ with $n\ge1$ is optimal;
Lemma 1 uses the published RevenueOrdered.Ratio.IsRegular, whose monotonicity includes the no-purchase option, as the proof uses; " $q_i=q_i(q_0)$ convex" means $f_i$ nonnegative and convex on a convex set $D_i$ containing $q_0(S)$ for every $S\ni i$ ; its conclusion allows $S_0=\emptyset$ ;
milestones 2 and 3 are stated on the open interval $0<q_{i'}<1$ , since the formula is $0/0$ at $q_{i'}=1$ .

A complete development needs elementary real analysis of $\log$ and $\exp$ (monotonicity and concavity via derivatives, inverse functions on intervals) and finite-sum algebra; Lemma 1 is reusable for any regular choice model. Contributions on the analytic lemmas and on regularity of model (1) are welcome.

Selected references

R. Wang, What Is the Impact of Non-Randomness on Random Choice Models?, SSRN 3579781; Manufacturing & Service Operations Management, 2021. https://ssrn.com/abstract=3579781, doi:10.1287/msom.2020.0951
D. Besanko, M. K. Perry, R. H. Spady, The logit model of monopolistic competition: Brand diversity, The Journal of Industrial Economics 38(4), 397–415, 1990 (reference as listed in Wang's bibliography, p. 31).
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
G. Berbeglia, G. Joret, Assortment optimisation under a general discrete choice model: a tight analysis of revenue-ordered assortments, Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371

7 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Coordination for Assembly: With at Most M − 1 Feedback Periods, the Subgame-Perfect Secure Equilibrium Has Every Contractor Exert the Minimum Effort in Every PeriodResearch Paper

Motivation

Assembly projects such as aircraft programs or large software releases split work among several contractors, each responsible for one component. The finished product can only be as advanced as its least-developed component, so the contractors play a minimum-effort game (also called a weakest-link game): the project's value depends on the minimum of the efforts, while each contractor pays for its own effort. Such games have a continuum of Nash equilibria, ranked by payoff, and laboratory evidence since Van Huyck, Battalio and Beil (1990) shows that groups often settle on low-effort equilibria, with larger groups faring worse.

An original-equipment manufacturer (OEM) can affect coordination through the information it shares. Zhang, Shokoohyar, Qi and Katok, Coordination for Assembly (Manufacturing & Service Operations Management, doi:10.1287/msom.2023.0342), study a periodic information-feedback mechanism: the project runs over $N$ periods, and at the start of each period every contractor sees every contractor's progress. Their theoretical prediction, tested in the laboratory, is that the number of feedback periods relative to the number of contractors decides whether coordination succeeds. This mission formalizes the negative half of that prediction: with too few feedback periods, the selected equilibrium is the worst one.

Setting

There are $M$ contractors and $N$ periods. Each contractor's total effort lies in $[\underline q, \bar q]$ and its effort in each period lies in $[\underline q/N, \bar q/N]$ , with $0 \le \underline q < q^* < \bar q$ , where $q^*$ is the OEM's target level. All contractors start at zero effort. In period $n$ each contractor observes all efforts so far and then all simultaneously choose $q_{i,n}$ ; the effort level of contractor $i$ after period $n$ is $\hat q_{i,n} = \sum_{t \le n} q_{i,t}$ .

The project level is $q_{\min}(\hat{\mathbf q}_N) = \min_i \hat q_{i,N}$ , the OEM's payoff is $S = p \min\{q_{\min}(\hat{\mathbf q}_N), q^*\}$ , and contractor $i$ receives the share $\gamma$ of it and pays $c$ per unit of effort:

\pi_i(\hat{\mathbf q}_N) = \gamma\, p\min\{q_{\min}(\hat{\mathbf q}_N), q^*\} - c\, \hat q_{i,N}.

The parameters satisfy $p, \gamma, c > 0$ .

A history is the list of effort profiles played so far; a strategy maps each history to the current period's effort. A subgame-perfect equilibrium (SPE) is a strategy profile from which no contractor gains by deviating after any history. For a history $h$ , write $\hat E(h)$ for the set of final level vectors reached by continuing some SPE from $h$ .

A subgame-perfect secure equilibrium (SPSE) (Definition 2 of the paper's Online Appendix) is an SPE $\sigma^\dagger$ such that, at the start of every period along its own path, each contractor's own final level $y$ maximizes its worst-case profit

\inf_{x \in \hat E(h)} \pi_i(y;\, x_{-i})

among the levels $y$ that contractor $i$ attains in some SPE continuation. This is the paper's condition (24): among equilibria, contractors favour the one that protects them against the other contractors' least favourable equilibrium behaviour.

Formalization targets

Goal: Proposition 2(i)

If $N \le M - 1$ , then an SPSE exists in which every contractor exerts the minimum effort in every period, every SPSE has this property along its path, and the project level is minimal:

q_{i,n} = \frac{\underline q}{N}\quad (i \le M,\ n \le N), \qquad q_{\min}(\hat{\mathbf q}_N) = \underline q .

Milestones

Lemma OA2(i). If $N \le M-1$ and at least $N+1$ contractors share the lowest initial effort level, some SPE has every contractor exert $\underline q/N$ in every period.
Proof of Proposition 2, Step 1. Along a path on which every contractor exerts $\underline q/N$ , continuing that path gives each contractor the minimum profit among all SPE continuations of each subgame (the paper's condition (25)).
Proof of Proposition 2, Step 1 (uniqueness). In an SPE where one contractor exerts $\underline q/N$ in every period, all contractors do.

Significance

The result says that frequent progress reports are not enough by themselves: when there are fewer feedback periods than contractors minus one, the secure refinement of subgame perfection selects the lowest project level, the same outcome as without feedback. It is the theoretical half of the paper's comparison between feedback regimes, which the laboratory experiment then tests with groups of two and four contractors and 1 to 6 feedback periods.

The result has a printed proof in the paper's Online Appendix. No machine-checked version exists. Formalizing it pins down a solution concept (an SPE refined by a maxmin criterion over the set of equilibrium outcomes of each subgame) whose verbal definition admits several inequivalent readings, and fixes which one the proposition holds for.

The companion part (ii) of Proposition 2, for $N > M - 1$ , is false as printed and is not part of this mission: with $M = 2$ , $N = 3$ , $\underline q = 3$ , $\bar q = 9$ , $q^* = 7$ , $\gamma = p = 1$ , $c = 3/4$ , the profile with path $(1,1), (1,1), (3,3)$ is an SPE with project level $5$ , and no SPSE reaches $q^* = 7$ , although part (ii) predicts that level at $N = N^* = 3$ . Corollary 2 and Proposition 3, which rest on part (ii), are omitted for the same reason.

Difficulty

The existence half is a statement about whole strategy profiles, including play after every history off the equilibrium path. The constant profile that plays $\underline q/N$ after every history is not an SPE when $\gamma p > c$ : after a history that leaves one contractor strictly behind with one period to go, that contractor gains by catching up. An SPE with the all-minimum path must therefore prescribe different, history-dependent behaviour off the path, and the count $N + 1 \le M$ of tied contractors is what keeps a single deviation from breaking the tie at the bottom.

The SPSE condition quantifies over the set of all SPE outcomes of each subgame, so neither half can be checked by looking at one profile: both existence and uniqueness require knowing that the all-minimum outcome lies in that set at the relevant histories.

Formalization scope

All quantities are real numbers; there is no probability. Contractors are indexed by Fin M and periods are 0-based (pathHist σ n is the history before the paper's period $n+1$ ). A history is a List (Fin M → ℝ) and strategies are arbitrary functions of the history: under feedback every past effort is observed, and restricting to state-dependent or open-loop strategies would change the set of SPEs that the definition compares against.

Committed conventions:

the standing assumptions $1 \le M$ , $1 \le N$ , $0 \le \underline q < q^* < \bar q$ , $p, \gamma, c > 0$ are explicit hypotheses; $\gamma p > c$ is not assumed;
$N \le M-1$ is written N + 1 ≤ M;
(24) is stated with final level vectors rather than the totals of periods $n$ to $N$ (a bijection once the history is fixed), its "min" as an infimum and its " $=$ arg max" as membership in the argmax;
(24) is imposed only at the SPSE's own on-path histories, as Definition 2 says ("with the state of period $n$ , $\hat{\mathbf q}^\dagger_{n-1}$ ");
"unique SPSE" is stated as "every SPSE has the all-minimum path"; the off-path part of an SPSE is never unique.

Trivializing encodings are ruled out: the SPSE carries the SPE clause, the condition is neither dropped nor imposed at every history (under which no SPSE would exist), and the goal includes an existence conjunct, so it cannot hold vacuously.

The development needs the game, its SPE and SPSE (one definition file in the mission), and arguments about backward induction in a finite-horizon game with continuous actions. Proofs of the milestones, of the goal, and reusable lemmas about cumulative-effort games are all welcome.

Selected references

W. Zhang, S. Shokoohyar, A. Qi, E. Katok, Coordination for Assembly, Manufacturing & Service Operations Management, 2025. doi:10.1287/msom.2023.0342 (cited from the authors' manuscript of 10 July 2025).
J. B. Van Huyck, R. C. Battalio, R. O. Beil, Tacit Coordination Games, Strategic Uncertainty, and Coordination Failure, American Economic Review 80(1), 1990, 234–248.

5 thms1 active userReviewed

Algorithmic Game Theory Linear Optimization Mechanism Design+1·Captain: mikedeng1

Spatio-Temporal Pricing for Ridesharing Platforms: The STP Mechanism Is Subgame-Perfect Incentive Compatible, Welfare-Optimal, Envy-Free and Core-Selecting from Any HistoryResearch Paper

Motivation

Ridesharing platforms set prices and dispatch drivers over a road network whose demand changes within minutes: a stadium empties, rush hour starts, a neighbourhood goes quiet. Drivers are not employees. They may decline a dispatch, drive somewhere else, or stop working, and the platform pays no one in advance for staying in place. Prices that look only at the current moment (myopic pricing) jump sharply in space and time and reward drivers who wait for a surge instead of taking the dispatch they are given (Ma, Fang, Parkes 2022, §2).

H. Ma, F. Fang and D. C. Parkes ask for a dynamic mechanism under which following the platform's dispatches is in every driver's interest at every moment, including after other drivers have deviated, while the outcome stays efficient and fair. Their answer, the spatio-temporal pricing (STP) mechanism, was published in Operations Research in 2022 and builds on the competitive-equilibrium theory of assignment and flow markets (Shapley and Shubik 1971; Murota 2003).

Setting

Time runs over $t = 0, 1, \dots, T$ . There is a finite set $\mathcal L$ of locations and travel times $\delta(a,b) \ge 1$ with $\delta(a,a) = 1$ . A trip $(a,b,t)$ leaves $a$ at time $t$ and arrives at $b$ at time $t + \delta(a,b)$ ; it costs the driver $c_{a,b,t} \ge 0$ , and the trips that end by $T$ form the set $\mathcal T$ . A driver who stops working $\Delta$ periods before $T$ pays $\kappa_\Delta \ge 0$ , with $\kappa_0 = 0$ .

Each driver $i$ has a type $(\beta_i, \ell_i, \tau_i)$ : she can start at location $\ell_i$ at time $\tau_i$ , and $\beta_i = 1$ if she is already working, $\beta_i = 0$ if she still decides whether to enter (not entering costs nothing). Each rider $j$ asks for the single trip $(o_j, d_j, \tau_j) \in \mathcal T$ and values it at $v_j \ge 0$ . A path of driver $i$ is a chain of trips starting at $(\ell_i,\tau_i)$ ; its cost $\lambda$ is the sum of its trip costs plus the early-exit cost at its end. A dispatching assigns each driver a path and each picked-up rider to a driver whose path covers her trip; its welfare is the value of the riders picked up minus the drivers' costs, and $W(\mathcal D, \mathcal R)$ is the largest welfare over all dispatchings.

Anonymous trip prices $p_{a,b,t}$ charge every picked-up rider the price of her trip and pay it to the driver who carries her. Together with a dispatching they form a competitive equilibrium (CE) when every rider who values her trip above its price is picked up, nobody pays more than her value, and every driver's utility is the best that any of her paths could earn at these prices. The welfare gain from an additional driver at $(a,t)$ is

\Phi_{a,t} = W(\mathcal D \cup \{(1,a,t)\}) - W(\mathcal D).

The STP mechanism computes a welfare-optimal dispatching, dispatches every available driver along it, and prices every trip by

p_{a,b,t} = \Phi_{a,t} - \Phi_{b,\,t+\delta(a,b)} + c_{a,b,t}.

It recomputes the dispatching and the prices on the remaining economy $E^{(t)}(s_t)$ whenever some driver has deviated at time $t-1$ . A driver who declines a dispatch is paid nothing in that period and pays no penalty.

Formalization targets

Goal: Theorem 2

For every rule that picks a welfare-optimal dispatching, the STP mechanism

is temporally consistent: after a deviation, the new plan is the plan the mechanism would compute at time $0$ for the remaining economy;
is subgame-perfect incentive compatible (SPIC): from every history, no driver gains from any strategy while the others follow the dispatches,

\sum_{t'=t}^{T-1} \hat\pi_{i,t'}(\sigma^*_i|_{h_t}, \sigma^*_{-i}|_{h_t}) \ \ge\ \sum_{t'=t}^{T-1} \hat\pi_{i,t'}(\sigma_i|_{h_t}, \sigma^*_{-i}|_{h_t});

is individually rational for riders and strictly budget balanced for every strategy profile;
produces, from every history onward, an outcome that is welfare-optimal, in the core, envy-free for drivers and riders, and individually rational for drivers.

Milestones

The static theory of §3 comes first: Lemma 1 (non-negative prices), Lemma 6 (relocation trips have non-positive price), Lemma 2 (integrality of the LP relaxation), Lemma 3 (welfare theorem), Lemma 7 (correspondence of the two dual LPs), Lemma 4 (CE driver utilities form a lattice with bottom $\Phi_{D_i}$ and top $\Psi_{D_i}$ ) and Lemma 5 (core equivalence). The proof of Theorem 2 then contributes:

Step 1: the STP prices make every welfare-optimal plan a CE in which driver $i$ earns $\Phi_{D_i}$ ;
its consequence, a driver's continuation utility under the current plan;
the three inequalities (i)–(iii) of Step 2 between replica gains $\Phi^{(t)}_{a,t}(s_t)$ of successive time-shifted economies.

Significance

Theorem 2 shows that a platform can align incentives without long-term contracts, penalties or the threat of firing: the deviating driver's payoff is computed from a re-planned economy, and the replica-gain prices make that payoff no larger than the payoff of following the dispatch. The paper also proves that no mechanism with these properties makes following the dispatch a dominant-strategy equilibrium (Theorem 3), so subgame perfection is the right notion here.

The result is proved in the paper; it has not been formalized. A search of the Prove2Me library found no machine-checked statement of a dynamic ridesharing mechanism, of the CE lattice of a path economy, or of the replica-gain characterization of the driver-pessimal CE. A complete development would give a checked welfare theorem and core equivalence for a flow-based market, a lattice of CE utilities identified with marginal welfare gains, and a subgame-perfection argument for a re-planning mechanism.

Difficulty

The static part reduces to linear programming over paths, whose number grows exponentially with $|\mathcal L|$ and $T$ . Integrality and the lattice structure come from a translation to a minimum-cost flow problem and its dual, which has to be set up and connected back to paths.

The dynamic part is harder. A naive argument would compare a deviating driver's payoff against prices fixed at time $0$ , but STP re-plans after the deviation: the deviator's later payments come from a different economy, computed with different prices. Recomputing a driver-pessimal CE at every step breaks incentive compatibility (Example 3). STP is incentive compatible only because of an exchange inequality between replica gains (part (iii)). It says that adding a driver at the node a deviator drives to lowers the marginal value of another driver there at least as much as the deviator's planned position does. This is a local exchange property of M♮-concave functions, the optimal values of flow problems (Murota 2016), and has no counterpart in Mathlib.

Formalization scope

Lean represents an economy by a finite type of locations, drivers indexed by a finite type ι, riders indexed by a finite type κ, times in ℕ with explicit ≤ T guards, and money in ℝ. The replica of a driver is the index none of Option ι, removal is the subtype {k // k ≠ i}, and a coalition is a pair of subsets. W is the supremum of the welfares of feasible integral dispatchings, a finite nonempty set for every valid economy.

The conventions that the formalization commits to:

Under assumption (S1) every driver stays until $T$ , so the exit time $\bar\tau_i$ is dropped and the replica in $\Phi_{a,t}$ is the type $(1,a,t)$ .
Every requested trip lies in $\mathcal T$ , part of a valid economy.
A blocking coalition must use a budget-balanced plan among its members.
In the time-shifted economy, an available driver who has not entered keeps $\beta = 0$ . This corrects a slip on p. 20, and the proof uses it.
Definitions 8–10 bundle SPIC as condition (i). Here SPIC is stated once and the other properties state their condition (ii).
Rider envy-freeness (26) is read from the history $h_{\tau_j}$ .
Theorem 2 is claimed for every selector of welfare-optimal dispatchings, since Definition 12 leaves the choice of optimum open.

The goal must not be trivialized. It is not satisfied by some unspecified mechanism, by SPIC only at time $0$ , by SPIC only against one-shot deviations along the equilibrium path, or by one fixed selector. Temporal consistency compares the mechanism's plan after a deviation with its own time- $0$ plan of a different economy, so it is not a comparison of STP with itself.

A complete development needs:

path enumeration and the reduction to minimum-cost flow;
LP duality and complementary slackness for the flow problem;
integrality of flows;
the M♮-concavity of flow values;
a principle of optimality for continuations of optimal plans.

The CE, core and lattice layers do not depend on ridesharing. Contributions to any milestone, or to these general tools, are welcome.

Selected references

H. Ma, F. Fang, D. C. Parkes, Spatio-Temporal Pricing for Ridesharing Platforms, Operations Research, 2022; read here as arXiv:1801.04015v5, 2021. https://arxiv.org/abs/1801.04015v5
L. S. Shapley, M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971. https://doi.org/10.1007/BF01753437
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
K. Murota, Discrete convex analysis: A tool for economics and game theory, Journal of Mechanism and Institution Design 1(1), 2016. https://doi.org/10.22574/jmid.2016.12.005
M. J. Osborne, A. Rubinstein, A Course in Game Theory, MIT Press, 1994.

16 thms1 active userReviewed

Algorithmic Game Theory Machine Learning Optimization·Captain: mikedeng1

Greedy Adversarial Equilibrium: An Efficient Alternative to Nonconvex–Nonconcave Min-Max Optimization: Every Bounded Function with Lipschitz Hessian Has a Greedy Adversarial EquilibriumResearch Paper

Motivation

Min-max problems $\min_x\max_y f(x,y)$ model two-player zero-sum games and appear across machine learning and operations research: adversarial training of classifiers, generative adversarial networks, and robust optimization against an adversarial perturbation. When $f$ is convex in $x$ and concave in $y$ , von Neumann's minimax theorem gives a saddle point, and first-order methods find approximate ones. In the nonconvex–nonconcave case, which is the case of every neural-network objective, a global min-max point is intractable to find, and local notions such as local min-max points or local Nash equilibria need not exist at all (Jin, Netrapalli and Jordan, ICML 2020; Daskalakis, Skoulakis and Zampetakis, STOC 2021). Without existence there is nothing for an algorithm to converge to.

Mangoubi and Vishnoi propose an equilibrium notion that exists for every smooth bounded objective and can be computed in time polynomial in the dimension and the accuracy (arXiv:2006.12363). The max-player is modelled as an adversary that can only improve $f$ by local, "greedy" moves, and the min-player minimizes the value the adversary can reach this way.

Setting

Write $\mathbb R^d$ for each player's strategy space, with the Euclidean norm, and give $\mathbb R^d\times\mathbb R^d$ the norm $\sqrt{\|x\|^2+\|y\|^2}$ . Throughout, $f:\mathbb R^d\times\mathbb R^d\to\mathbb R$ is $C^2$ , $b$ -bounded ( $|f(x,y)|\le b$ ) and has an $L$ -Lipschitz Hessian, $\|\nabla^2f(x,y)-\nabla^2f(\tilde x,\tilde y)\|_{\mathrm{op}}\le L\sqrt{\|x-\tilde x\|^2+\|y-\tilde y\|^2}$ .

A point $y$ is an $(\varepsilon,\sqrt{L\varepsilon})$ -approximate local maximum of $f(x,\cdot)$ if $\|\nabla_yf(x,y)\|\le\varepsilon$ and $\lambda_{\max}(\nabla_y^2f(x,y))\le\sqrt{L\varepsilon}$ .

An $\varepsilon$ -greedy path for $f(x,\cdot)$ is a continuous path $\varphi:[0,\tau]\to\mathbb R^d$ , differentiable at all but finitely many points, travelling at unit speed, along which $\frac{d}{dt}f(x,\varphi_t)\ge-\varepsilon$ and, at every point, either $f$ increases at rate more than $\varepsilon$ or its second derivative in the direction of travel exceeds $\sqrt{L\varepsilon}$ . Let $S_{\varepsilon,x,y}$ be the set of endpoints of $\varepsilon$ -greedy paths starting at $y$ . The greedy max is

g_\varepsilon(x,y)=\sup\{f(x,z):z\in S_{\varepsilon,x,y}\}.

The greedy max is in general discontinuous in $x$ , so the min-player's stationarity is defined after truncation and Gaussian smoothing. For a bounded $\psi$ , a point $x^\star$ is an $(\varepsilon,\sigma)$ -approximate local minimum of $\psi$ if

\mathcal S(x)=\mathbb E_{\zeta\sim N(0,I_d)}\big[\min(\psi(x+\sigma\zeta),\psi(x^\star))\big]

satisfies $\|\nabla\mathcal S(x^\star)\|\le\varepsilon$ and $\lambda_{\min}(\nabla^2\mathcal S(x^\star))\ge-\sqrt\varepsilon$ .

A pair $(x^\star,y^\star)$ is an $(\varepsilon,\sigma)$ -greedy adversarial equilibrium if $y^\star$ is an $(\varepsilon,\sqrt{L\varepsilon})$ -approximate local maximum of $f(x^\star,\cdot)$ and $x^\star$ is an $(\varepsilon,\sigma)$ -approximate local minimum of $g_\varepsilon(\cdot,y^\star)$ .

Formalization targets

Goal: existence (Theorem 3.1, first two sentences, p. 10)

For every $d\ge1$ , $\varepsilon,\sigma>0$ with $\sigma\le1/\sqrt{\varepsilon d}$ , and every $f$ as above,

\exists\,\varepsilon^\star\in(0,\varepsilon]\ \ \exists\,(x^\star,y^\star):\quad (x^\star,y^\star)\text{ is an }(\varepsilon^\star,\sigma)\text{-greedy adversarial equilibrium of }f.

The accuracy $\varepsilon^\star$ is not fixed in advance; the theorem asserts that some accuracy at least as fine as $\varepsilon$ is attained.

Milestones

Lemma 7.2 (24)–(25): the output $y_{\mathrm{LocalMax}}$ of the greedy-path subroutine (Algorithm 1) satisfies $\|\nabla_yf\|\le\varepsilon'$ and $\lambda_{\max}(\nabla_y^2f)\le\sqrt{L\varepsilon'}+\mu_4$ .
Proposition 7.4: the polygonal path traced by Algorithm 1 is a $\frac1{1+\delta}\varepsilon'$ -greedy path.
Proposition 7.5: the computable lower bound $h_{\varepsilon^\circ}(x,y)=f(x,y_{\mathrm{LocalMax}})$ satisfies $h_{\varepsilon^\circ}\le g_{\varepsilon^\circ}$ .
Proposition 7.7: the zeroth-order estimator $\hat\Gamma=[\mathbb h(x+\sigma u)-c]\frac1\sigma u$ is unbiased for $\nabla_x\mathfrak h$ and has a sub-Gaussian tail.
Lemma 7.3: if $h_\varepsilon$ is a lower bound for $g_\varepsilon$ that agrees with it at $(x^\star,y^\star)$ , and the smoothed truncated $h_\varepsilon$ is very nearly second-order stationary at $x^\star$ with a small stochastic gradient, then $x^\star$ is an $(\varepsilon,\sigma)$ -approximate local minimum of $g_\varepsilon(\cdot,y^\star)$ .

Significance

The theorem gives the first equilibrium notion for nonconvex–nonconcave min-max optimization that is both guaranteed to exist for every $C^2$ bounded objective with Lipschitz Hessian and computable with polynomially many gradient, Hessian and function evaluations. It requires no convexity, monotonicity, bilinearity or initialization near an equilibrium. At an equilibrium, neither player can improve by a local move of the kind second-order methods make: the max-player cannot climb by a greedy path, and the min-player cannot decrease the value the adversary will reach. Appendix A of the paper shows that in the strongly convex–strongly concave case the duality gap at such a point is small, so the notion refines the classical saddle point.

The result is proved on paper and has not been machine-checked. A formalization adds three things beyond the paper. First, a verified calculus of second-order approximate stationarity for discontinuous functions through truncated Gaussian smoothing, reusable for other nonsmooth objectives. Second, a precise account of the paper's conventions: Definition 2.1's second derivative has to be read directionally, (25) holds only with an added $\mu_4$ , and Lemma 7.3 holds only for $\sigma,\varepsilon\le1$ , as its proof requires. Third, it settles whether the existence statement holds for every $\sigma\le1/\sqrt{\varepsilon d}$ , including $\sigma>1$ , which the printed proof does not cover.

Difficulty

The obvious approach is to minimize $x\mapsto\max_zf(x,z)$ , but that function is intractable to evaluate and need not have approximate local minima reachable by local moves. The greedy max $g_\varepsilon$ replaces it, but $g_\varepsilon$ is a supremum over an uncountable family of paths, cannot be computed exactly, and jumps as $x$ moves: Example 2.4 shows a smooth $f$ whose greedy max is discontinuous. Convolution with a Gaussian restores smoothness but moves local minima (Example 5.5), which is why the definition truncates at $\psi(x^\star)$ before smoothing. The central difficulty is to obtain second-order information about the smoothed truncated $g_\varepsilon$ while only ever evaluating a computable lower bound $h_\varepsilon$ ; Lemma 7.3 is the step that transfers stationarity from one to the other, and its constants are tight enough that the transfer fails if any hypothesis is weakened.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and the joint variable lives in WithLp 2 (ℝᵈ × ℝᵈ), so that the Lipschitz-Hessian condition uses the paper's Euclidean norm rather than Lean's sup norm on products. Eigenvalue bounds are quadratic-form bounds on the second Fréchet derivative. Expectations over $N(0,I_d)$ are integrals against stdGaussian, and Gaussian smoothing is the published definition RandomGradFree.Shared.smoothing.

Conventions and readings, each disclosed in the item it affects:

Definition 2.1 is read with the second derivative of $f(x,\cdot)$ along the direction of travel, $\dot\varphi^\top\nabla_y^2f\,\dot\varphi$ , as the paper's proofs use it; "points of differentiability" are interior points.
$d\ge1$ is added to every statement involving $\sqrt d$ or $1/\sqrt{\varepsilon d}$ .
Definition 2.3 requires the Gaussian integrand to be integrable and asserts the first and second derivatives of $\mathcal S$ before bounding them.
Algorithm 1 takes an eigen-oracle with $\lambda\ge\lambda_{\max}-\mu_4$ and its hyperparameters $\delta,\mu_1,\mu_3,\mu_4$ as parameters; each milestone assumes exactly the step-size inequalities its proof uses, with $L_2$ a Lipschitz constant of $\nabla f$ .
Lemma 7.2's (25) carries $+\mu_4$ , as in the proof's (29).
Lemma 7.3 carries $\sigma\le1$ , $\varepsilon\le1$ and $b\ge1$ , which its proof uses; the printed form fails for $\sigma>1$ .

The goal cannot be satisfied through Lean's junk values: a non-integrable truncated greedy max would make $\mathcal S\equiv0$ , and fderiv of a non-differentiable function is $0$ , so Definition 2.3 demands integrability and asserted derivatives, and the supremum defining $g_\varepsilon$ ranges over a set that contains $y$ and is bounded by $b$ .

Not formalized: the algorithmic sentences of Theorem 3.1 (success probability $9/10$ , polynomial oracle complexity), Algorithm 2 and the milestones about its randomized run (Lemma 7.1, Lemma 7.2 (26)–(27), Propositions 7.6, 7.8–7.10), Lemma 5.1, Corollary 5.2, Appendix A and Appendix B. Algorithm 2 and Propositions 7.8–7.10 are natural follow-up contributions, as is the strongly convex–strongly concave duality-gap bound (Theorem A.1), which reuses this mission's definitions. A complete development needs Gaussian integration by parts in $\mathbb R^d$ , differentiation under the integral for Gaussian convolutions of bounded measurable functions, and concentration of $\|\zeta\|$ for $\zeta\sim N(0,I_d)$ ; all three are reusable beyond this mission.

Selected references

O. Mangoubi, N. K. Vishnoi, Greedy Adversarial Equilibrium: An Efficient Alternative to Nonconvex–Nonconcave Min-Max Optimization, Mathematics of Operations Research, 2025; read as arXiv:2006.12363v4, 2021. https://arxiv.org/abs/2006.12363
C. Jin, P. Netrapalli, M. I. Jordan, What is Local Optimality in Nonconvex–Nonconcave Minimax Optimization?, ICML 2020. https://arxiv.org/abs/1902.00618
C. Daskalakis, S. Skoulakis, M. Zampetakis, The Complexity of Constrained Min-Max Optimization, STOC 2021. https://arxiv.org/abs/2009.09623
Y. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming 108, 2006. https://doi.org/10.1007/s10107-006-0706-8
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2

9 thms1 active userReviewed

Control Theory Dynamic Programming Operations Research·Captain: mikedeng1

Driving Supply to Marketplaces: Optimal Platform Pricing When Suppliers Share Inventory: The Supplier Shares Its n-th Unit Exactly When the Time-to-Go Is at Most a Threshold tₙResearch Paper

Motivation

Online marketplaces such as Zalando, Amazon or Farfetch let brands sell through the platform's storefront in addition to their own stores. One common arrangement is inventory sharing: the brand keeps ownership of its stock, but makes it visible to the platform's customers, and pays the platform a commission on every unit the platform sells. For a supplier with a fixed stock and a finite selling season, this creates a timing question. Sharing brings more customers, but each platform sale earns less than a direct one. Early in the season there is plenty of time to sell the stock at full margin; late in the season unsold units are worth nothing.

Martínez-de-Albéniz, Pinto and Amorim (SSRN 3643261, 2020; published in Manufacturing & Service Operations Management, 2022) model this problem as a continuous-time optimal control problem with Poisson demand, solve the supplier's problem, and use the solution to study how the platform should set its commission. The supplier's problem is a binary-control relative of the dynamic pricing problem of Gallego and van Ryzin (Management Science 1994): sharing switches the effective price and the demand rate between two values. Its solution is the building block for the paper's platform-pricing results.

Setting

A supplier sells a single item during a season. Time is measured as the time-to-go $t \ge 0$ until the end of the season ( $t = 0$ at the end). The item sells at the price $\pi > 0$ . Customers of the supplier's own (direct) channel arrive as a Poisson process of rate $\lambda_D > 0$ ; customers of the platform arrive at rate $\lambda_P > 0$ . On a direct sale the supplier earns $\pi$ ; on a platform sale it keeps $(1-\theta)\pi$ , where $\theta \in [0,1]$ is the commission. Revenue is discounted at rate $r \ge 0$ , and leftover units are worth nothing.

At every moment the supplier chooses $z \in \{0,1\}$ : $z = 1$ shares the inventory with the platform, $z = 0$ does not. Write $V_n(t)$ for the revenue-to-go with $n$ units left and time-to-go $t$ , and $\Delta V_n(t) = V_n(t) - V_{n-1}(t)$ for the marginal revenue-to-go of the $n$ -th unit. The revenue-to-go solves the Hamilton–Jacobi–Bellman equation (3)

\frac{dV_n}{dt} = \sup_{z\in\{0,1\}}\Bigl[\bigl(\pi\lambda_D + z(1-\theta)\pi\lambda_P\bigr) - (\lambda_D + z\lambda_P)\,\Delta V_n(t) - rV_n(t)\Bigr], \qquad n \ge 1,

with $V_0 \equiv 0$ and $V_n(0) = 0$ . A decision is optimal for unit $n$ at time $t$ if it attains this supremum. The threshold of unit $n$ is

t_n = \sup\{t \ge 0 : \Delta V_n(t) \le (1-\theta)\pi\} \in [0, \infty], \qquad t_0 = 0,

which is $\infty$ when $\Delta V_n$ never exceeds the platform margin $(1-\theta)\pi$ . In Lean these objects are Params, hamiltonian, hjbRHS, IsRevenueToGo, marginal, IsOptimalDecision and threshold in the namespace MarketplaceSharing.Threshold.

Formalization targets

Goal: Theorem 1 (p. 9)

For every revenue-to-go $V$ and every $n \ge 1$ :

\Delta V_n \text{ is strictly increasing on } [0,\infty), \qquad \Delta V_n(t) = (1-\theta)\pi \iff t = t_n,

z = 1 \text{ is optimal at } (t, n) \iff t \le t_n, \qquad t > t_n \implies z = 0 \text{ is optimal and } z = 1 \text{ is not},

and on each interval $I_{nj} = [t_{j-1}, t_j]$ , $1 \le j \le n$ , and on $I_{n,n+1} = [t_n, \infty)$ , there are constants with

V_n(t) = C_{nj} + \sum_{i=0}^{n-j} A_{nji}\,t^i e^{-(\lambda_D+\lambda_P+r)t} + \sum_{i=0}^{j-2} B_{nji}\,t^i e^{-(\lambda_D+r)t}. \tag{4}

The coefficients are existential, as on the page; their recursions are not part of the goal.

Milestones

In attack order: well-posedness of (3) (a solution exists and is unique on $[0,\infty)$ ); the sharing condition of p. 8, $z = 1$ optimal $\iff \Delta V_n(t) \le (1-\theta)\pi$ ; Lemma 1, $V_{n+1} \ge V_n$ ; Lemma 2, $\Delta V_{n+1} \le \Delta V_n$ ; Lemma 3, $V_n$ nondecreasing in $t$ ; Lemma 4, $\Delta V_n$ nondecreasing in $t$ ; the explicit $t_1$ of footnote 4 (at $r = 0$ ); the first bullet of Theorem 1; and Corollary 1, $t_{n+1} \ge t_n$ .

Significance

Theorem 1 reduces the supplier's policy, a function of time and stock, to one number per unit: share the $n$ -th remaining unit exactly when the time-to-go is at most $t_n$ . Corollary 1 orders these numbers, so the season splits into an early period of direct-only sales and a late period of sharing, which begins earlier the more stock is left. The closed form (4) makes $V_n$ and the thresholds computable. The paper's analysis of the platform's commission (Theorems 2 and 3) takes this policy as the supplier's best response.

The results are proved in the paper, by an induction on $n$ that runs through Lemmas 1–4. None of it has a machine-checked proof. A formalization produces a checked proof of a threshold structure for a two-mode Poisson control problem, a checked statement of where the printed text needs correcting (see below), and reusable pieces: well-posedness of a recursive system of Lipschitz ODEs and comparison arguments for HJB equations of this type.

Difficulty

The HJB system (3) is a recursive family of ODEs whose right-hand side switches between two affine laws according to the sign of $(1-\theta)\pi - \Delta V_n(t)$ . The monotonicity statements are comparison results for such switched systems: the obvious argument (differentiate $\Delta V_n$ and read off the sign) gives an equation for $\Delta V_n'$ that involves $\Delta V_{n-1}'$ and the switching times of both units, so monotonicity in $t$ and in $n$ have to be established together, unit by unit. The closed form (4) then needs the switching times of all lower units to be ordered (Corollary 1) before the ODE on each interval has constant decisions, and the polynomial factors $t^i$ come from repeated resonance of the exponential $e^{-(\lambda_D+\lambda_P+r)t}$ across units.

Formalization scope

The paper defines $V_n$ by a stochastic control problem (2) over Poisson sales processes and derives (3) informally. The mission works with (3) only: the revenue-to-go is any family $V : \mathbb{N} \to \mathbb{R} \to \mathbb{R}$ satisfying IsRevenueToGo ( $V_0 = 0$ on $[0,\infty)$ , $V_n(0) = 0$ , and the HJB equation for $n \ge 1$ as a derivative within $[0,\infty)$ , one-sided at $0$ ), and every theorem takes this as a hypothesis. The well-posedness milestone shows such a family exists and is unique on $[0,\infty)$ , so no theorem is vacuous. Values at $t < 0$ are unconstrained. Decisions are Booleans (true = share).

Conventions and added hypotheses: $\pi > 0$ , $\lambda_D > 0$ , $\lambda_P > 0$ and $r \ge 0$ are standing hypotheses (with $\lambda_P = 0$ or $\pi = 0$ the two decisions tie everywhere and the threshold statement fails); $\theta \in [0,1]$ is printed. The paper's range $n \in \{1,\dots,N\}$ is read as $n \ge 1$ , since $V_n$ does not depend on $N$ . The threshold lives in the extended reals with $t_n = \infty$ when $\Delta V_n = (1-\theta)\pi$ has no solution (p. 10); the literal "there is an unique $t_n$ " fails for instance at $\theta = 0$ . Three printed formulas are corrected and disclosed: the exponents of (4) carry $r$ , as the proof on p. 30 does (the printed form is exact only at $r = 0$ ); Lemma 4 is stated in the direction of its words and proof, $\Delta V_n(t_1) \le \Delta V_n(t_2)$ for $t_2 \ge t_1 > 0$ (the printed display is reversed); and the $t_1$ formula of footnote 4 is stated at $r = 0$ (with $\theta > 0$ ), the only case in which it is exact.

The encoding rules out the trivializing readings: "optimal" is attainment of the supremum in (3), not membership in $[0, t_n]$ ; $t_n$ is the supremum of a sublevel set that always contains $0$ , not a solution of $\Delta V_n = (1-\theta)\pi$ that could make uniqueness definitional; monotonicity of $\Delta V_n$ is a conclusion of the goal, never a hypothesis; and the hypothesis IsRevenueToGo is satisfiable by the well-posedness milestone.

Not formalized: the stochastic formulation (2) and its identification with (3); the recursions for $A_{nji}$ , $B_{nji}$ , $C_{nj}$ (pp. 31–32); the numerical study of §3.3; and the platform-pricing results (Theorems 2 and 3, §4) and §5. A complete development needs one-dimensional ODE existence and uniqueness (Picard–Lindelöf and Grönwall, available in Mathlib), comparison of solutions of scalar ODEs, and calculus with $t^i e^{-ct}$ . Proofs of any milestone, and reusable comparison lemmas for switched affine ODEs, are welcome.

Selected references

V. Martínez-de-Albéniz, C. Pinto, P. Amorim, Driving Supply to Marketplaces: Optimal Platform Pricing When Suppliers Share Inventory, SSRN 3643261, version of June 30, 2020; Manufacturing & Service Operations Management, 2022. https://ssrn.com/abstract=3643261
G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
V. Martínez-de-Albéniz, K. Talluri, Dynamic Price Competition with Fixed Capacities, Management Science 57(6), 1078–1093, 2011. https://doi.org/10.1287/mnsc.1110.1337

11 thms1 active userReviewed

Operations Research Optimization Probability·Captain: mikedeng1

On Policies for Single-Leg Revenue Management with Limited Demand Information: the Valuation Tracking Pricing Policy Is c*(P)-CompetitiveResearch Paper

Motivation

Single-leg revenue management asks how a seller holding $k$ units of a perishable item (seats on one flight leg, rooms for one night) should price or ration them to customers who arrive one at a time. The classical theory assumes a demand forecast. When no forecast is available, a standard robust criterion is competitiveness: an online policy is $c$ -competitive if, on every arrival sequence, its expected revenue is at least $c$ times the revenue of an offline optimum that knows the whole sequence in advance.

Two earlier lines of work found the best possible constant $c^*(\mathcal P)$ for a discrete price set $\mathcal P$ , each in a model that gives the seller more power than posted pricing. Ball and Queyranne (2009) studied booking limits: customers arrive with a fare class that the seller observes before accepting or rejecting. Eren and Maglaras (2010) studied price skimming with a known number of customers. Both show that no online algorithm can be more than $c^*(\mathcal P)$ -competitive. Ma, Simchi-Levi and Teo (arXiv:1810.10900v2; Operations Research 2021) ask whether the same ratio is achievable by dynamic posted pricing, where the seller commits to a price before seeing the customer's valuation and does not know the horizon. Their answer is yes, through a randomized policy built on a new valuation tracking subroutine.

Setting

Fix $m\ge1$ prices $0<r^{(1)}<\dots<r^{(m)}$ and set $r^{(0)}=0$ (no customer) and $r^{(m+1)}=\infty$ (shutting off demand). The firm holds $k\ge1$ units. Customers $t=1,\dots,T$ arrive in order; $T$ is unknown to the firm. Customer $t$ has a deterministic valuation $V_t=r^{(j_t)}$ , $j_t\in\{0,\dots,m\}$ , chosen by an adversary. Before seeing $V_t$ , the firm posts a price $P_t\in\{r^{(1)},\dots,r^{(m+1)}\}$ that may depend only on $V_1,\dots,V_{t-1}$ and the past prices; the customer buys ( $X_t=1$ ) iff $V_t\ge P_t$ . The revenue is $\mathsf{ALG}=\sum_{t=1}^T P_tX_t$ . The offline optimum $\mathrm{OPT}$ is the sum of the $\min\{k,T\}$ largest valuations. An online algorithm is $c$ -competitive if

\mathbb E[\mathsf{ALG}(V_1,\dots,V_T)]\ \ge\ c\cdot \mathrm{OPT}(V_1,\dots,V_T)\qquad\text{for all }T\ge1,\ (V_1,\dots,V_T)\in(\mathcal P\cup\{0\})^T .

Definition 1 sets $q^{(j)}=1-r^{(j-1)}/r^{(j)}$ for $j\in[m]$ , $q=\sum_{j=1}^m q^{(j)}$ and $c^*(\mathcal P)=1/q$ .

Algorithm 1 (valuation tracking). Each unit $i$ carries a level $\ell_{i}\in\{0,\dots,m\}$ (initially $0$ ) and a flag $\mathtt{sold}[i]$ (initially false). Customer $t$ is assigned to a unit $i_t$ of minimal level; let $\ell=\ell_{i_t}$ . If $\mathtt{sold}[i_t]$ is false, the algorithm posts $r^{(p)}$ , $\ell<p\le m$ , with probability $q^{(p)}/\sum_{j=\ell+1}^m q^{(j)}$ ; otherwise it posts $\infty$ . After observing $V_t$ it sets $\ell_{i_t}\leftarrow\max\{\ell,j_t\}$ and marks $i_t$ sold if a sale occurred. The levels $\ell_{i,t}$ and the assignments $i_t$ are deterministic functions of the valuations; only the sold vector $(S_{1,t},\dots,S_{k,t})$ is random.

Formalization targets

Goal: Theorem 1 (p. 14)

\mathbb E[\mathsf{ALG}(V_1,\dots,V_T)]\ \ge\ \frac1q\,\mathrm{OPT}(V_1,\dots,V_T)\quad\text{for every valuation sequence},

i.e. Algorithm 1 is $c^*(\mathcal P)$ -competitive, for every price grid, every inventory $k$ , and every minimal-level tie-break.

Milestones (Appendix B, pp. ec1–ec5)

The remark of §3.3 (p. 13): a unit at level $m$ is sold with probability $1$ , so line 8 is never reached with $\ell_t=m$ .
Lemma EC.1: $\mathbb E[S_{i,t}]=\frac1q\sum_{j=1}^{\ell_{i,t}}q^{(j)}$ .
Lemma EC.2: if $j_t>\ell_{i_t,t-1}$ then $\mathbb E[P_tX_t]=\frac1q\bigl(r^{(j_t)}-r^{(\ell_{i_t,t-1})}\bigr)$ , and $\mathbb E[P_tX_t]=0$ otherwise.
Lemma EC.3: $\sum_{t'=1}^t\mathbb E[P_{t'}X_{t'}]=\frac1q\sum_{i=1}^k r^{(\ell_{i,t})}$ .
$\mathrm{OPT}=\sum_{i=1}^k M^k_i(T)$ , where $M^k(t)$ lists the $k$ largest of $V_1,\dots,V_t$ padded with zeros (Definition EC.2).
Lemma EC.4: $(r^{(\ell_{1,t})},\dots,r^{(\ell_{k,t})})$ is a permutation of $M^k(t)$ .
The closing display of the proof: $\mathrm{OPT}=\sum_{i=1}^k r^{(\ell_{i,T})}=q\cdot\mathbb E[\mathsf{ALG}]$ , the exact-ratio form of Theorem 1.

Significance

Theorem 1 shows that the competitive ratio of single-leg revenue management under public posted pricing with deterministic valuations equals $c^*(\mathcal P)$ , the same constant as for booking limits and for price skimming with a known horizon. The seller loses nothing, in the worst case, by committing to a price before seeing the customer and by not knowing $T$ . The paper builds on Theorem 1 directly: an inventory-state version of Algorithm 1 (Theorem 2), the structural monotonicity of its prices (Theorem 3), and the extension to stochastic valuations (Theorems 4 and 5) all start from it.

The result is proved in the paper. This mission produces a machine-checked version of the full argument of Appendix B: an explicit model of a randomized online pricing policy as a finite Markov chain on the sold vector, the probability invariant of Lemma EC.1, the per-step revenue identity, and the combinatorial fact that the levels of the algorithm track the $k$ largest valuations. None of these has a formal proof on the platform.

Difficulty

The obvious policies fail: booking limits implemented by price, or price skimming with an unknown horizon, lose a constant factor against a single high-value customer who arrives while the price is low (§3.1). The difficulty of Theorem 1 is that the algorithm must earn, in each step, exactly $1/q$ of the increase of $\mathrm{OPT}$ without seeing $V_t$ . In the formal proof the two hard parts are: maintaining Lemma EC.1 as an exact identity on the law of the sold vector (a statement about a distribution on $\{0,1\}^k$ pushed forward through a randomized transition), and Lemma EC.4, a permutation invariant between the level vector and a sorted, zero-padded list, which holds only because each customer is assigned to a unit of minimal level.

Formalization scope

Prices are a function $r:\mathbb N\to\mathbb R$ with hypotheses $r(0)=0$ and $r(j)<r(j+1)$ for $j<m$ ; values above $m$ are never used, and $r^{(m+1)}=\infty$ is encoded as "no offer".
Valuations are indices: a sequence is a list over $\{0,\dots,m\}$ . $T$ is the list length and is never read by the algorithm. Every theorem holds for every list, including the empty one; this is a strengthening of the paper's $T\ge1$ .
Units are $\mathrm{Fin}\,k$ with $k\ge1$ , $m\ge1$ .
Tie-break. Line 4's $\arg\min$ is a selector function on level vectors; theorems quantify over every selector that returns a unit of minimal level.
Randomness. The law of the sold vector is an explicit probability mass function on $\mathrm{Fin}\,k\to\mathrm{Bool}$ , built by one transition per customer. $\mathbb E[P_tX_t]$ is computed from the law after $t-1$ customers and from $V_t$ only, so the price is online. $\mathbb E[\mathsf{ALG}]=\sum_{t=1}^T\mathbb E[P_tX_t]$ .
Line 8. The printed last offer probability ℓt+1/q_tot is a typo; the definition uses $q^{(m)}/q_{\mathrm{tot}}$ , as the text and proofs do. At a unit of level $m$ the step is a rejection; milestone 1 shows this case never matters.
OPT is the offline maximum of $\sum_{t\in S}V_t$ over sets $S$ of at most $k$ customers; $M^k(t)$ is a sorted, zero-padded list.
$q>0$ is not assumed; it follows from $q^{(1)}=1$ .

A trivializing formalization is ruled out: $\mathbb E[\mathsf{ALG}]$ must be computed from the law of Algorithm 1's random prices and purchases, and $\mathrm{OPT}$ as the offline maximum. Defining either through the levels (e.g. $\mathbb E[\mathsf{ALG}]:=\frac1q\sum_i r^{(\ell_{i,T})}$ ) would make the goal true by definition.

The mission covers only Section 3: public pricing with deterministic valuations. The stochastic-valuation algorithms of Section 4 (Theorems 4–5), the continuous-price variant of §5.1, and the structural results (Theorems 2–3, Corollary 1) are not formalized. The finite-distribution machinery (pushing a mass function through a randomized transition, top- $k$ sums of lists) is reusable for other online-algorithm missions. Proofs of the milestones in any order are welcome; Lemma EC.4 is pure combinatorics and independent of the probabilistic milestones.

Selected references

W. Ma, D. Simchi-Levi, C.-P. Teo, On Policies for Single-Leg Revenue Management with Limited Demand Information, Operations Research, 2021; preprint arXiv:1810.10900v2, 2020 (the version cited throughout). https://arxiv.org/abs/1810.10900v2
M. O. Ball, M. Queyranne, Toward Robust Revenue Management: Competitive Analysis of Online Booking, Operations Research 57(4):950–963, 2009.
S. S. Eren, C. Maglaras, Monopoly Pricing with Limited Demand Information, Journal of Revenue and Pricing Management 9(1–2):23–48, 2010.

9 thms1 active userReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Portfolio Optimization Based on Almost Second-Degree Stochastic Dominance: Approximate ASSD Under a Discretization Scheme Implies ASSDResearch Paper

Motivation

Second-order stochastic dominance (SSD) is the standard ordering of risky prospects for risk-averse investors: a return $X$ dominates a return $Y$ by SSD when every investor with a nondecreasing concave utility weakly prefers $X$ . Portfolio models that require a chosen portfolio to dominate a benchmark by SSD go back to Dentcheva and Ruszczyński (2003) and are used to beat an index while controlling risk. The order is very demanding: many portfolios that almost every investor would prefer fail it because of a small violation in a tail. Leshno and Levy (2002) introduced almost stochastic dominance, which tolerates a violation that is small relative to the region where dominance holds; Tzeng, Huang and Shih (2013) refined the second-order version (ASSD); in the parametrization used here, $\tau$ -ASSD is tied to the risk-averse utilities whose second derivatives deviate by no more than a factor $\tau$ , and Luo and Tan (Decision Analysis, 2020) review the variants.

ASSD is hard to impose in an optimization model because its definition involves integrals of the lower partial moment over the (unknown) set where dominance fails. Luo, Chen and Jaillet (Management Science, 2025) replace these integrals by a closed-form quantity computed on a grid, define approximate ASSD (AASSD) from it, and prove that AASSD implies ASSD. The mission formalizes that implication.

Setting

There are $n$ base assets and $T$ scenarios. Scenario $t$ has probability $p_t$ , and asset $i$ returns $x_{i,t}\in[a,b]$ in it, where $a<b$ are real. A portfolio is a weight vector $\lambda$ in the simplex $\Lambda=\{\lambda\in\mathbb R^n:\sum_i\lambda_i=1,\ \lambda_i\ge0\}$ ; its return $X$ equals $X_t=\sum_i x_{i,t}\lambda_i$ in scenario $t$ . A benchmark $Y$ takes the value $b_{t'}\in[a,b]$ with probability $p_{t'}$ , $t'=1,\dots,T_b$ . Means and variances are the finite sums $\mathbb EX=\sum_tp_tX_t$ and $\mathrm{Var}(X)=\sum_tp_t(X_t-\mathbb EX)^2$ .

The first-order lower partial moments (LPMs) are

F^{(2)}_\lambda(z)=\sum_{t=1}^Tp_t\,(z-X_t)^+,\qquad G^{(2)}(z)=\sum_{t'=1}^{T_b}p_{t'}\,(z-b_{t'})^+ .

Let $S_2=\{t\in[a,b]:F^{(2)}_\lambda(t)>G^{(2)}(t)\}$ be the set where SSD of $X$ over $Y$ is violated and $\bar S_2=[a,b]\setminus S_2$ . For $\tau>1$ , $X$ dominates $Y$ by $\tau$ -ASSD when $\mathbb EX\ge\mathbb EY$ and

\tau\int_{S_2}\big(F^{(2)}_\lambda-G^{(2)}\big)\,dt\ \le\ \int_{\bar S_2}\big(G^{(2)}-F^{(2)}_\lambda\big)\,dt .

A discretization scheme is a grid $a=d_1<d_2<\dots<d_{T_D}=b$ that contains every benchmark value $b_{t'}$ . On each sub-interval $[d_s,d_{s+1}]$ , the approximate SSD violation $A_{D,s,\lambda}$ is the area where the chord of $F^{(2)}_\lambda$ between the grid points lies above $G^{(2)}$ , written in closed form in four cases from the four values $F^{(2)}_\lambda(d_s),F^{(2)}_\lambda(d_{s+1}),G^{(2)}(d_s),G^{(2)}(d_{s+1})$ . The chord itself is the interpolated LPM $\hat F^{(2)}_{D,\lambda}$ . Then $X$ dominates $Y$ by $\tau$ -AASSD under $D$ when $\mathbb EX\ge\mathbb EY$ and

2(\tau-1)\sum_{s=1}^{T_D-1}A_{D,s,\lambda}\ \le\ \mathrm{Var}(Y)+(b-\mathbb EY)^2-\mathrm{Var}(X)-(b-\mathbb EX)^2 .

The right-hand side and every $A_{D,s,\lambda}$ involve only moments and LPM values at grid points, so AASSD is a finite system of constraints in $\lambda$ .

In the paper's Example 1 (pp. 14–15), $X$ is uniform on $\{-0.1,0.1,0.3,0.5\}$ and $Y$ uniform on $\{0.02,0.04\}$ . There $\int_{S_2}(F^{(2)}-G^{(2)})=0.002767$ , while $\sum_sA_{D,s,\lambda}$ is $0.003087$ on the grid $\{-0.1,0.02,0.04,0.5\}$ and decreases towards $0.002767$ as the grid is refined.

Formalization targets

Goal: Theorem 1 (p. 12)

For a portfolio $\lambda\in\Lambda$ and $\tau>1$ ,

\exists D:\ X \text{ dominates } Y \text{ by } \tau\text{-AASSD under } D\quad\Longrightarrow\quad X\text{ dominates }Y\text{ by }\tau\text{-ASSD}.

Milestones

§2, p. 7: $F^{(2)}_\lambda$ is nonnegative, nondecreasing and convex.
Lemma 1, p. 45: for a finite distribution on $[a,b]$ , $\mathrm{Var}(X)+(b-\mathbb EX)^2=2\int_a^bF^{(2)}(x)\,dx$ .
Proposition 1, p. 10: $\hat F^{(2)}_{D,\lambda}\ge F^{(2)}_\lambda$ on $\mathbb R$ .
Proposition 3, p. 11: $\int_{\hat S_2}(\hat F^{(2)}_{D,\lambda}-G^{(2)})=\sum_sA_{D,s,\lambda}$ , with $\hat S_2=\{t\in[a,b]:\hat F^{(2)}_{D,\lambda}(t)>G^{(2)}(t)\}$ .
Proof of Theorem 1, step (12b), p. 46: $\int_{S_2}(F^{(2)}_\lambda-G^{(2)})\le\int_{\hat S_2}(\hat F^{(2)}_{D,\lambda}-G^{(2)})$ .
Proof of Theorem 1, step (12c), p. 46: $\mathrm{Var}(Y)+(b-\mathbb EY)^2-\mathrm{Var}(X)-(b-\mathbb EX)^2=2\int_a^b(G^{(2)}-F^{(2)}_\lambda)$ .

Significance

The result. Theorem 1 makes AASSD a safe surrogate for ASSD: any portfolio admitted by the AASSD constraints is a genuine $\tau$ -ASSD improvement on the benchmark, for every grid that contains the benchmark's values. This is what licenses the paper's optimization models (§4), in which the AASSD constraint (5d) is imposed with the $A_{D,s,\lambda}$ as auxiliary variables and solved by a cutting-plane method. The converse fails in general; the gap is controlled by the grid (Theorem 2, not part of this mission).

Formalizing it. The paper proves Theorem 1 by a chain of four inequalities resting on a cited identity (Lemma 1, taken from Luo and Tan, 2020, without proof), on a convexity argument stated in one line (Proposition 1), and on a case-by-case area computation (Proposition 3). A machine-checked development makes each step explicit, including where the requirement that the grid contain every benchmark value is used. To the best of current knowledge none of these results has been formalized; the definitions of ASSD and AASSD are new to the platform.

Difficulty

The obvious argument compares the two violation areas sub-interval by sub-interval. The comparison $\hat F^{(2)}\ge F^{(2)}$ is a chord-above-convex-function fact, but the area identity of Proposition 3 needs $\hat F^{(2)}_{D,\lambda}-G^{(2)}$ to be affine on each sub-interval, which holds only because every kink of $G^{(2)}$ is a grid point. Without that condition both Proposition 3 and Theorem 1 are false. The four closed-form cases of Definition 2 must then be matched to the positive part of an affine function on an interval, including the degenerate cases where a value coincides at an end point. Lemma 1 requires an exchange of a finite sum with an interval integral of piecewise-linear functions. Finally, the sets $S_2$ , $\hat S_2$ , $\bar S_2$ are defined by strict and non-strict inequalities between continuous functions, and the split of $\int_a^b$ into the integrals over $S_2$ and $\bar S_2$ has to be justified measure-theoretically.

Formalization scope

Everything is finite and real-valued; there is no probability space. Distributions are probability vectors on Fin T and Fin Tb, LPMs are the explicit sums above, expectations and variances are finite sums (the variance in the scenario form $\sum_tp_t(X_t-\mathbb EX)^2$ , which equals the paper's $\lambda^\top\mathrm{Cov}\,\lambda$ ). Integrals are Lebesgue integrals of continuous functions over subsets of $[a,b]$ . The standing assumptions of §2 and §3.1 are bundled in one predicate: $a<b$ , both probability vectors, all returns in $[a,b]$ . The benchmark's ascending order (p. 7, "without loss of generality") is not imposed. The grid is indexed from $0$ : d : Fin (K+1) → ℝ, $T_D=K+1$ .

Two readings are fixed. First, $\bar S_2$ is the complement of $S_2$ inside $[a,b]$ . Second, both dominance notions are written with the ratios cross-multiplied (Definition 3 in the paper's own form (5d)), which is equivalent to the printed ratios when the denominators are positive and gives the intended meaning when the SSD violation is zero. Outside $[a,b]$ the interpolated LPM is set equal to $F^{(2)}_\lambda$ .

Formalizations that would trivialize the goal are excluded: literal ratios with Lean's $x/0=0$ , integration over $\mathbb R\setminus S_2$ (divergent, hence $0$ ), a grid not required to contain the benchmark values, a fixed grid instead of "there exists a grid", and an arbitrary convex function in place of the LPM of the portfolio return.

A complete development needs the convexity of positive parts and finite sums, interval integrals of piecewise-linear functions, and measurability of sub- and super-level sets of continuous functions. The LPM identities (Lemma 1, milestone 6) are reusable for any finite-scenario stochastic-dominance model. Proofs of any milestone, and supporting lemmas such as the continuity and choice-independence of the interpolated LPM, are welcome.

Selected references

C. Luo, P. Chen, P. Jaillet, Portfolio Optimization Based on Almost Second-Degree Stochastic Dominance, Management Science, 2025 (accepted manuscript, April 2024). https://doi.org/10.1287/mnsc.2022.01092
M. Leshno, H. Levy, Preferred by "All" and Preferred by "Most" Decision Makers: Almost Stochastic Dominance, Management Science 48(8), 1074–1085, 2002. https://doi.org/10.1287/mnsc.48.8.1074.169
L. Y. Tzeng, R. J. Huang, P.-T. Shih, Revisiting Almost Second-Degree Stochastic Dominance, Management Science 59(5), 1250–1254, 2013. https://doi.org/10.1287/mnsc.1120.1616
D. Dentcheva, A. Ruszczyński, Optimization with Stochastic Dominance Constraints, SIAM Journal on Optimization 14(2), 548–566, 2003. https://doi.org/10.1137/S1052623402420528
C. Luo, C. H. Tan, Almost Stochastic Dominance for Most Risk-Averse Decision Makers, Decision Analysis 17(2), 169–184, 2020 (cited by the paper for Lemma 1).

8 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Forewarned Is Forearmed? Contingent Sourcing, Shipment Information and Supplier Competition: Contingent Sourcing Makes Both Suppliers Weakly Better Off but Can Make the Buyer Worse OffResearch Paper

Motivation

Firms that source from a low-cost but unreliable supplier often hedge with a second, reliable supplier. A recent development is that buyers can now track a shipment in transit (temperature loggers for perishables, GPS and inspection reports) and learn, before the selling season, whether the cheap order has been damaged. With that information the buyer can wait and place an emergency order with the reliable supplier only when the shipment is spoiled. This is contingent sourcing. The operational value of such information is clear for a buyer facing fixed prices. Lu and Tomlin (MSOM, doi:10.1287/msom.2021.0540; author manuscript SSRN 4260604) ask what happens when the suppliers set their prices strategically, anticipating how the buyer will use the information. Their answer is that shipment information softens the price competition between the suppliers, and the buyer can end up worse off with the information than without it.

The model without shipment information reduces to the model of Shan, Li and Sethi (2022), in which a responsive-pricing retailer sources from competing suppliers facing disruptions; Lu and Tomlin add the Time-1 signal and the emergency price.

Setting

A buyer sells a product at the price $p(q)=m-q$ , with market potential $m>0$ ; with an available quantity $Q$ its revenue is $R(Q)=mQ-Q^2$ for $Q\le m/2$ and $m^2/4$ otherwise. Supplier U has unit cost $c_U$ and delivers successfully with probability $P_1\in(0,1)$ ( $P_0=1-P_1$ ); the buyer pays U only on delivery. Supplier R is reliable with unit cost $c_R$ . Standing assumptions: $0\le c_U\le P_1m$ , $0\le c_R\le m$ .

Timing: at Time 0 the suppliers simultaneously set prices, $w_U$ for U and a regular price $w_R$ and emergency price $w_E\ge w_R$ for R, within the strategy spaces $c_U/P_1\le w_U\le m$ and $c_R\le w_R\le w_E\le m$ . The buyer then orders $Q_U$ and $Q_R$ . At Time 1 it observes a signal $s\in\{B,G\}$ of accuracy $\rho$ : a spoiled shipment shows $B$ with probability $\rho$ , an intact one always shows $G$ . It may then order $Q_E(s)$ from R at price $w_E$ . The buyer maximizes its expected profit (2) over the four nonnegative quantities; its value is the optimum.

Supplier R's payoff is $\pi_R=(w_R-c_R)Q_R+P_B(w_E-c_R)Q_E$ and U's is $\pi_U=(P_1w_U-c_U)Q_U$ , evaluated at the buyer's optimal order (Table 1 of the paper, with footnote 11's tie-break: an indifferent buyer sources contingently). An equilibrium is a Pareto-dominant Nash equilibrium: a Nash equilibrium that no other Nash equilibrium improves for both suppliers. Scenario I is $\rho=1$ (perfect information, contingent sourcing possible); Scenario N is $\rho=0$ (no information). The thresholds are

\psi_2=\frac{P_0m+2c_U/P_1}{P_0+2},\qquad \phi_1=\frac{(1+P_0)m+c_U}{2},\qquad t=m-\frac{P_1m-c_U}{\sqrt{4-P_1+P_1^2}} .

Formalization targets

Goal: Proposition 4(i)–(iii)

For $c_R>\psi_2$ equilibria exist in both scenarios, and for every equilibrium $w^I$ at $\rho=1$ and every equilibrium $w^N$ at $\rho=0$ , writing $\pi_B$ for the buyer's value:

\begin{aligned} &c_R\ge\phi_1: && \pi_U(w^I)=\pi_U(w^N),\ \pi_B(w^I)\ge\pi_B(w^N),\ \pi_R(w^I)\ge\pi_R(w^N)\ \text{(strict for } c_R<m),\\ &t<c_R<\phi_1: && \pi_B,\pi_U,\pi_R \text{ all strictly larger at } w^I,\\ &\psi_2<c_R\le t: && \pi_B(w^I)\le\pi_B(w^N)\ (\text{strict for } c_R<t),\quad \pi_U,\pi_R \text{ strictly larger at } w^I. \end{aligned}

The third case is the headline: the buyer loses from information while both suppliers gain.

Milestones

Lemma 1 and Proposition 1 (the buyer's optimal orders), Lemma A.1 (supplier R's best response at $\rho=1$ ), Proposition 2(i) (the equilibria at $\rho=1$ for $c_R>\psi_2$ : contingent sourcing at the prices of Table 2) and Proposition 3(i)–(ii) (the equilibria at $\rho=0$ for $c_R>\psi_3$ : sole sourcing from U or diversification at the prices of Table 3).

Significance

The result separates two effects of shipment information: the operational value of reacting to spoilage, and a strategic effect, since the option of a later emergency order lets supplier U raise its price without losing the buyer. The interval $(\psi_2,t]$ is where the second effect dominates. The managerial reading in the paper is that a buyer should make sure the unreliable supplier is cost-efficient enough relative to the reliable one before investing in monitoring.

The mission produces a machine-checked version of the equilibrium analysis of a two-supplier pricing game with a discontinuous buyer response. The paper's results are proved on paper only; nothing in this model is formalized elsewhere. The formal statements also fix a reading of the printed results where the printing is wrong: Proposition 2(ii), Proposition 4(iv) and Lemma A.2(ii)–(iii) of the paper are false as printed (see below), and the mission states only the parts that hold.

Difficulty

The buyer's response is piecewise: four ordering regimes, with boundaries $w_R=w_U$ , $w_R=\eta_1$ and $w_R=\eta_2$ , and the suppliers' payoffs jump across them. Best responses therefore are not first-order conditions of a smooth payoff; each supplier compares the best interior price in each regime with limit prices that push the buyer to a regime boundary. At $\rho=1$ the boundary between contingent sourcing and diversification is a tie for the buyer, and the equilibrium (i-b) exists only because of the tie-break. The selection of Pareto-dominant equilibria adds a further layer: at $\rho=1$ there is a continuum of Nash equilibria (lower $w_U$ with the same R-payoff), and the goal quantifies over all undominated ones. A natural first idea, comparing the closed-form Table 2 and Table 3 payoffs, proves the inequalities only for those particular profiles; the goal also needs that every equilibrium has those payoffs, which is Propositions 2(i) and 3(i)–(ii).

Formalization scope

Everything is real-valued and deterministic: yield and signal enter only through $P_1$ , $P_B=P_0\rho$ , $P_G=1-P_0\rho$ and the posteriors $P_{0G},P_{1G}$ , with $P_{0B}=1$ , $P_{1B}=0$ . The accuracy $\rho$ is an argument; the literals $1$ and $0$ give the two scenarios, and Proposition 3 is the same game at $\rho=0$ . Parameters are a structure Params with a Standing predicate ( $0<m$ , $0<P_1<1$ , $0\le c_U\le P_1m$ , $0\le c_R\le m$ ; the nonnegativity of $m$ and the costs is implicit in the paper). The buyer's value is sSup of (2) over feasible orders, which is meaningful at nonnegative prices, in particular at every equilibrium. The buyer's response in the payoffs is Table 1 by case in the order (iv), (i) with $\eta_1\le w_R$ , (ii), (iii), which is footnote 11's tie-break. Pareto dominance is weak dominance, as in the proof of Proposition 2. Lemma 1 and Proposition 1 add nonnegative $w_U,w_R$ and $0\le\rho\le1$ .

Departures from the printed statements, all disclosed in the items:

Proposition 4 is stated weakly at three endpoints where the printed strict claims fail ( $c_R=m$ : R and the buyer tie; $c_R=\phi_1$ : U is unaffected, covered by case (i); $c_R=t$ : the buyer ties).
Proposition 4(iv), Proposition 2(ii) and Lemma A.2(ii)–(iii) are false and omitted. Counterexample: $m=10$ , $P_1=1/2$ , $c_U=0$ , $c_R=3/2<\psi_2=2$ . At $\rho=1$ the profile $(w_U,w_R,w_E)=(3/2,29/8,23/4)$ is an equilibrium (the buyer is contingent at the tie $\eta_1=w_R$ ) with payoffs U $51/16$ , R $289/64$ , alongside the diversification equilibrium $(13/7,26/7,\cdot)$ with payoffs U $169/98$ , R $961/196$ , which is the unique equilibrium at $\rho=0$ . Neither dominates the other, so contingent sourcing does change payoffs below $\psi_2$ .

Trivializing formalizations are ruled out: the payoffs and equilibria are defined from the game, not from the Table 2/3 profiles; the goal quantifies over all equilibria and asserts their existence, so it is neither a statement about closed forms nor vacuous; R chooses $w_E$ freely; and the strategy spaces are exactly those of p. 16.

All objects live in one definitions file, ContingentSourcing.Competition.Model. Proofs of any milestone are welcome, as are proofs of the omitted Proposition 2(iii) and Proposition 3(iii). A reusable byproduct would be lemmas on piecewise-quadratic two-stage newsvendor-type programs with linear demand.

Selected references

T. Lu and B. Tomlin, Forewarned Is Forearmed? Contingent Sourcing, Shipment Information and Supplier Competition, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2021.0540 (author manuscript: https://ssrn.com/abstract=4260604)
B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5), 2006. https://doi.org/10.1287/mnsc.1060.0515
X. Shan, T. Li and S. P. Sethi, A responsive-pricing retailer sourcing from competing suppliers facing disruptions, Manufacturing & Service Operations Management 24(1):196–213, 2022 (cited by the paper for Proposition 3).
V. Babich, A. N. Burnetas and P. H. Ritchken, Competition and diversification effects in supply chains with supplier default risk, Manufacturing & Service Operations Management 9(2), 2007. https://doi.org/10.1287/msom.1060.0122

7 thms1 active userReviewed

Economics Operations Research Probability·Captain: mikedeng1

Can a Supplier’s Yield Risk Be Truthfully Communicated via Cheap Talk?: Truthful Yield Reporting Is an Equilibrium Iff Expected Market Potentials Bracket the Adjusted Wholesale RateResearch Paper

Motivation

A firm that outsources a new product or component to a supplier with an immature production process faces random yield: only a random fraction of the input becomes a usable unit. In semiconductor manufacturing, for instance, yield losses on new-generation chips have been reported at 30–45%. The supplier usually knows her own yield better than the buyer does, and in practice she shares it through nonbinding channels such as self-assessment reports. Whether such reports can be believed is a question about cheap talk: costless, unverifiable messages, in the tradition of Crawford and Sobel (Econometrica 1982).

Tao Lu (MSOM 2024, doi:10.1287/msom.2023.0089) asks when a supplier's yield report can be truthful in equilibrium. A babbling equilibrium, in which messages carry no information, always exists in cheap-talk games; the substantive question is whether a truth-revealing equilibrium exists, and under which conditions on demand, yield and contract. The paper's answer is an explicit inequality, Proposition 2, and it is the goal of this mission.

Setting

The supplier has a privately known type $t \in T = \{H, L\}$ . A type- $t$ supplier's yield $\xi_t$ is a random variable with values in $[0,1]$ , mean $\theta_t$ and coefficient of variation $\delta$ common to both types, so that its variance is $\delta^2\theta_t^2$ ; the high type has the higher mean, $\theta_H > \theta_L$ . If the buyer orders $Q$ units, $\xi_t Q$ units are delivered.

The buyer privately knows the market state $m \in M = \{H, L\}$ and faces the inverse demand $P(x \mid m) = a_m - bx$ with market potentials $a_H > a_L$ and slope $b > 0$ . Type and state are drawn from a common-knowledge joint distribution $p_{tm} > 0$ , which defines the conditionals $\mu(m \mid t) = p_{tm}/\sum_{m'} p_{tm'}$ (the supplier's view of the market) and $\lambda(t \mid m) = p_{tm}/\sum_{\hat t} p_{\hat t m}$ (the buyer's prior on the type).

The contract $(w, \eta)$ with $0 \le \eta \le 1$ is exogenous: the buyer pays $\eta w$ per unit ordered and $(1-\eta) w$ per effective unit delivered, and the supplier pays $c$ per unit of input. The model assumes $a_m\theta_t > \eta w + (1-\eta) w\theta_t > c$ for all $m, t$ : ordering and producing are always profitable.

The game: the supplier sends a message $t' \in T$ ; the buyer, given $t'$ and $m$ , forms a belief $\beta(t \mid t', m)$ and orders $Q^*(t', m)$ to maximize

\Pi_B(Q \mid t', m) = \sum_{t} \beta(t \mid t', m)\, E\big[\xi_t Q (a_m - b\xi_t Q) - \eta w Q - (1-\eta) w \xi_t Q\big];

the supplier of type $t$ sending $t'$ earns

\Pi_S(t' \mid t) = \sum_{m} \mu(m \mid t)\, E\big[(\eta w + (1-\eta) w\xi_t - c)\, Q^*(t', m)\big].

A perfect Bayesian equilibrium (PBE) is a messaging map $r : T \to T$ , an ordering strategy $Q^*$ and beliefs $\beta$ such that each type's message maximizes $\Pi_S$ , each order maximizes $\Pi_B$ over $Q \ge 0$ , and beliefs follow Bayes' rule on the equilibrium path. It is truth-revealing if $r(t) = t$ for both types.

Formalization targets

Goal: Proposition 2

Under the standing assumptions, a truth-revealing equilibrium exists if and only if

\sum_{m\in M}\mu(m\mid H)\,a_m \;\le\; \Big[1 + \eta\Big(\frac{1}{\theta_H} + \frac{1}{\theta_L} - 1\Big)\Big] w \;\le\; \sum_{m\in M}\mu(m\mid L)\,a_m. \tag{6}

Both directions are part of the goal.

Milestones

In a truth-revealing equilibrium, $\beta(t \mid t, m) = 1$ (§3, p. 9).
Under symmetric information the buyer's expected profit is $a\theta Q - b\theta^2(1+\delta^2)Q^2 - \eta w Q - (1-\eta) w\theta Q$ (proof of Proposition 1).
Proposition 1, (3): the buyer's unique optimal order under symmetric information is

Q^r(\theta, a) = \frac{[a - (1-\eta)w]\theta - \eta w}{2b(1+\delta^2)\theta^2}.

(5), p. 11: in a truth-revealing equilibrium $Q^*(t, m) = Q^r(\theta_t, a_m)$ , and such an equilibrium exists iff $Q^r(\theta_t, a_H)\mu(H\mid t) + Q^r(\theta_t, a_L)\mu(L\mid t) \ge Q^r(\theta_{t'}, a_H)\mu(H\mid t) + Q^r(\theta_{t'}, a_L)\mu(L\mid t)$ for $t \ne t'$ .
(B.4)–(B.5): the IC condition splits into the two types' conditions, and the high type's is the left inequality of (6).
The low type's condition (B.5) is the right inequality of (6).

Significance

The result. Condition (6) is explicit in the primitives, so it says which contracts and which markets support credible yield reports. It requires the low-yield type to expect a higher market potential than the high-yield type, so truthful communication needs market size and yield to be negatively correlated — the situation the paper argues is typical for hard-to-make high-tech products. Through the factor $1 + \eta(1/\theta_H + 1/\theta_L - 1)$ the condition also shows how the input-payment share $\eta$ moves the bracket; with $\eta = 0$ it cannot hold (Corollary 2), so paying for part of the input is necessary for credibility. Corollaries 1–2 and the welfare comparisons of §4.3 (Propositions 3–5) build on Proposition 2.

Formalizing it. The result is proved in the paper (main text and Online Appendix B); no machine-checked version is known. The mission produces a formal definition of the paper's game with its full PBE notion (optimality of the order over all $Q \ge 0$ , Bayes' rule on path, arbitrary beliefs off path), a formal proof that the expectation-based buyer problem has the closed-form optimum (3) for any yield law with the given mean and variance, and the reduction of equilibrium existence to an algebraic condition. The two-type model and the moment-based profit identity are reusable for other random-yield models with linear demand.

Difficulty

The algebra from (5) to (6) is short; the difficulty is everything before it. The buyer's profit is an expectation over an arbitrary yield law on $[0,1]$ , not a parametric family, so the closed form (3) has to be justified from the first two moments, with integrability coming from the support. The equilibrium notion quantifies over all orders $Q \ge 0$ and all belief systems, so the reduction to closed forms is a genuine two-directional argument about the game rather than a substitution, and the naive shortcut of identifying the equilibrium order with $Q^r$ by definition proves nothing about the paper's PBE. Finally, (6) involves $1/\theta_H$ and $1/\theta_L$ , and positivity of the mean yields is not an assumption of the paper but a consequence of its profitability assumption together with $w > 0$ .

Formalization scope

All objects live in the namespace YieldCheapTalk.Truthful. Types and market states are the two-element type Level. A Model records $a, b, \theta, \delta, c, w, \eta, p$ and the yield laws xi t : Measure ℝ; expectations are integrals against these laws. The predicate Standing bundles the paper's assumptions of §3 and $a_H > a_L$ (assumed from p. 12 on): $\theta_H > \theta_L$ ; each yield law is a probability measure carried by $[0,1]$ with mean $\theta_t$ and variance $\delta^2\theta_t^2$ (the coefficient of variation $\delta$ in the paper's sense; $\delta = 0$ is allowed); $0 \le \eta \le 1$ ; $p_{tm} > 0$ summing to one; $a_m\theta_t > \eta w + (1-\eta) w\theta_t > c$ . Two hypotheses are added and used tacitly by the paper: $b > 0$ and $w > 0$ . With $w > 0$ the model forces $\theta_t > 0$ . The bound $\theta_t \le 1/(1+\delta^2)$ of footnote 2 is a consequence of the yield law and is not assumed. The supplier's cost in (2) is the base model's single $c$ . Beliefs in the PBE are probability distributions on $T$ .

$Q^r$ is a closed-form definition; that it is the buyer's optimum is Milestone 3 and is never built into the equilibrium. The goal is the existence of a PBE with $r = \mathrm{id}$ as defined on pp. 8–9; an encoding in which the buyer's condition is replaced by " $Q = Q^r$ ", in which beliefs need not be distributions, or in which the goal is the equivalence of (5) and (6) would not state Proposition 2 and is ruled out. Contributions of proofs of any milestone, of the goal from the milestones, and of a general moment identity for expectations of quadratics under a law on $[0,1]$ are welcome.

Not formalized here: properties (i)–(ii) of Proposition 1, Lemmas 1–4, Corollaries 1–2, Propositions 3–5 (welfare), and the extensions of Online Appendices C–E.

Selected references

Tao Lu, Can a Supplier’s Yield Risk Be Truthfully Communicated via Cheap Talk?, Manufacturing & Service Operations Management, 2024; author manuscript of 14 July 2024. https://doi.org/10.1287/msom.2023.0089
Vincent P. Crawford and Joel Sobel, Strategic Information Transmission, Econometrica 50(6), 1431–1451, 1982. https://doi.org/10.2307/1913390
Oded Berman, Mohammad M. Fazel-Zarandi and Dmitry Krass, Truthful Cheap Talk: Why Operational Flexibility May Lead to Truthful Communication, Management Science 65(4), 1624–1641, 2019.
Gad Allon and Achal Bassamboo, Buying from the Babbling Retailer? The Impact of Availability Information on Customer Behavior, Management Science 57(4), 713–726, 2011.
Sammi Yu Tang and Panos Kouvelis, Supplier Diversification Strategies in the Presence of Yield Uncertainty and Buyer Competition, Manufacturing & Service Operations Management 13(4), 439–451, 2011.
Rajendra Bhatia and Chandler Davis, A Better Bound on the Variance, The American Mathematical Monthly 107(4), 353–357, 2000. https://doi.org/10.2307/2589180

8 thms1 active userReviewed

Algorithmic Game Theory Bandit Algorithms Machine Learning+1·Captain: mikedeng1

V-Learning—A Simple, Efficient, Decentralized Algorithm for Multiagent Reinforcement Learning: Independent V-Learning Finds a Coarse Correlated Equilibrium with Gap O((H²S/K)Ξ(A,K/S,ι) + √(H⁵Sι/K))Research Paper

Motivation

In multi-agent reinforcement learning several agents act in a shared, changing environment, each pursuing its own reward. The standard model is the Markov game (stochastic game), going back to Shapley (1953). When agents learn from experience rather than from a known model, the natural target is an equilibrium of the game, and the natural question is how many episodes of play are needed to find one.

Before V-learning, sample-efficient algorithms for general-sum Markov games were centralized and model-based: they estimated quantities indexed by the joint action, so their sample complexity grew with $\prod_{j=1}^m A_j$ , exponentially in the number of players $m$ . This is the curse of multiagents. Jin, Liu, Wang and Yu (arXiv:2110.14555, journal version in Mathematics of Operations Research, 2024) introduced V-learning, in which every agent runs its own simple algorithm, sees only its own reward and the states, and never needs the other agents' actions. Theorem 6 of the paper shows that the agents' combined output is an approximate coarse correlated equilibrium (CCE) after a number of episodes polynomial in $H$ , $S$ and $\max_j A_j$ only.

Timeline:

2018: Jin, Allen-Zhu, Bubeck and Jordan analyse optimistic Q-learning with the learning rate $\alpha_t=(H+1)/(H+t)$ , the rate V-learning reuses (arXiv:1807.03765).
2020: Bai and Jin (arXiv:2002.04017) and Xie et al. give the first sample-efficient algorithms for two-player zero-sum Markov games, based on optimistic value iteration. Bai, Jin and Yu (arXiv:2006.12007, NeurIPS 2020) introduce V-learning, coupled with FTRL, for Nash equilibria of two-player zero-sum games.
2021: Liu, Yu, Bai and Jin (arXiv:2010.01604, ICML 2021) learn Nash, CE and CCE of multi-player general-sum games with a centralized model-based method in $O(H^4S^2\prod_jA_j/\varepsilon^2)$ episodes.
2021: the present paper (arXiv v1, 27 October 2021) presents V-learning as a generic class of algorithms with any adversarial bandit subroutine and proves Theorem 6; two concurrent works (references [32] and [47] of the paper) obtain CCE guarantees for V-learning-style algorithms with one more factor of $H$ .

Setting

A tabular episodic $m$ -player Markov game has $S$ states, episodes of $H$ steps, and $A_j$ actions for player $j$ ; $A=\max_jA_j$ . At step $h$ in state $s$ the players choose actions simultaneously, forming a joint action $\boldsymbol a$ ; player $j$ receives the deterministic reward $r_{j,h}(s,\boldsymbol a)\in[0,1]$ , and the next state is drawn from $\mathbb P_h(\cdot\mid s,\boldsymbol a)$ . Every episode starts at a fixed state $s_1$ .

A joint policy $\pi$ may be correlated: the players share a random seed. $V^\pi_{j,1}(s_1)$ is player $j$ 's expected total reward. The best response value $V^{\dagger,\pi_{-j}}_{j,1}(s_1)$ is the largest value player $j$ can obtain by switching to a policy of its own, independent of the shared seed, while the others keep playing $\pi_{-j}$ . A joint policy is an $\varepsilon$ -CCE if $\max_j\big(V^{\dagger,\pi_{-j}}_{j,1}-V^\pi_{j,1}\big)(s_1)\le\varepsilon$ .

V-learning (Algorithm 1). Each player keeps, for every state $s$ and step $h$ , a visit count $N_h(s)$ , a value estimate $V_{j,h}(s)$ and an adversarial bandit algorithm. After visiting $s$ at step $h$ for the $t$ -th time it updates

\tilde V_{j,h}(s)\leftarrow(1-\alpha_t)\tilde V_{j,h}(s)+\alpha_t\big(r_{j,h}+V_{j,h+1}(s_{h+1})+\beta_{j,t}\big),\qquad V_{j,h}(s)\leftarrow\min\{H+1-h,\tilde V_{j,h}(s)\},

with $\alpha_t=(H+1)/(H+t)$ and a bonus $\beta_{j,t}$ , and feeds the loss $(H-r_{j,h}-V_{j,h+1}(s_{h+1}))/H$ of its own action to the $(s,h)$ -th bandit, whose next strategy becomes the policy at $(s,h)$ . The weights $\alpha^i_t=\alpha_i\prod_{j=i+1}^t(1-\alpha_j)$ express $\tilde V$ as a weighted average of past updates.

The bandit subroutine must satisfy Assumption 1: against any adaptive adversary with noisy, conditionally unbiased feedback, with probability at least $1-\delta$ the $\alpha^i_t$ -weighted regret after $t$ rounds is at most $\xi(B,t,\log(1/\delta))$ , where $\xi$ is non-decreasing in the number of arms $B$ and has a partial-sum upper bound $\Xi(B,t,\cdot)$ concave in $t$ .

The output policy $\hat\pi$ (Algorithm 3) samples an episode index $k$ uniformly from $[K]$ ; at each step, in state $s$ with $t=N^k_h(s)$ earlier visits in episodes $k^1<\dots<k^t$ , it samples $i$ with probability $\alpha^i_t$ , sets $k\leftarrow k^i$ , and plays the policies the players held at the beginning of episode $k^i$ . For the CCE all players use the same sample $i$ (shared seed, §5.1).

Formalization targets

Goal: Theorem 6

With $\iota=\log(mHSAK/\delta)$ and bonuses satisfying $\sum_{i=1}^t\alpha^i_t\beta_{j,i}=\Theta\big(H\xi(A_j,t,\iota)+\sqrt{H^3\iota/t}\big)$ for $t\in[K]$ , with probability at least $1-\delta$

\max_{j\in[m]}\Big[V^{\dagger,\hat\pi_{-j}}_{j,1}(s_1)-V^{\hat\pi}_{j,1}(s_1)\Big]\le O\Big(\frac{H^2S}{K}\,\Xi(A,K/S,\iota)+\sqrt{\frac{H^5S\iota}{K}}\Big).

The goal leaves the bandit algorithm abstract: it holds for every subroutine satisfying Assumption 1.

Milestones

Lemma 10: the properties of the weights $\alpha^i_t$ .
Lemma 11: $\tilde V$ as a weighted sum of past updates.
Lemma 12: Assumption 1 transported to every $(s,h,j)$ -bandit of the run, with failure probability $\delta$ .
Lemma 13 (optimism): $V^k_{j,h}\ge V^{\dagger,\hat\pi^k_{-j,h}}_{j,h}$ .
Lemma 14 (pessimism): $\underline V^k_{j,h}\le V^{\hat\pi^k_h}_{j,h}$ for the analysis-only estimate $\underline V$ .
The summed gap $\sum_k\max_j[V^k_{j,1}-\underline V^k_{j,1}](s_1)\le O(H^2S\Xi(A,K/S,\iota)+\sqrt{H^5SK\iota})$ (p. 24).

Two further steps of the proof of Theorem 6 are included as items without milestone status: the one-step recursion of $\delta^k_h=\max_j(V^k_{j,h}-\underline V^k_{j,h})(s^k_h)$ (p. 23) and the pigeonhole bound on the summed bonus terms (pp. 23–24).

Significance

With the FTRL subroutine of the paper (Corollary 19: $\Xi(B,t,\log(1/\delta))=20\sqrt{HBt\log(B/\delta)}$ ), Theorem 6 gives an $\varepsilon$ -CCE after $\tilde O(H^5SA/\varepsilon^2)$ episodes, against $H^4S^2\prod_jA_j/\varepsilon^2$ for the earlier centralized method. The same analysis, with a swap-regret subroutine, gives correlated equilibria (Theorem 7) and, specialized to two players with opposite rewards, Nash equilibria of zero-sum games (Theorem 5). The algorithm is decentralized: each agent's computation depends only on the visited states and its own actions and rewards.

The result is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization adds a precise statement of what "independent learning finds a CCE" means for non-Markov, history-dependent output policies, and of the adversary class Assumption 1 must cover for the reduction from the Markov game to the bandits to go through. It also makes explicit the boundary cases the paper leaves implicit (first visits, the last step, the initialization of $\tilde V$ ).

Difficulty

The deterministic steps (Lemmas 10–11, the recursion and the pigeonhole bound) are algebra on weighted sums. The difficulty is probabilistic. Lemma 12 must view each $(s,h,j)$ -bandit as playing against an adversary formed by the rest of the run: the other players, the transitions and the player's own other bandits, all adapted to the past. Lemmas 13 and 14 need concentration of $\alpha^i_t$ -weighted martingale sums over random visit times, uniformly over all states, steps, episodes and players.

The best response is the other obstacle. The output policy is not Markov: it carries a latent episode index. The opponent of $\hat\pi_{-j}$ may use the whole history of states and joint actions, and the best response to a non-Markov policy is not given by a Bellman equation. Lemma 13's step (v) handles this; the obvious per-state argument does not apply.

Formalization scope

Everything is finite and real-valued. States, players, actions, steps and episodes are Fin types; steps and episodes are 0-based, so the cap $H+1-h$ is H - h. The bandit rule is a deterministic function from the feedback history to a probability vector, starting uniform. The adversaries of Assumption 1 range over a finitary class: private randomness in an arbitrary finite type, losses chosen from the past before the learner's action, and conditionally unbiased feedback in $[0,1]$ . The training law is a finite product of policy and transition probabilities, and every probability is a finite sum over episode sequences. The best response is a supremum over deterministic history-dependent deviations, taken outside the average over the output policy's initial index. $\Theta$ and $O$ are read with a universal lower constant $c_0$ before every instance and an $O$ -constant depending only on the upper constant $c_1$ .

Added hypotheses, each disclosed in its item: nonnegative bonuses; $K\ge1$ ; per-player bandit rules sharing one $\xi$ ; $\xi\ge0$ in the pigeonhole step and the summed-gap milestone; $mHSAK\ge2$ in milestone 6, whose printed form is false without it. The output policy's convention at a first visit ( $t=0$ ) keeps the current index and plays the uniform initial policy.

Two formalizations would trivialize the goal and are ruled out: an Assumption 1 that no algorithm satisfies (a sorry-free check shows every valid rule satisfies it with $\xi\equiv1$ ), and a best response averaged per latent index or restricted to Markov deviations.

Needed infrastructure: weighted martingale concentration (Azuma–Hoeffding is on the platform), finite-sum manipulation of the training law, and Jensen's inequality for concave functions. Contributions to any milestone are welcome; the deterministic milestones 1, 2 and 6, and the recursion and pigeonhole steps, are independent of the probabilistic ones.

Selected references

C. Jin, Q. Liu, Y. Wang, T. Yu, V-Learning—A Simple, Efficient, Decentralized Algorithm for Multiagent RL, arXiv:2110.14555v1, 2021; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2110.14555
C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
Y. Bai, C. Jin, Provable Self-Play Algorithms for Competitive Reinforcement Learning, ICML 2020. https://arxiv.org/abs/2002.04017
Y. Bai, C. Jin, T. Yu, Near-Optimal Reinforcement Learning with Self-Play, NeurIPS 2020. https://arxiv.org/abs/2006.12007
Q. Liu, T. Yu, Y. Bai, C. Jin, A Sharp Analysis of Model-based Reinforcement Learning with Self-Play, ICML 2021. https://arxiv.org/abs/2010.01604
L. S. Shapley, Stochastic Games, PNAS 39(10), 1953. https://doi.org/10.1073/pnas.39.10.1095

10 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

Cross-Category Retailing Management: Substitution and Complementarity: Optimal Cross-Selling Prices Equalize Aggregate Markups, and the Optimal Profit Is the Unique Fixed Point of HResearch Paper

Motivation

Retailers often sell products from two categories that are bought one after the other: a television and then a speaker, a laptop and then a mouse, a suit and then a tie. The first purchase changes how much the second is worth to the consumer, which is called a complementarity effect, and online stores act on it by showing secondary products only after a main product is in the cart. A retailer pricing both categories must then trade off two things. A lower main-product price brings in more customers, and each of those customers adds secondary-product profit.

For a single category under the multinomial logit (MNL) model, the optimal prices are well understood. Li and Huh (2011) and Gallego and Wang (2014) show that the markup $p_i - c_i$ is the same for every product at optimality, under the MNL and nested logit models. Ke and Wang (Manufacturing & Service Operations Management, accepted 2020) extend this to a two-stage, cross-category model. Their Theorem 1 states that the invariant quantity becomes an aggregate markup: the main-product margin plus the profit the product brings in from its secondary products. They also show that the optimal total profit is the unique fixed point of a scalar function. This mission formalizes that theorem.

Setting

A firm offers a finite set $S$ of main products, drawn from a set $\mathcal M$ , and sells secondary products from a finite set $\mathcal N$ . Write $S^+ = S \cup \{0\}$ , where $0$ means that no main product is bought. Each $i \in S^+$ has a set $T_i \subseteq \mathcal N$ of secondary products offered after outcome $i$ ; $T_0$ is what a consumer who bought no main product can still buy. These sets may be disjoint, overlap, coincide or be empty. Main product $i$ has intrinsic utility $u_i$ , marginal cost $c_i$ and price $p_i$ . Secondary product $l$ has marginal cost $s_l$ , price $r_l$ (one price, whatever main product it follows) and intrinsic utility $v_{il}$ after outcome $i$ .

A consumer first chooses within $S^+$ by MNL, with probabilities

d_i(S,\mathbf p) = \frac{e^{u_i - p_i}}{1 + \sum_{j\in S} e^{u_j - p_j}} \ (i \in S), \qquad d_0(S,\mathbf p) = \frac{1}{1 + \sum_{j\in S} e^{u_j - p_j}}.

After outcome $i$ she chooses within $T_i \cup \{0'\}$ , buying $l \in T_i$ with probability $q_{l|i} = e^{v_{il} - r_l}/(1 + \sum_{k\in T_i} e^{v_{ik} - r_k})$ . The secondary profit of outcome $i$ is $t_i(\mathbf r) = \sum_{l\in T_i}(r_l - s_l)\,q_{l|i}$ . The total expected profit is

\Pi(S,\mathbf T,\mathbf p,\mathbf r) = \sum_{i\in S}(p_i - c_i)\,d_i + \sum_{i\in S^+} d_i\, t_i(\mathbf r),

and the aggregate markup of $i \in S$ is $p_i - c_i + t_i(\mathbf r)$ . Finally,

H(\mathbf r; z) = \sum_{i\in S}\exp\big((u_i - c_i - 1 - z) + t_i(\mathbf r)\big) + t_0(\mathbf r), \qquad H(z) = \sup_{\mathbf r} H(\mathbf r; z).

In Lean these are mainProb, secProb, secProfit, profit, aggMarkup, Hr and Hmax in the namespace CrossSell.Pricing.

Formalization targets

Goal: Theorem 1 (p. 12)

For fixed $S$ and $\mathbf T$ , with prices ranging over all real vectors:

at every joint maximizer $(\mathbf p, \mathbf r)$ of $\Pi$ , the aggregate markups $p_i - c_i + t_i(\mathbf r)$ , $i \in S$ , are equal;
$\{H(\mathbf r; z)\}_{\mathbf r}$ is bounded above for every $z$ ;
the equation $z = H(z)$ has exactly one solution $z^*$ , and

z^* = \sup_{\mathbf p,\mathbf r}\Pi(S,\mathbf T,\mathbf p,\mathbf r);

if $S \neq \emptyset$ , $H$ is strictly decreasing.

Milestones

Eq. (6), p. 12: $\Pi = \sum_{i\in S^+} d_i\big((p_i - c_i) + t_i(\mathbf r)\big)$ with $p_0 - c_0 = 0$ .
Theorem 1(b), p. 12: clauses 2–4 above without the profit identification.
The price formula, p. 13: if $z^* = H(z^*)$ and $\mathbf r^*$ maximizes $H(\cdot; z^*)$ , then $p_i^* = z^* + c_i - t_i(\mathbf r^*) + 1$ gives $\Pi(\mathbf p^*, \mathbf r^*) = z^*$ , and no prices give more.
Theorem 1(a), p. 12: clause 1 above.

Significance

The joint pricing problem has up to $M + N$ variables and its objective is not concave, so general solvers give no optimality guarantee. Theorem 1 replaces it with a problem over the secondary prices alone, $\max_{\mathbf r} H(\mathbf r; z)$ , plus a one-dimensional fixed-point search. Because $H$ is strictly decreasing, this search can be done by bisection. The main prices then follow from the p. 13 formula. The paper builds its later results on this reduction: the closed form for $T_0 = \emptyset$ (Proposition 1), the comparative statics of main prices in $t_i^*$ (Proposition 2), the pair-markup structure for disjoint secondary sets (Theorem 2), and the near-optimality bound for the same-markup/same-markup policy (Theorem 3).

The result is proved in the paper's Online Appendix. As far as a search of Prove2Me shows, it has no machine-checked proof, and no formal development of a two-stage logit model exists there. Formalizing it would give a reusable encoding of sequential MNL demand and a checked version of the reduction that the later results use. Other two-stage logit pricing models could follow the same template.

Difficulty

The single-category same-markup argument relies on a change of variables under which the profit becomes concave in the market shares. In this model the secondary prices $\mathbf r$ enter every segment's profit $t_i(\mathbf r)$ at once, through overlapping sets $T_i$ , so the problem in $(\mathbf p, \mathbf r)$ is not concave and does not separate by product. The main difficulty is that $H(z)$ is a supremum over all of $\mathbb R^{\mathcal N}$ , which need not be attained, of functions that may be unbounded below. Its finiteness, its continuity in $z$ , the existence and uniqueness of the fixed point, and its identification with the supremum of $\Pi$ all have to be established for this supremum, not for a closed form. Strict decrease needs the main-product terms to stay away from zero along near-maximizing $\mathbf r$ . That is false when $S = \emptyset$ , and showing it for $S \neq \emptyset$ needs a real argument.

Formalization scope

Model. Main products form a type ι and the offer set is S : Finset ι. Secondary products form a finite type κ. $S^+$ is Finset.insertNone S in Option ι, with none the outcome $0$ . The secondary sets are T : Option ι → Finset κ. The utilities v : Option ι → κ → ℝ are free reals. The paper's factorization $v_{il} = \beta_{il} v_l$ is not imposed; this is the same generality. The Gumbel derivation of the choice probabilities is not formalized: the closed forms with scale $\mu = 1$ are the model.
Optimality. A joint maximizer is a global maximizer of $\Pi$ over $\mathbb R^{\mathcal M}\times\mathbb R^{\mathcal N}$ , with no sign constraints on prices. The optimal total profit is the least upper bound of the profit values. The page's "max" presumes attainment, which the price-formula milestone supplies whenever $H(\cdot; z^*)$ has a maximizer.
Suprema. $H(z)$ is a real supremum, and its finiteness is part of the statement.
Added hypothesis. Strict decrease of $H$ is stated for $S \neq \emptyset$ only; for $S = \emptyset$ , $H$ is constant. The page does not state this exclusion.
Trivializations ruled out. Defining the optimal prices by the formula $z + c_i - t_i + 1$ , or the optimal profit as the fixed point, would make the goal circular. Here optimality is defined through $\Pi$ alone, and the goal identifies the fixed point with the supremum of $\Pi$ .
Needed infrastructure. Elementary real analysis (the bound $(x - s)e^{w - x} \le e^{w - s - 1}$ , continuity and monotonicity of suprema of parametric families) and finite sums. Nothing beyond Mathlib is required. The single-category same-markup lemma for MNL is reusable on its own. Proofs of the milestones in any order are welcome.

Selected references

C. Ke, R. Wang, Cross-Category Retailing Management: Substitution and Complementarity, Manufacturing & Service Operations Management, accepted 2020; accepted manuscript, SSRN 3383023. https://ssrn.com/abstract=3383023 (journal DOI 10.1287/msom.2021.0968)
H. Li, W. T. Huh, Pricing multiple products with the multinomial logit and nested logit models: Concavity and implications, Manufacturing & Service Operations Management 13(4), 2011. https://doi.org/10.1287/msom.1110.0344
G. Gallego, R. Wang, Price optimization and competition for multi-products under the nested logit model with product-differentiated price coefficients, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2013.1249

6 thms1 active userReviewed

Machine Learning Operations Research Optimization+1·Captain: mikedeng1

Stochastic Optimization Forests: the approximate risk criterion consistently approximates the oracle splitting criterion as the region to split shrinksResearch Paper

Motivation

In contextual stochastic optimization a decision $z\in\mathbb R^d$ is chosen after observing features $X\in\mathbb R^p$ , and the ideal policy solves, for each feature value,

z^*(x)\in\arg\min_{z}\ \mathbb E[c(z;Y)\mid X=x]

for a cost $c(z;y)$ and an uncertain outcome $Y$ (inventory demand, asset returns). Kallus and Mao (arXiv:2008.07473, Management Science 2023, doi:10.1287/mnsc.2022.4458) estimate such policies with stochastic optimization forests: random forests whose trees are grown to minimize the downstream decision cost rather than the prediction error of $Y$ .

The bottleneck is choosing a split. The natural rule, the oracle criterion, re-solves an optimization problem for every candidate split of every node, which is too expensive inside a forest. The paper replaces it by an approximate risk criterion that needs only a gradient per child and one Hessian per parent, and justifies the replacement by a second-order perturbation analysis. This mission formalizes that justification.

Setting

Let $\mu$ be the law of $X$ on $\mathbb R^p$ and let $\bar c(x,z)=\mathbb E[c(z;Y)\mid X=x]$ be the regression cost. For a region $R\subseteq\mathbb R^p$ with $\mu(R)>0$ write

p_R=\mu(R),\qquad f_R(z)=\mathbb E[c(z;Y)\mid X\in R]=\frac1{\mu(R)}\int_R\bar c(x,z)\,d\mu(x).

A node of a tree is a region $R_0$ ; a candidate split is a partition $R_0=R_1\cup R_2$ into disjoint measurable pieces. Abbreviate $p_j=p_{R_j}$ , $f_j=f_{R_j}$ for $j=0,1,2$ ; note $p_1f_1+p_2f_2=p_0f_0$ . Let $z_0$ be the unique minimizer of $f_0$ , $\nabla f$ the gradient and $\nabla^2 f$ the Hessian in $z$ , and $\mathcal D_0=\sup_{x,x'\in R_0}\|x-x'\|_2$ the diameter of $R_0$ .

The oracle criterion (eq. (8)) is the optimal cost after the split,

\mathcal C^{\mathrm{oracle}}(R_1,R_2)=p_1\min_z f_1(z)+p_2\min_z f_2(z),

and the approximate risk criterion (eq. (13)) is

\mathcal C^{\mathrm{apx\text{-}risk}}(R_1,R_2)=-\frac12\sum_{j=1,2}p_j\,\nabla f_j(z_0)^\top\bigl(\nabla^2 f_0(z_0)\bigr)^{-1}\nabla f_j(z_0).

For $g:\mathbb R^d\to\mathbb R$ the norm (70) is $\|g\|_{\mathcal F}=\max\{\sup_z|g|,\sup_z\|\nabla g\|_2,\sup_z\|\nabla^2 g\|\}$ , and $v(f)=\min_z f(z)$ .

Formalization targets

Goal: Theorem 2 (pp. 9–10)

Assume $\bar c(x,\cdot)$ is $C^2$ for every $x$ ; $\bar c$ , $\nabla_z\bar c$ , $\nabla_z^2\bar c$ are $L$ -Lipschitz in $x$ uniformly in $z$ ; and at an anchor point $\bar x$ the function $\bar c(\bar x,\cdot)$ has a unique, nondegenerate, level-bounded minimizer. Then for every $\varepsilon>0$ there is $\delta>0$ such that every split of a region $R_0\subseteq B(\bar x,\delta)$ satisfying the paper's conditions 1–3 for $j=1,2$ obeys

\bigl|\mathcal C^{\mathrm{oracle}}(R_1,R_2)-p_0f_0(z_0)-\mathcal C^{\mathrm{apx\text{-}risk}}(R_1,R_2)\bigr|\le\varepsilon\,p_0\,\mathcal D_0^2 .

Since $p_0f_0(z_0)$ does not depend on the split, the two criteria rank splits of a small node alike.

Milestones

Region identity (p. 8): $p_1f_1(z)+p_2f_2(z)=p_0f_0(z)$ .
Example 5 (p. 11): region averages are $C^2$ , with gradient and Hessian the region averages of those of $\bar c$ .
Lipschitz step (p. 81): $\|f_j-f_0\|_{\mathcal F}\le L\mathcal D_0$ .
Minimizer consistency (p. 74): minimizers of uniformly close functions are close to a unique, level-bounded minimizer.
Corollary 1 (p. 64): $v(f+t\delta_f)=v(f)+t\delta_f(z^*)-\tfrac12t^2\nabla\delta_f(z^*)^\top(\nabla^2f(z^*))^{-1}\nabla\delta_f(z^*)+o(t^2)$ , and the first-order expansion of the minimizer.
Theorem 9 (p. 65): the same expansions at $t=1$ with errors $o(\|\delta_f\|^2_{\mathcal F})$ and $o(\|\delta_f\|_{\mathcal F})$ .
Uniform Theorem 9 (p. 81): the value expansion of Theorem 9, uniformly over base functions $f_0$ that are $\mathcal F$ -close to a fixed nondegenerate $\bar f$ .

Significance

Theorem 2 is the guarantee behind the paper's algorithm: the criterion that is cheap to evaluate agrees with the expensive oracle criterion to second order in the node size, so a forest grown with it splits nodes the way a forest grown with the oracle would, while inverting only one Hessian per node. The same perturbation analysis drives the approximate solution criterion (Theorem 3) and, with constraints, Theorems 4 and 6; the unconstrained milestones here (Corollary 1, Theorem 9) are the reusable core.

The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. The mission produces a formal model of region-averaged costs, a quantitative second-order perturbation theory for unconstrained minimization (Corollary 1 and Theorem 9, which are standard in the Bonnans–Shapiro theory but absent from Mathlib), and a version of Theorem 2 with its limit, uniformity and error scale made explicit.

Difficulty

The expansions are about global minima, and Taylor's theorem only controls local behaviour. The obvious argument expands $f_0+\delta_f$ around $z_0$ and minimizes the quadratic model; it fails when the perturbation creates a competing minimum far from $z_0$ , which a small $\|\delta_f\|_{\mathcal F}$ does not rule out when $f_0$ is flat at infinity. Theorem 9 is true only because the minimizer is unique along the whole path $f_0+t\delta_f$ , $t\in[0,1]$ , which keeps it from jumping.

The second obstacle is uniformity. Theorem 9 is stated for a fixed $f_0$ , but in Theorem 2 the base function $f_0$ is the average over $R_0$ and moves as $R_0$ shrinks. The little- $o$ must hold uniformly over base functions near the limit $\bar c(\bar x,\cdot)$ ; Milestone 7 isolates this step.

Finally, a literal reading of the printed bound $o(\mathcal D_0^2)$ is weak: both $\mathcal C^{\mathrm{oracle}}-p_0f_0(z_0)$ and $\mathcal C^{\mathrm{apx\text{-}risk}}$ are $O(p_0\mathcal D_0^2)$ , so the printed bound holds without any second-order cancellation whenever $p_0\to0$ . The content is the factor $p_0$ .

Formalization scope

Features are EuclideanSpace ℝ (Fin p), decisions EuclideanSpace ℝ (Fin d) (unconstrained, §2). The law $\mu$ is a probability measure. The regression cost $\bar c$ is the primitive; $Y$ and $c(z;y)$ enter only through it (tower property). Gradients are Mathlib's gradient; the Hessian is the derivative of the gradient, and the inverse Hessian is ContinuousLinearMap.inverse, always paired with a positive-definiteness hypothesis so that it is a true inverse. Minima are real infima, and every statement assumes or derives attainment. Little- $o$ claims are $\varepsilon$ – $\delta$ statements; " $\|\delta_f\|_{\mathcal F}\le N$ " bounds the value, the gradient and the Hessian pointwise, with the Hessian in operator norm (weaker than the paper's Frobenius norm, so the statements are stronger).

Choices made where the page is silent or misprinted, all disclosed in the items:

the anchor point $\bar x$ and regions in $B(\bar x,\delta)$ name the limit "as the partition becomes finer";
the error bound carries the factor $p_0$ , which implies the printed $o(\mathcal D_0^2)$ ;
condition 4 is read as $x$ -Lipschitz bounds on $\bar c$ , $\nabla_z\bar c$ , $\nabla^2_z\bar c$ , uniformly in $z$ , which is how the proof uses it;
the minimizer in condition 3 depends on $t$ (the page calls it $z_0$ for every $t$ );
the Lipschitz step is $\|f_j-f_0\|_{\mathcal F}=O(\mathcal D_0)$ , not the printed $O(\mathcal D_0^2)$ , which is false.

The bound without the factor $p_0$ , a reading of condition 3 that forces $f_1=f_2=f_0$ at the optimum, a sup-norm defined by a supremum that is $0$ for unbounded functions, and a radius $\delta$ chosen after the regions would each make the goal trivial; the statements exclude all four.

Infrastructure needed: differentiation of set integrals with $C^2$ integrands (Mathlib's dominated-derivative lemmas suffice), consistency of minimizers under uniform perturbation, local strong convexity from a positive definite Hessian, and the second-order Taylor bound with remainder. The perturbation results (Milestones 4–7) are reusable for any unconstrained parametric minimization. Proofs of any milestone, and of the goal from Milestones 1, 3 and 7, are welcome.

Selected references

N. Kallus, X. Mao, Stochastic Optimization Forests, Management Science 69(4), 2023. arXiv:2008.07473v6 (2022): https://arxiv.org/abs/2008.07473 ; https://doi.org/10.1287/mnsc.2022.4458
J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973433
S. Athey, J. Tibshirani, S. Wager, Generalized Random Forests, Annals of Statistics 47(2), 2019. https://doi.org/10.1214/18-AOS1709

9 thms1 active userReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Information Disclosure and Promotion Policy Design for Platforms: Under Myopic Pricing, the Long-Run Average Optimal Consumer Surplus Equals the Concavification of the Best Confounding SurplusResearch Paper

Motivation

Online marketplaces decide which products to show first. A promotion puts a seller's product in front of consumers who will not search further, so it changes both the seller's sales and the surplus of the consumers who see it. A seller who is uncertain about the market sets prices from the sales they observe, and the platform's promotion decisions shape what those sales reveal. Gur, Macnamara, Morgenstern and Saban (arXiv:1911.09256, Management Science 2023) study how a platform that maximizes consumer surplus should combine an initial disclosure of information with a dynamic promotion policy when the seller learns and prices myopically.

The question joins two literatures. Bayesian persuasion (Kamenica and Gentzkow 2011) describes the value of a one-shot signal by the concave envelope of a value function. Learning-and-earning in dynamic pricing (Harrison, Keskin and Zeevi 2012) studies how a seller's beliefs converge when sales are informative. The paper's central result says what the platform can achieve in the long run when it controls both the starting point and the drift of the seller's belief.

Setting

A fraction $\phi\in\{\phi_L,\phi_H\}$ of consumers is impatient, with $0<\phi_L<\phi_H<1$ ; the platform observes $\phi$ and the seller holds the prior $\mu_0=\mathbb P(\phi=\phi_H)$ . The seller sets prices in a compact interval $\mathcal P$ containing $0$ . In each period $t=1,\dots,T$ one consumer arrives. A patient consumer buys with probability $\bar\rho_c(p)$ . An impatient consumer buys with probability $\bar\rho_0(p)$ if the seller is promoted and with probability $0$ otherwise. Consumer surplus is $\bar W_c(p)$ , $\bar W_0(p)$ or $\bar W_{\mathrm{out}}$ in the three cases. The purchase probabilities are decreasing and Lipschitz, the revenues $p\bar\rho_c(p)$ and $p\bar\rho_0(p)$ are strictly concave, $\bar\rho_0\ge\bar\rho_c$ , and $\bar W_c,\bar W_0$ are decreasing and Lipschitz.

Before the first period the platform commits to a signaling mechanism $\sigma$ , a distribution over signals for each value of $\phi$ , and to a promotion policy $\alpha$ , where $\alpha_t(p,\phi,\bar h_t)\in[0,1]$ is the probability of promoting the seller at price $p$ after the history $\bar h_t$ of the signal, past prices and past sales. The seller updates a belief $\mu_t$ about $\phi$ by Bayes' rule and follows a myopic Bayesian pricing policy $\pi^*$ : in each period they choose a price that maximizes the current expected revenue, breaking ties in favour of the current consumer surplus. The platform's payoff is the expected total consumer surplus $W_T^{\alpha,\sigma,\pi^*}(\mu_0)$ .

A promotion policy is confounding if it keeps the seller's belief constant, which requires the probability of a sale to be the same under $\phi_H$ and $\phi_L$ at the price the seller sets. Let $W^C(\mu)$ be the largest one-period expected consumer surplus of a confounding policy at belief $\mu$ , and let $co(W^C)$ be its concavification, the smallest concave function above $W^C$ on $[0,1]$ .

Formalization targets

Goal: Theorem 1

For every prior $\mu_0\in[0,1]$ ,

\lim_{T\to\infty}\ \sup_{\alpha,\sigma}\ \frac1T W_T^{\alpha,\sigma,\pi^*}(\mu_0)=co(W^C)(\mu_0),

and for every $T$ some signal and confounding policy achieve average surplus exactly $co(W^C)(\mu_0)$ . The goal is stated as a uniform upper bound for large $T$ together with exact attainment at every $T$ .

Milestones

Lemma 1 and Proposition 1: under myopic pricing it is without loss to use promotion policies that depend on the history only through the belief, that promote a single price, and two signals.
Proposition 3: for every belief a confounding policy exists.
Lemma 2: a period whose surplus exceeds $co(W^C)(\mu)+\epsilon$ separates the purchase probabilities under $\phi_H$ and $\phi_L$ by some $\delta(\epsilon)>0$ .
Lemma 3: the belief converges to the truth exponentially fast in the number of such periods.
Lemma 4: $co(W^{\max})-co(W^C)$ is bounded by $\epsilon/2+\bar C\mu$ and by $\epsilon/2+\bar C(1-\mu)$ .
Step (a) of (31): beliefs are a martingale and $\mathbb E[co(W^C)(\mu_t)]\le co(W^C)(\mu_0)$ .
The finite-horizon bound $\frac1T W_T<co(W^C)(\mu)+\frac54\epsilon$ for $T>\bar T$ .
The two existence steps: a repeated one-period confounding rule realizes its surplus in every period, and a two-signal mechanism attains $co(W^C)(\mu_0)$ .

Significance

The theorem identifies the long-run value of the platform's joint design problem with a static object. The platform's levers act on the belief process: the signal sets its starting point and the promotion policy its drift. The theorem says that, in the long run, the best use of the second lever is to stop the drift. Information is then disclosed only once, as in a persuasion problem with value function $W^C$ . A consequence is that a policy maximizing the current surplus in every period, which lets the seller learn $\phi$ , is generally not long-run optimal. The paper quantifies the gap on its uniform-willingness-to-pay example. The characterization is also the basis of the paper's later results on approximately optimal policies without signals and on equilibria with a forward-looking seller.

The result is proved in the paper; no part of it has been machine-checked. The formalization produces a finite, measure-free encoding of a dynamic Bayesian game with history-dependent policies, reusable for other learning-and-earning models, and makes the uniformity of every constant explicit.

Difficulty

The obvious argument treats each period separately: the surplus of a period is at most $W^{\max}(\mu_t)$ , and by Jensen's inequality the average is at most $co(W^{\max})(\mu_0)$ . This bound is too weak, because $W^{\max}$ exceeds $W^C$ at interior beliefs. The proof must show that periods whose surplus exceeds $co(W^C)$ by $\epsilon$ cannot recur often. This requires two quantitative statements that hold uniformly over all beliefs, policies and signals: each such period reveals information about $\phi$ by a fixed amount, and beliefs then concentrate exponentially fast. The surplus gained before concentration must also be controlled near the degenerate beliefs. The myopic tie-break makes the one-period problems discontinuous in the policy, so the compactness arguments behind $W^C$ need care.

Formalization scope

The game is encoded without measure theory. The state is a Boolean, the signal set is Fin n for an arbitrary $n$ , pricing policies are deterministic, and the expectation $W_T$ is a finite sum over the state, the signal and the sale outcomes, with path probabilities given by products of the sale probabilities. Beliefs follow Bayes' rule, and a probability-zero observation leaves the belief unchanged. Definitions 1–3 quantify over histories whose recorded prices lie in $\mathcal P$ . The tie-break of Definition 1 uses the current expected surplus under the seller's belief. $W^C$ and $W^{\max}$ are real suprema over one-period rules and myopic responses. $co$ is the supremum over the convex hull of the hypograph restricted to $[0,1]$ and is used only on $[0,1]$ . The standing assumptions add $0\le\bar\rho_c$ and $\bar\rho_0\le1$ , since these are probabilities. Only policies admitting a myopic response are considered, as the paper presumes. Constants in Lemmas 2 and 3 and in the finite-horizon bound are chosen before the horizon, the signal and the policies.

$W^C$ is the one-period version of (10) under myopic pricing with the tie-break, not the static program (11). The goal quantifies over all history-dependent promotion policies, all finite signals and all myopic pricing policies, so it cannot be trivialized by restricting the policy class or stating only the upper bound. The attainment conjunct requires a confounding policy with a myopic response at every history.

The paper asserts that $T\cdot W^C(\mu_1)$ is attained for every $\mu_1$ . Under the tie-break the supremum defining $W^C(\mu_1)$ can fail to be attained, so the corresponding milestone states only the repetition step. Proposition 1 is stated with the prior fixed before the policies are chosen.

A complete development needs Bayesian updating on finite trees, the martingale property and Jensen's inequality for finite mixtures, concave envelopes on an interval and their attainment by two-point splits, Berge-type continuity of constrained one-period optima, and exponential concentration of posteriors under separated likelihoods. The last three are reusable beyond this mission. Contributions to any milestone, and to general lemmas on concave envelopes and posterior concentration, are welcome.

Selected references

Y. Gur, G. Macnamara, I. Morgenstern, D. Saban, Information Disclosure and Promotion Policy Design for Platforms, Management Science, 2023; arXiv:1911.09256v5. https://arxiv.org/abs/1911.09256
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
J. M. Harrison, N. B. Keskin, A. Zeevi, Bayesian Dynamic Pricing Policies: Learning and Earning Under a Binary Prior Distribution, Management Science 58(3), 2012. https://doi.org/10.1287/mnsc.1110.1426
R. J. Aumann, M. Maschler, Repeated Games with Incomplete Information, MIT Press, 1995. https://mitpress.mit.edu/9780262011471/

12 thms1 active userReviewed

Machine Learning Operations Research Statistics·Captain: mikedeng1

Fixing Inventory Inaccuracies at Scale: The Entrywise Algorithm's Expected Anomaly-Detection Cost Is Within O(log^1.5(m)/√m) of the Optimal CostResearch Paper

Motivation

Retail inventory records are often wrong. A store's system may report units on the shelf that are not there (phantom inventory), so the replenishment system never reorders and the product silently stops selling. Audits fix such errors but are expensive, so a retailer wants to decide which store–SKU pairs to audit from sales data alone. The classical way, studying each pair's sales history over a long period, needs time-homogeneous data that rarely exists.

Farias, Li and Peng (arXiv:2006.13126v3, Manufacturing & Service Operations Management, 2024) instead use a single cross-sectional snapshot of sales across $n$ stores and $m$ SKUs. Expected demand is modelled as a low-rank matrix, anomalies corrupt a random subset of entries, and only some entries are observed. The paper proposes the entrywise (EW) algorithm and proves that its expected decision cost approaches that of an oracle knowing the model, at rate $\log^{1.5}(m)/\sqrt m$ . A matching $\Omega(1/\sqrt m)$ lower bound (Proposition 1) is also proved. The paper evaluates the method on synthetic data and on real data from a consumer goods retailer.

Setting

An instance has an expected-demand matrix $M^*\in\mathbb R_+^{n\times m}$ with $2\le m\le n$ , rank $r$ and SVD $M^*=U\Sigma V^\top$ with singular values $\sigma_1^*\ge\dots\ge\sigma_r^*>0$ and $\kappa=\sigma_1^*/\sigma_r^*$ . It also has an anomaly model $\mathrm{Anom}(\alpha,M)$ , which is a family of laws on $\mathbb N$ indexed by a parameter $\alpha\in\Gamma\subset\mathbb R^d$ and a mean level $M\ge0$ . The remaining data are a true parameter $\alpha^*$ , an anomaly probability $p_A^*$ , an observation probability $p_O$ , and costs $c^{(0)}_{ij}$ (flagging a normal entry) and $c^{(1)}_{ij}$ (missing an anomaly). Independently for every entry:

the entry is observed with probability $p_O$ ; the observed set is $\Omega$ ;
$B_{ij}\sim\mathrm{Bernoulli}(p_A^*)$ marks an anomaly;
sales are $X_{ij}\sim\mathrm{Poisson}(M^*_{ij})$ if $B_{ij}=0$ and $X_{ij}\sim\mathrm{Anom}(\alpha^*,M^*_{ij})$ if $B_{ij}=1$ .

Assumptions (§2):

$\|M^*\|_{\max}$ lies between a constant $c_M>0$ and $L$ .
Incoherence: $\|U\|_{2,\infty}\le\sqrt{\mu r/n}$ and $\|V\|_{2,\infty}\le\sqrt{\mu r/m}$ .
Sparsity: $\sqrt{p_O}\ge C\log^{1.5}(m)\mu r\kappa^2/\sqrt m$ .
$p_A^*\le1-c_A$ .
$\mathrm{Anom}(\alpha^*,M^*_{ij})$ has sub-exponential norm $\le L$ .
$\mathbb P(\mathrm{Anom}(\alpha,M)=k)$ is $K$ -Lipschitz in $(\alpha,M)$ .
Mean decomposition: $\mathbb E\,\mathrm{Anom}(\alpha,M)=g(\alpha)M$ with $g$ valued in $[0,1]$ and $K$ -Lipschitz.

The oracle $\pi^*$ knows $\theta^*=(\alpha^*,p_A^*)$ and $M^*$ . It computes the posterior $f^*_{ij}=\mathbb P(B_{ij}=0\mid X_\Omega)=y^*_{ij}/(x^*_{ij}+y^*_{ij})$ , where $x^*_{ij}=p_A^*\mathbb P_{\mathrm{Anom}(\alpha^*,M^*_{ij})}(X_{ij})$ and $y^*_{ij}=(1-p_A^*)\mathbb P_{\mathrm{Poisson}(M^*_{ij})}(X_{ij})$ . It flags $(i,j)$ iff $c^{(1)}_{ij}/(c^{(0)}_{ij}+c^{(1)}_{ij})\ge f^*_{ij}$ . The EW algorithm $\pi^{EW}$ runs four steps:

It computes $\hat M=\frac{nm}{|\Omega|}\mathrm{SVD}(X_\Omega)_r$ , a rescaled best rank- $r$ approximation of the zero-filled observations.
It estimates $\hat\theta$ by matching $T$ empirical CDF values $|\{X_{ij}\le t,(i,j)\in\Omega\}|/|\Omega|$ to their model predictions $g_t(\theta,\hat M/e(\theta))$ , where $e(\theta)=p_Ag(\alpha)+1-p_A$ .
It forms plug-in estimates $\hat f_{ij}$ of $f^*_{ij}$ .
It applies the oracle's threshold rule to $\hat f$ .

The cost of decisions $A$ is

\mathrm{cost}^A(X_\Omega)=\frac1{|\Omega|}\sum_{(i,j)\in\Omega}\Big(c^{(0)}_{ij}\mathbf 1\{A_{ij}=1\}f^*_{ij}+c^{(1)}_{ij}\mathbf 1\{A_{ij}=0\}(1-f^*_{ij})\Big).

Formalization targets

Goal: Theorem 1 (p. 12)

\mathbb E_{X_\Omega}\Big(\mathrm{cost}^{\pi^{EW}}(X_\Omega)-\mathrm{cost}^{\pi^*}(X_\Omega)\Big)\le c_{\max}\,C_0\,(1+K+L+\kappa+\mu+r+p_O^{-1})^k\,\frac{\log^{1.5}(m)}{\sqrt m}.

The constants $C_0$ and $k$ and the sparsity constant depend only on $d$ , $c_M$ , $c_A$ and the regularity constant $C_{RC}$ . The statement asserts the paper's rate with polynomial dependence on the model parameters. It does not fix the polynomial, so a sharper analysis still proves it.

Milestones, in the proof's order

Lemma 8: $\|\mathrm{Poisson}(\lambda)\|_{\psi_1}\le4\lambda+1$ .
Lemma 14: a Bernstein bound for $\sum_{(i,j)\in\Omega}T_{ij}$ .
Theorem 2: the entrywise bound $\|\hat M-e(\theta^*)M^*\|_{\max}\le C\delta'$ with $\delta'=\kappa^4\mu rL\sqrt{\log m/(p_Om)}$ .
Lemmas 15 and 16: the model moments and the objective $h(\theta^*)$ .
Lemma 2: $\|F(\hat\theta)-F(\theta^*)\|\lesssim(K+L)\delta'$ .
Lemma 17: a quantitative inverse-function bound.
Lemma 1: $\|\hat\theta-\theta^*\|\lesssim(K+L)\delta'$ .
Lemmas 18 and 19: plug-in likelihoods and the ratio perturbation bound.
Lemma 3: $|f^*_{ij}-\hat f_{ij}|\le\min(C\delta/(x^*_{ij}+y^*_{ij}),1)$ .
Step 4 of the proof sketch: the excess cost is at most $\frac1{|\Omega|}\sum_\Omega|a_{ij}-b_{ij}|$ .

Significance

Theorem 1 says that the value of cross-sectional data grows with the number of stores and SKUs. A retailer that can only see one snapshot does nearly as well as one that knows the demand matrix and the anomaly law exactly. With Proposition 1, the rate is optimal up to the logarithmic factor. Theorem 2 is, per the authors, the first entrywise guarantee for matrix completion under Poisson (more generally sub-exponential) noise, and it is reusable outside inventory problems.

The results are proved on paper: Theorem 1 by a proof sketch in §5.1 plus Appendix B, and Theorem 2 in Appendix A, which builds on a cited entrywise eigenvector perturbation theorem of Abbe et al. None of this is formalized. A machine-checked proof would also settle the constants and conventions that the paper leaves implicit. These include the dimension restriction in Lemma 17, the unspecified constant in Lemma 3, the form of the sparsity assumption used in the proof of Theorem 2, and the closed range of $p_A$ in $\Theta$ .

Difficulty

The obvious argument plugs consistent estimates of $M^*$ and $\theta^*$ into the Bayes rule. It breaks at the first step: a Frobenius-norm bound for $\hat M$ , which is what standard matrix completion gives, does not control any single $\hat f_{ij}$ . An entrywise bound is needed, under heavy-tailed (sub-exponential, not sub-Gaussian) noise, and with the anomalies corrupting the mean by the unknown factor $e(\theta^*)$ . The second step inverts the moment map $F$ . Closeness of moments yields closeness of parameters only through a quantitative inverse-function argument, which needs the regularity conditions of Lemma 1. A third subtlety is that $f^*_{ij}$ is a ratio whose denominator $x^*_{ij}+y^*_{ij}$ can be tiny. The error bound of Lemma 3 therefore degrades on rare sales values, and Theorem 1 averages this over the law of $X$ .

Formalization scope

One definitions module, InventoryAnomaly.EW.Model, holds the instance, the product sampling law over $\{$ observed $\}\times\{$ anomalous $\}\times\mathbb N$ per entry, the estimators, the costs and four predicates:

Model: §2's assumptions;
SparsityMax: the sparsity condition as read in the proof of Theorem 2, p. 41;
Regular: Lemma 1's conditions;
CostBound: costs in $[0,c_{\max}]$ .

The sub-exponential norm is the published HighDimProb.Concentration.subexponentialNorm.

Conventions:

Parameters. $\theta=(\alpha,p_A)\in\mathbb R^{d+1}$ , and $T=d+1$ moments are matched.
Parameter set. $\Theta=\Gamma\times[0,1-c_A]$ .
Clamped means. Laws are evaluated at the mean $\max(M,0)$ .
Cost. The cost is the closed form (5) with $f^*$ by Bayes' rule (8). $c^{(0)}$ is the false-positive cost (the display on p. 12 swaps the labels).
Estimators. $\mathrm{SVD}_r$ is any exact best rank- $r$ approximation. $\hat\theta$ is any point of $\Theta$ with $h(\hat\theta)\le h(\theta^*)$ , which every minimiser of (7) satisfies.
Constants. " $O(\cdot)$ " and "with probability $1-O(1/nm)$ " are existential constants. They come after $d,c_M,c_A,C_{RC}$ and before the instance.
Added conditions. $2\le m\le n$ , $1\le r\le m$ , finite anomaly means, and nonnegative costs. Lemma 17 is stated for square Jacobians. Lemma 3 has a constant $C$ in place of 2. Lemma 19's $\delta/(\hat x+\hat y)$ clause is stated when $\hat x+\hat y>0$ . Each item's Formalization Note lists these.

The algorithm's selections are universally quantified together with their defining properties. Neither may be replaced by unconstrained functions. The cost of $\pi^*$ must use $f^*$ , not $\hat f$ . The goal must keep the explicit rate $\log^{1.5}(m)/\sqrt m$ and the full probability model, without assuming Theorem 2's event.

Not formalized: Proposition 1 (the lower bound), Appendix E (the TPR/FPR-constrained variant), the cited Lemmas 6–7, and the internal Lemmas 9–13 and Propositions 2–3 of Appendix A.

Useful infrastructure includes entrywise singular-subspace perturbation bounds, Bernstein's inequality for bounded independent sums, and Orlicz-norm bounds for Poisson variables. All three are reusable beyond this mission. Proofs of individual milestones are welcome, especially Lemmas 8, 14, 17 and 19 and Step 4, which are self-contained.

Selected references

V. F. Farias, A. A. Li, T. Peng, Fixing Inventory Inaccuracies at Scale, Manufacturing & Service Operations Management, 2024; arXiv:2006.13126v3 (2022). https://arxiv.org/abs/2006.13126
E. Abbe, J. Fan, K. Wang, Y. Zhong, Entrywise Eigenvector Analysis of Random Matrices with Low Expected Rank, Annals of Statistics 48(3), 2020. https://arxiv.org/abs/1709.09565
A. D. McRae, M. A. Davenport, Low-rank matrix completion and denoising under Poisson noise, Information and Inference 10(2), 2021. https://arxiv.org/abs/1907.05325
R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. https://doi.org/10.1017/9781108231596

15 thms1 active userReviewed

Calculus of Variations Machine Learning Optimization+1·Captain: mikedeng1

Game on Random Environment, Mean-Field Langevin System, and Neural Networks: First-Order Condition for Entropy-Regularized Minimization over Probability Measures with a Fixed MarginalResearch Paper

Motivation

Several problems in machine learning and game theory are optimization problems over probability measures. Training a wide two-layer neural network can be viewed as minimizing a functional $F(\nu)$ of the distribution $\nu$ of the network's parameters (Mei, Montanari, Nguyen, PNAS 2018; Hu, Ren, Šiška, Szpruch, arXiv:1905.07769). Adding a relative-entropy penalty $\eta H(\nu)$ makes the problem strictly convex in the density and connects its minimizers to the invariant measures of Langevin-type diffusions, the mean-field Langevin dynamics. The first-order condition for the unconstrained problem is Hu et al., Proposition 2.4.

Conforti, Kazeykina and Ren (arXiv:2004.02457v2) add a random environment: a variable $y$ with a fixed law $\mathsf m$ that every player observes, such as the time index in a dynamic game or a shared signal. The strategies are then probability measures on $\mathbb R^d\times\mathbb Y$ whose $\mathbb Y$ -marginal is prescribed. Their Theorem 3.1 extends the first-order condition to this constrained problem. The introduction names it "one of our main contributions": it gives the necessary condition for Nash equilibria of games on a random environment (Corollary 3.3), and it identifies the invariant measure of the mean-field Langevin system studied in the rest of the paper.

Setting

Let $\mathbb Y$ be a Polish space with a probability measure $\mathsf m$ , and let $p\ge1$ . Write $\bar{\mathbb R}^d=\mathbb R^d\times\mathbb Y$ and $\bar x=(x,y)$ . The strategy set is

\Pi=\{\bar\pi\in\mathcal P_p(\bar{\mathbb R}^d):\ \bar\pi(\mathbb R^d,\cdot)=\mathsf m\},

the probability measures on $\bar{\mathbb R}^d$ with finite $p$ -th moment and $\mathbb Y$ -marginal $\mathsf m$ . By disintegration, $\bar\pi(d\bar x)=\pi(dx|y)\,\mathsf m(dy)$ .

A function $F:\Pi\to\mathbb R$ has a linear functional derivative $\frac{\delta F}{\delta\bar\pi}:\Pi\times\bar{\mathbb R}^d\to\mathbb R$ if for all $\nu,\nu'\in\Pi$

F(\nu')-F(\nu)=\int_0^1\int_{\bar{\mathbb R}^d}\frac{\delta F}{\delta\bar\pi}\big((1-\lambda)\nu+\lambda\nu',\bar x\big)\,(\nu'-\nu)(d\bar x)\,d\lambda. \tag{2.1}

Assumption 2.1 asks that $F$ have such a derivative, that $F$ and $\frac{\delta F}{\delta\bar\pi}(\cdot,\bar x)$ be continuous for the $p$ -Wasserstein distance $\mathcal W_p$ , that $\frac{\delta F}{\delta\bar\pi}(\bar\pi,\cdot,y)$ be continuously differentiable in $x$ , and that $\sup_{\bar\pi\in\Pi}|\frac{\delta F}{\delta\bar\pi}(\bar\pi,\bar x)|\le C(1+|\bar x|^p)$ .

The regularizer is the relative entropy with respect to $\mathrm{Leb}\times\mathsf m$ : if $\bar\pi$ has density $\pi(x|y)$ with respect to $\mathrm{Leb}\times\mathsf m$ , then $H(\bar\pi)=\int\ln\pi(x|y)\,\bar\pi(d\bar x)$ , and $H(\bar\pi)=+\infty$ otherwise. For $\eta>0$ the objective is

V(\bar\pi)=F(\bar\pi)+\eta H(\bar\pi).

Formalization targets

Goal: Theorem 3.1 (p. 4)

If $\bar\pi^*\in\operatorname{argmin}_{\bar\pi\in\Pi}V(\bar\pi)$ , then $\bar\pi^*$ has a density $\pi^*(x|y)$ which, for $\mathsf m$ -a.e. $y$ , is positive with $\ln\pi^*(\cdot|y)$ differentiable and

\nabla_x\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,x,y)+\eta\nabla_x\ln\pi^*(x|y)=0\qquad\text{for all }x\in\mathbb R^d. \tag{3.1}

Conversely, if $F$ is also convex on $\Pi$ , every $\bar\pi^*\in\Pi$ satisfying (3.1) minimizes $V$ over $\Pi$ . The goal states both directions, as printed.

Milestones (proof of Theorem 3.1, §5.1, pp. 9–11)

Step 1 (p. 9): for $\bar\pi,\bar\pi^*\in\Pi$ and $\bar\pi^\lambda=\lambda\bar\pi+(1-\lambda)\bar\pi^*$ , $\frac1\varepsilon\int_0^\varepsilon\int\frac{\delta F}{\delta\bar\pi}(\bar\pi^\lambda,\cdot)\,d(\bar\pi-\bar\pi^*)\,d\lambda\to\int\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot)\,d(\bar\pi-\bar\pi^*)$ .
(5.1) (p. 10): for a minimizer $\bar\pi^*$ and $\bar\pi\in\Pi$ with $H(\bar\pi)<\infty$ , $0\le\int\big(\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot)+\eta\ln\pi^*\big)\,d(\bar\pi-\bar\pi^*)$ .
(5.2) (p. 10): for a minimizer, $\Xi_y=\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot,y)+\eta\ln\pi^*(\cdot|y)$ is $\pi^*(\cdot|y)$ -a.s. constant for $\mathsf m$ -a.e. $y$ .
Step 3 (p. 11): a minimizer is equivalent to $\mathrm{Leb}\times\mathsf m$ .
Sufficiency, $F$ -part (p. 11): for convex $F$ , $F(\bar\pi)-F(\bar\pi^*)\ge\int\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot)\,d(\bar\pi-\bar\pi^*)$ .
Sufficiency, entropy part (p. 11): under (3.1), $H(\bar\pi)-H(\bar\pi^*)\ge\int\ln\pi^*\,d(\bar\pi-\bar\pi^*)$ .

Significance

Theorem 3.1 says that each fibre of an entropy-regularized minimizer is a Gibbs measure, $\pi^*(x|y)\propto\exp\big(-\frac1\eta\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,x,y)\big)$ . In the paper this yields the Nash-equilibrium condition (3.2) for $n$ -player games on a random environment, the uniqueness of equilibria under a monotonicity condition (Corollary 3.4), and the identification of the stationary measures of the mean-field Langevin system (2.2) with these equilibria, the basis of the convergence results (Theorems 3.8–3.12). For a one-player problem it is the optimality condition behind gradient-descent training of mean-field neural networks with an environment variable.

The result is proved in the paper; it is not formalized anywhere known. The mission produces the first machine-checked first-order condition for optimization over probability measures, with or without a marginal constraint, and the supporting objects: the strategy set $\Pi$ , the linear functional derivative, and relative entropy with respect to the infinite reference measure $\mathrm{Leb}\times\mathsf m$ . The unconstrained case ( $\mathbb Y$ a point) is a special case.

Difficulty

The sufficiency direction is two convexity inequalities and a cancellation of the $y$ -dependent constants, which uses the common marginal $\mathsf m$ . The necessity direction is harder. The first variation of $V$ at $\bar\pi^*$ gives only an inequality (5.1) in the directions $\bar\pi-\bar\pi^*$ with $H(\bar\pi)<\infty$ , and the entropy's difference quotient is not dominated where $\pi^*$ is small, so the limit requires a one-sided Fatou argument. The inequality (5.1) is not yet a pointwise equation. Converting it into " $\Xi_y$ is constant" needs admissible competitors with bounded density relative to $\bar\pi^*$ , built fibre by fibre in $y$ , and these only reach the support of $\bar\pi^*$ . Ruling out zeros of $\pi^*$ (Step 3) needs a separate competitor that charges a set where $\pi^*$ vanishes. Finally (3.1) concerns a smooth version of the density, which has to be produced from an almost-everywhere identity. The obvious idea of differentiating $V$ along $\bar\pi^*+\varepsilon\varphi$ for a signed perturbation $\varphi$ fails: such perturbations leave $\Pi$ unless they preserve positivity and the $\mathbb Y$ -marginal.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure; $\mathbb Y$ is a complete separable metric space with its Borel $\sigma$ -algebra (a Polish space with a fixed compatible metric, needed to state moments and $\mathcal W_p$ ); $\bar{\mathbb R}^d$ carries the max product metric, and $|\bar x|$ in the growth bound is the distance to a base point $(0,y_0)$ , with $C$ and $y_0$ fixed once for all $\bar\pi\in\Pi$ . $\mathcal W_p$ is the coupling infimum over this metric, valued in $[0,\infty]$ , and continuity is the $\varepsilon$ – $\delta$ notion on $\Pi$ . $F$ and $\frac{\delta F}{\delta\bar\pi}$ are functions on all measures of which only the values on $\Pi$ matter; $\frac{\delta F}{\delta\bar\pi}$ is part of the data and the theorem holds for every derivative satisfying (2.1). The definition of the derivative makes explicit what (2.1) presupposes: joint measurability in $\bar x$ and integrability in $\lambda$ . Mixtures are $(1-t)\nu+t\nu'$ for $t\in[0,1]$ , and convexity of $F$ is along these mixtures. $H$ and $V$ take values in $(-\infty,+\infty]$ , with $H=+\infty$ off absolute continuity. (3.1) is required of some measurable version of the density, for $\mathsf m$ -a.e. $y$ and every $x$ , together with positivity and differentiability of $\ln\pi^*(\cdot|y)$ .

The Lean logarithm satisfies $\ln 0=0$ , a non-integrable Bochner integral is $0$ , and the gradient of a non-differentiable function is $0$ . These would trivialize the statements, so (3.1) demands differentiability, and the milestones that integrate $\ln\pi^*$ assert integrability and that $\bar\pi$ does not charge $\{\pi^*=0\}$ , which is what the paper's convention $\ln0=-\infty$ encodes.

A complete development needs: mixtures and moments of measures in $\Pi$ ; $\mathcal W_p$ -convergence of mixtures; dominated convergence along mixtures; the entropy of a mixture and its one-sided derivative; disintegration with respect to the $\mathbb Y$ -marginal; and the passage from an a.e. identity to a smooth version of the density. The mixture, moment and entropy lemmas are reusable for any mean-field optimization problem. Contributions of any of these intermediate results, and of proofs of the milestones in any order, are welcome.

Selected references

G. Conforti, A. Kazeykina, Z. Ren, Game on random environment, mean-field Langevin system and neural networks, arXiv:2004.02457v2, 2020; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2004.02457v2
K. Hu, Z. Ren, D. Šiška, L. Szpruch, Mean-field Langevin dynamics and energy landscape of neural networks, arXiv:1905.07769, 2019. https://arxiv.org/abs/1905.07769
S. Mei, A. Montanari, P.-M. Nguyen, A mean field view of the landscape of two-layer neural networks, PNAS 115 (2018), E7665–E7671. https://doi.org/10.1073/pnas.1806579115
P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The master equation and the convergence problem in mean field games, arXiv:1509.02505, 2015. https://arxiv.org/abs/1509.02505
R. Jordan, D. Kinderlehrer, F. Otto, The variational formulation of the Fokker–Planck equation, SIAM J. Math. Anal. 29 (1998), 1–17. https://doi.org/10.1137/S0036141096303359

8 thms1 active userReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

“Sherlocking” and Platform Information Policy: The Full-Commitment Outcome Is Implementable by an Information Policy If and Only If the No-Entry Obedience Constraint (OC0) HoldsResearch Paper

Motivation

Large online marketplaces are hybrid platforms: they host third-party sellers and also sell their own products. Running the marketplace gives the platform access to sellers' sales data, and it can use that data to identify successful products and launch imitations of its own. The practice is colloquially called "Sherlocking". It has drawn regulatory attention: the European Commission's case against Amazon over the use of non-public seller data, and proposals to ban platforms from using such data or from competing with their own sellers at all.

Choi, Kim and Mukherjee (CESifo WP 10769 / SSRN 4643950, 2023; Management Science, 2025, doi:10.1287/mnsc.2024.05215) study the problem as a tension between the platform's fee, its entry decision and its information policy. The threat of imitation discourages sellers from joining, so a platform would like to commit not to imitate too aggressively. Commitment to an entry policy is rarely credible, but commitment to a data policy (what the product division is allowed to learn about a seller) is something a platform can build into its organization. The paper asks when the second kind of commitment is as good as the first.

Setting

A seller decides whether to join a marketplace run by a platform. Time has two periods of lengths $1-\delta$ and $\delta$ . The platform posts a referral fee $r\in[0,1]$ , a share of the seller's profit. The seller's type $\theta$ , his profit per unit time as a monopolist, is uniform on $[0,1]$ and known only to him; entry costs him $K$ . Assumption 1 is $1-\delta<K<\delta$ .

If the seller enters, the platform collects $r(1-\delta)\theta$ in the first period. At the start of the second period it may imitate at cost $K$ , taking the whole second-period profit $\delta\theta$ ; otherwise it collects $\delta r\theta$ . If the platform enters with probability $q$ , the entering seller's expected payoff is $[(1-\delta)+\delta(1-q)](1-r)\theta-K$ . Two cutoffs organize the analysis:

\theta_S(r)=\min\Big\{\frac{K}{1-r},1\Big\},\qquad \theta_P(r)=\min\Big\{\frac{K}{\delta(1-r)},1\Big\}.

The seller enters against a platform that never imitates iff $\theta\ge\theta_S(r)$ ; the platform gains from imitating type $\theta$ iff $\theta\ge\theta_P(r)$ .

Full commitment. If the platform could commit to an entry probability for each type, its optimal policy is to stay out on $[\theta_S(r),\theta_P(r))$ and to enter on $[\theta_P(r),1]$ with the largest probability that keeps the seller willing to enter,

\alpha(\theta;r)=\frac1\delta\Big(1-\frac{K}{(1-r)\theta}\Big).

Its value is $\Pi^C_P(r)$ , and $r^C$ denotes a fee maximizing $\Pi^C_P$ on $[0,1]$ . The resulting entry pattern is the full commitment outcome.

Information policy. Without commitment, the platform chooses an information policy: a set $X$ of realizations and a signal $\sigma(\theta)$ , a probability distribution on $X$ for each type. Its product division sees only the realization $x$ and then decides whether to imitate, in its own interest. The seller anticipates this. The solution concept is weak perfect Bayesian equilibrium. The full commitment outcome is implementable by an information policy if some signal has an equilibrium in which exactly the types in $[\theta_S(r),1]$ enter and the platform imitates type $\theta$ with probability $\alpha(\theta;r)$ on $[\theta_P(r),1]$ and $0$ below.

Under the binary signal (3), which reports $x=1$ with probability $\alpha(\theta;r)$ for $\theta\ge\theta_P(r)$ and $x=0$ otherwise, the platform obeys the recommendation "stay out" iff

\text{(OC0)}\qquad \mathbb E[\theta\mid x=0;\ \theta\ge\theta_S(r)]\le\theta_P(r).

Formalization targets

Goal: Proposition 3

For $r^C$ a maximizer of $\Pi^C_P$ on $[0,1]$ , the full commitment outcome at $r^C$ is implementable by an information policy if and only if (OC0) holds at $r=r^C$ , which is equivalent to

\int_{\theta_P(r^C)}^{1}(\theta-\theta_P(r^C))(1-\alpha(\theta;r^C))\,d\theta\ \le\ \int_{\theta_S(r^C)}^{\theta_P(r^C)}(\theta_P(r^C)-\theta)\,d\theta. \tag{4}

Milestones

The bounds $0\le\alpha(\theta;r)<1$ on $[\theta_P(r),1]$ and $0<\theta_S(r)\le\theta_P(r)\le1$ , and the monotonicity of $\theta_S,\theta_P,\alpha$ (§4).
The full-commitment policy solves the platform's §4 commitment problem at every fee, with value $\Pi^C_P(r)$ .
Lemma 1: every equilibrium outcome of any signal is the outcome of a binary signal with obedient play.
Signal (3) produces the full commitment outcome, is an equilibrium iff (OC0) holds, and always satisfies (OC1).
(OC0) is equivalent to (4) at every fee $r<1-K$ .

Significance

Proposition 3 gives a checkable condition under which information design substitutes for commitment to entry. When (4) holds, the platform obtains its full-commitment profit by restricting what its product division learns, and the seller faces the same entry threat as under full commitment. When (4) fails, the paper's Proposition 4 shows the platform must distort the outcome by excluding an interval of types. The comparison underlies the paper's policy conclusions about bans on data use and on imitation.

The result is proved in the paper; nothing in this mission is open mathematically. What the mission adds is a machine-checked development of a small information-design model: a formal revelation principle for this game (Lemma 1), with an equilibrium notion that handles a continuum of signal realizations, and a formal check that the integral conditions are equivalent. No part of the paper has been formalized before, to our knowledge.

Difficulty

The sufficiency direction is a computation with signal (3). The necessity direction is not: implementability quantifies over every signal space and every equilibrium, so (OC0), which is a property of one specific binary signal, has to be derived from an arbitrary equilibrium. The naive route of conditioning on each realization fails for a continuum of realizations, where conditional expectations are defined only almost everywhere and off-path behaviour is unconstrained. Separately, the goal is stated at the maximizer $r^C$ , and nothing in the hypotheses says directly that $r^C$ lies in the non-degenerate range $r^C<1-K$ , where some type enters.

Formalization scope

Everything is real-valued, in the namespace Sherlocking.InfoPolicy, with a single definitions module.

Cutoffs are written in guarded form ( $K/(1-r)$ if $K<1-r$ , else $1$ ), equal to the printed minimum for $r<1$ ; at $r=1$ this avoids Lean's $K/0=0$ .
Signals are a measurable map $\sigma$ from $\mathbb R$ to probability measures on any X : Type with a σ-algebra. Platform strategies are measurable maps $X\to[0,1]$ , the probability of imitating after each realization.
Equilibrium: the seller's conditions are pointwise for $\theta\in[0,1]$ , with either action allowed at indifference (the commitment outcome makes every type in $[\theta_P,1]$ exactly indifferent). The platform's sequential rationality is stated ex ante, as optimality against every measurable deviation, which is equivalent to Bayes-rational play after almost every on-path realization.
(OC0) and (OC1) are ratios of integrals over $[\theta_S(r),1]$ . Statements at a general fee assume $r<1-K$ , so that the conditioning event has positive probability.
Added hypotheses: $\delta<1$ throughout; $r<1-K$ in the general-fee milestones. The goal itself carries only Assumption 1, $\delta<1$ , $r^C\in[0,1]$ and maximality.

Implementability is never defined through (OC0) or through signal (3). It quantifies over all realization spaces, signals, strategies and entry sets, under the full equilibrium predicate; a definition that fixed the signal would make the necessity direction trivial.

A complete development needs interval and set integrals of bounded functions, measurability of kernels and parametric integrals, and the Giry monad on Bool, all available in Mathlib. The binary revelation argument is reusable for other sender–receiver models with a binary action. Proofs of any milestone are welcome, as are alternative proofs of Lemma 1.

Selected references

J. P. Choi, K. Kim, A. Mukherjee, “Sherlocking” and Platform Information Policy, CESifo Working Paper No. 10769, 2023. https://ssrn.com/abstract=4643950
J. P. Choi, K. Kim, A. Mukherjee, “Sherlocking” and Platform Information Policy, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.05215
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
D. Bergemann, S. Morris, Information Design: A Unified Perspective, Journal of Economic Literature 57(1), 2019. https://doi.org/10.1257/jel.20181489

8 thms1 active userReviewed

Operations Research Optimal Transport Optimization+1·Captain: mikedeng1

Distributionally Robust Linear and Discrete Optimization with Marginals: the worst-case expected optimal value over a Fréchet class equals its Lagrangian primal and dual formsResearch Paper

Motivation

Many decision problems in operations research end in a linear optimization over a finite set of alternatives whose objective coefficients are random: the longest path in a project network with random activity durations, a maximum-weight assignment or spanning tree with random weights, the best item in a ranking with random utilities. The quantity of interest is the expected optimal value $E[Z(\tilde c)]$ , where $Z(c) = \max_{x\in\mathcal X} c^T x$ . In practice the one-dimensional distributions of the coefficients $\tilde c_i$ can be estimated, while their dependence structure usually cannot. The marginal distribution model therefore asks for the largest expected optimal value over all joint distributions consistent with the given marginals, a distributionally robust bound that does not assume independence.

Chen, Ma, Natarajan, Simchi-Levi and Yan (Operations Research, 2022) study this bound for an arbitrary finite feasible set and arbitrary marginals.

Timeline. Meilijson and Nádas (1979) gave a convex formulation of the tight upper bound on the expected completion time of a PERT network when only the marginal distributions of the activity times are known. Bertsimas, Natarajan and Teo (2004) studied the analogous bound for 0–1 problems under marginal moment information. Natarajan, Song and Teo (Management Science 55(3), 2009) gave a concave maximization formula for the marginal distribution model when $\mathcal X$ consists of integer points and the marginals are absolutely continuous. The paper of this mission removes both restrictions: $\mathcal X$ is any finite point set, the marginals are arbitrary (discrete marginals allowed), and the bound is cast in Lagrangian primal and dual forms.

Setting

Fix $n \ge 0$ , a nonempty finite set $\mathcal X \subset \mathbb R^n$ , and probability measures $\mu_1,\dots,\mu_n$ on $\mathbb R$ . Write $\mathcal X_i = \{x_i : x\in\mathcal X\}$ for the coordinate projections of $\mathcal X$ .

The Fréchet class $\Gamma(\mu_1,\dots,\mu_n)$ is the set of probability measures $\theta$ on $\mathbb R^n$ whose $i$ -th one-dimensional marginal is $\mu_i$ for every $i$ .
$\mathcal P(\mathcal X)$ is the set of probability vectors $\nu$ on $\mathcal X$ . For $\nu\in\mathcal P(\mathcal X)$ , $\Pi_i\nu = \sum_{x}\nu(x)\delta_{x_i}$ is the law of the coordinate $x_i$ when $x\sim\nu$ .
For two laws $\mu,\nu$ on $\mathbb R$ , $\Gamma(\mu,\nu)$ is the set of couplings: probability measures on $\mathbb R^2$ with marginals $\mu$ and $\nu$ .
The Lagrangian of the problem, for functions $\psi_i : \mathcal X_i \to \mathbb R$ ("prices" on the coordinate values) and $\nu\in\mathcal P(\mathcal X)$ , is

L(\{\psi_i\}_i,\nu) = \sum_{i=1}^n\Big(\int\psi_i\,d\Pi_i\nu + \int\max_{x_i\in\mathcal X_i}\{c\,x_i - \psi_i(x_i)\}\,d\mu_i(c)\Big).

The quantile function is $F_\mu^{-1}(t) = \inf\{x : F_\mu(x) > t\}$ .

The value to be computed is

Z^* = \sup_{\theta\in\Gamma(\mu_1,\dots,\mu_n)} E_{\tilde c\sim\theta}\, Z(\tilde c).

The Lean development names these objects proj, Z, frechetClass, couplings, margMeasure ( $\Pi_i\nu$ ), conj (the inner maximum of $L$ ), lagrangian, quantile and quantileForm (the objective of (8)), all in MarginalDRO.Lagrange.

Formalization targets

Goal: Theorem 2 (Lagrange Form), p. 14

For marginals with finite variance and a nonempty finite $\mathcal X$ , with every optimum attained,

\max_{\theta\in\Gamma(\mu_1,\dots,\mu_n)} E_\theta Z = \max_{\nu\in\mathcal P(\mathcal X)}\sum_i\max_{\gamma_i\in\Gamma(\mu_i,\Pi_i\nu)}E_{\gamma_i}[\tilde c_i x_i] = \max_{\nu\in\mathcal P(\mathcal X)}\inf_{\{\psi_i\}}L(\{\psi_i\},\nu) = \min_{\{\psi_i\}}\sup_{\nu\in\mathcal P(\mathcal X)}L(\{\psi_i\},\nu).

Milestones

Kantorovich duality for the cost $c\,x$ on $\mathbb R\times\mathcal X_i$ , with the coupling maximum attained (proof of Theorem 2, pp. ec3–ec4).
Concavity and upper semicontinuity of $\nu\mapsto\max_{\gamma_i}E_{\gamma_i}[\tilde c_i x_i]$ on $\mathcal P(\mathcal X)$ (pp. ec3–ec4).
Lemma 1, the monotone coupling lemma for $h(x,y)=xy$ (pp. 13–14).
Theorem 3, the quantile form (p. 17):

\max_\theta E_\theta Z = \max_{\nu\in\mathcal P(\mathcal X)}\sum_i\sum_{x_i\in\mathcal X_i}x_i\int_{\Pi_i\nu((-\infty,x_i-e_i])}^{\Pi_i\nu((-\infty,x_i])}F_{\mu_i}^{-1}(t)\,dt .

The lower bound $\max_\theta E_\theta Z\ge\sum_i E_{\gamma_i}[\tilde c_i x_i]$ for couplings $\gamma_i\in\Gamma(\mu_i,\Pi_i\nu)$ (p. ec4).
A measurable selection of $\arg\max_{x\in\mathcal X}c^Tx$ (§3.1, p. 13).
The identity $E_\theta Z = \sum_i E_{\gamma_i}[\tilde c_i x_i]$ for $\nu=x^*\#\theta$ , $\gamma_i=(\mathrm{Proj}_i,x^*_i)\#\theta$ (p. ec4).
The exchange $\max_\nu\inf_\psi L=\inf_\psi\sup_\nu L$ (p. ec5).
Attainment of the dual infimum (p. ec5).

Significance

The result. Theorem 2 turns an optimization over joint distributions on $\mathbb R^n$ , an infinite-dimensional problem, into a saddle problem over probability vectors on $\mathcal X$ and univariate functions on the finite sets $\mathcal X_i$ . The dual form gives upper bounds on $Z^*$ from any choice of prices $\psi_i$ , and the primal form gives a worst-case joint distribution. The paper builds on it a compact reformulation (its §4) whenever $\mathcal X$ has a tractable description, and applications to appointment scheduling, robust maximum flow, ranking and project scheduling. Theorem 3 makes the primal side explicit as a concave program in the quantile functions, which holds for discrete marginals as well as continuous ones.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. The development needs pieces that are of independent use: Kantorovich duality for a signed, unbounded cost that is linear in one variable, the monotone (comonotone) coupling lemma, gluing of couplings along a common marginal, measurable selection of maximizers over a finite set, and a minimax exchange for a Lagrangian that is affine on a simplex and convex in an infinite family of functions. The ≥ step of the printed proof uses a product of couplings that does not give the inequality in general; a formal proof has to replace it by a gluing argument.

Difficulty

The obvious route to the first equality bounds $E_\theta Z$ from both sides by a joint law of $(\tilde c, x)$ . From above this needs a measurable optimal selection; from below it needs a joint law under which $x$ is a point of $\mathcal X$ and each pair $(\tilde c_i, x_i)$ has a prescribed coupling. Independent products of the couplings fail here, because their $x$ -coordinates no longer form a point of $\mathcal X$ . The Lagrangian equalities need duality for a cost $c\,x$ that is neither bounded nor of one sign, with $\mu_i$ supported on all of $\mathbb R$ , and attainment of the dual infimum over an unbounded family of potentials, which is invariant under the shifts $\psi_i\mapsto\psi_i+\alpha_i$ by arbitrary constants $\alpha_i$ and so has no compactness for free.

Formalization scope

$\mathcal X$ is a nonempty Finset (Fin n → ℝ); $\mathcal X_i$ is its coordinate projection; $\mathcal P(\mathcal X)$ is stdSimplex ℝ 𝒳, whose topology for finite $\mathcal X$ is the weak-* one.
The marginals are Measure ℝ with IsProbabilityMeasure. Finite variance is MemLp id 2. Lemma 1 and Theorem 3, which print no moment condition, assume a finite mean (Integrable id) so that every expectation is finite.
The functions $\psi_i$ are maps $\mathbb R\to\mathbb R$ ; only their values on $\mathcal X_i$ enter $L$ , and the inner maximum of $L$ runs over $\mathcal X_i$ . Potentials in the Kantorovich milestone are real-valued.
$\int\psi_i\,d\Pi_i\nu$ is written as $\sum_x\nu(x)\psi_i(x_i)$ . The lower limit $\Pi_i\nu((-\infty,x_i-e_i])$ of (8) is written $\Pi_i\nu((-\infty,x_i))$ , the same number since $\mathcal X_i$ is finite.
Every max and min is an attainment claim (IsGreatest, IsLeast); inner inf/sup are IsGLB/IsLUB. The quantile is a real infimum that takes the value $0$ outside $(0,1)$ , a null set for the integrals.
Lemma 1 is stated for $h(x,y)=xy$ and a finitely supported second law, sup half only. Theorem 3 is stated without its "persistence values" clause for absolutely continuous marginals.

The following formalizations would trivialize the goal and are excluded: $Z$ as a maximum over $\mathrm{conv}(\mathcal X)$ or $\mathbb R^n$ ; a class that fixes only some marginals; couplings without the second marginal $\Pi_i\nu$ ; a conjugate taken over $\mathbb R$ instead of $\mathcal X_i$ ; equalities decided by the default value of a real sSup/sInf; an empty $\mathcal X$ .

Welcome contributions: the monotone coupling lemma for general supermodular costs, Kantorovich duality on $\mathbb R\times F$ for finite $F$ , gluing of couplings, and proofs of any milestone.

Selected references

L. Chen, W. Ma, K. Natarajan, D. Simchi-Levi, Z. Yan, Distributionally Robust Linear and Discrete Optimization with Marginals, Operations Research 70(3), 2022. https://doi.org/10.1287/opre.2021.2243 (formalized from the 2018 author preprint).
K. Natarajan, M. Song, C.-P. Teo, Persistency Model and Its Applications in Choice Modeling, Management Science 55(3), 453–469, 2009.
I. Meilijson, A. Nádas, Convex Majorization with an Application to the Length of Critical Paths, Journal of Applied Probability 16(3), 671–677, 1979.
C. Villani, Optimal Transport: Old and New, Springer, 2009 (Theorem 5.10). https://doi.org/10.1007/978-3-540-71050-9
S. T. Rachev, L. Rüschendorf, Mass Transportation Problems, Vol. I, Springer, 1998 (Theorem 3.1.2). https://doi.org/10.1007/b98893

11 thms1 active userReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

On the Learning Benefits of Resource Flexibility: At the Break-Even Cost of Flexibility, the Flexible System Is More Profitable Below a Profit-Margin Threshold and Less Profitable Above ItResearch Paper

Motivation

A firm that sells several products must decide, before demand is known, how much capacity to build. It can build dedicated capacity, one resource per product, or a single flexible resource that can serve any product but costs more per unit. The classical argument for flexibility is risk pooling: one pooled resource absorbs the fluctuations of several demands, as studied by Fine and Freund (1990) and Van Mieghem (1998).

Chod, Markakis and Trichakis (SSRN 3212177, published in Management Science, 2021) identify a second, independent benefit. A firm usually observes its sales, not its demand: when a product stocks out, the firm learns only that demand exceeded capacity. This is demand censoring. Because flexible capacity can be shifted to whichever product is in demand, it stocks out less often for each product, and so the firm learns more about demand from a flexible system than from a dedicated one. When demand is correlated over time, that information is worth money in later periods. The paper calls this the learning benefits of flexibility and asks when they are positive.

To separate learning from pooling, the paper compares the two systems at the break-even cost of flexibility, the unit cost of flexible capacity at which both systems earn the same profit in a single period. Any difference that remains in a two-period model is then due to learning alone (Eq. (14) of the paper).

Setting

There are two products with a common unit price $p$ . Dedicated capacity costs $c$ per unit and flexible capacity costs $c_F$ per unit, with $0 \le c < p$ . The first-period demands $D^1_1, D^1_2$ are independent and each uniform on $[x, x+U]$ , with $x \ge 0$ and $U > 0$ . The profit margin is $(p-c)/p$ .

Static model. With dedicated capacities $\mathbf Q = (Q_1, Q_2)$ , product $i$ sells $\min\{D_i, Q_i\}$ , and the expected profit is $\pi_N(\mathbf Q) = p\,\mathbb E[\min\{D_1,Q_1\} + \min\{D_2,Q_2\}] - c(Q_1+Q_2)$ . With flexible capacity $Q_F$ , product 1 is served first: it sells $S_{F,1} = \min\{D_1, Q_F\}$ and product 2 sells $S_{F,2} = \min\{D_2, Q_F - S_{F,1}\}$ ; the expected profit is $\pi_F(c_F)(Q_F) = p\,\mathbb E[S_{F,1} + S_{F,2}] - c_F Q_F$ . The optimal static profits are

\bar\pi_N = \sup_{\mathbf Q \in \mathbb R^2_+} \pi_N(\mathbf Q), \qquad \bar\pi_F(c_F) = \sup_{Q_F \ge 0} \pi_F(c_F)(Q_F),

and $c_F$ is a break-even cost when $\bar\pi_F(c_F) = \bar\pi_N$ .

Learning. A product that had $q$ units available and demand $d$ reveals $d$ exactly if $d < q$ ; otherwise the firm learns only that $D \ge q$ and conditions its prior on that event. The firm's belief after period 1 is the product of the two products' posteriors. In period 2 demand repeats ( $D^2_i = D^1_i$ ), and both systems build dedicated capacity against the posterior belief $\mathbb G$ , earning

V^2(\mathbb G) = \sup_{\mathbf Q \in \mathbb R^2_+} \mathbb E_{\mathbb G}\big[p\min\{D_1,Q_1\} + p\min\{D_2,Q_2\} - c(Q_1+Q_2)\big].

The two-period optimal profits are

V_N = \sup_{\mathbf Q \in \mathbb R^2_+} \Big(\pi_N(\mathbf Q) + \mathbb E\big[V^2(\mathbb P(\cdot \mid \mathbf S^1_N))\big]\Big), \qquad V_F(c_F) = \sup_{Q_F \ge 0} \Big(\pi_F(c_F)(Q_F) + \mathbb E\big[V^2(\mathbb P(\cdot \mid \mathbf S^1_F))\big]\Big).

Formalization targets

Goal: Proposition 1

Take $x = 0$ . There is a threshold $\zeta \in (0,1)$ such that for all $p, c, U, c_F$ with $0 \le c < p$ , $U > 0$ , $c \le c_F < p$ and $\bar\pi_F(c_F) = \bar\pi_N$ ,

\frac{p-c}{p} \le \zeta \implies V_F(c_F) \ge V_N, \qquad \frac{p-c}{p} > \zeta \implies V_F(c_F) \le V_N.

The goal fixes no numerical value of $\zeta$ ; the paper reports $\zeta \approx 0.5904$ .

Milestones

Lemma 3: the uniform newsvendor optimum $\bar Q = x + U(p-c)/p$ with profit $(p-c)x + \tfrac U2 (p-c)^2/p$ .
The static non-flexible optimum $\bar\pi_N = 2(p-c)x + U(p-c)^2/p$ .
The static flexible optimum $\bar Q_F(c_F)$ , $\bar\pi_F(c_F)$ in the two branches $p \ge 2c_F$ and $p < 2c_F$ .
Eq. (8): the pooling benefits $\bar\pi_F(c_F) - \bar\pi_N$ are strictly decreasing in $c_F$ , and the break-even cost exists and is unique in $[c, p)$ .
The two-period non-flexible optimum: $V_N = 4x(p-c) + U(p-c)^2(3c+2p)/\Delta$ with $\Delta = (p-c)(p+c) + cp$ .
The flexible case $Q_F \ge 2x + U$ : concavity, the right derivative $(-c^2 + cp + p(p-2c_F))/(2p)$ at $2x+U$ , and the price threshold $\tilde p$ .

Significance

Proposition 1 says that learning favours flexibility when margins are low or moderate and favours dedicated capacity when margins are high. Combined with the risk-pooling analysis, it shows that the value of flexibility in a dynamic setting is not captured by static pooling models: a firm choosing a technology by comparing single-period profits misjudges it in both directions, depending on the margin. The comparison at the break-even cost is the cleanest available measurement of the information value of a capacity structure under censored demand.

The paper proves Proposition 1 by computing closed forms of all the value functions and then certifying a polynomial inequality over a semialgebraic parameter set with sum-of-squares methods (p. A8). No machine-checked proof exists. A formalization would replace a computer-algebra certificate whose details are not printed with a checked argument, and would fix the value-function closed forms (milestones 2–6), which the paper derives in a few lines each. The milestones are of independent use: Lemma 3 and the censored-sales posterior are standard in inventory learning models.

Difficulty

The value functions $V_N$ and $V_F(c_F)$ are suprema of first-period profit plus the expectation of a second-period value under a posterior that depends on whether each product stocked out. In the flexible system the capacity left for product 2 depends on product 1's realized demand, so the posterior of product 2 depends on product 1's demand, and the objective $v_F$ splits into regimes with different formulas; it is not concave in general (the paper notes "optimization of non-concave functions", p. 12). The break-even cost is defined implicitly by an equation involving square roots, so the final comparison is between two functions of $(p, c)$ along an implicit curve; the obvious approach of comparing closed forms branch by branch needs a sign certificate for a polynomial system rather than a one-line inequality.

Formalization scope

Everything is real-valued. The uniform prior is $U^{-1}$ times Lebesgue measure on $[x, x+U]$ ; the joint prior is the product measure. The stock-out posterior is Mathlib's conditional measure cond of the prior on $\{D \ge q\}$ , an exact observation is a Dirac measure, and a demand is observed exactly iff it is strictly below the available capacity (p. 9). The joint posterior is the product of the per-product posteriors, which is exact because the observation is a product event given product 1's demand. All optima are real suprema of images over nonnegative capacities, never closed forms. The symmetric case of §3 is built in ( $p_1 = p_2 = p$ , common $c$ , i.i.d. uniform demands), as is $\xi = 0$ (second-period demand equals first-period demand); at $x = 0$ the paper's noise $U[-\xi x, \xi x]$ is zero for every $\xi$ , so the goal loses nothing. Added hypotheses, disclosed in each statement: $U > 0$ , $0 \le c < p$ , $c \le c_F < p$ , and in the goal $0 < \zeta < 1$ .

The values must not be defined by their closed forms or by the paper's case split $j = 1, 2, 3$ ; that would make the goal a statement about polynomials rather than about the Bellman problems.

A complete development needs: integrals of piecewise-linear functions against uniform laws and their products, conditional uniform laws, measurability of the posterior-dependent second-period value, and a sign certificate for the final polynomial comparison. The newsvendor and censored-posterior lemmas are reusable in other inventory-learning models. Contributions are welcome on any milestone, on alternative proofs of the final comparison, and on the regime $j = 3$ of the flexible objective, which the milestones do not cover.

Selected references

J. Chod, M. G. Markakis, N. Trichakis, On the Learning Benefits of Resource Flexibility, SSRN preprint 3212177 (December 6, 2019); published in Management Science, 2021. https://ssrn.com/abstract=3212177, https://doi.org/10.1287/mnsc.2020.3795
C. H. Fine, R. M. Freund, Optimal Investment in Product-Flexible Manufacturing Capacity, Management Science 36(4), 1990. https://doi.org/10.1287/mnsc.36.4.449
J. A. Van Mieghem, Investment Strategies for Flexible Resources, Management Science 44(8), 1998. https://doi.org/10.1287/mnsc.44.8.1071
P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming 96, 2003. https://doi.org/10.1007/s10107-003-0387-5

8 thms1 active userReviewed

Machine Learning Optimization Reinforcement Learning·Captain: mikedeng1

Neural Temporal-Difference and Q-Learning Provably Converge to Global Optima: Neural TD with Stochastic Semigradients Converges to the Global Optimum of the MSPBE at Rate 1/√TResearch Paper

Why neural temporal-difference learning needs a convergence theory

Temporal-difference (TD) learning estimates the value of a policy in a Markov decision process from sampled transitions, by repeatedly moving a parametrized value function towards a one-step bootstrapped target (Sutton, 1988). With a linear parametrization its behaviour is well understood: TD converges to the fixed point of the projected Bellman equation (Tsitsiklis and Van Roy, 1997), with finite-sample rates for projected and stochastic variants (Bhandari, Russo and Singal, 2018). With a nonlinear parametrization the same update can diverge: Tsitsiklis and Van Roy (1997) give an example, and the TD direction is not the gradient of any objective. Deep reinforcement learning nonetheless runs TD with neural networks as a matter of course.

Cai, Yang, Lee and Wang (arXiv:1905.10027v2, Mathematics of Operations Research, 2024) prove that TD with an overparametrized two-layer ReLU network, projected onto a ball around its random initialization, converges at rate $T^{-1/2}$ to the global optimum of the mean-squared projected Bellman error (MSPBE) over a function class that becomes richer as the width grows. This mission formalizes that theorem for the stochastic-semigradient algorithm (Theorem 4.6 of the paper).

Setting

Transitions are tuples $(x, r, x')$ drawn i.i.d. from a sampling law $\mu$ : $x, x' \in \mathbb R^d$ are feature vectors of the current and next state–action pair, with $\|x\|_2 = \|x'\|_2 = 1$ , the reward satisfies $|r| \le \bar r$ , and $x$ and $x'$ have the same distribution (they are drawn from the stationary distribution of the policy). The discount factor is $0 \le \gamma < 1$ and $d \ge 3$ .

The value function is the two-layer network

\widehat Q(x; W) = \frac{1}{\sqrt m}\sum_{r=1}^m b_r\,\sigma(W_r^\top x), \qquad \sigma(y) = \max\{0, y\},

of width $m$ , with hidden weights $W = (W_1, \dots, W_m) \in \mathbb R^{md}$ and output weights $b \in \mathbb R^m$ . At initialization $b_r \sim \mathrm{Unif}\{-1, 1\}$ and $W_r(0) \sim N(0, I_d/d)$ , all independent; only $W$ is trained. The training set is the ball $S_B = \{W : \|W - W(0)\|_2 \le B\}$ .

Algorithm 1 (neural TD) samples a tuple at each step $t = 0, \dots, T-2$ , forms the Bellman residual $\delta = \widehat Q(x; W(t)) - r - \gamma \widehat Q(x'; W(t))$ , takes the semigradient step $W(t) - \eta\,\delta\,\nabla_W \widehat Q(x; W(t))$ , projects it onto $S_B$ , and outputs $\widehat Q_{\mathrm{out}} = \widehat Q(\cdot\,; \overline W)$ with $\overline W = \frac1T \sum_{t=0}^{T-1} W(t)$ .

The linearization of the network at initialization is

\widehat Q_0(x; W) = \frac{1}{\sqrt m}\sum_{r=1}^m b_r\,\mathbb 1\{W_r(0)^\top x > 0\}\, W_r^\top x,

a linear function of $W$ with random features. Writing $\delta_0$ for the Bellman residual of $\widehat Q_0$ , an approximate stationary point is a $W^* \in S_B$ with

\mathbb E_\mu\big[\delta_0(x, r, x'; W^*)\,\nabla_W \widehat Q_0(x; W^*)\big]^\top (W - W^*) \ge 0 \quad \text{for all } W \in S_B .

The function $\widehat Q_0(\cdot\,; W^*)$ solves the projected Bellman equation over the class $\mathcal F_{B,m} = \{\widehat Q_0(\cdot\,; W) : W \in S_B\}$ . The regularity condition (Assumption 4.3) asks for $c_0 > 0$ with $\mu(|w^\top x| \le \tau) \le c_0 \tau$ for every unit vector $w$ and every $\tau \ge 0$ .

Formalization targets

Goal: Theorem 4.6

With $\eta = \min\{(1-\gamma)/8,\ 1/\sqrt T\}$ and under Assumption 4.3, there is a constant $C = C(c_0, d, \bar r, \gamma)$ such that for all $m \ge 1$ , $B \ge 1$ , $T \ge 1$ and every approximate stationary point $W^*$ ,

\mathbb E_{\mathrm{init},\mu}\Big[\big(\widehat Q_{\mathrm{out}}(x) - \widehat Q_0(x; W^*)\big)^2\Big] \le \frac{16\,(B^2 + \sigma_g^2)}{(1-\gamma)^2\sqrt T} + C\big(B^3 m^{-1/2} + B^{5/2} m^{-1/4}\big),

where $\sigma_g^2 = 12 + 12B^2 + 3\bar r^2$ and the expectation is over the initialization, the samples of the run and a fresh $x \sim \mu$ .

Milestones

Lemma 4.2: approximate stationary points exist for every initialization; $\widehat Q_0(\cdot\,; W^*)$ is unique $\mu$ -a.e. and is the MSPBE optimum over $\mathcal F_{B,m}$ .
Lemmas H.1, H.2: the expected fraction of hidden units whose activation can flip inside $S_B$ is $O(B m^{-1/2})$ , alone and weighted by $\mathbb E_\mu[\widehat Q(x; W(0))^2]$ .
Lemmas 5.1, 5.2: the network and its population semigradient stay within $O(B^3 m^{-1/2})$ (in mean square) of their linearizations, for every random parameter in $S_B$ .
Lemma 4.5: the stochastic semigradient has variance at most $\sigma_g^2$ .
(C.16): the linearized population semigradient is monotone with modulus $1-\gamma$ in the $\mu$ -norm.
Lemma 5.4: the stochastic descent inequality for $\mathbb E\|W(t) - W^*\|_2^2$ .

Significance

The theorem gives a non-asymptotic guarantee for TD with a nonlinear function class, a setting in which the algorithm can diverge without further structure. The limit object $\widehat Q_0(\cdot\,; W^*)$ is a projected Bellman fixed point over a class that, as $m \to \infty$ , approaches a ball in the reproducing kernel Hilbert space of the neural tangent kernel; the paper uses this to bound the distance to the true value function $Q^\pi$ (Proposition 4.7) and to analyze neural Q-learning and policy gradient methods (Section 6). The argument is an instance of the "lazy training" or neural-tangent-kernel regime, in which an overparametrized network trained from a random initialization stays close to its linearization.

The result is proved in the paper and, to our knowledge, has no machine-checked proof. A formalization would also produce reusable components: Gaussian anti-concentration of random ReLU activation patterns (Lemmas H.1–H.2), the linearization error of wide two-layer networks (Lemma 5.1), and a projected stochastic-approximation template with averaged iterates. The appendix proofs are short and pass over several measure-theoretic steps (conditioning on the current iterate, independence of the samples from the initialization, Jensen for the averaged iterate), which a formal proof has to supply.

Difficulty

The TD update is not a gradient, so the convergence proof cannot be a descent argument on an objective. The paper's route is to compare the update with that of the linear TD problem defined by $\widehat Q_0$ , whose population semigradient is monotone, and to control the difference by overparametrization. The obvious first approach, linearizing the network in a deterministic neighbourhood of $W(0)$ , fails: the ReLU activation pattern $\mathbb 1\{W_r^\top x > 0\}$ can change for some units whatever $m$ is. The comparison holds only in expectation over the random initialization and a fresh input, through Assumption 4.3 and the finiteness of $\mathbb E\,\|w\|_2^{-2}$ for $w \sim N(0, I_d/d)$ , which is where $d \ge 3$ enters. The iterates and $W^*$ depend on the initialization, so these bounds are needed for random parameters that are correlated with $W(0)$ but independent of the evaluation point.

Formalization scope

Lean represents points as EuclideanSpace ℝ (Fin d) and parameters as PiLp 2 over Fin m, so all norms on $\mathbb R^{md}$ are $\ell_2$ . The MDP, the policy and the feature map are not modelled; the statements see only the sampling law $\mu$ on tuples $(x, r, x')$ with the properties listed above. The run's samples form an $\mathbb N$ -indexed i.i.d. sequence (product measure) independent of the initialization, and the evaluation tuple is a fresh draw. Expectations of nonnegative quantities are lower Lebesgue integrals, so non-integrability cannot make a bound hold vacuously. The ReLU semigradient uses the strict convention $\mathbb 1\{W_r^\top x > 0\}$ and keeps the factor $m^{-1/2}$ of (3.2).

Conventions and readings fixed by the formalization, all disclosed in the item statements:

the paper's " $\sigma_g^2 = O(B^2)$ " is pinned to the value $12 + 12B^2 + 3\bar r^2$ produced by its proof;
the paper's $O(B^3 m^{-1/2} + B^{5/2} m^{-1/4})$ is a constant $C$ depending only on $(c_0, d, \bar r, \gamma)$ and chosen before $m$ , $B$ , $T$ , $\mu$ and $W^*$ , with $B \ge 1$ so that lower powers of $B$ are absorbed;
approximate stationary points are required to lie in $S_B$ , as the proof uses;
Lemmas 5.1 and 5.2 are posed for every random parameter in $S_B$ (the paper's proofs need nothing else and apply them to $\overline W$ );
Lemma 5.4 carries the coefficient $4\eta B$ , which is what its proof establishes ( $\|W(t) - W^*\|_2 \le 2B$ ), in place of the printed $2\eta B$ .

A formalization in which the comparison point $W^*$ may lie outside $S_B$ , the expectation is a Bochner integral of a possibly non-integrable function, or the constant $C$ may depend on $m$ , $T$ or $\mu$ , would not express the theorem and is excluded. Approximate stationary points are compared through $\widehat Q_0(\cdot\,; W^*)$ , never through $\widehat Q(\cdot\,; W^*)$ .

A complete development needs Gaussian measures on $\mathbb R^d$ with the integrability of $\|w\|_2^{-2}$ for $d \ge 3$ , product and infinite-product probability measures with conditioning on the past of a sequence, existence of solutions to variational inequalities on compact convex sets, and nonexpansiveness of Euclidean projection onto a ball. Proofs of individual milestones are welcome independently; Lemmas H.1, 5.1 and (C.16) are self-contained.

Selected references

Q. Cai, Z. Yang, J. D. Lee, Z. Wang, Neural temporal-difference and Q-learning provably converge to global optima, Mathematics of Operations Research, 2024; arXiv:1905.10027v2. https://arxiv.org/abs/1905.10027
R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 1988. https://doi.org/10.1007/BF00115009
J. N. Tsitsiklis, B. Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
J. Bhandari, D. Russo, R. Singal, A finite time analysis of temporal difference learning with linear function approximation, COLT 2018. https://arxiv.org/abs/1806.02450
A. Jacot, F. Gabriel, C. Hongler, Neural tangent kernel: convergence and generalization in neural networks, NeurIPS 2018. https://arxiv.org/abs/1806.07572

10 thms1 active userReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Tracking Truth with Liquid Democracy: Upward Delegation Satisfies Probabilistic Do No Harm and Positive GainResearch Paper

Motivation

Liquid democracy lets each voter either vote directly or delegate the vote to another voter, who may delegate it further. It has been used in practice, for example by the German Pirate Party on the LiquidFeedback platform and in the Google Votes experiment, and has been studied in computational social choice as a way to give more weight to better-informed voters. A natural worry is that delegation concentrates power: if too many votes flow to a few voters, the outcome rests on those few judgements and the "wisdom of the crowd" of independent votes is lost. Kahng, Mackenzie and Procaccia (Journal of Artificial Intelligence Research, 2021) showed that no local delegation mechanism can guarantee, for every instance, that liquid democracy is never worse than direct voting and sometimes strictly better.

Berinsky, Halpern, Halpern, Jadbabaie, Mossel, Procaccia and Revel (arXiv:2107.11868v3; Management Science, 2025) replace the worst-case requirement by a probabilistic one: competencies and delegations are random, and the comparison is made with high probability as the number of voters grows. Their first main result, Theorem 1, concerns the simplest model in which delegation goes only upward in competence. It is the goal of this mission.

Setting

There are $n$ voters $[n]$ deciding a binary question with a correct answer. Voter $i$ has a competence $p_i\in[0,1]$ , the probability that its own vote is correct; given $\vec p_n=(p_1,\dots,p_n)$ , the votes $V_i\sim\mathrm{Bern}(p_i)$ are independent, with law $\mathbb P_{\vec p_n}$ .

A delegation graph $G_n$ is a directed graph on $[n]$ in which every voter has at most one outgoing edge, the voter it delegates to. A voter $i$ who votes directly has weight $\mathrm{weight}_i(G_n)=1+{}$ (the number of voters whose delegation chain ends at $i$ ); a delegating voter has weight $0$ ; voters on a delegation cycle, or delegating into one, are not counted. $\text{max-weight}(G_n)$ is the largest weight. Direct democracy gets $X^D_n=\sum_i V_i$ correct votes and liquid democracy $X^F_{G_n}=\sum_i\mathrm{weight}_i(G_n)V_i$ . The gain of the instance $(\vec p_n,G_n)$ is

\mathrm{gain}(\vec p_n,G_n)=\mathbb P_{\vec p_n}[X^F_{G_n}>n/2]-\mathbb P_{\vec p_n}[X^D_n>n/2].

A model $M=(q,\varphi)$ consists of $q:[0,1]\to[0,1]$ and $\varphi:[0,1]^2\to\mathbb R_{\ge0}$ . Competencies are drawn i.i.d. from a distribution $\mathcal D$ supported in $[0,1]$ ; then each voter $i$ independently keeps its vote with probability $1-q(p_i)$ and otherwise delegates to some $j\ne i$ with probability proportional to $\varphi(p_i,p_j)$ (and keeps its vote if all these weights vanish). This defines the law $\mathbb P_{\mathcal D,M,n}$ of the random instance.

$M$ satisfies probabilistic do no harm with respect to a class $\mathfrak D$ if for every $\mathcal D\in\mathfrak D$ and all $\varepsilon,\delta>0$ , eventually $\mathbb P_{\mathcal D,M,n}[\mathrm{gain}\ge-\varepsilon]>1-\delta$ (Definition 1).
$M$ satisfies probabilistic positive gain with respect to $\mathfrak D$ if for some $\mathcal D\in\mathfrak D$ and all $\varepsilon,\delta>0$ , eventually $\mathbb P_{\mathcal D,M,n}[\mathrm{gain}\ge1-\varepsilon]>1-\delta$ (Definition 2).

The Upward Delegation Model $M^U_p$ has $q\equiv p$ and $\varphi(x,y)=\mathbb 1\{y>x\}$ : each voter delegates with probability $p$ , to a strictly more competent voter chosen uniformly. $\mathfrak D^C$ is the class of continuous distributions on $[0,1]$ .

The proof runs through the infinite Pólya urn with attachment probability $p$ : at time $1$ there is one ball in one bin; each new ball opens a new bin with probability $1-p$ and otherwise joins an existing bin with probability proportional to its size. $L^p_t$ is the largest bin size at time $t$ .

Formalization targets

Goal: Theorem 1

For every $p\in(0,1)$ ,

M^U_p\ \text{satisfies probabilistic do no harm and probabilistic positive gain with respect to}\ \mathfrak D^C.

Milestones

The milestones are the statements the paper's proof uses, in attack order:

(14): $\mathrm{gain}(\vec p_n,G_n)\ge-\mathbb P_{\vec p_n}[X^D_n>X^F_{G_n}]$ for every instance.
Lemma 1 (core lemma): if every $\mathcal D\in\mathfrak D$ has $\alpha\in(0,1)$ and $C(n)\in o(n)$ with

\mathbb P_{\mathcal D,M,n}[\text{max-weight}(G_n)\le C(n)]=1-o(1),\quad \mathbb P_{\mathcal D,M,n}\Big[\textstyle\sum_i\mathrm{weight}_i(G_n)p_i-\sum_ip_i\ge2\alpha n\Big]=1-o(1),

then $M$ satisfies probabilistic do no harm. If moreover some $\mathcal D$ satisfies $\sum_ip_i+\alpha n\le n/2\le\sum_i\mathrm{weight}_i(G_n)p_i-\alpha n$ with probability $1-o(1)$ , it satisfies probabilistic positive gain.

(5): the bin $W^{(k)}$ born at time $k$ has $\mathbb E[W^{(k)}_n]=\Gamma(n+p)\Gamma(k)/(\Gamma(p+k)\Gamma(n))$ .
Domination: $W^{(k)}_t$ stochastically dominates the $k$ -th bin $U^{(k)}_t$ .
Early and late bins: for $3/4<\gamma<1$ and $p+(1-p)\gamma<\delta<1$ , $\sum_{k\le T^\gamma}\Pr[W^{(k)}_T>T^\delta]=o(1)$ and $\sum_{T^\gamma<k\le T}\Pr[W^{(k)}_T>T^\delta]=o(1)$ .
Lemma 2: there is $\delta<1$ with $\Pr[L^p_T\le T^\delta]=1-o(1)$ .
Urn coupling: under $M^U_p$ and a continuous $\mathcal D$ , the component sizes of $G_n$ have the law of the urn's bin sizes after $n$ steps, so $\text{max-weight}(G_n)$ has the law of $L^p_n$ .
Conditions (2) and (3) for $M^U_p$ (Appendix B.3): (2) for every $\mathcal D\in\mathfrak D^C$ ; (3) for some $\mathcal D\in\mathfrak D^C$ .

Significance

Theorem 1 shows that the impossibility result of Kahng et al. is an artefact of worst-case analysis: under a simple and natural random model, liquid democracy is asymptotically no worse than majority vote for every continuous competence distribution, and strictly better for some. Lemma 1 is the paper's general tool: it reduces both properties to two checkable conditions, a sub-linear largest weight and a linear increase of the expected number of correct votes, and is reused for the paper's two other models (Theorems 2 and 3). Lemma 2, a sub-linear bound on the largest bin of the infinite Pólya urn (the Simon–Yule preferential-attachment process), is of independent interest in random-structure theory.

The results are proved in the paper. None of them is formalized; Prove2Me has no liquid-democracy, delegation-graph or infinite-urn item. A formal development adds a checked version of the core lemma for arbitrary models, and a formal treatment of the urn that the later models' arguments can be compared with. Several steps of the paper are terse (the late-bin bound rests on a cited convergence rate; the arithmetic of Appendix B.3 is loose), so a checked proof adds more than a transcription.

Difficulty

The obvious argument — liquid democracy moves votes to better voters, so it should do at least as well — fails because concentration is lost when weights become large: if one voter carries a constant fraction of the votes, $X^F_{G_n}$ no longer concentrates, and the majority can be wrong with constant probability even though the expected number of correct votes rises. The heart of Theorem 1 is therefore Lemma 2, a bound $L^p_T\le T^\delta$ with $\delta<1$ on the largest bin of an infinite Pólya urn. A first-moment bound on each bin handles the bins born before time $T^\gamma$ , but the union bound over the remaining bins needs each to exceed $T^\delta$ with probability $o(1/T)$ , which first moments do not give. The coupling between the urn and $M^U_p$ needs the competencies to be distinct, which is where continuity of $\mathcal D$ enters.

Formalization scope

All declarations live in the namespace LiquidDemocracy.Upward, in two definition files (Setting, Urn) and one file per theorem, against the platform's default Mathlib.

Voters are Fin n; a delegation graph is a map g : Fin n → Fin n with g i = i meaning "votes directly". A voter's weight counts the voters whose chain, followed $n$ steps, ends at it; chains running into a cycle reach no direct voter, which implements the cycle convention.
$\mathbb P_{\vec p_n}$ is a finite sum over the $2^n$ vote vectors; both majorities are strict ( $>n/2$ ).
The instance law $\mathbb P_{\mathcal D,M,n}$ is a measure on competence vectors and graphs, built as a finite sum over graphs of $\mathcal D^{\otimes n}$ with the density given by the delegation probabilities; no push-forward along a non-measurable map occurs.
$\mathfrak D^C$ is the set of atomless probability measures on $\mathbb R$ giving $[0,1]^c$ measure $0$ ("continuous distribution" read as continuous CDF).
The urn and $W^{(k)}$ are measures built step by step with Measure.bind; bins are numbered from $1$ , time $t$ means $t$ balls, and the step into time $t$ divides by $t-1$ .
" $=1-o(1)$ " is convergence to $1$ ; $C(n)\in o(n)$ is =o[atTop]; Definitions 1–2 keep the paper's $\varepsilon,\delta,n_0$ form. In Lemma 1 the model is assumed typed as on p. 10 and measurable.

A trivializing formalization is excluded: the instance law is a probability measure for $M^U_p$ and $\mathfrak D^C$ is nonempty (the uniform distribution on $[0,1]$ belongs to it), both checked sorry-free, so neither property holds vacuously or fails for a degenerate reason.

A complete development needs Hoeffding's and Chebyshev's inequalities (in Mathlib), Gautschi's inequality for Gamma ratios, a coupling argument for stochastic domination of Markov chains, and the conditional-independence structure of the instance law. The urn results and Lemma 1 are reusable beyond this mission. Contributions to any milestone are welcome, including alternative proofs of the late-bin bound (for instance by second-moment recursions instead of the cited Beta-limit rate).

Selected references

A. J. Berinsky, D. Halpern, J. Y. Halpern, A. Jadbabaie, E. Mossel, A. D. Procaccia, M. Revel, Tracking Truth with Liquid Democracy, Management Science, 2025; arXiv:2107.11868v3. https://arxiv.org/abs/2107.11868v3
A. Kahng, S. Mackenzie, A. D. Procaccia, Liquid Democracy: An Algorithmic Perspective, Journal of Artificial Intelligence Research 70:1223–1252, 2021.
H. A. Simon, On a Class of Skew Distribution Functions, Biometrika 42, 1955. https://doi.org/10.1093/biomet/42.3-4.425
F. Chung, S. Handjani, D. Jungreis, Generalizations of Pólya's Urn Problem, Annals of Combinatorics 7(2):141–153, 2003.
W. Gautschi, Some Elementary Inequalities Relating to the Gamma and Incomplete Gamma Function, Journal of Mathematics and Physics 38(1):77–81, 1959. https://doi.org/10.1002/sapm195938177

13 thms1 active userReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Surge Pricing and Its Spatial Supply Response: Within an Attraction Region, Supply Fills the Congestion Bound Outward from the Sink at Locally Optimal Prices Without Loss of RevenueResearch Paper

Spatial pricing on ride-hailing platforms

Ride-hailing platforms change prices by location in real time, and drivers respond by moving. A price increase at one location changes where drivers go, how congested each location becomes, and therefore what every driver earns everywhere else. Besbes, Castro and Lobel, Surge Pricing and its Spatial Supply Response (SSRN 3124571, version of May 17, 2019; later published in Management Science, DOI 10.1287/mnsc.2020.3622), model this as a platform choosing prices over a continuous two-dimensional city, with non-atomic drivers who then relocate in equilibrium. Earlier work on ride-hailing pricing took space into account only in reduced form (e.g. Castillo, Knoepfle and Weyl, EC 2017) or on a finite network (Bimpikis, Candogan and Saban, Operations Research 2019). The platform's problem in this model is an infinite-dimensional optimization problem with equilibrium constraints. The paper's main result, the goal of this mission, characterizes optimal prices and supply locally, inside the regions drivers move into.

This mission formalizes that result from the SSRN preprint of May 17, 2019. Its online appendix contains the proofs, and every page and label cited here refers to it.

Setting

The city $\mathcal C\subseteq\mathbb R^2$ is convex and compact. It carries a finite city measure $\Gamma$ , a finite potential demand measure $\Lambda$ and a finite initial supply measure $\Theta$ , all concentrated on $\mathcal C$ , with $\Lambda,\Theta\ll\Gamma$ . The demand density is $\lambda=d\Lambda/d\Gamma$ , which is positive $\Gamma$ -a.e. At location $y$ the riders' willingness to pay has CDF $F_y$ , strictly increasing on its support $[0,\bar V]$ , with $\bar F_y=1-F_y$ and a continuous, unimodal revenue curve $q\mapsto q\bar F_y(q)$ . The driver receives a fraction $\alpha\in(0,1)$ of each fare.

The platform chooses a measurable price mapping $p:\mathcal C\to[0,\bar V]$ . Drivers relocate according to a flow $\mathcal T$ , a measure on $\mathcal C\times\mathcal C$ with first marginal $\Theta$ and second marginal $\mathcal T_2\ll\Gamma$ . The post-relocation supply is $s^{\mathcal T}=d\mathcal T_2/d\Gamma$ . A driver who ends at $y$ is matched with probability $R=\min\{1,\lambda(y)\bar F_y(p(y))/s^{\mathcal T}(y)\}$ (with conventions at zero supply), earns $U(y,p(y),s^{\mathcal T}(y))=\alpha\,p(y)\,R$ , and pays travel cost $\|y-x\|$ when coming from $x$ . The best utility available from $x$ is the $\Gamma$ -essential supremum

V(x\mid p,\mathcal T)=\operatorname*{ess\,sup}_{y\in\mathcal C}\big(U(y,p(y),s^{\mathcal T}(y))-\|y-x\|\big).

$\mathcal T$ is a supply equilibrium if almost every driver goes to a destination attaining this value. Problem (P2) maximizes $\gamma\int_{\mathcal C}V(x\mid p,\mathcal T)\,s^{\mathcal T}(x)\,d\Gamma(x)$ , with $\gamma=(1-\alpha)/\alpha$ , over price–equilibrium pairs; the paper shows (P2) is equivalent to maximizing platform revenue.

A single location run as a capacitated monopoly with supply $s$ has revenue $R^{loc}_x(s)=\max_{q\in[0,\bar V]}q\min\{s,\lambda(x)\bar F_x(q)\}$ and optimal price $\rho^{loc}_x(s)$ . The congestion function $\psi_x(s)=\alpha R^{loc}_x(s)/s$ , with $\psi_x(0)=\alpha\bar V$ , is the utility per driver at that location. The indifference region of $x$ is $\mathcal{IR}(x)=\{y\in\mathcal C:V(y)-\|y-x\|=V(x)\}$ . The attraction region of $z$ is $A(z\mid p,\mathcal T)=\{x\in\mathcal C:z\in\mathcal{IR}(x)\}$ . The point $z$ is a sink if $A(z)\neq\emptyset$ and $z\notin A(z')$ for every $z'\neq z$ . Along each ray $a$ from $z$ , $X_a(z\mid p,\mathcal T)$ is the last point of $A(z)$ .

Formalization targets

Goal: Theorem 1 (p. 18)

For every feasible $(p,\mathcal T)$ of (P2) and every sink $z$ , there are a feasible $(\hat p,\hat{\mathcal T})$ with at least the same (P2) value, points $r_a\in[z,X_a(z\mid p,\mathcal T)]$ and numbers $s_a\ge0$ , such that on $A(z\mid p,\mathcal T)$

s^{\hat{\mathcal T}}(x)=\begin{cases}\psi_x^{-1}\big(V(z\mid p,\mathcal T)-\|x-z\|\big)&x\in\bigcup_a[z,r_a),\\ s_a&x=r_a,\\0&\text{otherwise},\end{cases}\qquad \hat p(x)=\begin{cases}\rho^{loc}_x(s^{\hat{\mathcal T}}(x))&x\notin\bigcup_a\{r_a\},\\ p_a&x=r_a,\end{cases}

where $U(r_a,p_a,s_a)=V(r_a\mid p,\mathcal T)$ .

Milestones

In order: Lemma 1 (p. 13, $V_B$ is 1-Lipschitz); Lemma A-1 (bounds $[-H,\alpha\bar V]$ on $V_B$ ; $V\ge0$ on the support of $\Gamma$ ); Lemma A-2 (equilibrium utilities); Lemma A-3 ( $\psi_x$ strictly decreasing); Proposition 2 (p. 15, the congestion bound $V(x)\le\psi_x(s^{\mathcal T}(x))$ $\Gamma$ -a.e.); Lemma B-2 (indifference propagates along segments); Lemma B-1 (attraction regions are closed unions of segments $[z,X_a]$ ); Lemma B-3 (positive flow contains an indifferent pair); Proposition B-1 (flow separation at the endpoints and at the sink); Proposition B-2 (pasting a local equilibrium into an attraction region).

Significance

Theorem 1 shows that, within any attraction region, an optimal solution has a simple structure. Supply is filled ray by ray outward from the sink up to the congestion bound, and each location is priced as a local monopolist given its supply. It reduces the platform's infinite-dimensional problem with equilibrium constraints to a choice of one cutoff point per ray. In the paper it is an ingredient of the explicit global solution of the one-dimensional demand-shock family of §8 (Theorem 3).

The result is proved in the paper (Appendix C). None of it has been formalized. A formal proof would check a long measure-theoretic argument (Appendix C, about nine pages) that works with densities, essential suprema and a.e. statements throughout. The milestones are smaller results with short proofs, and are self-contained targets.

Difficulty

The goal is an existence statement over flows, so the new equilibrium $\hat{\mathcal T}$ must be constructed and its equilibrium property checked. Changing supply inside $A(z)$ changes utilities at every location whose drivers could move there. The supply and prices therefore cannot be optimized pointwise and pasted back without controlling flows that cross the boundary of the region. Matching the drivers available in $A(z)$ to the congestion bound along each ray must work for an arbitrary finite $\Gamma$ , which may have atoms or be concentrated on curves. Every density identity holds only $\Gamma$ -a.e., and the region boundaries $\bigcup_a\{X_a\}$ or $\bigcup_a\{r_a\}$ can carry positive measure.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). The paper says "a norm", but the ray geometry of Appendix B needs a strictly convex one. Measures are measures on $\mathbb R^2$ concentrated on $\mathcal C$ , and flows are measures on $\mathbb R^2\times\mathbb R^2$ . Densities are Radon–Nikodym derivatives converted to reals, so every pointwise claim about $s^{\mathcal T}$ , $\lambda$ or prices built from them is stated $\Gamma$ -a.e. $V_B$ is the Mathlib essSup with respect to $\Gamma|_B$ ; it is finite under the standing assumptions, so no boundedness hypothesis is added. Rays are indexed by unit vectors.

The standing assumptions of §3.1 are one hypothesis, Market.Standing, of every theorem. It contains: convex compact city; finite measures concentrated on it, with $\Lambda,\Theta\ll\Gamma$ ; $\bar V>0$ ; $0<\alpha<1$ ; $F_y$ a CDF supported on $[0,\bar V]$ and strictly increasing there; continuous, unimodal revenue; $\lambda>0$ $\Gamma$ -a.e.; joint measurability of $(y,q)\mapsto F_y(q)$ . The last assumption and the CDF properties are implicit in the paper and are added openly. A sanity file shows that these assumptions hold for a one-point city.

In Theorem 1, $\psi_x^{-1}(v)$ is written as $\psi_x(s^{\hat{\mathcal T}}(x))=v$ . The supply cases are read in the printed order at the sink. Prices $\rho^{loc}_x$ come from (5), so $\rho^{loc}_x(0)=\bar V$ . In Proposition B-1, the printed $\bigcup_a[z,X_a$ is read as the half-open $\{z\}\cup\bigcup_a[z,X_a)$ used in its proof. Proposition B-2 adds $\Gamma(A)>0$ , the precondition of Definition 3.

Two formalizations would make the goal trivial, and both are excluded. Dropping the equilibrium condition from feasibility would let any flow "dominate". Taking $V$ as a pointwise supremum or $s^{\mathcal T}$ as a free function would decouple the objective from the flow. Feasibility includes Definition 1, $V$ is an essential supremum, and $s^{\mathcal T}$ is the density of the flow.

Contributions welcome: proofs of the milestones, general lemmas on essential suprema of Lipschitz families, and general measure-theoretic results about finite planar measures and rays from a point, which can be reused outside this mission.

Selected references

O. Besbes, F. Castro, I. Lobel, Surge Pricing and its Spatial Supply Response, SSRN 3124571, version of May 17, 2019. https://ssrn.com/abstract=3124571 (published: Management Science, 2021, https://doi.org/10.1287/mnsc.2020.3622)
K. Bimpikis, O. Candogan, D. Saban, Spatial pricing in ride-sharing networks, Operations Research, 2019. https://doi.org/10.1287/opre.2018.1800
J. C. Castillo, D. Knoepfle, G. Weyl, Surge pricing solves the wild goose chase, Proceedings of EC, 2017, pp. 241–242. https://doi.org/10.1145/3033274.3085098
L. Ambrosio, A. Pratelli, Existence and stability results in the L¹ theory of optimal transportation, in Optimal Transportation and Applications, Springer LNM 1813, 2003, pp. 123–160. https://doi.org/10.1007/978-3-540-44857-0_5

12 thms1 active userReviewed

Algorithmic Game Theory Economics Linear Optimization+1·Captain: mikedeng1

Fully Polynomial-Time Approximation Schemes for Fair Rent Division: Algorithm 1 on the Slope-Rounded Instance Halts in Polynomially Many Iterations with an ε-Envy-Free SolutionResearch Paper

Fair rent division beyond quasilinear utilities

Housemates who share a house must decide who gets which room and how the total rent is split. A solution pairs an assignment of rooms to agents with a rent for each room, and it is envy-free if no agent prefers another room at that room's rent. Envy-free rent division is the textbook example of fair division with money and is the mathematical core of two-sided matching markets with transfers, where an envy-free solution is a competitive equilibrium.

For quasilinear utilities (a room's value minus its rent) envy-free solutions are computed by an assignment problem and a linear program (Aragones, 1995), and this method is in practical use. Real preferences are often not quasilinear: an agent may have a budget, or be less sensitive to rent at low prices. Existence of envy-free solutions for general continuous, decreasing utilities was established by Svensson (1983) and by Alkan, Demange and Gale (1991), whose perturbation lemma lowers the rents of an envy-free solution while keeping it envy-free. Alkan (1989) gave an algorithm that finds an equilibrium in finite time, with no polynomial bound. Arunachaleswaran, Barman and Rathi (arXiv:1807.04163; Mathematics of Operations Research, 2022) give the first fully polynomial-time approximation scheme for continuous, decreasing piecewise-linear utilities. They also show that the exact problem lies in PPAD ∩ PLS.

Setting

There are $n$ agents and $n$ rooms. Agent $a$ 's utility for room $r$ at rent $x\ge0$ is $v_a(r,x)$ , given by a base value $v_a(r,0)$ (of either sign), break points $0=b_1<b_2<\dots<b_t$ and slope magnitudes $\lambda_1,\dots,\lambda_t>0$ , so that $v_a(r,\cdot)$ is continuous, strictly decreasing and linear with slope $-\lambda_i$ on $[b_i,b_{i+1}]$ (the last piece is unbounded). The total number of pieces is $\ell$ , and $\beta$ bounds $|\log\lambda|$ over all slopes. A solution $(\pi,p)$ is a bijection $\pi$ from agents to rooms and a rent vector $p$ . It is envy-free if $v_a(\pi(a),p_{\pi(a)})\ge v_a(r,p_r)$ for all $a,r$ . For $\varepsilon>0$ it is $\varepsilon$ -EF (Definition 2) if every agent with nonnegative utility satisfies $(1+\varepsilon)\,v_a(\pi(a),p_{\pi(a)})\ge v_a(r,p_r)$ for all $r$ , and every agent with negative utility satisfies $v_a(\pi(a),p_{\pi(a)})\ge(1+\varepsilon)\,v_a(r,p_r)$ for all $r$ .

Algorithm 1 works on a modified instance $\hat{\mathcal I}$ : above a threshold $M$ with $v_a(r,M)<v_a(r',0)$ for all $a,r,r'$ , every utility is continued with slope $1$ (equation (1)). It starts from any envy-free solution of $\hat{\mathcal I}$ with all rents at least $M$ . While all rents are positive it (i) takes a maximum-weight perfect matching $\pi^{i}$ of the first-choice graph at $p^{i-1}$ , with the weight of edge $(a,r)$ equal to $\log$ of the current slope of $v_a(r,\cdot)$ ; (ii) sets $p^{i}$ to a minimum-total-rent solution of the linear program that keeps $\pi^i$ envy-free, keeps the rents nonnegative, and keeps them inside the current linear domain (the box of rents between consecutive slope changes, Definition 1).

The approximation scheme rounds every slope up to a power of $(1+\varepsilon)$ , $\bar\lambda=(1+\varepsilon)^{\lceil\log_{1+\varepsilon}\lambda\rceil}$ . Each piece is replaced by two pieces of slopes $\bar\lambda/(1+\varepsilon)$ and $\bar\lambda$ that meet the original function at the piece's end points, after the zero of each utility has been made a break point. The resulting instance is $\bar{\mathcal I}$ .

Formalization targets

Goal: Theorem 2 (p. 9, restated p. 18)

There is a constant $c$ such that for every instance with $n\ge1$ , every $\varepsilon\in(0,1)$ and every admissible threshold $M$ for $\bar{\mathcal I}$ , Algorithm 1 run on $\bar{\mathcal I}$

has a run that halts;
halts in every run after at most

T\le c\,(n+\ell+\beta+1/\varepsilon+1)^c

iterations, whatever Step 2 solution, matchings and LP optima are chosen; 3. outputs rents $p^T\ge0$ such that $(\pi^T,p^T)$ is an $\varepsilon$ -EF solution of the original instance.

The polynomial is left unspecified; the paper's proof gives a small explicit one, and any polynomial establishes the scheme.

Milestones

The proof has two halves. Theorem 1 (p. 9, proof pp. 13–14) is the same statement with "envy-free" in place of " $\varepsilon$ -EF" for any instance whose slopes are already powers of $(1+\varepsilon)$ . It rests on Lemma 16 (quasilinear envy-free allocations are the maximum-weight matchings), Lemma 18 (its multiplicative form), the perturbation Lemma 2, the run invariants Lemmas 3–5 and the per-domain count (3), $|S|\le 6\beta n/\varepsilon$ . Lemma 9 (p. 17) states that every envy-free solution of $\bar{\mathcal I}$ with nonnegative rents is $\varepsilon$ -EF for the original instance, through Lemmas 6–8 on the rounded functions.

Significance

Theorem 2 gives an efficient algorithm for approximately fair rent division under general piecewise-linear utilities: budgets, rent-sensitive valuations and concave utilities. Exact envy-free solutions for this class are only known to lie in PPAD ∩ PLS. Because envy-free solutions are equilibria of unit-demand markets with money, the theorem also yields approximate equilibria for such markets with non-quasilinear utilities. Theorem 1 gives an exact polynomial algorithm whenever slopes are powers of $(1+\varepsilon)$ .

The result is proved in the paper. None of it has been machine-checked: there is no formal model of envy-free rent division, of the perturbation lemma, or of a price-descent algorithm of this kind in Mathlib or on the platform. A complete development would give a checked proof that a fair-division algorithm terminates within a polynomial number of iterations with a fairness guarantee.

Difficulty

Envy-freeness of the output is not the hard part: every iterate of Algorithm 1 is envy-free for $\hat{\mathcal I}$ by construction, and the rounding lemmas are elementary inequalities on single pieces. The difficulty is termination with a polynomial bound. Lowering rents by the perturbation lemma alone need not stop: Alkan gives an instance in which the perturbations do not converge. A bound has to control how many iterations the algorithm spends inside one linear domain and how many domains it visits. The first count fails for arbitrary slopes, where up to $n!$ matchings of distinct weight can occur in one domain; the power-of- $(1+\varepsilon)$ structure is what the rounding provides. The perturbation lemma is also needed in the form of Lemma 2, for every maximum-weight matching of the weighted first-choice graph, not only for one matching it produces. A formal proof must further show that each step can be carried out: the matching exists and each linear program attains its minimum.

Formalization scope

Representation. A utility is a base value and a list of (start, slope) pieces. Standing requires first start $0$ , strictly increasing starts and positive slopes. Agents and rooms are Fin n, allocations are Equiv.Perm (Fin n), rents are real. $\log$ is the natural logarithm. $\beta$ bounds $|\log\lambda|$ and stands in for the bit complexity of the slopes. Base values may be negative.
The run. Algorithm 1 is a predicate on sequences $(\pi^i,p^i)$ . Every choice the pseudocode leaves open (the Step 2 solution, the maximum-weight matching, the LP optimum) is quantified universally in the bound and the output guarantee. Halting means some rent is $\le0$ . Only the number of while-iterations is bounded. The cost of one iteration (computing $\bar{\mathcal I}$ and $M$ , a matching, a linear program) and the bit length of the input are not formalized.
Conventions. Linear-domain boundaries are the break points where some slope actually changes, plus the rent $0$ . Below rent $0$ (used only by Lemma 2, whose rents may be negative) each utility continues its first piece. The paper describes the rounding only for bounded pieces. The unbounded last piece is rounded down to slope $\bar\lambda/(1+\varepsilon)$ ; after the zero split its utility is nonpositive, and this choice keeps Lemmas 6, 7 and 9 true. Lemmas 6 and 9 are stated for nonnegative rents, the paper's convention for solutions. Lemma 7 (d), (e) are stated on the open piece, because the printed closed-interval form fails at an end point equal to the zero of the utility. Lemma 4 and (3) assume the next iteration exists, which the page takes for granted. $n\ge1$ and $\varepsilon\in(0,1)$ are assumed where the paper assumes them.
Ruled out. The goal is about Algorithm 1 run on the explicitly constructed $\bar{\mathcal I}$ . The bare existence of an $\varepsilon$ -EF solution (which follows from exact existence theorems) does not establish it, and the constant $c$ is fixed before the instance.
Infrastructure. Piecewise-linear functions on lists of pieces, assignment duality for permutations (Lemmas 16 and 18) and existence of optima of linear programs over closed sets are reusable beyond this mission. Proofs of any milestone are welcome, and so are independent proofs of Lemma 16 from LP duality.

Selected references

E. R. Arunachaleswaran, S. Barman, N. Rathi, Fully Polynomial-Time Approximation Schemes for Fair Rent Division, arXiv:1807.04163v1, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1807.04163
A. Alkan, G. Demange, D. Gale, Fair allocation of indivisible goods and criteria of justice, Econometrica 59(4):1023–1039, 1991 (reference [ADG91] of the paper above).
A. Alkan, Existence and computation of matching equilibria, European Journal of Political Economy, 1989 (reference [Alk89]).
E. Aragones, A derivation of the money Rawlsian solution, Social Choice and Welfare 12(3):267–276, 1995 (reference [Ara95]).
L.-G. Svensson, Large indivisibles: an analysis with respect to price equilibrium and fairness, Econometrica 51(4):939–954, 1983 (reference [Sve83]).

14 thms1 active userReviewed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Inner Moreau Envelope of Nonsmooth Conic Chance-Constrained Optimization Problems: Optimal Values and Solutions of the Moreau-Regularized Problems Converge to Those of the Original ProblemResearch Paper

Motivation

A chance constraint asks that a random inequality system hold with at least a prescribed probability $p$ . Such constraints appear throughout engineering and energy optimization: reservoir and power-system management, network design, and any decision that must stay feasible against uncertain demand or inflow with high reliability. The function $x\mapsto\mathbb P(\text{constraint holds at }x)$ is called a probability function. It is in general neither convex nor smooth, even when the underlying random inequality is convex in the random vector, and this is what makes chance-constrained problems hard to solve with standard nonlinear-programming methods.

One remedy is to replace the probability function by a regular approximation and to solve a sequence of approximate problems. van Ackooij, Pérez-Aros, Soto and Vilches (arXiv:2301.09803, Mathematics of Operations Research, 2024) propose an inner regularization built from the Moreau envelope of a scalarized constraint function, for conic constraints in infinite-dimensional decision spaces. The approximate feasible sets contain the original one, and the approximate problems have smooth data. A regularization is useful only if solving the approximate problems recovers the original problem in the limit. This mission formalizes that consistency statement, Theorem 5.4 of the paper.

Setting

Let $\mathcal H$ be a separable real Hilbert space (the decision space), $\mathcal Y$ a real Banach space with dual $\mathcal Y^*$ , and $\xi:\Omega\to\mathbb R^m$ a random vector on a probability space $(\Omega,\mathbb P)$ whose law has a density with respect to Lebesgue measure. A continuous map $\Phi:\mathcal H\times\mathbb R^m\to\mathcal Y$ and a nonempty closed convex cone $\mathcal K\subseteq\mathcal Y$ define the probability function

\varphi(x)=\mathbb P\big(\omega:\Phi(x,\xi(\omega))\in-\mathcal K\big).

The conic constraint is scalarized by a convex, weak $^*$ -compact set $\mathcal C\subseteq\mathcal Y^*$ whose generated cone has weak $^*$ closure equal to the positive polar cone $\mathcal K^+=\{v^*:\langle v^*,v\rangle\ge0\ \forall v\in\mathcal K\}$ . A convex, continuously differentiable $h:\mathcal H\to\mathbb R$ is assumed to make every scalarization $(x,z)\mapsto\langle v^*,\Phi(x,z)\rangle+h(x)$ , $v^*\in\mathcal C$ , jointly convex. The supremum function is $S^h_\Phi(x,z)=\sup_{v^*\in\mathcal C}\{\langle v^*,\Phi(x,z)\rangle+h(x)\}$ .

For $\lambda>0$ and $\psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ , the Moreau envelope is $\mathrm e_\lambda\psi(x)=\inf_z\{\psi(z)+\frac1{2\lambda}\|x-z\|^2\}$ . The inner regularization of $\varphi$ is

\varphi_\lambda(x)=\mathbb P\big(\omega:\mathrm e_\lambda S^h_\Phi(x,\xi(\omega))\le h(x)\big),

the envelope being taken on $\mathcal H\times\mathbb R^m$ with the Hilbert norm. For $p\in[0,1]$ put $M(p)=\{x:\varphi(x)\ge p\}$ and $M_\lambda(p)=\{x:\varphi_\lambda(x)\ge p\}$ . Given a proper, convex, lower semicontinuous objective $\psi$ , problem (P) minimizes $\psi$ over $M(p)$ and the regularized problem (Pλ) minimizes $\mathrm e_\lambda\psi$ over $M_\lambda(p)$ , with optimal values $v(P)$ and $v(P_\lambda)$ .

Formalization targets

Goal: Theorem 5.4 (p. 21)

If $\psi$ is moreover coercive and $M(p)\cap\operatorname{dom}\psi\neq\emptyset$ , then

v(P),\ v(P_\lambda)\in\mathbb R\ \ (\lambda>0),\qquad v(P_\lambda)\xrightarrow[\lambda\to0^+]{}v(P),

and for $\lambda_k\to0^+$ and optimal solutions $x_k$ of $(P_{\lambda_k})$ with $x_k\rightharpoonup x_0$ , the point $x_0$ is optimal for (P). If moreover $\operatorname{dom}\psi=\mathcal H$ and $\psi^*$ is Fréchet differentiable on $\operatorname{dom}\partial\psi^*$ , then $x_k\to x_0$ in norm.

Milestones

Proposition 2.1 a), c) (p. 5): $\mathrm e_\lambda g\nearrow g$ as $\lambda\searrow0$ , and $g(x)\le\liminf_k\mathrm e_{\lambda_k}g(x_k)$ for $x_k\rightharpoonup x$ , $\lambda_k\searrow0$ .
Proposition 2.6 (p. 8): $\varphi(x)=\mathbb P(S^h_\Phi(x,\xi)\le h(x))$ .
Theorem 3.1 a), b), d) (p. 9): $\inf_{\lambda>0}\varphi_\lambda=\varphi$ monotonically; $\limsup_k\varphi_{\lambda_k}(x_k)\le\varphi(x)$ ; weak upper semicontinuity of $\varphi$ and $\varphi_\lambda$ .
Proposition 5.1 (p. 19): $M_\lambda(p)\to M(p)$ in the Painlevé–Kuratowski sense, and in the Mosco sense when $h$ is sequentially weakly continuous.

Significance

Theorem 5.4 justifies the regularization as a solution method: optimal values converge, and weak limits of regularized optimal solutions solve the original problem, with strong convergence under a smoothness condition on $\psi^*$ . Combined with the paper's differentiability results for $\varphi_\lambda$ (§4, not part of this mission), it reduces a nonsmooth chance-constrained problem to a sequence of problems with smooth data whose solutions approximate the true ones. The intermediate results (monotone convergence of $\varphi_\lambda$ , the limsup estimate, convergence of feasible sets) are reusable for any analysis of envelope-based approximations of probability functions.

All statements are proved in the paper. None of them, and none of the general facts used (monotone and lower epi-convergence of Moreau envelopes in Hilbert space, Painlevé–Kuratowski and Mosco convergence), has a machine-checked proof on the platform at the time of writing. The mission produces a formal account of the conic scalarization, of the inner regularization, and of the consistency argument.

Difficulty

The obvious approach, "the regularized feasible sets converge, the regularized objectives converge, hence the minima converge", fails in two places. First, the decision space is infinite-dimensional, so bounded minimizing sequences only converge weakly, and the probability function must be controlled along weakly convergent sequences. This requires weak upper semicontinuity of $\varphi$ and a limsup estimate for $\varphi_{\lambda_k}(x_k)$ along weakly convergent $x_k$ , which do not follow from continuity of $\Phi$ . Second, convergence of values needs a liminf inequality for $\mathrm e_{\lambda_k}\psi(x_k)$ along weakly convergent sequences together with Mosco, not merely Painlevé–Kuratowski, convergence of the feasible sets. The probability function is not convex, so the usual convex-analytic route to Mosco convergence is unavailable.

Formalization scope

The Lean development uses H with [InnerProductSpace ℝ H] [CompleteSpace H] [SeparableSpace H], Y a real Banach space with dual StrongDual ℝ Y, and weak $^*$ notions through WeakDual ℝ Y. Extended-valued functions ( $\psi$ , $\mathrm e_\lambda\psi$ , $S^h_\Phi$ , $\psi^*$ , $v(P)$ , $v(P_\lambda)$ ) are EReal-valued, and infima and suprema are taken there, so no default value enters. Probabilities are ℝ≥0∞-valued. The product $\mathcal H\times\mathbb R^m$ carries the ℓ² norm (WithLp 2), as the paper requires. Weak convergence is defined through inner products. The limit $\lambda\to0^+$ is the filter of right neighbourhoods of $0$ for values and positive sequences for solutions and feasible sets.

The definitions file contains $\mathrm e_\lambda$ , $\Gamma_0$ , coercivity, conjugate, subdifferential, Fréchet differentiability of an extended-valued function, weak convergence, sequential weak continuity, Painlevé–Kuratowski and Mosco convergence, the conic setting (9)–(10), $S^h_\Phi$ , $\varphi$ , $\varphi_\lambda$ , $M(p)$ , $M_\lambda(p)$ , $v(P)$ , $v(P_\lambda)$ and optimality for (P) and (Pλ).

Two hypotheses are added to the printed statements, each used by the paper's own proofs: $\mathcal K$ is closed (the bipolar step of Proposition 2.6), and $h$ is sequentially weakly continuous in Theorem 3.1 d) and throughout Theorem 5.4. The second is automatic when $\mathcal H$ is finite-dimensional. Both are disclosed in the statements.

Trivializing readings are excluded: the feasible set meets $\operatorname{dom}\psi$ ; $\psi$ is proper; the envelope uses the Hilbert, not the sup, norm on the product; $S^h_\Phi$ is an extended-real supremum over a nonempty set, not a real supremum with a default value; every $\lambda$ is positive. Item b) of the goal is vacuous only when some regularized problem has no optimal solution, exactly as in the paper.

Contributions welcome: Moreau-envelope convergence in Hilbert space, the bipolar theorem for closed convex cones in Banach spaces, measure-theoretic continuity arguments for $\varphi_\lambda$ , and the existence argument for optimal solutions of (P).

Selected references

W. van Ackooij, P. Pérez-Aros, C. Soto, E. Vilches, Inner Moreau envelope of nonsmooth conic chance constrained optimization problems, Mathematics of Operations Research, 2024; arXiv:2301.09803v1, 2023. https://arxiv.org/abs/2301.09803
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

10 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

On Optimality Conditions for Nonlinear Conic Programming: Under the Generalized Łojasiewicz Inequality, Feasible Limit Points of the Augmented Lagrangian Method Satisfy CAKKTResearch Paper

Motivation

Nonlinear conic programming covers nonlinear programming (NLP), nonlinear semidefinite programming (NLSDP) and nonlinear second-order cone programming (NSOCP) in one model: minimize a smooth objective subject to the requirement that a smooth map takes values in a closed convex cone. The classical first-order necessary condition, the Karush–Kuhn–Tucker (KKT) condition, holds at a local minimizer only under a constraint qualification such as Robinson's, and for conic constraints such qualifications are restrictive and hard to check.

Sequential optimality conditions avoid this. They require only that approximate KKT points exist along a sequence converging to the candidate, and they hold at every local minimizer with no constraint qualification. They are also what practical algorithms actually produce, since an algorithm only ever stops at an approximate point. For NLP, AGP was introduced by Martínez and Svaiter (2003) and CAKKT by Andreani, Martínez and Svaiter (2010); Andreani, Haeser and Martínez (2011) compare the sequential conditions. R. Andreani, W. Gómez, G. Haeser, L. M. Mito and A. Ramos (Mathematics of Operations Research, 2022) extend AGP and CAKKT to general conic programs, by means of projections onto the cone and its polar. They then show that a safeguarded augmented Lagrangian method generates sequences satisfying them. This mission formalizes that convergence theory (Section 4 of the paper).

Setting

Let $f:\mathbb R^n\to\mathbb R$ and $G:\mathbb R^n\to\mathbb E$ be continuously differentiable, where $\mathbb E$ is a finite-dimensional real inner product space. Let $\mathcal K\subseteq\mathbb E$ be a nonempty closed convex cone, and consider

\min_{x\in\mathbb R^n} f(x)\quad\text{subject to}\quad G(x)\in\mathcal K. \qquad\text{(NCP)}

A point $\bar x$ is feasible if $G(\bar x)\in\mathcal K$ . The polar cone is $\mathcal K^\circ=\{w:\langle w,k\rangle\le0\ \forall k\in\mathcal K\}$ . For a closed convex set $C$ , $\Pi_C(w)$ denotes the orthogonal projection of $w$ onto $C$ (its nearest point). $DG(x)^*$ is the adjoint of the derivative of $G$ at $x$ .

A feasible $\bar x$ satisfies AGP (Approximate Gradient Projection) if there are sequences $x^k\to\bar x$ and $\Lambda^k\in\mathcal K^\circ$ with

\nabla f(x^k)+DG(x^k)^*\Lambda^k\to0,\qquad \langle\Lambda^k,\Pi_{\mathcal K}(G(x^k))\rangle\to0 .

It satisfies CAKKT (Complementary Approximate KKT) if moreover, on the same sequences, $\langle\Lambda^k,\Pi_{\mathcal K^\circ}(G(x^k))\rangle\to0$ .

The augmented Lagrangian is $L_\rho(x,\Lambda)=f(x)+\frac\rho2\big[\|\Pi_{\mathcal K^\circ}(G(x)+\Lambda/\rho)\|^2-\|\Lambda/\rho\|^2\big]$ for $\rho>0$ . Algorithm 1 takes positive tolerances $\varepsilon_k\to0$ , a nonempty convex compact safeguarding set $\mathcal B\subset\mathcal K^\circ$ , and constants $\tau>1$ , $\sigma\in(0,1)$ , $\rho_0>0$ . At step $k$ it:

finds $x^k$ with $\|\nabla_xL_{\rho_k}(x^k,\hat\Lambda^k)\|\le\varepsilon_k$ ;
sets $\Lambda^k=\rho_k\Pi_{\mathcal K^\circ}(G(x^k)+\hat\Lambda^k/\rho_k)$ and picks any $\hat\Lambda^{k+1}\in\mathcal B$ ;
forms $V^k=\hat\Lambda^k/\rho_k-\Pi_{\mathcal K^\circ}(G(x^k)+\hat\Lambda^k/\rho_k)$ ;
keeps $\rho_{k+1}=\rho_k$ if $\|V^k\|\le\sigma\|V^{k-1}\|$ and otherwise picks any $\rho_{k+1}\ge\tau\rho_k$ .

A point $\bar x$ and a function $\Psi$ satisfy the generalized Łojasiewicz inequality if, for some $\delta>0$ and some $\psi$ continuous on $B(\bar x,\delta)$ with $\psi(x)\to0$ as $x\to\bar x$ ,

|\Psi(x)-\Psi(\bar x)|\le\psi(x)\,\|D\Psi(x)\|\quad\text{for all }x\in B(\bar x,\delta). \tag{28}

Formalization targets

Goal: Theorem 4.2

If $\bar x$ is a feasible limit point of a sequence $\{x^k\}$ generated by Algorithm 1, and $\bar x$ satisfies (28) for $\Psi(x)=\tfrac12\|\Pi_{\mathcal K^\circ}(G(x))\|^2$ , then

\bar x\ \text{satisfies CAKKT}.

Milestones

Nonexpansiveness of $\Pi_{\mathcal K}$ , and formula (1): $D(\operatorname{dist}^2_{\mathcal K})(w)=2(w-\Pi_{\mathcal K}(w))$ (p. 3).
Formula (20): $\nabla_xL_\rho(x,\Lambda)=\nabla f(x)+DG(x)^*\big(\rho\,\Pi_{\mathcal K^\circ}(G(x)+\Lambda/\rho)\big)$ (p. 8).
The Step 4 dichotomy: $\rho_k\to\infty$ , or $\rho_k$ is eventually constant and $\|V^k\|\to0$ (p. 9).
With bounded $\rho_k$ : $\Lambda^k-\hat\Lambda^k\to0$ and $\{\Lambda^k\}$ is bounded (proof of Theorem 4.1).
Theorem 4.1: every feasible limit point of Algorithm 1 satisfies AGP, with no further assumption (p. 9).
With unbounded $\rho_k$ and (28): $\rho_k\|\Pi_{\mathcal K^\circ}(G(x^k))\|^2\to0$ along the subsequence converging to $\bar x$ (proof of Theorem 4.2).

Significance

Theorem 4.1 shows that the augmented Lagrangian method, with no constraint qualification at all, produces AGP points. AGP was previously the condition behind inexact restoration methods, so this puts the two method families on a common footing. Theorem 4.2 adds the complementarity limit (18) under the generalized Łojasiewicz inequality. Every analytic function satisfies that inequality. For NLSDP the theorem refines the earlier guarantee that such methods generate TAKKT sequences. Combined with the paper's result that every local minimizer is a CAKKT point, it says the algorithm's limit points pass a necessary optimality test that is sharper than AGP. The theory allows cones with empty interior or without self-duality, such as the cone of Euclidean distance matrices.

The results are proved on paper. No machine-checked version is known. Formalizing them needs a working theory of projections onto closed convex cones in finite-dimensional inner product spaces: existence, nonexpansiveness, Moreau's decomposition, and the differentiability of the squared distance. It also needs derivative calculus for the augmented Lagrangian. These are reusable well beyond this paper, by any later formalization of conic optimization algorithms.

Difficulty

The algorithm is stated with free choices at every step, so nothing about it can be computed. Everything has to come from the inequalities that define a run. The main obstacle is the case of an unbounded penalty parameter in Theorem 4.2. In that case the multipliers $\Lambda^k$ may diverge, and it is not clear why $\langle\Lambda^k,\Pi_{\mathcal K^\circ}(G(x^k))\rangle$ should vanish. Without (28) it need not: the paper points to a counterexample in which the method produces sequences that are not CAKKT. The bounded case needs instead the observation that the Step 4 test forces $V^k\to0$ once the penalty stops growing. The calculus milestones depend on the differentiability of $\operatorname{dist}^2_{\mathcal K}$ , which is not in Mathlib in this form.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $\mathbb E$ is any finite-dimensional real inner product space.
$f$ and $G$ are ContDiff ℝ 1.
Cone, polar cone and nearest point come from the published definition MoreauProx.Decomposition.Cones. The polar uses the sign $\le0$ .
$\Pi_C(w)$ is a nearest point chosen by choice, with a default of $0$ . The default is never reached for the nonempty closed convex sets $\mathcal K$ and $\mathcal K^\circ$ .
$DG(x)^*$ is the adjoint of fderiv ℝ G x, and $\nabla f$ is Mathlib's gradient.
Algorithm 1 is the run predicate IsALRun on the produced sequences $(x^k,\hat\Lambda^k,\rho_k)$ . Every free choice of the page stays free. The convention $\|V^{-1}\|=\infty$ is encoded as $\rho_1=\rho_0$ . The initial point $x^{-1}$ plays no role and is omitted.
Step 1 is stated through the gradient of $y\mapsto L_{\rho_k}(y,\hat\Lambda^k)$ , not through the right-hand side of (20). Formula (20) is a milestone to prove, not a definition.
A "limit point" is a cluster point (MapClusterPt). In (28), $B(\bar x,\delta)$ is the open ball and $\|D\Psi(x)\|$ is the operator norm of the derivative.
CAKKT is defined with all three limits on one and the same pair of sequences. Defining it as "AGP and (18)" with independent sequences would be a weaker condition and is ruled out.

Contributions are welcome on the convex-projection layer: existence and uniqueness of $\Pi_C$ , nonexpansiveness, Moreau's decomposition (posed separately on the platform as MoreauProx.Decomposition.cone_decomposition), and the gradient of the squared distance. They are also welcome on the two case analyses of the convergence proofs.

Selected references

R. Andreani, W. Gómez, G. Haeser, L. M. Mito, A. Ramos, On Optimality Conditions for Nonlinear Conic Programming, Mathematics of Operations Research, 2022. https://doi.org/10.1287/moor.2021.1203 (formalized from the authors' manuscript revised 2021-04-20).
R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60(5), 2011. https://doi.org/10.1080/02331930903578700
R. Andreani, J. M. Martínez, B. F. Svaiter, A new sequential optimality condition for constrained optimization and algorithmic consequences, SIAM Journal on Optimization 20(6), 2010. https://doi.org/10.1137/090777189
J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, Journal of Optimization Theory and Applications 118, 2003. https://doi.org/10.1023/A:1024791525441
J. J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93, 1965. https://doi.org/10.24033/bsmf.1625

10 thms1 active userReviewed

Quantum Information·Captain: Goku

Bounding the energy-constrained quantum and private capacities of phase-insensitive bosonic Gaussian channelsResearch Paper

Motivation

We establish several upper bounds on the energy-constrained quantum and private capacities of all single-mode phase-insensitive bosonic Gaussian channels. The first upper bound, which we call the "data-processing bound," is the simplest and is obtained by decomposing a phase-insensitive channel as a pure-loss channel followed by a quantum-limited amplifier channel. We prove that the data-processing bound can be at most 1.45 bits larger than a known lower bound on these capacities of the phase-insensitive Gaussian channel. We discuss another data-processing upper bound as well. Two other upper bounds, which we call the " $\varepsilon$ -degradable bound" and the " $\varepsilon$ -close-degradable bound," are established using the notion of approximate degradability along with energy constraints. We find a strong limitation on any potential superadditivity of the coherent information of any phase-insensitive Gaussian channel in the low-noise regime, as the data-processing bound is very near to a known lower bound in such cases. We also find improved achievable rates of private communication through bosonic thermal channels, by employing coding schemes that make use of displaced thermal states. We end by proving that an optimal Gaussian input state for the energy-constrained, generalized channel divergence of two particular Gaussian channels is the two-mode squeezed vacuum state that saturates the energy constraint. What remains open for several interesting channel divergences, such as the diamond norm or the Renyi channel divergence, is to determine whether, among all input states, a Gaussian state is optimal.

This mission is the statement-level formalization of Bounding the energy-constrained quantum and private capacities of phase-insensitive bosonic Gaussian channels (arXiv:1708.07257v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 26: thermal gap bound (Theorem 26, PDF p. 34). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

51 results of the paper are not stated yet, because the library lacks an interface they need:

Remark 3: Approximate-degradability implication for state-supremum half-diamond errors on arbitrary separable channel systems, with a certified conversion of the cited full-diamond constants. (hard)
Lemma 1: Bit-valued conditional entropy for finite first-system entropy, spectral Gibbs entropy envelope, and the cited energy-constrained half-trace-distance continuity result on separable systems. (hard)
Theorem 8: As printed the reference R has no entropy restriction. A product of an infinite-entropy state on R and a vacuum input makes BOTH joint entropies infinite, so their displayed difference is undefined. The proof suggests a telescoping conditional-entropy extension, but the source never defines that extension; adding finite H(R) or changing the conclusion silently would change the theorem. (source-ambiguity)
Lemma 2: Common admissible parameter sets, finite real optimization suprema and existing regularized limits for both channels, with the uniform all-positive-n absolute difference bound. (hard)
Remark 9: Independently defined constrained and unconstrained operational quantum/private capacities with all-large-positive-blocklength achievability. (hard)
Theorem 11: Uniform-energy quantum codes and their capacity, state-supremum half-diamond distance, fixed complement, and output Gibbs entropy envelope. (hard)
Theorem 12: Uniform-energy operational Q and optimized coherent information for the actually degradable comparison channel, with all-blocklength receiver-energy bounds. (hard)
Theorem 13: Finite-dimensional operational private capacity from normalized POVM private codes and a common environment state, plus an attained entropy maximum and fixed complement. (hard)
Theorem 14: Operational private capacity with messagewise energy/security and Gibbs entropy envelope on the identified complementary output. (hard)
Theorem 15: Operational private capacity and optimized coherent information for the comparison channel, retaining average ensemble energy. (hard)
Remark 17: Unconstrained thermal Q and the supremum/limit of the clipped finite-energy expression, with infinity at eta=1. (hard)
Theorem 16: Full Fock thermal CPTP receiver and uniform-energy operational quantum capacity. (hard)
Remark 18: Operational thermal quantum capacity positivity and its necessary parameter restriction, including zero energy. (hard)
Theorem 19: Actual two-mode purified thermal complement and opposite-phase splitter degrading map (5.20), with arbitrary-reference diamond distance. (hard)
Theorem 20: The derivation applies Theorem 11 to TWO environment output modes with total photon budget Wprime=(1-eta)NS+(1+eta)NB, but substitutes the ONE-mode entropy g(Wprime/delta). For the natural sum-number Gibbs observable the maximum entropy is 2g(Wprime/(2delta)), generally larger. The source supplies no alternative Gibbs observable justifying (5.42). Neither silently increasing the correction nor assuming a missing entropy bound states the printed result faithfully. (source-ambiguity)
Proposition 21: Actual thermal receiver/degrader, saturating thermal state, and attained optimization over every normalized finite-energy input. (hard)
Remark 22: The stated conditions omit Gaussian extremality. Phase-averaging need not preserve Gaussianity. Concavity and local-unitary invariance alone do not single out a thermal maximizer among all states, so no faithful general optimizer theorem follows from the supplied bullet list. (source-ambiguity)
Remark 24: High-energy TMS output-fidelity limit for full Fock thermal channels at common 0<=eta<1, and its derived half-diamond lower bound. (hard)
Theorem 23: Thermal/pure-loss full Fock CPTP receivers at both transmissivity endpoints and arbitrary-reference normalized-state diamond supremum. (hard)
Theorem 25: Operational thermal Q with uniform encoder energy and source close-degradable entropy correction. (hard)
Unnumbered asserted gap limit: The fixed-channel equality is false: at NB=0 the thermal channel is pure loss and the two scalar expressions agree for every NS, so Delta is identically zero. The source applies a large-argument entropy expansion to a symplectic occupation that stays bounded. The valid inequality of Theorem 26 is kept at the seed; no false saturation limit is assumed. (source-ambiguity)
Remark 28: Unconstrained thermal P and the clipped finite-energy supremum/limit, including the infinite eta=1 endpoint. (hard)
Theorem 27: Full Fock thermal receiver and messagewise-energy operational private capacity. (hard)
Theorem 29: Theorem 29 inherits the unresolved two-environment-mode Gibbs entropy substitution of Theorem 20: it uses g(Wprime/delta) where the cited general theorem with the sum-number observable gives 2g(Wprime/(2delta)). The intended smaller correction is not justified or specified by the source; retain this theorem as deferred rather than quietly enlarging its bound. (source-ambiguity)
Unnumbered displaced-thermal private rate: Displaced-thermal Borel ensemble, trace-norm barycenter, private information with average ensemble energy, and achievable private rates; Dirac displacement at s=NS. (hard)
Theorem 30: Operational thermal P with messagewise energy/security and source close-degradable entropy correction. (hard)
Theorem 31: Full Weyl-action adapter identifying a centered phase-insensitive CPTP channel and constructed amplifier-then-loss maps, including G=1. (hard)
Theorem 32: Noisy-amplifier Fock CPTP receiver and both operational energy-constrained capacities. (hard)
Remark 33: Both unconstrained amplifier capacities, scalar high-energy supremum/limit, and complete PLOB-bound comparison. (hard)
Remark 34: Operational amplifier Q positivity implication using (G-1)NB<1, without division by NB. (hard)
Theorem 36: Fixed purified amplifier complement and environment-port degrading squeezer (9.24), with arbitrary-reference half-diamond distance. (hard)
Theorem 37: Printed expression is false at the allowed edge NB=NS=0 and G>1: epsilon=0, zeta occupations are G-1 and 0, so as epsilonPrime decreases to zero its RHS tends to -g(G-1)<0 although capacity is zero. The first output entropy omits spontaneous photons G-1; the complementary photon budget also omits them. In addition the two-mode continuity correction has the unresolved issue of Theorem 20. No single silent transcription fix recovers the claimed formula. (source-ambiguity)
Theorem 38: Printed expression is false at the allowed edge NB=NS=0 and G>1: epsilon=0, zeta occupations are G-1 and 0, so as epsilonPrime decreases to zero its RHS tends to -g(G-1)<0 although capacity is zero. The first output entropy omits spontaneous photons G-1; the complementary photon budget also omits them. In addition the two-mode continuity correction has the unresolved issue of Theorem 20. No single silent transcription fix recovers the claimed formula. (source-ambiguity)
Theorem 39: Noisy/quantum-limited Fock amplifier CPTP receivers and arbitrary-reference normalized-state diamond distance. (hard)
Theorem 40: Operational amplifier Q and corrected common receiver photon budget G NS+(G-1)(NB+1); delta denominator 1+epsilonPrime. (hard)
Theorem 41: Operational amplifier P and corrected common receiver photon budget G NS+(G-1)(NB+1); delta denominator 1+epsilonPrime. (hard)
Remark 43: Additive-noise CPTP channel, both unconstrained operational capacities, and high-energy supremum/limit. (hard)
Remark 45: Operational additive-noise quantum/private capacities and the cited converse (nbar-1)/ln2+log2(1/nbar), including its strict comparison on 0<nbar<1. (hard)
Theorem 42: Additive-noise CPTP channel and both energy-constrained capacities, with the finite-energy bound. (hard)
Theorem 46: Thermal operational Q/P and physical amplifier-then-loss bottleneck with increased encoder energy G NS+G-1 and clipping. (hard)
Remark 47: Thermal operational Q/P positivity implication, including zero capacities in entanglement-breaking cases. (hard)
Remark 49: The statement uses unquantified low-noise/low-energy regimes and supplies no analytic boundary. Plots and qualitative comparisons cannot be registered as a universal parameter inequality without inventing a threshold. (source-ambiguity)
Remark 50: Additive-noise unconstrained Q/P and the clipped high-energy supremum of Theorem 48 for all 0<nbar<1. (hard)
Remark 51: The high-noise regime is not quantified and the printed U4 expression is unclipped, whereas an operational bound must be clipped at zero. Choosing an exact threshold or either version without qualification would assert more than the source specifies. (source-ambiguity)
Theorem 48: Additive-noise CPTP channel and both operational energy-constrained capacities with max(0,U4). (hard)
Lemma 4: Dimension-compatible generalized divergence on actual trace-class systems with data processing and cq direct sums, and the finite/discrete ensemble group-averaging inequality. (hard)
Lemma 5: The text extends the finite-group result “by approximation” while requiring only that D is Borel. Borel measurability permits integration but does not give the semicontinuity/continuous-ensemble direct-sum law needed to pass this inequality to a continuous barycenter. The source neither supplies that law nor specifies a divergence class for which the limiting argument is valid; do not silently replace Borel by lower semicontinuous or assume the desired inequality. (source-ambiguity)
Proposition 54: The full statement uses the unresolved continuous-ensemble step of Lemma 5 with only Borel regularity. Additionally the Gaussian-attainment argument on p.56 invokes that only thermal Gaussian states are number-diagonal, but phase averaging a Gaussian state need not stay Gaussian (e.g. coherent-state dephasing is Poisson). No general Gaussian-extremality property of an arbitrary D is supplied. Retain BOTH conclusions as the deferred target; do not replace it by only the diagonal-state reduction or assert an unproved Gaussian optimizer. (source-ambiguity)
Unnumbered Gaussian diamond and C-distance optimizers: Explicit main corollaries of the deferred Gaussian-attainment clause of Proposition 54; the source has not supplied the missing Gaussian-extremality/continuous-ensemble argument. Keep both target equalities and do not promote them to unrestricted diamond or C-distance optimizer statements. (source-ambiguity)
Unnumbered joint displacement-covariance reduction: Same unresolved Borel-versus-continuous-ensemble issue as Lemma 5. The displaced input is purified afresh, and exact energy is a consequence; it cannot be assumed on the original <=NS optimization domain. (source-ambiguity)
Unnumbered joint phase-covariance reduction: This explicitly claimed generalization uses the unresolved continuous-group approximation of Lemma 5. Record the <=NS constraint accurately; without a specified divergence regularity/continuous-ensemble law, the stated generality is not pinned down. (source-ambiguity)

Selected references

Bounding the energy-constrained quantum and private capacities of phase-insensitive bosonic Gaussian channels, arXiv:1708.07257v3, https://arxiv.org/abs/1708.07257v3

10 thms1 active userReviewed