Operations Research

Completed

Economics Information Theory Optimization·Captain: mikedeng1

Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations I: The Rationally Inattentive Decision-Maker's Optimal Choice Probability in Closed FormResearch Paper

Motivation

A person using a machine's advice may decide more accurately, but attention is costly. Before asking what a machine changes, the baseline decision has to be understood: how often would the person choose the action associated with a good state without machine input? Boyacı, Canyakmaz, and de Véricourt study this question in a model of a decision maker who can acquire information about an unknown binary state and pays for the expected reduction in uncertainty. Their working paper derives a closed form for the decision maker's choice probability. That baseline is used later in the paper to compare decisions with and without machine input.

The information cost follows the rational inattention approach: a decision maker chooses how much information to process while considering its effect on the final action. In the discrete choice setting, Matějka and McKay (2015) characterize optimal conditional choice probabilities. The paper adopts their equivalent choice probability representation in §4. This mission isolates the first consequence of that representation, Theorem 1, before the paper introduces the machine.

Setting

The unknown state is good, $g$ , with prior probability $\mu$ , and bad, $b$ , with probability $1-\mu$ . The decision maker selects either $y$ (declare good) or $n$ (declare bad). A correct action earns one unit, and an incorrect action earns zero. Write $p_g$ for the probability of choosing $y$ when the state is $g$ , and $p_b$ for the probability of choosing $y$ when the state is $b$ . A strategy is any pair $(p_g,p_b)\in[0,1]^2$ ; the pair may lie on the no-information diagonal or on the boundary of the square.

The unconditional choice probability is $p=\mu p_g+(1-\mu)p_b$ . The accuracy is $A=\mu p_g+(1-\mu)(1-p_b)$ . Binary entropy, measured with the natural logarithm, is $H(t)=-t\log t-(1-t)\log(1-t)$ , with $H(0)=H(1)=0$ . Given an information-cost parameter $\lambda>0$ , the cognitive cost in the paper's choice probability representation is

C=\lambda\bigl[H(p)-(1-\mu)H(p_b)-\mu H(p_g)\bigr].

The decision maker maximizes net value $V=A-C$ over the whole square. An optimal pair is one whose value is at least that of every feasible pair. The source originally introduces a general distribution of information signals and a Bayes consistency condition in problem (2). Section 4 and footnote 8 adopt the equivalent conditional choice probability representation used here. The equivalence itself is an input from Matějka and McKay (2015), rather than a claim of this mission.

Formalization targets

Optimal choice probability

For $0<\mu<1$ and $\lambda>0$ , define the thresholds

\underline\mu(\lambda)=\frac{1}{e^{1/\lambda}+1},\qquad \overline\mu(\lambda)=\frac{e^{1/\lambda}}{e^{1/\lambda}+1}.

The goal is the paper's Theorem 1: every optimal pair has the same unconditional choice probability,

p^\star(\mu)= \begin{cases} 0,&\mu\le\underline\mu,\\ \displaystyle\frac{\mu}{1-e^{-1/\lambda}}-\frac{1-\mu}{e^{1/\lambda}-1},&\underline\mu<\mu<\overline\mu,\\ 1,&\mu\ge\overline\mu. \end{cases}

The same theorem states $\underline\mu<1/2<\overline\mu$ , that $p^\star$ is non-decreasing in the prior, and that the lower threshold increases while the upper threshold decreases as $\lambda$ increases. This mission includes all these clauses in its single goal. The intermediate milestones formalize the paper's conditional choice equations, the algebraic interior candidate, its threshold crossings, and its slope and threshold derivatives.

Significance

The formula partitions prior beliefs into three regimes. With a sufficiently low prior, the decision maker always chooses $n$ ; with a sufficiently high prior, the decision maker always chooses $y$ . Between the thresholds, the probability of choosing $y$ changes continuously with the prior. The threshold movements describe how a higher information cost changes the region in which information processing affects the choice. In the paper, these probabilities feed into accuracy, error rate, effort, and machine input comparisons.

The paper proves the result mathematically. The statements here are open Lean targets, so compilation of their declarations does not amount to machine-checked proofs. A complete development would verify the optimality characterization and the closed form, then provide reusable binary entropy and constrained optimization lemmas. It would also expose a precise baseline that subsequent missions can import after publication.

Difficulty

Equations (4)–(6) alone do not select the optimum: both $p=0$ and $p=1$ satisfy them for every prior. The printed uniqueness phrase in Lemma 1 therefore cannot be carried into a theorem about all solutions of those equations. The formal target says instead that every maximizing strategy satisfies the conditional choice equations, and Theorem 1 identifies the probability selected by maximization. The endpoint strategies, where entropy is evaluated at zero or one, must remain in the feasible set. One must also distinguish the algebraic interior root from the optimizer when that root leaves $[0,1]$ .

Formalization scope

Lean represents probabilities and costs as real numbers. The strategy space is the full closed square $[0,1]^2$ , and IsOptimal compares net value against every point in that square. The prior in the goal and Lemma 1 lies strictly between zero and one, as in the paper's §4 setting; $\lambda$ is strictly positive. Boolean state and action types are unnecessary in this first mission because the paper's §4 representation is already the pair of conditional probabilities. The general-signal distribution of problem (2) is not encoded here.

The entropy function is Mathlib's Real.binEntropy, with natural logarithms and the endpoint values used by the paper. The threshold definitions reproduce Theorem 1 exactly. pBar is the interior algebraic expression from Appendix A, and pClosed is only the right-hand side of equation (11). Neither defines the optimizer. In particular, defining the starred optimal probability by the closed form would remove the theorem's main claim. The goal quantifies over every optimal pair and asserts that its computed choice probability equals that expression.

Contributions to the proof will need results about binary entropy at the boundary, derivatives of the objective in the interior, existence and characterization of maximizers on a compact square, and elementary inequalities for the exponential thresholds. The entropy and compact optimization infrastructure can support later formalizations beyond this paper. The four listed milestones follow the authors' Appendix A argument; alternative proofs of the same faithful statements are welcome.

Selected references

Tamer Boyacı, Caner Canyakmaz, and Francis de Véricourt, Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations, ESMT Working Paper 20-02, November 30, 2020, §§3–4 and Appendix A. Working paper record.
Filip Matějka and Alisdair McKay, Rational Inattention to Discrete Choices: A New Foundation for the Multinomial Logit Model, American Economic Review 105(1), 2015, pp. 272–298. DOI.

6 thms2 active usersReviewed

Algorithmic Game Theory Analysis Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 3: The Price of Anarchy Is Locally Lipschitz at Games with Constant Costs or Strictly Increasing C¹ CostsResearch Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum total cost. Worst-case bounds on it over whole classes of cost functions are classical (Roughgarden and Tardos, 2002; Correa, Schulz and Stier-Moses, 2004). In practice the demands and cost functions of a traffic model are estimated, never known exactly, so a second question matters as much as the worst case: how much does the PoA of a given game move when its data move?

Wu and Möhring (arXiv:2007.13979v3, published in Mathematics of Operations Research, 2023) answer this with a metric on games that compares demands and cost functions simultaneously. They show that the PoA is continuous, that it is Hölder continuous with exponent $1/2$ near every game whose costs are Lipschitz, and that it is not uniformly Hölder continuous. This mission formalizes their Theorem 12 (§4.3): at two special classes of games, games with constant costs and games with strictly increasing continuously differentiable costs, the exponent improves to $1$ , so the PoA is locally Lipschitz. The authors motivate the result by the differentiability results of Cominetti, Dose and Scarsini (2020), which suggest Lipschitz behaviour at games whose costs have strictly positive derivatives.

Setting

Fix a finite set $A$ of arcs, a finite nonempty set $K$ of origin–destination (O/D) pairs, and for each $k\in K$ a set $S_k$ of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game $\Gamma=(\tau,d)$ consists of arc cost functions $\tau_a$ , continuous, non-decreasing and non-negative on $[0,\infty)$ , and demands $d_k\ge 0$ with total demand $T(d)=\sum_k d_k>0$ ; moreover $\tau_a(x)>0$ for $x\in(0,T(d)]$ . These games form the game space $\mathcal G(G,K,S)$ .

A flow $f=(f_s)_{s\in S}\ge 0$ routes each demand, $\sum_{s\in S_k} f_s=d_k$ . The arc flow is $f_a=\sum_{s\ni a} f_s$ , the path cost $\tau_s(f)=\sum_{a\in s}\tau_a(f_a)$ , and the total cost $C(\Gamma,f)=\sum_a f_a\tau_a(f_a)$ . A flow $\tilde f$ is a Wardrop equilibrium (WE) if every used path of a pair is a cheapest path of that pair. The SO cost $C^*(\Gamma)$ is the minimum total cost, the WE cost $\tilde C(\Gamma)$ is the total cost of a WE flow (all WE flows have the same cost), and the PoA is

\rho(\Gamma)=\frac{\tilde C(\Gamma)}{C^*(\Gamma)}.

The distance of two games $\Gamma=(\tau,d)$ and $\Gamma'=(\sigma,d')$ is

\|\Gamma-\Gamma'\|=\max\Big\{\|d-d'\|_\infty,\ \max_{a\in A}\max_{x\in[0,\min\{T(d),T(d')\}]}|\tau_a(x)-\sigma_a(x)|,\ \|\tau(T(d))-\sigma(T(d'))\|_\infty\Big\},

which compares cost functions only on the range both games use, plus their values at the respective total demands.

Formalization targets

Goal: Theorem 12

Let $\Gamma=(\tau,d)\in\mathcal G(G,K,S)$ .

If every $\tau_a$ is constant on $[0,T(d)]$ , or
if every $\tau_a$ is continuously differentiable on $[0,T(d)]$ with $\tau_a'\ge m_\Gamma>0$ there,

then there are $\epsilon_\Gamma>0$ and $\kappa_\Gamma>0$ such that

|\rho(\Gamma)-\rho(\Gamma')|\le\kappa_\Gamma\cdot\|\Gamma-\Gamma'\|\qquad\text{for all }\Gamma'\in\mathcal G(G,K,S)\text{ with }\|\Gamma-\Gamma'\|<\epsilon_\Gamma.

The goal leaves the constants unspecified; only their existence, depending on $\Gamma$ alone, is asserted.

Milestones

Proof of Theorem 12a), p. 37. A game whose costs are constant on $[0,T(d)]$ has $\rho(\Gamma)=1$ .
(4.33), p. 37. Near such a game, $0\le\rho(\Gamma')-\rho(\Gamma)\le\frac{8\,|A|\,T(d)\,(|K|+1)}{C^*(\Gamma)}\|\Gamma-\Gamma'\|$ .
(4.39), p. 38. For WE flows $\tilde f,\tilde g$ of two games $\Gamma_1=(\pi^1,w)$ , $\Gamma_2=(\pi^2,w)$ with equal demands,

0\le\sum_a(\pi^1_a(\tilde f_a)-\pi^2_a(\tilde g_a))(\tilde g_a-\tilde f_a)\le\sum_a(\pi^1_a(\tilde g_a)-\pi^2_a(\tilde f_a))(\tilde g_a-\tilde f_a)\le 2|A|\,T(w)\,\|\Gamma_1-\Gamma_2\|.

(4.40), p. 38, first four inequalities. If moreover the costs of $\Gamma_1$ are $C^1$ on $[0,T(w)]$ with derivative $\ge m>0$ , then

m\sum_a|\tilde g_a-\tilde f_a|^2\le\sum_a(\pi^1_a(\tilde g_a)-\pi^1_a(\tilde f_a))(\tilde g_a-\tilde f_a)\le\sum_a(\pi^1_a(\tilde g_a)-\pi^2_a(\tilde g_a))(\tilde g_a-\tilde f_a)\le\|\Gamma_1-\Gamma_2\|\sum_a|\tilde g_a-\tilde f_a|.

Significance

At a general game with Lipschitz costs the PoA is only Hölder continuous with exponent $1/2$ in this metric, and the paper shows that no exponent works uniformly over the game space. Theorem 12 identifies two natural classes of games at which the sensitivity is linear: constant costs (the PoA equals $1$ and grows at most linearly under perturbation) and strictly increasing $C^1$ costs, which include affine costs with positive slopes. For these games an estimation error of size $\delta$ in demands and costs changes the PoA by $O(\delta)$ .

The result is proved in the paper; it is not formalized anywhere. A complete development would also provide machine-checked equilibrium-comparison estimates between two games of one demand slice ((4.39)–(4.40)), which are reusable for any stability analysis of Wardrop equilibria. The paper's explicit constants in (4.41)–(4.46) are off by a factor $\sqrt{|A|}$ (the last step of (4.40) uses $\sum_a|x_a|\le\sqrt{\sum_a x_a^2}$ ); the existential Theorem 12 is unaffected, and a formalization with correct explicit constants is a welcome addition.

Difficulty

The PoA is a ratio of two optimal values, and the perturbed game $\Gamma'$ may change the demand vector and the costs at once, including the costs on $(T(d),T(d')]$ , which $\Gamma$ 's hypotheses do not control. A direct comparison of $\Gamma$ and $\Gamma'$ therefore fails: the WE flows live in different feasible sets, and the hypotheses on $\Gamma$ say nothing beyond $T(d)$ . The general Hölder- $1/2$ argument loses a square root exactly where it bounds the distance between the arc flows of the two equilibria through an approximate-equilibrium estimate; obtaining exponent $1$ requires an estimate in which the flow difference enters linearly, and this is where strict monotonicity of the costs is needed. Constant costs are degenerate in the opposite direction: the WE is far from unique, and only costs, not flows, can be compared.

Formalization scope

The model follows §2–§3.2 of the paper and reuses the published definition KellyStochasticNetworks_Wardrop for arc flows, feasibility and the Wardrop condition. Paths are nonempty $0/1$ incidence columns (a generalization of loop-free paths that the proofs do not use); $K$ is nonempty and Condition 1 is standing ( $|S_k|\ge 2$ , every arc on a path). Costs are functions $\mathbb R\to\mathbb R$ constrained on $[0,\infty)$ only. $C^*$ is an infimum over all flows, $\tilde C$ a supremum over WE flows, $\rho=\tilde C/C^*$ ; the distance is (3.3) with the sup norm on demand and endpoint vectors and a supremum over the compact set $A\times[0,\min\{T(d),T(d')\}]$ . The derivative in Theorem 12b) is derivWithin on $[0,T(d)]$ , one-sided at the endpoints, and $C^1$ is ContDiffOn ℝ 1 on that interval.

Every statement quantifies over games in the game space only: off it, $\rho$ would be a junk ratio such as $0/0=0$ . The paper prints the conclusions of Theorem 12 and (4.33) with a strict inequality, which fails at $\Gamma'=\Gamma$ ; the non-strict form is posed, and no hypothesis $\Gamma'\neq\Gamma$ is added (distinct games can have distance $0$ ). Milestones (4.39) and (4.40) are posed for two arbitrary games of one demand slice, the general form of the paper's step for its auxiliary game.

A complete development needs existence of SO and WE flows on the game space, the variational characterization of Wardrop equilibria, the mean value theorem on a closed interval with one-sided derivatives, and continuity of $C^*$ in the metric; contributions of any of these as separate lemmas are welcome. The source is the arXiv preprint v3; the published Mathematics of Operations Research version is not the cited artifact.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in non-atomic congestion games, Mathematics of Operations Research 48(3), 2023; cited as arXiv:2007.13979v3, 2021. https://arxiv.org/abs/2007.13979v3
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
J. R. Correa, A. S. Schulz, N. E. Stier-Moses, Selfish routing in capacitated networks, Mathematics of Operations Research 29(4), 2004. https://doi.org/10.1287/moor.1040.0098
R. Cominetti, V. Dose, M. Scarsini, The price of anarchy in routing games as a function of the demand, arXiv:1907.10101v2, 2020. https://arxiv.org/abs/1907.10101
J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3), 1952. https://doi.org/10.1680/ipeds.1952.11259

8 thms2 active usersReviewed

Algorithmic Game Theory Analysis Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 1: The Price of Anarchy Is Hölder Continuous with Exponent 1/2 at Every Game with Costs Lipschitz on [0, T(d)]Research Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum possible total cost. It quantifies how much selfish routing loses compared with central coordination, and it has been studied intensively since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), mostly through worst-case bounds over classes of cost functions.

Worst-case bounds say nothing about how the PoA of one particular network behaves when its data change. In transport applications both the cost functions (capacities, tolls, travel-time models) and the demands are estimated, so the PoA is only useful if small errors in the data cause small errors in the PoA. Wu and Möhring (arXiv:2007.13979, published in Mathematics of Operations Research, 2023) study this sensitivity question in a setting where cost functions and demands change simultaneously. Earlier sensitivity results changed only the demands, with the cost functions fixed: Englert, Franke and Olbrich (2010) bounded the growth of the PoA of a single-O/D network with polynomial costs of degree at most $\beta$ by a factor $(1+\epsilon)^\beta$ when the demand grows by a factor $1+\epsilon$ ; Takalloo and Kwon (2020) extended this to several O/D pairs whose demands are scaled together; and Cominetti, Dose and Scarsini (arXiv:1907.10101) studied differentiability of the PoA as a function of the demand of a single O/D pair. The main theorem of the paper, Theorem 9, is the subject of this mission.

Setting

A network consists of a finite set $A$ of arcs, a finite non-empty set $\mathcal K$ of origin–destination (O/D) pairs, and for every $k \in \mathcal K$ a non-empty set $\mathcal S_k$ of paths; each path is a non-empty set of arcs. From §3.1 onward the paper also assumes every arc lies on some path and every $\mathcal S_k$ has at least two paths (Condition 1).

A game $\Gamma = (\tau, d)$ on the network consists of cost functions $\tau_a : [0,\infty) \to [0,\infty)$ , one per arc, that are continuous and non-decreasing, and demands $d_k \ge 0$ , one per O/D pair. The total demand is $T(d) = \sum_k d_k$ . The game space $\mathcal G(G,\mathcal K,\mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for all $x \in (0, T(d)]$ .

A flow $f = (f_s)$ assigns a non-negative amount to every path, with $\sum_{s\in\mathcal S_k} f_s = d_k$ . Its arc flows are $f_a = \sum_{s \ni a} f_s$ , its path costs $\tau_s(f) = \sum_{a\in s}\tau_a(f_a)$ , and its total cost

C(\Gamma, f) = \sum_{a\in A} f_a\,\tau_a(f_a).

A Wardrop equilibrium (WE) is a flow in which every used path of a pair is a cheapest path of that pair. The SO cost $\mathcal C^*(\Gamma)$ is the minimum total cost over all flows, the WE cost $\tilde{\mathcal C}(\Gamma)$ is the total cost of a WE flow (all WE flows have the same cost), and

\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)}.

Games are compared by the distance

\|\Gamma - \Gamma'\| = \max\Big\{\|d-d'\|_\infty,\ \max_{a\in A}\max_{x\in[0,\min\{T(d),T(d')\}]}|\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}

for $\Gamma = (\tau, d)$ and $\Gamma' = (\sigma, d')$ . It compares cost functions only on the range of flow values both games can produce, plus the values at the respective total demands. A function $h$ is Lipschitz continuous on $[0,T]$ with constant $M$ if $|h(x) - h(y)| \le M|x-y|$ for all $x, y \in [0,T]$ .

Formalization targets

Goal: Theorem 9 (p. 26)

Let $\Gamma = (\tau, d)$ be a game of the game space whose cost functions are Lipschitz continuous on $[0, T(d)]$ . Then there are $\epsilon_\Gamma > 0$ and $\kappa_\Gamma > 0$ , depending only on $\Gamma$ , such that

|\rho(\Gamma) - \rho(\Gamma')| \le \kappa_\Gamma\,\|\Gamma - \Gamma'\|^{1/2}\quad\text{for every game } \Gamma' \text{ of the game space with } \|\Gamma - \Gamma'\| < \epsilon_\Gamma.

The goal fixes the exponent $1/2$ and leaves the radius and the constant existential, which is the form the paper claims.

Milestones

Lemma 1a)–c) (p. 13): properties of $\epsilon$ -approximate WE flows, ending with

|C(\Gamma, f) - C(\Gamma, \tilde f)| \le |A|\sqrt{M\epsilon}\,T(d) + \epsilon

for an $\epsilon$ -approximate WE flow $f$ and a WE flow $\tilde f$ when all costs are $M$ -Lipschitz on $[0,T(d)]$ . 2. Lemma 10a)–d) (p. 27): on a demand slice (games with a common demand vector $w$ ), $\mathcal C^*$ is Lipschitz, WE flows of one game are $|A|\,T(w)\,\|\Gamma_1-\Gamma_2\|$ -approximate WE flows of the other, and $\tilde{\mathcal C}$ and $\rho$ are Hölder with exponent $1/2$ with explicit constants. 3. Lemma 11a)–c) (p. 31): on a cost slice (games with a common cost vector and $T(w') \le T(w)$ ), explicit Hölder bounds of exponent $1/2$ for $\tilde{\mathcal C}$ and $\rho$ and a Lipschitz bound for $\mathcal C^*$ .

Significance

Theorem 9 is the first pointwise Hölder continuity result for the PoA on the whole game space, with demands and costs perturbed together. Its hypothesis is mild (Lipschitz costs on a compact interval, which covers polynomial, BPR-type and piecewise linear costs), and such games are dense in the game space. Together with Theorem 8 of the same paper, which shows that no uniform Hölder bound exists, it describes exactly what kind of stability the PoA has: local, with a constant depending on the game, and exponent $1/2$ in general. The explicit constants of Lemmas 10 and 11 give computable error bounds for the PoA of a network whose data are known only approximately.

The result is proved in the paper; no machine-checked proof exists. This mission formalizes the statement and the explicit slice estimates the proof rests on. Lemma 1 is a self-contained statement about approximate Wardrop equilibria that is useful well beyond this paper, for instance for analysing iterative traffic-assignment algorithms, which only ever produce approximate equilibria.

Difficulty

The obvious approach compares an equilibrium of $\Gamma$ with an equilibrium of $\Gamma'$ directly. This fails because the two games have different demand vectors, so their flows live in different polytopes: an equilibrium of one game is not even a flow of the other. The paper separates the perturbation into a change of costs at fixed demand and a change of demand at fixed costs, through an auxiliary game, and each half needs its own argument. On a demand slice an equilibrium of one game is only an approximate equilibrium of the other, and the passage from an approximate equilibrium to its cost loses a square root (Lemma 1c), which is tight by Example 2). On a cost slice the demand has to be removed path by path from an equilibrium while keeping it an equilibrium of a shifted game. Finally, the constants of the slice estimates depend on the auxiliary game, and they must be controlled uniformly near $\Gamma$ .

Formalization scope

The Lean development fixes the following conventions.

The network is a structure with $|A|$ arcs, $|\mathcal S|$ paths and $|\mathcal K|$ O/D pairs, a 0/1 arc–path incidence matrix and the map sending a path to its pair. Lemma 1 uses the §2 model assumptions: 0/1 incidence, non-empty paths, $\mathcal K \neq \emptyset$ , and $|\mathcal S_k| \ge 1$ . The later results add Condition 1 (every arc on a path, $|\mathcal S_k| \ge 2$ ), as assumed from §3.1. Paths are arbitrary non-empty 0/1 columns, not necessarily loop-free paths of a digraph; the results do not use loop-freeness.
Cost functions are maps $\mathbb R \to \mathbb R$ required to be continuous, non-decreasing and non-negative on $[0,\infty)$ only.
Arc flows, Wardrop equilibria (2.1) and the potential (2.6) come from the published definition KellyStochasticNetworks_Wardrop. $\epsilon$ -approximate WE flows follow (2.7) in arc form. The total cost uses the arc form, which equals the path form for 0/1 incidence.
$\mathcal C^*$ is the infimum of costs over flows, $\tilde{\mathcal C}$ the supremum of costs over WE flows, $\rho$ their quotient. The middle term of the distance is the supremum of the image of the compact set $A\times[0,\min\{T(d),T(d')\}]$ , and $\|\cdot\|_\infty$ is the sup norm.
Every statement about $\rho$ , $\mathcal C^*$ or $\tilde{\mathcal C}$ quantifies over games of the game space, where $\rho$ is a genuine ratio of positive numbers. Off the game space Lean's division by zero would give $\rho = 0$ , so quantifying over all pairs $(\tau, d)$ would trivialize the statements; this is ruled out. In the goal, $\epsilon_\Gamma$ and $\kappa_\Gamma$ are chosen before $\Gamma'$ .
Several printed strict inequalities are posed as non-strict, because they fail at $\Gamma' = \Gamma$ or are attained in the paper's own Example 2. In Lemma 11 the printed constants are corrected by a factor $|\mathcal K|$ that the paper's own argument needs; each item's Formalization Note quotes the printed form.

A complete development needs: existence of Wardrop equilibria and uniqueness of their cost on the game space, existence of social optima, the integral inequality (2.9) for monotone costs, positivity of $\mathcal C^*$ on the game space, and the path-by-path demand-reduction construction of Lemma 11. The existence and uniqueness results and Lemma 1 are reusable in any formalization of selfish routing. Proofs of any milestone are welcome, as are the supporting lemmas above.

The source is the arXiv preprint arXiv:2007.13979v3 (23 Aug 2021); all page and theorem numbers refer to it, not to the published version.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in non-atomic congestion games, arXiv:2007.13979v3, 2021; Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979, https://doi.org/10.1287/moor.2022.1292
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
E. Koutsoupias, C. Papadimitriou, Worst-case equilibria, STACS 1999. https://doi.org/10.1007/3-540-49116-3_38
J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3), 1952. https://doi.org/10.1680/ipeds.1952.11259
M. Englert, T. Franke, L. Olbrich, Sensitivity of Wardrop equilibria, Theory of Computing Systems 47(1):3–14, 2010.
M. Takalloo, C. Kwon, Sensitivity of Wardrop equilibria: revisited, Optimization Letters 14(3):781–796, 2020.
R. Cominetti, V. Dose, M. Scarsini, The price of anarchy in routing games as a function of the demand, 2020. https://arxiv.org/abs/1907.10101

13 thms2 active usersReviewed

Algorithmic Game Theory Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 4: The Price of Anarchy Is Not Uniformly Hölder Continuous and No Game Has the Whole Space as a Hölder NeighborhoodResearch Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game measures how much total cost is lost when a continuum of selfish users routes traffic instead of a central planner. Worst-case bounds on the PoA over classes of cost functions are classical: $4/3$ for affine costs and $\Theta(\beta/\ln\beta)$ for polynomial costs of degree at most $\beta$ (Roughgarden and Tardos 2002; Roughgarden 2003). Worst-case bounds say nothing about how the PoA of one particular instance reacts when its demands and cost functions are perturbed, which is what matters when traffic data are measured with error or change over time.

Z. Wu and R. H. Möhring (arXiv:2007.13979v3, published in Mathematics of Operations Research, 2023) study this sensitivity through Hölder continuity of the PoA map $\Gamma \mapsto \rho(\Gamma)$ on a metric space of games. Earlier work considered changes of the demand alone: Englert et al. (2010), Takalloo and Kwon (2020) and Cominetti et al. (2020), as cited in the paper, fix the cost functions and vary the demand. Wu and Möhring vary both. Their main positive results are local: Hölder continuity with exponent $1/2$ near every game with Lipschitz costs. This mission formalizes their negative result, Theorem 8, which says that no global version of this regularity is possible.

Setting

Fix a network with arcs $A$ , a non-empty finite set $K$ of origin–destination (O/D) pairs, and for each pair $k$ a set $S_k$ of paths, each a non-empty set of arcs, with $|S_k| \ge 2$ and every arc on some path (Condition 1). A game $\Gamma = (\tau, d)$ consists of cost functions $\tau_a$ , continuous, non-decreasing and non-negative on $[0,\infty)$ , and demands $d_k \ge 0$ with total demand $T(d) = \sum_k d_k$ . The game space $\mathcal G(G,K,S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for $x \in (0, T(d)]$ (Condition 2).

A flow splits each $d_k$ non-negatively over $S_k$ ; its arc flows are $f_a = \sum_{s \ni a} f_s$ and its total cost is $C(\Gamma, f) = \sum_a f_a \tau_a(f_a)$ . A Wardrop equilibrium (WE) is a flow in which every used path of a pair has minimal cost among the paths of that pair. With $C^*(\Gamma)$ the minimum total cost and $\tilde C(\Gamma)$ the total cost of a WE flow,

\rho(\Gamma) = \frac{\tilde C(\Gamma)}{C^*(\Gamma)}.

The distance of two games $\Gamma = (\tau, d)$ , $\Gamma' = (\sigma, d')$ is

\|\Gamma - \Gamma'\| = \max\Big\{\|d - d'\|_\infty,\ \max_{a,\ x \in [0, \min\{T(d),T(d')\}]} |\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}.

The cost normalization $\Psi_\upsilon(\tau, d) = (\tau/\upsilon, d)$ , $\upsilon > 0$ , divides all costs by $\upsilon$ . A $\gamma$ -neighborhood of $\Gamma$ is an open set $U \ni \Gamma$ of games on which $|\rho(\Gamma) - \rho(\Gamma')| \le \varkappa_\Gamma \|\Gamma - \Gamma'\|^\gamma$ for some constant $\varkappa_\Gamma > 0$ .

Formalization targets

Goal: Theorem 8b)

For every game $\Gamma \in \mathcal G(G,K,S)$ and every $\gamma > 0$ ,

\neg\,\exists\, \varkappa > 0\ \ \forall \Gamma' \in \mathcal G(G,K,S):\ |\rho(\Gamma) - \rho(\Gamma')| \le \varkappa\, \|\Gamma - \Gamma'\|^\gamma,

that is, the whole game space is never a $\gamma$ -neighborhood: Hölder continuity of $\rho$ holds at best locally, even with a constant depending on the game.

Milestones

$\rho(\Psi_\upsilon(\Gamma)) = \rho(\Gamma)$ for $\upsilon > 0$ (§3.5).
$\|\Psi_\upsilon(\Gamma) - \Psi_\upsilon(\Gamma')\| = \|\Gamma - \Gamma'\|/\upsilon$ when $d = d'$ (3.11).
Some demand vector carries two games with different PoA (p. 24).
Theorem 8a): no $\gamma > 0$ , $\varkappa > 0$ make $\rho$ uniformly Hölder continuous on $\mathcal G(G,K,S)$ .
$\rho$ is unbounded on the demand slice $\{\Gamma' : d' = d\}$ whenever $d$ is supported on a single O/D pair (p. 25, corrected; see below).

Significance

Theorem 8 separates what can be proved about the sensitivity of the PoA from what cannot. Part a) rules out uniform Hölder (in particular Lipschitz) bounds; part b) rules out global bounds even with a game-dependent constant. Together they explain the shape of the paper's positive results (Theorems 9 and 12), which hold on balls around a game with constants that depend on that game.

The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact hypotheses under which it holds. Two are not visible on the page: paths must form an antichain (otherwise $\rho \equiv 1$ is possible), and the unboundedness step of part b) does not hold on every demand slice. The milestones on cost normalizations are reusable for any scale-invariance argument about the PoA.

Difficulty

The invariance and scaling milestones are bookkeeping about suprema and infima. The substance is in the constructions. For 8a), two games with equal demands and different PoA are needed, which requires an explicit game whose Wardrop equilibrium is strictly inefficient on an arbitrary network satisfying Condition 1 and the antichain condition, so the WE cost and the SO cost must be computed or bounded, not just estimated asymptotically.

For 8b), the paper argues that a global Hölder bound makes $\rho$ bounded on the demand slice of $\Gamma$ , and that $\rho$ is unbounded there because the slice contains Pigou-like games. The second step fails in general: with several O/D pairs, other pairs can be forced through the arcs that distinguish the paths of every pair, and on such a slice $\rho$ can be bounded (an explicit three-pair network with $\rho \le 5/2$ on the slice $d = (1,1,1)$ is recorded in the milestone). The natural repair compares $\Gamma$ with games on a different slice, whose demand sits on one pair, and requires bounding the distance between games with different demands as the costs are normalized away.

Formalization scope

Lean represents paths as $0/1$ columns of an arc–path incidence matrix and pairs as a map from paths to pairs, on top of the published KellyStochasticNetworks_Wardrop definitions (arc flows, feasible flows, Wardrop's first principle). The commitments are:

the standing assumptions are G1–G2 (non-empty $K$ , non-empty paths), $0/1$ incidences and Condition 1;
the antichain condition (no path of a pair inside another path of the same pair) is an added hypothesis of every theorem. It holds for loop-free paths of a digraph, which the paper assumes;
costs are real functions whose properties are required on $[0,\infty)$ only;
$C^*$ is an infimum over all flows and $\tilde C$ a supremum over WE flows. All WE flows have the same cost;
the distance uses the sup norm and a supremum over the compact set $A \times [0, \min\{T(d),T(d')\}]$ ;
powers are real powers with $\gamma > 0$ .

Every game in every statement ranges over the game space. A formalization quantifying over arbitrary pairs $(\tau, d)$ would be trivial: Lean's $0/0 = 0$ gives such pairs $\rho = 0$ , and a junk game next to a real one breaks any Hölder bound for free.

The unboundedness milestone is posed for single-pair demand slices instead of the page's arbitrary slice, because the page's version is false for some multi-pair networks. Its asymptotic rate $\Theta(\beta/\ln\beta)$ is cited by the paper and not posed. Contributions of the two constructions (a strictly inefficient game for 8a, Pigou-type games on one pair for 8b) and of the distance estimates are welcome; related Pigou statements exist as SelfishRouting.Linear.figure_3_pigou (Roughgarden–Tardos).

The source is the arXiv preprint v3; the published MOR version is not the cited artifact.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in nonatomic congestion games, Mathematics of Operations Research 48(3), 2023; cited as arXiv:2007.13979v3 (2021). https://arxiv.org/abs/2007.13979v3
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
T. Roughgarden, The price of anarchy is independent of the network topology, Journal of Computer and System Sciences 67(2), 2003. https://doi.org/10.1016/S0022-0000(03)00044-8

8 thms2 active usersReviewed

Algorithmic Game Theory Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 5: For Small Total Demand the Price of Anarchy Exceeds 1 by at Most an Explicit Multiple of the Total DemandResearch Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio between the total travel cost at a Wardrop equilibrium, where every traveller uses a cheapest route, and the minimum total cost a central planner could achieve. Worst-case bounds on the PoA are classical (Roughgarden and Tardos, 2002), but traffic studies observe that the empirical PoA is close to $1$ both in light and in heavy traffic (Youn, Gastner and Jeong, 2008; O'Hare, Connors and Watling, 2016). This raises the question of how the PoA of a fixed network with fixed cost functions behaves as the demand varies.

For decreasing demand the literature had one convergence result: for polynomial costs, Colini-Baldeschi, Cominetti, Mertikopoulos and Scarsini (2020) show $\rho \to 1$ when the total demand tends to $0$ with fixed demand proportions, at rate $O(T(d))$ . Wu and Möhring (2021) obtain a rate for arbitrary cost functions that are strictly positive and Lipschitz near $0$ , with no condition on the demand proportions, as a corollary of their sensitivity analysis of the PoA. This mission formalizes that corollary, Corollary 5.1 of arXiv:2007.13979v3.

Setting

A structure consists of a finite set $A$ of arcs, a finite nonempty set $\mathcal K$ of origin–destination (O/D) pairs, and for every pair $k$ a set $\mathcal S_k$ of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game $\Gamma = (\tau, d)$ is a vector of arc cost functions $\tau_a : [0,\infty) \to [0,\infty)$ , continuous and non-decreasing, together with demands $d_k \ge 0$ of total $T(d) = \sum_k d_k$ . The game space $\mathcal G(G, \mathcal K, \mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ on $(0, T(d)]$ .

A flow $f = (f_s)$ routes $d_k$ over $\mathcal S_k$ with $f_s \ge 0$ . Arc flows are $f_a = \sum_{s \ni a} f_s$ and the total cost is $C(\Gamma, f) = \sum_a f_a \tau_a(f_a)$ . A flow is a Wardrop equilibrium if every used path is a cheapest path of its pair. With $\mathcal C^*(\Gamma)$ the minimum total cost and $\tilde{\mathcal C}(\Gamma)$ the cost of a Wardrop equilibrium (all equilibria have the same cost),

\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)} \ge 1.

Games are compared by the distance (3.3),

\|\Gamma - \Gamma'\| = \max\Big\{\|d - d'\|_\infty,\ \max_{a,\ x \in [0, \min\{T(d), T(d')\}]} |\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\},

and the demand normalization $\Lambda_\upsilon(\tau, d) = (\tau \circ \upsilon, d/\upsilon)$ , with $(\tau_a \circ \upsilon)(x) = \tau_a(x\upsilon)$ , rescales a game to a different total demand. The cost slice of $\tau$ is the set of games whose costs agree with $\tau$ on $[0, T(d)]$ .

Formalization targets

Goal: Corollary 5.1 (p. 43)

Let the costs $\tau_a$ be strictly positive on $[0,\infty)$ and Lipschitz on $[0, b]$ with constant $M_\tau > 0$ , and let $\tau_{\min}(0) = \min_a \tau_a(0)$ . There is $\delta > 0$ such that for every demand vector $d \ge 0$ with $0 < T(d) < \delta$ ,

\rho(\tau, d) \le 1 + \frac{8 \cdot |A| \cdot (|\mathcal K| + 1)}{\tau_{\min}(0)} \cdot M_\tau \cdot T(d).

Milestones

§3.5, p. 22. $\Lambda_\upsilon$ preserves the game space, maps WE and SO flows to WE and SO flows (divided by $\upsilon$ ), scales the total cost by $1/\upsilon$ , and leaves $\rho$ unchanged.
p. 43, first display. With $\sigma_a \equiv \tau_a(0)$ and $\Gamma' = (\sigma, d/T(d))$ : $\|\Gamma' - \Lambda_{T(d)}(\tau, d)\| = \max_a |\tau_a(T(d)) - \tau_a(0)| \le M_\tau T(d)$ when $T(d) \le b$ .
p. 43. $\mathcal C^*(\Gamma') \ge \tau_{\min}(0)$ for every $d$ .
p. 43, second display. For $T(d)$ below a threshold independent of $d$ : $\rho(\Gamma') = 1$ and $|\rho(\Lambda_{T(d)}(\tau,d)) - \rho(\Gamma')| \le 8|A|(|\mathcal K|+1) M_\tau T(d)/\tau_{\min}(0)$ .

Significance

The corollary gives a rate of convergence of the PoA to $1$ in light traffic for every cost vector that is strictly positive at $0$ and Lipschitz near $0$ , with an explicit constant depending only on the number of arcs, the number of O/D pairs, the Lipschitz constant and the free-flow costs $\tau_a(0)$ . It removes the fixed-proportion condition on the demands needed in the earlier polynomial result, and it combines with the heavy-traffic results for regularly varying costs to show that the PoA is bounded on whole cost slices (p. 43).

The result is proved in the paper, in a few lines on top of the local Lipschitz estimate (4.33) of Theorem 12a). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean model of nonatomic congestion games with demand normalizations and the metric (3.3), together with the comparison between a game of total demand $1$ and the constant-cost game at the same demand, which is reusable for other light-traffic statements.

Difficulty

A direct bound $\rho(\tau, d) \le 1 + c\,T(d)$ cannot simply be read off as $T(d) \to 0$ : the costs $\mathcal C^*$ and $\tilde{\mathcal C}$ both tend to $0$ with the demand, so their ratio is a quotient of two vanishing quantities, and an additive estimate on each cost says nothing about the ratio. The difficulty is to obtain a bound in which neither the threshold on $T(d)$ nor the constant depends on the demand vector $d$ , including the proportions $d_k/T(d)$ , which may vary arbitrarily, and some of which may vanish. Any argument whose constants depend on the particular game near which it works (as a pointwise Hölder constant does) gives only a pointwise statement, not the uniform one asserted here.

Formalization scope

The Lean development lives in the namespace SensitivityPoA.SmallDemand and builds on the published definition KellyStochasticNetworks_Wardrop (flows, arc flows, Wardrop's first principle). Conventions:

The structure is a 0/1 arc–route incidence matrix with a map from routes to O/D pairs. Standing assumptions (disclosed): every route contains an arc, $\mathcal K$ is nonempty, and Condition 1 (every arc on some route, $|\mathcal S_k| \ge 2$ ). Routes are arbitrary 0/1 columns, a generalization of loop-free paths.
Cost functions are functions $\mathbb R \to \mathbb R$ that are continuous, non-decreasing and non-negative on $[0,\infty)$ . "Strictly positive" means $\tau_a(x) > 0$ for all $x \ge 0$ . "Lipschitz on $[0,b]$ with constant $M_\tau$ " means $|\tau_a(x) - \tau_a(y)| \le M_\tau |x-y|$ for $x, y \in [0,b]$ ; nothing is assumed beyond $b$ .
$\mathcal C^*$ is the real infimum of the total cost over flows, $\tilde{\mathcal C}$ the real supremum over WE flows, $\rho$ their quotient. The maxima in (3.3) are real suprema of images of compact sets and Mathlib's sup norm.
The corollary is stated for the game $(\tau, d)$ itself; games of the cost slice agree with it on $[0, T(d)]$ .
Corrected slip. The corollary prints the constant $8 \cdot M_\tau \cdot |A| \cdot (|\mathcal K|+1)/\tau_{\min}(0) \cdot M_\tau$ , with $M_\tau$ twice. The display it summarizes has $M_\tau$ once, which is what is posed; it implies the printed form whenever $M_\tau \ge 1$ .

A trivializing formalization is ruled out: the threshold $\delta$ is chosen before $d$ (choosing it after $d$ makes the statement vacuous), $T(d) > 0$ is required (at $T(d) = 0$ Lean's $0/0 = 0$ would make $\rho = 0$ ), every game considered lies in the game space, and the bounds use $\le$ , which holds at equality cases.

Contributions welcome: proofs of the milestones, the comparison of WE costs under pointwise cost perturbation (the variational inequality of Wardrop equilibria), and existence of Wardrop equilibria for costs that are continuous and monotone only on $[0,\infty)$ . The source is the arXiv preprint v3; the published version in Mathematics of Operations Research is not the cited artifact.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the PoA in non-atomic congestion games, arXiv:2007.13979v3, 2021; published as A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games, Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979 , https://doi.org/10.1287/moor.2022.1292
R. Colini-Baldeschi, R. Cominetti, P. Mertikopoulos, M. Scarsini, When is selfish routing bad? The price of anarchy in light and heavy traffic, Operations Research 68(2), 2020. https://doi.org/10.1287/opre.2019.1894
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
H. Youn, M. T. Gastner, H. Jeong, Price of anarchy in transportation networks: efficiency and optimality control, Physical Review Letters 101, 2008. https://doi.org/10.1103/PhysRevLett.101.128701
S. J. O'Hare, R. D. Connors, D. P. Watling, Mechanisms that govern how the price of anarchy varies with travel demand, Transportation Research Part B: Methodological 84:55–80, 2016 (cited in arXiv:2007.13979v3, p. 50).

7 thms2 active usersReviewed

Algorithmic Game Theory Analysis Optimization+1·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 2: The Social Optimum Cost, the Wardrop Equilibrium Cost and the Price of Anarchy Are Continuous on the Game SpaceResearch Paper

Motivation

Traffic users choose routes for themselves, while a planner may choose routes that minimize everyone's combined travel cost. The price of anarchy measures the cost of the users' equilibrium relative to the planner's optimum. Travel demand and arc latency functions are estimated from data and change over time, so a ratio that changes abruptly under a small input change would be difficult to interpret or use. Wu and Möhring study this sensitivity for nonatomic congestion games, where each individual user has negligible influence on arc flows. Their preprint proves that the optimum cost, equilibrium cost, and their ratio vary continuously over the game space they define. This mission isolates that foundational continuity result. It supplies the qualitative starting point for the paper's later Hölder and Lipschitz estimates.

The cited artifact is arXiv:2007.13979v3, dated 2021. The article subsequently appeared in Mathematics of Operations Research in 2023, but theorem numbers and pages here refer to the preprint.

Setting

Fix finite sets $A$ of arcs, $S$ of routes, and $K$ of origin–destination pairs. Each route $s$ serves one pair $k$ and contains at least one arc. Every arc belongs to some route, and every pair has at least two routes. A game $\Gamma=(\tau,d)$ assigns each arc $a$ a nonnegative, nondecreasing, continuous latency function $\tau_a:[0,\infty)\to[0,\infty)$ and each pair $k$ a nonnegative demand $d_k$ . The total demand is $T(d)=\sum_{k\in K}d_k$ . These are the paper's basic model and standing combinatorial assumptions (pp. 10–11 and 14).

A feasible flow $f$ puts nonnegative traffic on routes so that the traffic for each pair sums to its demand. The induced arc flow is $f_a=\sum_{s\ni a}f_s$ . Its total cost is

C(\Gamma,f)=\sum_{a\in A} f_a\tau_a(f_a).

A social optimum (SO) is a feasible flow minimizing total cost. A Wardrop equilibrium (WE) is a feasible flow in which every route carrying positive traffic has minimum cost among the routes serving the same pair. Write $C^*(\Gamma)$ for the SO cost and $\widetilde C(\Gamma)$ for the WE cost. The paper shows that all SO flows have the same cost and all WE flows have the same cost (pp. 11–12 and 18).

A generalized game has the stated nonnegative demands and regular latency functions. The game space $\mathcal G(G,K,S)$ further requires $T(d)>0$ and $\tau_a(x)>0$ for every arc and every $0<x\le T(d)$ , the paper's Condition 2. On this space, the optimum cost is positive and the price of anarchy is defined by

\rho(\Gamma)=\frac{\widetilde C(\Gamma)}{C^*(\Gamma)}.

For $\Gamma=(\tau,d)$ and $\Gamma'=(\sigma,d')$ , the paper's distance $\operatorname{Dist}(\Gamma,\Gamma')$ is the maximum of three discrepancies: the sup norm of $d-d'$ , the largest $|\tau_a(x)-\sigma_a(x)|$ for $a\in A$ and $0\le x\le\min\{T(d),T(d')\}$ , and the sup norm of $\tau(T(d))-\sigma(T(d'))$ . The last term compares costs at the two games' respective demand endpoints. Games with equal demands and equal latency functions up to that demand are identified as equivalent (pp. 15–17, (3.1)–(3.3)).

Formalization targets

The supporting milestones establish a positive lower bound for $C^*$ and an upper bound for $\rho$ (Lemma 3), the distance properties of generalized games (Lemma 4), and behavior of feasible, SO, and WE flows under convergent game sequences (Lemma 5). The goal is the paper's Theorem 6, p. 19: for any sequence $\Gamma_n\in\mathcal G(G,K,S)$ with $\operatorname{Dist}(\Gamma_n,\Gamma)\to0$ and $\Gamma\in\mathcal G(G,K,S)$ ,

C^*(\Gamma_n)\to C^*(\Gamma),\qquad \widetilde C(\Gamma_n)\to\widetilde C(\Gamma),\qquad \rho(\Gamma_n)\to\rho(\Gamma).

Significance

The theorem establishes that sufficiently small changes in both demand and latency data produce small changes in the two total costs and their ratio. It allows the PoA to be treated as a stable observable of a game, including where the identity of an optimum or equilibrium flow changes. The result is qualitative: it does not supply a uniform rate of change. The same paper investigates sharper rates under additional assumptions (§4).

The mathematical result is proved in the paper. In this mission its statements and definitions are compiled Lean drafts, while proofs of Theorem 6 and its milestone lemmas remain open. A completed development would make the game-space metric, limit-of-flow statements, and cost continuity available for later sensitivity results on nonatomic routing.

Difficulty

Pointwise continuity of each $\tau_a$ does not by itself control an optimum or equilibrium when demands change: the feasible-flow sets change with $d$ , and a flow for one game need not be feasible for another. A converging sequence of games can also have different optimal or equilibrium flows at every index. The distance compares functions only on demand-relevant intervals, so limits of costs must respect those varying intervals. Finally, continuity of the quotient requires a positive optimum cost throughout the game space; the paper's Condition 2 is what makes that denominator meaningful (pp. 15–19).

Formalization scope

Lean uses finite types for arcs, routes, and pairs; a route is a nonempty $0$ – $1$ incidence column and is assigned to one pair. This admits arbitrary route collections rather than insisting on loop-free directed graph paths. The standing network predicate records the nonempty pair set, nonempty routes, every arc's membership in a route, and at least two routes per pair. Costs are total functions on the reals, with continuity, monotonicity, and nonnegativity required only on $[0,\infty)$ . Flow feasibility, arc flow, the Wardrop condition, and the potential reuse the published KellyStochasticNetworks_Wardrop definition. The total cost uses the arc formula; $C^*$ is an infimum over feasible flows and $\widetilde C$ a supremum over WE flows. On valid games these recover the paper's common SO and WE costs.

The distance uses the sup norm on finite vectors and a real supremum over the bounded shared demand interval. Convergence is stated sequentially, following the paper, without imposing a metric-space instance on raw games that may be equivalent. Every theorem involving $\rho$ quantifies over the game space, so a zero denominator or an empty equilibrium set cannot supply a spurious value. The route-count and arc-count factors in Lemma 3 are the actual finite cardinalities. Contributions that establish existence and compactness of relevant flow sets, equivalence of the arc and path cost formulas, and the stated limit properties are useful beyond this theorem.

Selected references

Z. Wu and R. H. Möhring, A sensitivity analysis of the PoA in non-atomic congestion games, arXiv:2007.13979v3, 2021. Preprint.
Z. Wu and R. H. Möhring, A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games, Mathematics of Operations Research 48(3), 2023. DOI.

9 thms2 active usersReviewed

Completed

Probability Theoretical Computer Science·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 4: For Every τ ∈ (0, 1) Some τ-Bounded Instance Gives No Value-Ordered Policy More Than (β^τ_k + ε) Times the OptimumResearch Paper

Why offer sets with overbooking matter

A firm with $k$ open positions often cannot interview and offer sequentially: hiring seasons are short, and offers go out in one batch. Some recipients decline, so the firm overbooks, sending more offers than it has positions, and pays for every hire beyond capacity. The same trade-off appears in airline and hotel overbooking and in university admissions. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study this Simultaneous Offering problem as one of three hiring-pipeline models, and analyse the natural class of value-ordered policies, which offer to the best candidates first. Their Theorem 3 shows that a value-ordered policy built from a linear-programming relaxation guarantees a fraction $\alpha^\tau_k$ of the optimum when every value is at least $\tau$ . This mission formalizes the converse, Theorem 4: no value-ordered policy can guarantee more than $\beta^\tau_k$ .

Setting

An instance has $k \ge 1$ positions and $n \ge k$ candidates. Candidate $i$ accepts an offer with probability $p_i \in [0,1]$ , independently of the others, and then adds value $v_i \ge 0$ . The firm chooses a set $S$ of candidates and sends all offers at once. If $A \subseteq S$ is the random set of acceptances, the reward is

\sum_{i \in A} v_i - [\,|A| - k\,]^+,

so each hire beyond capacity costs $1$ (the paper rescales values so that this cost is $1$ ). Write $R(I, S)$ for the expected reward of offering to $S$ , and $\mathrm{OPT}_{\mathrm{sim}}(I) = \max_S R(I, S)$ for the best expected reward; randomizing over offer sets cannot do better.

Candidates are labelled so that $v_1 \ge v_2 \ge \cdots \ge v_n$ . A value-ordered policy with parameter $m \in [n]$ offers to $\{1, \dots, m\}$ . An instance is $\tau$ -bounded, $I \in \mathcal{I}^\tau_{\mathrm{sim}}$ , if $v_i \ge \tau$ for all $i$ . Without such a bound value-ordered policies can be arbitrarily poor (§6.1); $\tau$ measures how soft the capacity is, from nearly hard ( $\tau$ close to $0$ ) to nearly compensated by any hire ( $\tau$ close to $1$ ), and both theorems take $\tau \in (0,1)$ .

For $\lambda \ge 0$ let $\mathbb{E}[\min\{\mathrm{Pois}(\lambda), k\}]$ be the mean of a Poisson variable truncated at $k$ , and

f_{k,\tau}(s) = s - \frac{s}{\tau} + \frac{\mathbb{E}[\min\{\mathrm{Pois}(sk), k\}]}{\tau k}, \qquad \alpha^\tau_k = \sup_{0 \le s \le 1} f_{k,\tau}(s), \qquad \beta^\tau_k = \sup_{s \ge 0} f_{k,\tau}(s).

In Lean these are SimInstance, reward, OPTsim, valueOrdered, TauBounded, expMinPois, ratioObj, alpha and beta in the namespace HiringLP.SimUpper.

Formalization targets

Goal: Theorem 4 (p. 30)

For every $k \ge 1$ , $\varepsilon > 0$ and $\tau \in (0,1)$ there is a valid, sorted instance $I \in \mathcal{I}^\tau_{\mathrm{sim}}$ with $k$ positions such that

R(I, \{1, \dots, m\}) \le (\beta^\tau_k + \varepsilon)\,\mathrm{OPT}_{\mathrm{sim}}(I) \quad \text{for every } m \in [n].

Milestones on the hard instance (App. D.7)

The instance has $j^2$ type-1 candidates with $p_i = k/j$ , $v_i = \tau + \delta$ , $\delta = \varepsilon\tau/j$ , and $k$ type-2 candidates with $p_i = 1$ , $v_i = \tau$ . With $B \sim \mathrm{Bin}(m, k/j)$ and $0 \le m \le j^2$ :

\mathrm{OPT}_{\mathrm{sim}}(I) \ge k\tau,

R(I, \{1,\dots,m\}) = (\tau + \delta)\frac{km}{j} + \mathbb{E}[\min\{0, k - B\}] \le k + \frac{km}{j}\bigl(\tau + \delta - \Pr[B > k]\bigr) \quad \text{(EC.15)},

R(I, \{1,\dots,m\}) \le \varepsilon k \tau + \frac{km}{j}(\tau - 1) + \mathbb{E}[\min\{k, B\}] \quad \text{(EC.18)}.

Companions: the maximisers (App. D.8)

Proposition EC.5: optimal $s^*_\alpha$ , $s^*_\beta$ exist, $s^*_\alpha = \min\{s^*_\beta, 1\}$ , and $\tau = 1 - e^{-s^*_\beta k}\sum_{j<k} (s^*_\beta k)^j/j!$ . Proposition EC.6: $s^*_\alpha = s^*_\beta$ if and only if $\tau \le 1 - e^{-k}\sum_{j<k} k^j/j!$ , which holds whenever $\tau \le 1/2$ .

Significance

Theorem 4 bounds what any value-ordered policy can guarantee on $\tau$ -bounded instances, against the true optimum rather than an LP relaxation. With Theorem 3 it brackets the best guarantee of the class between $\alpha^\tau_k$ and $\beta^\tau_k$ , and by Proposition EC.6 the two coincide when $\tau \le \Pr[\mathrm{Pois}(k) \ge k]$ , in particular for all $k$ when $\tau \le 1/2$ . In that region the paper's truncated-LP policy is the best value-ordered policy in the worst case. The instance also shows why the restriction to value-ordered policies costs something: the optimum offers to the reliable type-2 candidates, while a value-ordered policy must first exhaust the slightly more valuable unreliable ones.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces a formal version of Theorem 4 and the finite- $j$ estimates on which its proof rests, together with a reusable finite-sum encoding of independent acceptances, truncated Poisson and Binomial expectations, and the constants $\alpha^\tau_k$ , $\beta^\tau_k$ .

Difficulty

The milestones are exact identities and inequalities at a fixed $j$ ; the hard part is the passage to the limit. The page's proof lets $j \to \infty$ with $m_j/j \to s$ and replaces $\mathrm{Bin}(m_j, k/j)$ by $\mathrm{Pois}(sk)$ . The goal, however, asks for one finite instance on which the bound holds for every $m$ simultaneously, including $m$ of order $j^2$ and the values $m > j^2$ that also offer to type-2 candidates. A pointwise limit for each fixed $s$ does not give this; the Binomial–Poisson error has to be controlled uniformly in $m$ , and the error must fit inside the slack $\varepsilon$ , part of which the term $\delta$ already uses. Note also that the comparison runs the wrong way for the obvious argument: $\min\{\cdot, k\}$ is concave and the Binomial is less spread than the Poisson, so $\mathbb{E}[\min\{k, B\}]$ is at least its Poisson counterpart and a one-sided comparison cannot replace an approximation bound.

Formalization scope

All randomness is finite. The expected reward is an explicit sum over the $2^n$ accepting sets with product probabilities; the Binomial pmf, its truncated mean and its tail are finite sums written by hand. The truncated Poisson mean is the series with the Poisson pmf. All quantities are real. Candidates are Fin n, so the paper's candidate $i$ is index $i - 1$ ; sortedness is the hypothesis Antitone v in Valid, which also contains $1 \le k \le n$ , $p \in [0,1]^n$ and $v \ge 0$ . $\mathrm{OPT}_{\mathrm{sim}}$ is the maximum over all offer sets, never over value-ordered ones. $\beta^\tau_k$ is the supremum over $[0, \infty)$ and $\alpha^\tau_k$ over $[0, 1]$ . The page leaves $k$ implicit in $\beta^\tau_k$ ; the goal quantifies over every $k \ge 1$ and requires the instance to have exactly $k$ positions. The quantifiers are "for all $k, \varepsilon, \tau$ , there is an instance, for all $m$ ".

The goal does not fix the hard instance: any instance proves it. A formalization in which the comparison is with the best value-ordered policy, in which $\beta^\tau_k$ is a free parameter, or in which the reward is defined by the proof's Binomial formula would be a different statement and is ruled out by the definitions above. The definitions are not specialized to the hard instance, which appears only as a separate definition used by the milestones.

A complete development needs: finite sums over subsets with product weights and the reduction to a Binomial count for identical candidates; summability and continuity of the truncated Poisson mean; a Binomial–Poisson approximation bound uniform in the number of trials; concavity of $f_{k,\tau}$ in $s$ . The Poisson and Binomial infrastructure is reusable well beyond this mission. Proofs of the milestones, of the companions, and of auxiliary approximation lemmas are all welcome.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2210.04059
M. Mitzenmacher, E. Upfal, Probability and Computing, 2nd ed., Cambridge University Press, 2017 (Exercise 5.14, cited for $\Pr[\mathrm{Pois}(k) \ge k] \ge 1/2$ ). https://doi.org/10.1017/9781316651124
A. D. Barbour, P. Hall, On the rate of Poisson convergence, Mathematical Proceedings of the Cambridge Philosophical Society 95, 1984. https://doi.org/10.1017/S0305004100061402

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Probability·Captain: mikedeng1

Designing Approximately Optimal Search on Matching Platforms 2: Every Set of Assortments Has a Unique Profile of Thresholds Equal to Expected UtilitiesResearch Paper

Motivation

Online matching platforms for dating, freelancing or ride sharing do not match agents themselves. They decide whom each agent gets to see and how often, and the agents then accept or reject. Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search. The platform designs assortments, which are rates at which types of agents meet, and the agents play an equilibrium of the induced search game. The platform's design problem only makes sense if every choice of assortments leads to a single, well-defined equilibrium outcome. Otherwise "the welfare of an assortment" is not a function of the assortment. This is not automatic: even for simple asymmetric preferences under random meetings, multiple stationary equilibria can arise (Burdett and Coles 1997).

This mission formalizes that well-posedness result, Proposition 3.1(1) of the paper, together with the fixed-point and iteration lemmas of Appendix A.3 and Appendix B.3 on which its proof rests. It is the companion of the mission on the paper's quarter-approximation theorem (Theorem 4.1), which uses the same model.

The source is the arXiv v2 preprint (18 Aug 2021). The Management Science version may number results differently.

Setting

There are finitely many agent types on each side of the market, a set $\mathcal M$ and a set $\mathcal W$ , with $\Theta=\mathcal M\cup\mathcal W$ . Agents of every type leave the market unmatched at a life-event rate $\delta>0$ , and type $\theta$ arrives at rate $\alpha_\theta>0$ . When an agent of type $m$ meets an agent of type $w$ , the pair draws one utility $u\sim F_{mw}$ . Valuations are symmetric: both agents receive $u$ if they match, and $F_{wm}:=F_{mw}$ . Each $F_{mw}$ is a probability law on $\mathbb R$ with no atoms (a "continuous distribution").

An assortment for type $\theta$ is a family of rates $\lambda_\theta(\theta')\ge0$ at which type- $\theta$ agents meet type- $\theta'$ agents on the opposite side. Under a threshold strategy with threshold $\tau_\theta$ , a type- $\theta$ agent accepts a meeting if and only if $u\ge\tau_\theta$ . A meeting turns into a match when both agents accept, i.e. when $u\ge\max(\tau_\theta,\tau_{\theta'})$ . If every type plays a threshold strategy, the expected utility of a type- $\theta$ agent is (equation (5))

\bar u_\theta(\tau)=\frac{\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty u\,dF_{\theta\theta'}}{\delta+\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty dF_{\theta\theta'}} .

A type's own threshold enters its own utility through $\max(\tau_\theta,\tau_{\theta'})$ .

One type's equation. Fix the thresholds $\tau_i$ of the opposite types. Write $B(t)$ for the right-hand side of (5) with $\tau_\theta$ replaced by $t$ . Lemma A.3 states that $t=B(t)$ has exactly one solution. The best-response map of Appendix A.3 sends a profile $\tau$ to the profile in which each type's new threshold is that solution, computed against the opposite side's thresholds in $\tau$ . A best-response sequence starts at the all-zero profile and applies this map repeatedly.

Formalization targets

Goal: Proposition 3.1, item 1 (fixed-point form)

For any fixed assortments there is exactly one threshold profile $\tau\in\mathbb R^{\mathcal M}\times\mathbb R^{\mathcal W}$ with

\tau_\theta=\bar u_\theta(\tau)\qquad\text{for every }\theta\in\Theta .

Uniqueness ranges over all real profiles.

Milestones

Lemma B.1 (p. 40). With $\lambda_i>0$ and $\tau_i\ge0$ , $\rho=\max_{t\ge0}B(t)$ is attained and satisfies $B(\rho)=\rho$ . $B$ is weakly increasing on $(-\infty,\rho]$ and weakly decreasing on $[\rho,\infty)$ .
Lemma A.3 (p. 35). With $\lambda_i\ge0$ and arbitrary $\tau_i$ , the equation $t=B(t)$ has exactly one real solution.
§A.3, p. 37, first claim. Along a best-response sequence $\tau^{(0)}\equiv0,\tau^{(1)},\dots$ , the odd iterates are weakly decreasing and the even iterates are weakly increasing, componentwise.
§A.3, p. 37, second claim. Every odd iterate dominates every even iterate: $\tau^{(2j)}\le\tau^{(2i+1)}$ .
Proposition A.4 (p. 36). There is a universal $C$ such that $\tau^{(C|\Theta|)}$ is a fixed point of the best-response map, and the sequence is constant from that index on.

Significance

Proposition 3.1 is what makes the platform's problem OptimalDirectedSearch well defined. Assortments determine a unique threshold profile. That profile determines the matching rates (Lemma 3.2) and, through stationarity, the population masses. Welfare is then a function of the assortments, and the program (6) used for Theorem 4.1 encodes exactly this fixed point as its incentive constraint (6e). The constructive proof also yields an algorithm: iterate best responses from zero, and the iteration stops after $O(|\Theta|)$ rounds.

Formalizing it adds three things beyond the paper. First, a checked version of an argument the paper gives informally, including the odd/even sandwich of the iteration, which the paper proves in a few lines. Second, a reusable fixed-point and unimodality lemma for ratios of tail integrals, $B(t)=\int_t^\infty u\,dG\,/\,(\delta+\int_t^\infty dG)$ , which recurs in reservation-value arguments in search theory. Third, an exact accounting of the hypotheses: integrable utilities and the reading of the best-response map. To our knowledge none of these results has been machine-checked.

Difficulty

The obvious route to uniqueness, a contraction argument for the map $\tau\mapsto\bar u(\tau)$ , fails. That map is neither monotone nor contractive in general, since raising a type's own threshold can raise or lower its utility. Existence by Brouwer's fixed-point theorem gives no uniqueness and no algorithm. The best-response iteration does not converge monotonically either: its odd and even iterates move in opposite directions, so convergence in finitely many rounds is a combinatorial statement about the order of the thresholds, not a limit argument. A formal proof also needs continuity and monotonicity of tail integrals of atomless laws, which Mathlib provides only in pieces.

Formalization scope

The two sides are separate finite types M and W. A threshold profile is a pair of functions (M → ℝ) × (W → ℝ), ordered componentwise. A market records $\delta$ , $\alpha$ and the laws F m w : Measure ℝ. The standing assumptions are:

$\delta>0$ ;
$\alpha_\theta>0$ , which is implicit in the paper and stated explicitly;
each $F_{mw}$ is a probability measure with no atoms (NullSingletonClass);
each $F_{mw}$ has an integrable identity. This is implicit in the paper, which uses $\int u\,dF$ as a real number, and is stated explicitly.

Tails are $\int_a^\infty dF=F([a,\infty))$ and $\int_a^\infty u\,dF=\int_{[a,\infty)}u\,dF$ . Capacity (2), flow balance (3) and stationarity (1) are not hypotheses, because Proposition 3.1 holds for any fixed assortments.

The best-response map is encoded as a relation: each new threshold solves its own equation $t=B(t)$ against the opposite side's input thresholds. This is the paper's reading ("This map is a best response by Lemma A.3"). Evaluating (5) at the old profile, own old threshold included, would be a different map. Under that reading finite convergence and the p. 37 claims are false: with one type per side, $\lambda\equiv1$ , $\delta=1$ and $F$ uniform on $[0,1]$ , its iterates are rational and converge only in the limit to $2-\sqrt3$ .

Two formalizations would trivialize the goal, and both are ruled out. Uniqueness is over all real profiles, not only nonnegative ones or those reached by the iteration. The tail integrals are not allowed to vanish by default for non-integrable laws, because integrability is a hypothesis. $O(|\Theta|)$ is encoded with a constant chosen before the market.

Not formalized: the agents' Markov decision process of Appendix A.1. Consequently "this strategy profile is a Nash equilibrium", item 2 of Proposition 3.1, Lemmas A.1–A.2 and the best-response sentences of Lemma A.3 and Proposition A.4 are out of scope.

Contributions welcome: continuity and monotonicity lemmas for $a\mapsto\int_{[a,\infty)}u\,dF$ and $a\mapsto F([a,\infty))$ for atomless integrable laws, which are reusable well beyond this mission, and proofs of the milestones in any order.

Selected references

N. Immorlica, B. Lucier, V. Manshadi, A. Wei, Designing Approximately Optimal Search on Matching Platforms, Management Science, 2023; preprint arXiv:2102.09017v2, 2021. https://arxiv.org/abs/2102.09017
K. Burdett, M. G. Coles, Marriage and Class, Quarterly Journal of Economics 112(1), 1997. https://doi.org/10.1162/003355397555127

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design·Captain: mikedeng1

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 3: The k-HL Mechanism Is Ex-Post IC-IR and a (k+3)-Approximation to Welfare with k Signal ValuesResearch Paper

Motivation

In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent $i$ holds a private signal $s_i$ , and every agent's value is a publicly known function of the whole signal profile $\mathbf s=(s_1,\dots,s_n)$ .

With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor $n$ (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking $k$ values.

Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, $c$ -single-crossing condition, with ratios depending on $c$ and $n$ . Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.

Setting

There are $n$ agents and $m$ items, and $k\ge1$ signal values. Each agent $i$ has a signal $s_i\in\{0,1,\dots,k-1\}$ , and $\{0,\dots,k-1\}^n$ is the grid. Agent $i$ 's value for a bundle $T\subseteq[m]$ at the profile $\mathbf s$ is $v_{iT}(\mathbf s)\ge0$ ; the empty bundle is worth $0$ , and for nonempty $T$ , $v_{iT}$ is weakly increasing in every signal and strictly increasing in $s_i$ . We write $(\mathbf s_{-i},x_i)$ for the profile with agent $i$ 's signal replaced by $x$ , and $(\mathbf s_A,\mathbf 0_B)$ for the profile that keeps the signals of the agents in $A$ and sets those in $B$ to $0$ .

A function $w$ of the profile is SOS if for every coordinate $j$ , all $x,\delta\ge0$ with $x+\delta\le k-1$ , and grid profiles with $\mathbf s'_{-j}\le\mathbf s_{-j}$ coordinatewise,

w(\mathbf s_{-j},x+\delta)-w(\mathbf s_{-j},x)\;\le\;w(\mathbf s'_{-j},x+\delta)-w(\mathbf s'_{-j},x).

The setting is SOS when every $v_{iT}$ is.

A feasible allocation gives disjoint bundles $T_1,\dots,T_n$ ; its welfare at $\mathbf s$ is $\sum_i v_{iT_i}(\mathbf s)$ . A deterministic mechanism maps reported profiles to an allocation and payments. Agent $i$ 's utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

The mechanism k-HL runs, with probability $p_{RT}=\frac{k-1}{k+3}$ , Random Threshold: choose $\ell$ uniformly in $\{1,\dots,k-1\}$ , call $N_{\ge\ell}=\{i:s_i\ge\ell\}$ the high agents, allocate to them a feasible allocation maximizing $\sum_{i\in N_{\ge\ell}}v_{iS_i}(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ , and charge agent $i$ receiving $\bar T_i$ the price $v_{i\bar T_i}(\mathbf s_{-i},s_i=\ell-1)$ . Otherwise it runs Random Sampling: split the agents uniformly at random into $A$ and $B$ , allocate to $B$ a feasible allocation maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$ , and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.

Formalization targets

Goal: Theorem 6.1 (p. 20)

For SOS valuations with $k$ signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile $\mathbf s$ and every feasible allocation $T^*$ ,

\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(k+3)\,\mathbb E\bigl[\text{welfare of k-HL at }\mathbf s\bigr],

where the expectation is over $\ell$ , over $(A,B)$ and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.

Milestones

Displays (6)–(7): the welfare of any allocation is at most $\mathsf{OTHER}+\mathsf{SELF}$ , where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$ and $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$ .
Random Sampling is ex-post IC-IR for every partition.
Random Threshold is ex-post IC-IR for every threshold.
Lemma 6.2: $\mathsf{SELF}\le(k-1)\,\mathbb E[\text{welfare of Random Threshold}]$ .
Lemma 6.3: $\mathsf{OTHER}\le4\,\mathbb E[\text{welfare of Random Sampling}]$ .

Significance

Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio $k+3$ depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the $(2\log_2k+4)$ -approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.

The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.

Difficulty

Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within $\{\ell,\dots,k-1\}$ leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data $(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid $\{0,\dots,k-1\}^n$ , with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in $A$ receive nothing, agents outside $N_{\ge\ell}$ receive nothing) must match the mechanism exactly.

Formalization scope

Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below $k$ ; a condition on all of $\mathbb N^n$ would be stronger than the paper's. The empty bundle is worth $0$ and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive $\emptyset$ .

The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of $B$ ) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, $\frac1{k-1}\sum_{\ell=1}^{k-1}$ and $2^{-n}\sum_{B\subseteq[n]}$ , never an existential or universal quantifier over $\ell$ or $B$ . The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of $B$ , the agent's own included (the page's " $v_{ij}(\mathbf s_A,\mathbf 0_B)$ " is read as $v_{iT}(\mathbf s_A,\mathbf 0_B)$ ). For $k=1$ , $p_{RT}=0$ and the threshold average is the empty sum.

Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing $T^*$ .

Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.

The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.

Selected references

A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, ACM EC 2018 (cited as [Eden et al., 2018] in the source).
E. Maskin, Auctions and Privatization, in H. Siebert (ed.), Privatization, 1992 (cited as [Maskin, 1992] in the source).
P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737
P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00248

9 thms2 active usersReviewed

Completed

Economics Optimization·Captain: mikedeng1

Climate Impact Investing 2: With Poisson Climate Uncertainty λ, If the Green Portfolio Is Green Then y*_λ Rises to 1 in λ, So Equilibrium Emissions Rise as Uncertainty GrowsResearch Paper

Motivation

Climate impact investing refers to investors who tilt their portfolios away from companies with large greenhouse-gas emissions. Its stated aim goes beyond aligning portfolios with values: by raising the cost of capital of polluting companies, it is meant to change what those companies do. De Angelis, Tankov and Zerbib (SSRN 3562534, published in Management Science, 2022, doi:10.1287/mnsc.2022.4472) build an equilibrium model in which this mechanism can be computed. Green investors penalize the expected climate externalities of companies. Companies choose emission schedules to maximize their market value net of abatement costs. Prices, portfolios and emissions are determined jointly.

Section 4 of the paper asks what happens when the green investors are uncertain about future climate externalities, for instance because news on climate risk or regulation arrives in rare large shocks. Its answer is that, in the most common market configuration, more uncertainty makes green investors hedge by holding more brown assets, which weakens the incentive to abate, so that equilibrium emissions rise as climate uncertainty grows. This mission formalizes that result and the chain of statements behind it.

Setting

Fix a date $t$ in a horizon $[0,T]$ ; every object below is evaluated at that date, and its subscript is dropped where harmless. There are $n$ companies, indexed by $i$ , with asset covariance matrix $\Sigma_t$ (positive definite). Green investors hold wealth share $\alpha\in(0,1)$ , regular investors the rest, with risk aversions $\gamma^g,\gamma^r>0$ .

Company $i$ emits at rate $\psi^i_t\ge 0$ and pays the marginal abatement cost $c^i_t\ge 0$ . The green investors attach to company $i$ the climate externality $\theta^i_t(\psi)=\kappa_{0,t}-\frac{\kappa_t}{2}\psi^2$ , the companies use $\theta^{c,i}_t(\psi)=\kappa^c_{0,t}-\frac{\kappa^c_t}{2}\psi^2$ , and all $\kappa$ 's are positive. With a rate of time preference $\rho>0$ , the time factors are $\beta^c_t=(e^{-\rho t}-e^{-\rho T})/(1-e^{-\rho T})$ and $\beta_t=(1-e^{-\rho t})/(1-e^{-\rho T})$ .

Climate uncertainty is a Poisson process of intensity $\lambda>0$ : a smaller $\lambda$ means rarer, larger shocks, i.e. more uncertainty. For a fixed externality vector $\theta$ , the equilibrium of Proposition 5 is described by a scalar $y_\lambda>0$ solving

y_\lambda=\exp\Big\{-\frac{\alpha\gamma^g}{\lambda}\Big(\mathbf 1^\top\theta+\frac{y_\lambda}{\gamma^r}\theta^\top\Sigma_t^{-1}\theta\Big)\Big\},

and the green portfolio is $N^{g,\lambda}=\alpha(\mathbf 1+\frac{y_\lambda}{\gamma^r}\Sigma_t^{-1}\theta)$ . Without uncertainty, $y=1$ and the portfolio is $N^g$ . When the companies take $y$ as given (the large-market assumption), company $i$ 's optimal emission rate is

\psi^i_t(y)=\frac{c^i_t}{\alpha\beta_t\kappa_t\,y+\beta^c_t\kappa^c_t},

and $y$ itself must then solve the fixed-point equation $y=\exp\{-\frac{\alpha\gamma^g}{\lambda}g^*(y)\}$ , where

g^*(y)=\mathbf 1^\top\theta_t(\psi_t(y))+\frac{y}{\gamma^r}\theta_t(\psi_t(y))^\top\Sigma_t^{-1}\theta_t(\psi_t(y)).

Its solution is $y^*_\lambda$ . Finally, $\psi^{*,0}_t=\psi_t(1)$ is the schedule without uncertainty.

Formalization targets

Goal: Proposition 8(iii)

Assume condition (24) at the date $t$ : $\sum_j(\Sigma_t^{-1})_{ij}\,y\,\theta^j_t(\psi^j_t(y))\ge-\gamma^r/2$ for all $i$ and all $y>0$ . Let $\lambda\mapsto y^*_\lambda$ solve the fixed-point equation. Then the sign of the green portfolio's externality without uncertainty decides the direction of the response:

\theta_t(\psi^{*,0}_t)^\top N^g_t>0\ \Longrightarrow\ y^*_\lambda\uparrow 1\ \text{strictly in }\lambda,\quad \lambda\mapsto\psi^{*,i}_t\ \text{nonincreasing},

the opposite if $\theta_t(\psi^{*,0}_t)^\top N^g_t<0$ , and $y^*_\lambda\equiv 1$ with unchanged emissions if it is $0$ .

Milestones

In the order of the attack:

Proposition 7: for fixed $y>0$ , $\psi^i_t(y)$ is the unique maximizer of the company's pointwise objective.
Proposition 8(i): the fixed-point equation has a positive solution for every $\lambda>0$ .
Under (24), $g^*$ is increasing.
Proposition 8(ii): under (24), the solution is unique.
$\psi^*_t(1)=\psi^{*,0}_t$ , and $\alpha g^*(1)=\theta_t(\psi^{*,0}_t)^\top N^g_t$ .
Equation (20) has exactly one positive solution $y_\lambda$ .
Proposition 6(ii)–(iv): the same three-way comparative static at a fixed schedule, for $y_\lambda$ , the green portfolio and the expected returns.

Companion statements cover Proposition 6(i) (the green portfolio's market risk increases in $\lambda$ ), Lemma 1, and the algebraic core of Proposition 5.

Significance

The result. Proposition 8(iii) is the paper's headline claim about uncertainty, and it is quoted in its abstract: uncertainty about future climate externalities, by making green investors hedge, can push companies to increase their emissions. The paper's Lemma 1 shows that the positive case, a green portfolio with positive climate externality, is the common one. The sign condition is therefore not a curiosity. It separates markets where uncertainty undermines impact investing from markets where it strengthens it.

Formalizing it. The proofs in the appendix are short and leave several steps implicit, and in two places the printed formulas do not match their own derivation (see the scope section). A machine-checked version settles the precise hypotheses under which the comparative statics hold. It also provides reusable statements about scalar fixed-point equations of the form $-\lambda\log y=G(y)$ with nondecreasing $G$ . No part of this paper has been formalized before.

Difficulty

At a fixed schedule, everything follows from the fact that $g$ is affine and nondecreasing in $y$ . Once the schedule is endogenous, $g^*$ is nonlinear and in general not monotone, so neither uniqueness nor monotonicity in $\lambda$ comes for free. The work lies in turning condition (24) into monotonicity of $g^*$ . That requires differentiating the quadratic form $\theta(\psi(y))^\top\Sigma^{-1}\theta(\psi(y))$ through the schedule and controlling its sign company by company. The limit $y^*_\lambda\to 1$ as $\lambda\to\infty$ needs bounds on $g^*$ along the solution path rather than the formal Taylor expansion in $1/\lambda$ the paper gives for (20).

Formalization scope

The stochastic layer is not formalized: Brownian cash-flow news, subjective measures built by Girsanov's theorem, CARA utility maximization, the Poisson process of climate shocks, and Propositions 1 and 5 as equilibrium statements. The statements start from the objects the proofs start from: the first-order and market-clearing system (45), and equations (20), (22) and (23). Everything is stated at one fixed date $t$ , with vectors in $\mathbb R^n$ indexed by Fin n, $\Sigma_t$ positive definite and $\Sigma_t^{-1}$ Mathlib's matrix inverse.

The standing assumptions are hypotheses of the statements:

$\rho,T>0$ and $t\in[0,T]$ ;
$0<\alpha<1$ ;
$\gamma^r,\gamma^g>0$ ;
all $\kappa$ 's positive;
$c^i_t\ge0$ .

The relation $\alpha=\gamma^r/(\gamma^r+\gamma^g)$ is assumed only where it is used, in the core of Proposition 5. The solution maps $\lambda\mapsto y_\lambda$ and $\lambda\mapsto y^*_\lambda$ enter only through the hypothesis that each value solves its equation. A theorem that assumed monotonicity of $g^*$ , uniqueness, or the sign of $g^*(1)$ would trivialize the goal; the goal assumes only condition (24).

Disclosed corrections of the printed text:

(23) and $g^*$ . The page prints a factor $\alpha y/\gamma^r$ in the quadratic term. Footnote 25 derives (23) from (20), which has $y/\gamma^r$ , and only that version makes the sign test of (iii) agree with the sign of $g^*(1)$ . The formalization uses $y/\gamma^r$ .
(24). The derivative of the quadratic form on p. 72 omits the factor 2 that the symmetry of $\Sigma^{-1}$ produces. With the corrected $g^*$ , the argument needs the bound $-\gamma^r/2$ , not $-\gamma^r/\alpha$ . Whether uniqueness holds under the printed bound is not claimed.
Existence at $t=T$ . The proof of (i) uses $\beta^c_t>0$ , so existence is stated for $t\in[0,T)$ .
Asymptotic uniqueness. The last sentence of (ii), uniqueness as $\lambda\to\infty$ , has no proof in the paper and is not stated.

Two readings are fixed. "Monotonically increasing" for $y_\lambda$ is strict. The emission response is weak, because at $t=0$ the schedule does not depend on $y$ . "Reallocate towards brown assets" means that the green portfolio's climate externality $\theta^\top N^{g,\lambda}$ falls as $\lambda$ falls.

The development needs elementary real analysis: the intermediate value theorem on $(0,\infty)$ , monotonicity from derivatives, and limits at infinity. It also needs finite-dimensional linear algebra for positive definite matrices. The lemmas about $-\lambda\log y=G(y)$ are reusable beyond this mission. Proofs of the companion statements, which are algebraic, are welcome as warm-ups.

Selected references

T. De Angelis, P. Tankov, O. D. Zerbib, Climate Impact Investing, SSRN 3562534, version of June 25, 2021. https://ssrn.com/abstract=3562534
T. De Angelis, P. Tankov, O. D. Zerbib, Climate Impact Investing, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4472
L. Pástor, R. F. Stambaugh, L. A. Taylor, Sustainable investing in equilibrium, Journal of Financial Economics 142(2), 2021. https://doi.org/10.1016/j.jfineco.2020.12.011

13 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Reinforcement Learning·Captain: mikedeng1

A First-Order Approach to Accelerated Value Iteration 4: Safe Accelerated Value Iteration Converges to v* at Rate O(λ′^s) for Every λ′ ∈ [λ, 1)Research Paper

Motivation

Value iteration (VI) is the standard method for computing the optimal value function of a discounted Markov decision process (MDP). It applies the Bellman operator repeatedly, and because that operator is a $\lambda$ -contraction in the sup norm, the error after $s$ steps is at most $\lambda^s$ times the initial error. When the discount factor $\lambda$ is close to $1$ , as in long-horizon planning, this rate is slow.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read value iteration as a gradient-type method and transfer momentum schemes from convex optimization (Nesterov acceleration, heavy-ball momentum) to the Bellman operator. On reversible policy chains these accelerated schemes provably converge faster than VI. On general MDPs, however, the accelerated iterates need not converge at all: the paper exhibits instances on which Accelerated Value Iteration (A-VI) oscillates or diverges. Section 7 of the paper resolves this tension with Safe Accelerated Value Iteration (S-AVI, Algorithm 1), which tries an accelerated step at every period and keeps it only when it makes enough progress on the Bellman equation $v = T(v)$ . This mission formalizes the convergence guarantee of S-AVI, Theorem 7.1.

Setting

Let $\mathbb S$ be a finite set of states and $\mathbb A$ a nonempty finite set of actions. A discounted MDP is given by a transition kernel $P$ , with $P_{iaj}\ge 0$ the probability of moving from state $i$ to state $j$ under action $a$ and $\sum_j P_{iaj} = 1$ ; a reward $r_{ia}\in\mathbb R$ for each state-action pair; and a discount factor $\lambda \in (0,1)$ . The Bellman operator $T : \mathbb R^{\mathbb S} \to \mathbb R^{\mathbb S}$ is

T(v)_i = \max_{a\in\mathbb A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj}\, v_j \Big\}.

The sup norm is $\|v\|_\infty = \max_i |v_i|$ . The optimal value function $v^*$ is the unique fixed point of $T$ . For a vector $v$ , the quantity $\|v - T(v)\|_\infty$ is its Bellman residual.

S-AVI (Algorithm 1) takes a scalar $\lambda' \in [\lambda, 1)$ , step sizes $\alpha, \gamma > 0$ and any starting vector $v_0$ . It sets $v_1 = T(v_0)$ , and at each period $s \ge 1$ forms

h_s = v_s + \gamma\,(v_s - v_{s-1}), \qquad v_{s+1/2} = h_s - \alpha\,\big(h_s - T(h_s)\big).

If $\|v_{s+1/2} - T(v_{s+1/2})\|_\infty \le \lambda'^{\,s+1}\,\|v_0 - T(v_0)\|_\infty$ , the accelerated candidate is accepted, $v_{s+1} = v_{s+1/2}$ ; otherwise the algorithm takes a value-iteration step, $v_{s+1} = T(v_s)$ . In the Lean development the MDP is AccelVI.SafeAVI.MDP with validity predicate MDP.Valid, the operator is bellman M, and the iterates are savi M lam' α γ v0 : ℕ → (S → ℝ).

Formalization targets

Goal: Theorem 7.1

For a valid MDP, any $\lambda' \in [\lambda, 1)$ , any $\alpha, \gamma > 0$ and any $v_0$ , the S-AVI iterates converge to $v^*$ , and

v_s = v^* + O(\lambda'^{\,s}), \quad \forall s \ge 0,

that is, there is a constant $C$ with $\|v_s - v^*\|_\infty \le C\,\lambda'^{\,s}$ for every $s \ge 0$ . The constant is left unspecified, as in the paper.

Milestones

$T$ is a $\lambda$ -contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
The first period: $\|v_1 - T(v_1)\|_\infty \le \lambda\|v_0 - T(v_0)\|_\infty \le \lambda'\|v_0 - T(v_0)\|_\infty$ (p. 13).
Geometric decay of the residual: $\|v_s - T(v_s)\|_\infty \le \lambda'^{\,s}\|v_0 - T(v_0)\|_\infty$ for all $s$ (p. 14).
The residual controls the error: $\|v - v^*\|_\infty \le (1-\lambda)^{-1}\|v - T(v)\|_\infty$ for every $v$ (p. 14).

Significance

The result. Theorem 7.1 says that the safeguard costs nothing in the worst case: S-AVI converges on every MDP at rate $\lambda'$ , and with $\lambda' = \lambda$ it matches the rate of value iteration, which Theorem 6.3 of the same paper shows cannot be beaten by any first-order method uniformly over MDPs. At the same time it accepts accelerated steps whenever they reduce the residual fast enough, so it keeps the empirical speed-ups of A-VI. Remark 7.2 of the paper describes the role of $\lambda'$ : values closer to $1$ admit more accelerated steps. The guarantee also gives a computable stopping rule, since the residual bounds the distance to $v^*$ .

Formalizing it. The result is proved in the paper; to our knowledge it has not been machine-checked. This mission produces a Lean statement of the finite discounted MDP layer, the Bellman operator and Algorithm 1 itself (including its two-step recursion and its data-dependent branch), and a formal proof that the safeguarded iteration converges. The contraction property of $T$ and the residual-to-error bound are reusable for any later value-iteration development on the platform. Three sibling missions of this series pose the paper's other main results: the rate of Accelerated Value Computation on reversible chains (Theorem 5.1), the rate of Momentum Value Computation (Theorem 5.5), and the first-order lower bound (Theorem 6.3).

Difficulty

The accelerated candidate $v_{s+1/2}$ is built from two past iterates through a momentum step, and on a general MDP nothing controls it: A-VI is not a descent method, and its iterates may diverge. The natural first attempt, proving that A-VI steps contract the error, therefore fails. The difficulty in the formal setting lies elsewhere: the iterates are defined by a two-step recursion with a branch on a real inequality, so any argument must handle both branches at every period and keep the paper's indexing straight (the threshold at period $s$ is $\lambda'^{\,s+1}$ and it compares with the residual of $v_0$ , not of $v_s$ ). Existence and uniqueness of $v^*$ and the contraction property of a max of affine maps also need to be established for the specific operator, from the stochasticity of $P$ .

Formalization scope

States and actions are finite types, [Fintype S], [Fintype A], and [Nonempty A] so that the maximum in $T$ exists. Vectors are functions S → ℝ with Mathlib's sup norm, which is $\|\cdot\|_\infty$ . Rewards are arbitrary reals. The discount factor is M.lam with $0 < \lambda < 1$ inside MDP.Valid; the initial distribution $p_0$ of the paper's tuple is omitted because no statement uses it. The optimal value function enters each statement as a vector vstar with bellman M vstar = vstar; this is not vacuous, since a valid MDP has exactly one such vector. The scalar $\lambda'$ ranges over the closed interval $[\lambda, 1)$ , and $\alpha, \gamma > 0$ as in Algorithm 1, although the convergence argument does not need the step sizes to be positive. The sequence savi is indexed as the paper's $v_s$ : its recursive case s + 2 is the paper's period $s+1$ , with threshold lam' ^ (s + 2). " $v_s = v^* + O(\lambda'^s)$ for all $s \ge 0$ " is encoded as a single constant valid for every $s$ , which is stronger than an eventual big-O.

A formalization that replaced the test by the per-step condition (7.2) of Remark 7.3, used the residual of $v_s$ instead of $v_0$ , fell back to $T(v_{s+1/2})$ , or allowed $\lambda \ge 1$ would be a different theorem; none of these is posed. Remark 7.4's extension to arbitrary contractions is not posed either.

The development needs the contraction property of $T$ , the Banach fixed-point bound relating error and residual, and an induction over the iterates. Proofs of the milestones as separate lemmas are welcome, as are general statements about safeguarded fixed-point iterations for $\lambda$ -contractions that specialize to this one.

Selected references

V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, reprinted 2014 (Chapter 6.3, value iteration). https://doi.org/10.1002/9780470316887
Y. Nesterov, A method for solving the convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27, 1983.

8 thms2 active usersReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 3: The Midpoint Fixed-Fraction Rule Is the Shapley Value and the Nucleolus of the Liability GameResearch Paper

Motivation

When one breached contract forces the next party to breach its own contract, a single failure travels down a loss chain: agent 1 (the initiator) causes a loss $\ell_1$ to agent 2, which can then no longer honour its agreement with agent 3 and causes it a loss $\ell_2$ , and so on until agent $n$ causes a loss $\ell_n$ to a final victim. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss should be shared among the agents of the chain, with the aim of encoding the answer in a smart contract that settles such disputes automatically.

Their central rules are the fixed-fraction rules $\varphi^\lambda$ , under which every agent pays a fixed fraction $\lambda$ of the loss it caused and the initiator also pays the remaining fraction $1-\lambda$ of the total. An axiomatic characterization (their Theorem 1) singles out the whole family $\lambda\in[0,1]$ but not a particular member. This mission formalizes the paper's game-theoretic argument for the midpoint $\lambda=1/2$ : the cooperative game that records which coalitions are liable for which losses has the midpoint allocation as both its Shapley value and its nucleolus, the two best-known single-valued solutions of cooperative game theory.

Setting

Agents are $N=\{1,\dots,n\}$ with $n\ge1$ . A loss problem is a vector $\ell=(\ell_1,\dots,\ell_n)\in\mathcal L^n=\mathbb R^n_{\ge0}$ , where $\ell_i$ is the loss agent $i$ causes to agent $i+1$ ; the total loss is $L=\ell_1+\dots+\ell_n$ . The fixed-fraction rule with parameter $\lambda$ assigns

\varphi^\lambda_1(\ell)=\lambda\ell_1+(1-\lambda)L,\qquad \varphi^\lambda_i(\ell)=\lambda\ell_i\ (i\ge2).

A transferable-utility game on $N$ is a function $v$ assigning a real number to every coalition $S\subseteq N$ . The liability game of $\ell$ is

v_\ell(S)=\begin{cases}\sum_{i\in S}\ell_i&\text{if }1\in S,\\0&\text{otherwise:}\end{cases}

a coalition is liable for the losses its members caused only if it contains the initiator, without whom no loss would have occurred. The contribution of player $i$ to the grand coalition is $M_i(v)=v(N)-v(N\setminus\{i\})$ .

Two solution concepts are compared with $\varphi^{1/2}(\ell)$ .

The Shapley value gives player $i$

\mathrm{Sh}_i(v)=\sum_{S\subseteq N\setminus\{i\}}\frac{|S|!\,(n-|S|-1)!}{n!}\bigl(v(S\cup\{i\})-v(S)\bigr).

An imputation is a vector $x$ with $\sum_{i\in N}x_i=v(N)$ and $x_i\ge v(\{i\})$ for all $i$ . The excess of $S$ at $x$ is $e(S,x)=v(S)-\sum_{i\in S}x_i$ , and the excess vector $\theta(x)$ lists the $2^n$ excesses in non-increasing order. The nucleolus $\nu(v)$ (Schmeidler 1969) is the imputation whose excess vector is lexicographically smallest.

A game is convex if $v(\emptyset)=0$ and $v(S)+v(T)\le v(S\cup T)+v(S\cap T)$ for all $S,T$ .

Formalization targets

Goal: Theorem 3 (p. 15)

For every $\ell\in\mathcal L^n$ ,

\mathrm{Sh}(v_\ell)=\varphi^{1/2}(\ell)\qquad\text{and}\qquad \nu(v_\ell)=\varphi^{1/2}(\ell),

where the second identity is stated as: $\varphi^{1/2}(\ell)$ is an imputation of $v_\ell$ with lexicographically minimal sorted excess vector, and every imputation with this property equals $\varphi^{1/2}(\ell)$ .

Milestones (Appendix A, proof of Theorem 3, p. 24)

$v_\ell$ is convex.
(§4.2, p. 15; referenced, already on the platform) the core of a convex game is non-empty and contains its Shapley value, which applies to $v_\ell$ by milestone 1.
$M_1(v_\ell)=L$ and $M_i(v_\ell)=\ell_i$ for $i\ne1$ .
Every nucleolus $\nu$ of $v_\ell$ satisfies $\nu_i=M_i(v_\ell)/2=\ell_i/2=\varphi^{1/2}_i(\ell)$ for $i\ne1$ , and $\nu_1=\varphi^{1/2}_1(\ell)$ .
The Shapley value of $v_\ell$ is a nucleolus of $v_\ell$ .

Significance

The result. Theorem 1 of the paper leaves a one-parameter family of rules, and a designer who writes the rule into a contract must still choose $\lambda$ . Theorem 3 gives a reason for $\lambda=1/2$ that does not depend on the axioms: if losses are treated as the worth of coalitions, two solution concepts that are built on unrelated principles (average marginal contributions on one side, lexicographic minimization of complaints on the other) both return $\varphi^{1/2}(\ell)$ . Together with the paper's Theorem 2 (equidistance from ideal allocations, a separate mission of this series) it makes the midpoint the paper's recommended rule.

Formalizing it. The paper proves Theorem 3 by citing two results of Muto, Nakayama, Potters and Tijs (1988) on big boss games, the nucleolus formula (their Theorem 4.2) and the coincidence of Shapley value and nucleolus for convex big boss games (their Theorem 4.5); the paper itself proves only convexity and the marginal contributions. A formal proof must therefore establish the nucleolus of $v_\ell$ directly from Schmeidler's lexicographic definition. No nucleolus definition exists on the platform (searched 2026-10-14), and this mission introduces one. The Shapley value and convex games are reused from the platform's published definitions, and the core-contains-the-Shapley-value theorem for convex games is already proved there.

Difficulty

Convexity and the marginal contributions are finite case analyses. The Shapley identity is a weighted sum over all coalitions not containing a player and needs the combinatorial identities behind the weights; for $v_\ell$ only the position of the initiator relative to $S$ matters.

The substantive part is the nucleolus. Its definition compares sorted vectors of $2^n$ excesses, so an argument cannot treat one coalition at a time: showing that a candidate is lexicographically minimal requires controlling how a change of the payoff vector permutes the order of all excesses. The obvious first idea, minimizing only the largest excess (the least core), generally leaves a set of imputations rather than a point, so the comparison must go down the whole sorted list. Coalitions whose excesses tie, which happens for instance when some $\ell_i=0$ , are where informal arguments about sorted excess vectors are usually loose, and a formal proof has to handle them.

Formalization scope

Agents are Fin n with the initiator at index 0; [NeZero n] encodes $n\ge1$ , which the paper assumes because $1\in N$ . Loss vectors are Fin n → ℝ with the hypothesis IsLoss ℓ ( $\ell_i\ge0$ ).
A game is Finset (Fin n) → ℝ. The Shapley value is the published Supermodularity.Cooperative.ShapleyValue and convexity the published Supermodularity.Cooperative.IsConvexGame (the supermodular form, equivalent to the increasing-marginal-contribution form used on p. 24).
The nucleolus is defined in the mission's Nucleolus file: imputations with efficiency and individual rationality, excess $v(S)-\sum_{i\in S}x_i$ over all $2^n$ coalitions including $\emptyset$ and $N$ , sorted by ≥ into a list, and compared with List.Lex (· < ·). Including $\emptyset$ and $N$ does not change the order, since their excess is $0$ at every imputation.
The goal states both identities. The nucleolus half is not replaced by membership in the core or by minimality of the largest excess, the minimization runs over imputations and not over all of $\mathbb R^n$ , and uniqueness is stated explicitly rather than taken from Schmeidler's theorem.
The paper never defines the nucleolus or the Shapley value; the standard definitions (Schmeidler 1969; Shapley 1953) are used.

Contributions welcome: proofs of the milestones; general lemmas on sorted excess vectors (e.g. Kohlberg-type criteria for the nucleolus), which are reusable for every later nucleolus result; Schmeidler's existence and uniqueness theorem; and the general big boss game results of Muto et al. (1988).

Selected references

J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3):1773–1786, 2024 (accepted manuscript, 2023). https://doi.org/10.1287/mnsc.2023.4772
S. Muto, M. Nakayama, J. Potters, S. Tijs, On big boss games, The Economic Studies Quarterly 39(4):303–321, 1988. https://doi.org/10.11398/economics1986.39.303
D. Schmeidler, The nucleolus of a characteristic function game, SIAM Journal on Applied Mathematics 17(6):1163–1170, 1969. https://doi.org/10.1137/0117107
L. S. Shapley, A value for n-person games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
L. S. Shapley, Cores of convex games, International Journal of Game Theory 1:11–26, 1971. https://doi.org/10.1007/BF01753431

13 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Reinforcement Learning·Captain: mikedeng1

A First-Order Approach to Accelerated Value Iteration 3: On the n-State Chain MDP, Every First-Order Method Has ‖v_s − v*‖∞ ≥ λ^s/(1+λ) for s = 1, …, n − 1Research Paper

Motivation

Value iteration (VI) is the basic algorithm for computing the optimal value function of a discounted Markov decision process (MDP). Its error contracts by the discount factor $\lambda$ per step, so it needs on the order of $(1-\lambda)^{-1}\log(1/\epsilon)$ iterations, which is slow when $\lambda$ is close to $1$ , the regime of interest in long-horizon planning and reinforcement learning. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read VI as gradient descent on the residual map $v \mapsto v - T(v)$ and import Nesterov's acceleration and heavy-ball momentum from convex optimization. In convex optimization the corresponding lower bounds of Nesterov (2004/2013) show that acceleration is optimal among first-order methods. The question this mission formalizes is the MDP counterpart: can any method that only combines past iterates and their Bellman images beat the rate $\lambda$ of plain VI on every MDP? Theorem 6.3 of the paper answers no.

Setting

A finite MDP consists of a state set $S$ with $|S| = n$ , a finite nonempty action set $A$ , transition probabilities $P_{iaj} \ge 0$ with $\sum_j P_{iaj} = 1$ , rewards $r_{ia} \in \mathbb{R}$ , and a discount factor $\lambda \in (0,1)$ . Its Bellman operator $T : \mathbb{R}^n \to \mathbb{R}^n$ is

T(v)_i = \max_{a \in A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj} v_j \Big\}, \qquad i \in S,

a $\lambda$ -contraction for the sup norm $\|\cdot\|_\infty$ . Its unique fixed point $v^*$ is the optimal value function.

A sequence $(v_s)_{s \ge 0}$ in $\mathbb{R}^n$ is a first-order sequence for $T$ if

v_0 = 0, \qquad v_{s+1} \in \operatorname{span}\{v_0, \dots, v_s, T(v_0), \dots, T(v_s)\}, \quad s \ge 0 .

VI from $v_0 = 0$ ( $v_{s+1} = T(v_s)$ ) and relaxed VI ( $v_{s+1} = v_s - \alpha_s(v_s - T(v_s))$ ) from $0$ produce such sequences.

The chain MDP of Figure 1 has $n$ states and a single action. State $1$ is absorbing with reward $r_1 = 1$ ; every state $i \ge 2$ moves deterministically to $i - 1$ and earns nothing. In Lean (namespace AccelVI.LowerBound) the MDP is MDP, validity is MDP.Valid, $T$ is bellman, the chain is chainMDP n lam, and the first-order condition is IsFirstOrder T v.

Formalization targets

Goal: Theorem 6.3 (p. 12)

For every $n$ , every $\lambda \in (0,1)$ , the fixed point $v^*$ of the Bellman operator $T$ of the $n$ -state chain, every first-order sequence $(v_s)$ for $T$ , and every $s \in \{1, \dots, n-1\}$ ,

\|v_s - v^*\|_\infty \ge \frac{\lambda^s}{1+\lambda}.

Milestones

$T$ is a $\lambda$ -contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
(3.5): $(1-\lambda)\|v - w\|_\infty \le \|(I-T)(v) - (I-T)(w)\|_\infty$ (p. 6).
(3.6): $\|(I-T)(v) - (I-T)(w)\|_\infty \le (1+\lambda)\|v - w\|_\infty$ (p. 6).
On the chain, the value function is $v^*_i = \lambda^{i-1}/(1-\lambda)$ , and it is the only fixed point of $T$ (p. 12).
On the chain, every first-order sequence satisfies $v_{s,i} = 0$ for $i \ge s+1$ (p. 12).
(6.2)–(6.4): on the chain, $\|v_s - T(v_s)\|_\infty \ge \lambda^s$ for $1 \le s \le n-1$ (p. 12).

Significance

The result. Theorem 6.3 shows that, measured by the number of Bellman evaluations, no first-order method improves on the worst-case rate $\lambda$ of value iteration uniformly over MDPs, as long as the number of steps is below the number of states. In convex optimization the analogous class admits acceleration from $1 - \mu/L$ to $1 - \sqrt{\mu/L}$ ; with $\mu = 1-\lambda$ , $L = 1+\lambda$ , the analogue for MDPs would be a rate of about $1 - \sqrt{1-\lambda}$ , and this theorem rules it out. It is the reason the paper's accelerated schemes are analysed under extra structure, such as reversible policy-evaluation chains, or are safeguarded.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked lower bound for fixed-point iterations of Bellman operators, the contraction inequalities (3.5)–(3.6) for a general finite MDP, and an explicit value function for a hard instance. The paper's other main results, Theorems 5.1, 5.5 and 7.1, are posed as the sibling missions 1, 2 and 4.

Difficulty

The obvious argument that the error is at least the contribution of states never reached fails without control of the span: the first-order class allows arbitrary real coefficients, including ones that change with $s$ and depend on all past iterates, so one has to show that no such combination puts mass on states beyond index $s$ . The support claim has to be carried through the nonlinear max in $T$ , which is benign here only because the chain has a single action. The second ingredient converts a bound on a few coordinates of $v_s - v^*$ into a bound in sup norm with the exact constant $1/(1+\lambda)$ , which requires the two-sided inequalities (3.5)–(3.6) for $I - T$ and the explicit value $v^*_{s+1} = \lambda^s/(1-\lambda)$ .

Formalization scope

States are Fin n and are 0-based: the paper's state $i$ is index $i - 1$ , so $v^*_i = \lambda^{i-1}/(1-\lambda)$ is lam ^ k / (1 - lam) at index $k$ and " $i \ge s+1$ " is $s \le k$ . The action set of the chain is Unit.
$\|\cdot\|_\infty$ is Mathlib's sup norm on Fin n → ℝ. "span" is the real linear span Submodule.span ℝ, with both lists running to index $s$ inclusive.
$v^*$ enters the goal through its defining equation $T(v^*) = v^*$ ; it is not replaced by the explicit vector. The initial distribution $p_0$ of the paper's MDP tuple is omitted, since no result here uses it.
Pinned quantifiers. As printed, Theorem 6.3 asserts that there exists an MDP instance, with $n$ its own number of states; read literally, an instance with $n = 1$ has no admissible $s$ . The proof fixes an arbitrary $n$ and $\lambda \in (0,1)$ and uses the chain. The goal states that claim for every $n$ and $\lambda$ on the explicit chain, which implies the printed form.
$n - 1$ is natural-number subtraction, so the goal has content exactly when $n \ge 2$ .
The goal's constant is $\lambda^s/(1+\lambda)$ as printed; the sharper bound $\lambda^s/(1-\lambda)$ , which the proof's chain also gives, is not the target.
The Bellman operator and the kernel condition are the published platform definitions FoundationsML_ReinforcementLearning_BellmanOperator and FoundationsML_ReinforcementLearning_IsTransitionKernel.
A trivializing formalization would take an unsatisfiable fixed-point hypothesis or an empty first-order class. Both are satisfiable: the explicit vector is a fixed point (milestone 4), and VI from $0$ is first-order.

Contributions welcome: proofs of the contraction inequalities for general finite MDPs (reusable by every Bellman-operator mission), of the support recursion, and of the final chain of inequalities.

Selected references

V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994/2014. https://doi.org/10.1002/9780470316887

10 thms2 active usersReviewed

Combinatorics Probability·Captain: mikedeng1

Secretary Problems with Biased Evaluations Using Partial Ordinal Information I: ProxyLabel with a Width Estimate ω′ ≥ ω/c Is e^c(ω′+1)/(1−1/k)^{k−1}-CompetitiveResearch Paper

Motivation

In the classical secretary problem, candidates arrive one at a time in uniformly random order, and a decision maker must accept or reject each one irrevocably. The decision maker sees exact scores, or at least a total ranking of the candidates seen so far. In hiring, admissions and procurement the observed scores are often biased: evaluations of candidates from different groups, or produced by different evaluators, cannot be compared reliably, even when comparisons inside a group can. Salem and Gupta (SSRN 3444283; Management Science, 2023, doi:10.1287/mnsc.2023.4926) model this by giving the algorithm only the comparisons it can trust. These form a partial order on the candidates, and the true scores remain hidden.

The question is how much is lost when only partial ordinal information is available. The paper's answer is governed by the width of the partial order, the largest number of mutually incomparable candidates. Width 1 is the classical totally ordered problem. Width $N$ means that no comparison is available at all. This mission formalizes the paper's first positive result with explicit constants: an algorithm, ProxyLabel, whose competitive ratio grows linearly in a known estimate of the width.

Setting

A finite set $C$ of $N$ elements carries a partial order $\preceq$ . Each element $a$ has a hidden true score $w(a) \ge 0$ . The scores are pairwise distinct and consistent with the order: $a \prec b$ implies $w(a) < w(b)$ . The width $\omega$ of $(C, \preceq)$ is the largest size of an antichain, a set of pairwise incomparable elements.

The elements arrive in a uniformly random order. The algorithm knows $N$ and a selection capacity $k \ge 1$ . At each time it sees the comparisons of $\preceq$ among the elements that have arrived. It may select at most $k$ elements, and every decision is irrevocable. The offline optimum $\mathrm{OPT}$ is the largest total score of at most $k$ elements. An algorithm is $\rho$ -competitive if, on every instance,

\mathbb E\Big[\frac{w(\mathrm{Alg})}{\mathrm{OPT}}\Big] \ge \frac1\rho,

where $w(\mathrm{Alg})$ is the total score of the selected elements and the expectation is over the arrival order and the algorithm's randomness.

ProxyLabel (Algorithm 1 of the paper) takes a width estimate $\omega' \in \mathbb N$ . It works as follows.

Each element receives a label $\ell(a) \in \{1, \dots, k\}$ , uniformly and independently.
It draws $m \sim \mathrm{Bin}(N, \omega'/(\omega'+1))$ and lets the sample $S$ be the first $m$ arrivals. Sampled elements are never selected.
A later element $a$ is selected if it is maximal among all previously seen elements with its label, sampled or not, and no element with its label has been selected yet.

Each label class therefore contributes at most one element: the first non-sampled one that beats everything of its label seen before.

Formalization targets

Goal: Proposition 5.2

If $\omega' \ge \omega / c$ for some $c \ge 1$ , then ProxyLabel has competitive ratio at most

\rho = \frac{e^{c}(\omega'+1)}{\big(1 - \frac1k\big)^{k-1}} \ \le\ e^{c+1}(\omega'+1),

with the convention $0^0 = 1$ . That is, $\mathbb E[w(\mathrm{Alg})] \ge \mathrm{OPT}/\rho$ .

Milestones, from the proof (pp. 16–17)

Under uniform labels, the $j$ -th best element is the maximum of its label class with probability $(1 - 1/k)^{j-1} \ge (1 - 1/k)^{k-1} \ge 1/e$ .
Display (3): conditional on that event, it is selected with probability at least $\frac{1}{\omega'+1}\big(1 - \frac{1}{\omega'+1}\big)^{\omega}$ .
If $\omega/c \le \omega'$ with $c \ge 1$ , this quantity is at least $1/(e^{c}(\omega'+1))$ .
Hence each of the top $k$ elements is selected with probability at least $(1 - 1/k)^{k-1}/(e^{c}(\omega'+1))$ .
$\mathbb E[w(\mathrm{Alg})] \ge \sum_{i=1}^k \mathbb P(a_i \in \mathrm{Alg})\, w(a_i)$ over the top $k$ elements $a_1, \dots, a_k$ .

Companion: Corollary 5.1

With the exact width $\omega' = \omega$ , the ratio is at most $e(\omega+1)/(1 - 1/k)^{k-1} \le e^2(\omega+1)$ , and it is $e(\omega+1)$ for $k = 1$ .

Significance

Proposition 5.2 shows that partial ordinal information costs at most a factor linear in the width, provided a width estimate within a constant factor is available. Proposition 5.1 of the same paper shows that no algorithm beats ratio $\omega$ , so the bound is order-optimal. ProxyLabel is also the building block of the paper's width-free algorithm PosetLabel (§5.4), which estimates the width from a first sample and then runs ProxyLabel's selection phase.

The result is proved in the paper and has not been machine-checked. A complete development would give a formal model of online selection on a poset under random arrival, with an explicit selection rule and exact finite averages for probabilities. It would also contain a formal use of Dilworth's theorem inside a probabilistic argument, and the elementary inequalities $(1 - 1/k)^{k-1} \ge 1/e$ and $(1 - 1/(\omega'+1))^{\omega} \ge e^{-c}$ in the form the proof needs.

Difficulty

The events of the algorithm are tangled. The sample is a prefix of a random order with a random length. Whether an element is selected depends on everything that arrived before it, on the labels, and on whether an earlier element of the same label was already selected. The bound must be proved for every finite poset and every consistent scoring, with exact constants, on the finite probability space of arrival orders, labellings and sample sizes. The width enters only through the structure of a single label class, a subposet whose width is at most $\omega$ , so the argument has to pass from the global width to an arbitrary random subposet.

A tempting simplification lets every passing unsampled element be selected. That algorithm can select several elements of one label, so its expected score is larger and the bound becomes easier. It is not ProxyLabel.

Formalization scope

Elements are a finite type α with a PartialOrder, so $N$ is Fintype.card α. The width $\omega$ is the published definition AppliedComb.Posets.width α, the maximum size of an antichain. Dilworth's theorem is the published, proved theorem AppliedComb.Posets.dilworth.
A consistent scoring is $w : \alpha \to \mathbb R$ with $w \ge 0$ , $w$ injective, and $a < b \Rightarrow w(a) < w(b)$ . These three conditions are the paper's standing assumptions (§3.1, §3.3), not additions.
Arrival orders are bijections α ≃ Fin N, and labellings are functions α → Fin k. Labels are independent of the order, which is the same distribution as assigning labels on arrival.
Probabilities and expectations are explicit finite averages with weights $1/N!$ , $1/k^N$ and the binomial weights $\binom{N}{m}p^m(1-p)^{N-m}$ with $p = \omega'/(\omega'+1)$ .
The selection rule is encoded exactly. An element is selected iff it is unsampled, no earlier element of its label (sampled or not) is above it, and no earlier unsampled element of its label passed the same test.
OPT is the maximum of $\sum_{a \in s} w(a)$ over sets with $|s| \le k$ , so it is the total score when $k \ge N$ .
The competitive ratio is stated as $\mathrm{OPT}/\rho \le \mathbb E[w(\mathrm{Alg})]$ . This agrees with Definition 3.4 when $\mathrm{OPT} > 0$ ; the page's ratio is undefined when $\mathrm{OPT} = 0$ .
$(1 - 1/k)^{k-1}$ has a natural exponent, so $k = 1$ gives $0^0 = 1$ . The width estimate $\omega'$ is a natural number.
The proposition's "interval order" is a slip of the page: the algorithm and the proof concern arbitrary posets, and the goal is stated for every finite poset.
The order-optimality clause of Corollary 5.1 refers to Proposition 5.1, the subject of mission II of this series, and is not stated here.
The goal is a statement about the full expectation of the selected score over arrival order, labels and sample size. It is not the conditional bound (3). A formalization in which several elements per label can be selected, or in which "previously seen" excludes the sample, proves a statement about a different algorithm.

Contributions are welcome on every milestone. The prefix-of-a-random-order lemma (a binomially sized prefix is an i.i.d. Bernoulli sample) is reusable well beyond this mission.

Selected references

J. Salem and S. Gupta, Secretary Problems with Biased Evaluations Using Partial Ordinal Information, SSRN 3444283 (version of 2022-04-17); Management Science, 2023. https://ssrn.com/abstract=3444283, https://doi.org/10.1287/mnsc.2023.4926
R. P. Dilworth, A Decomposition Theorem for Partially Ordered Sets, Annals of Mathematics 51(1), 1950, 161–166. https://doi.org/10.2307/1969503
R. Kleinberg, A Multiple-Choice Secretary Algorithm with Applications to Online Auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519

9 thms2 active usersReviewed

Number Theory Optimization·Captain: mikedeng1

Integer Factorization: Why Two-Item Joint Replenishment Is Hard 1: For Odd Composite M, Every Optimal Plan of an Explicit Two-Item Aperiodic JRP Instance Has q₂ = M and 1 < gcd(q₁, M) < MResearch Paper

Motivation

The joint replenishment problem (JRP) is one of the basic models of multi-item inventory control. Each item follows the economic order quantity (EOQ) model of Harris (1913): ordering costs a fixed amount, holding stock costs a rate proportional to the stock, and the classical trade-off between the two determines how often to reorder. In a JRP, items replenished together share part of the fixed cost, so the reorder cycles of the items should be coordinated. The problem has been studied for decades, with a large literature of heuristics and approximation algorithms (see the survey of Khouja and Goyal 2008; Porras and Dekker 2008 compare the two ways of charging joint costs), yet its exact complexity remained unclear even for very few items.

Schulz and Telha (arXiv:2007.09045, 2020; Operations Research, 2024) give a striking answer for the smallest non-trivial case, two items. They show that solving the two-item problem exactly is at least as hard as integer factorization (their Theorem 1), and, assuming the Riemann hypothesis, that the two-item periodic JRP is NP-hard under randomized reductions (Theorem 2). This mission formalizes the mathematical core of Theorem 1(a), for the aperiodic JRP: the paper's Lemma 1.

Timeline. The complexity of both JRP variants was open for a long time. Schulz and Telha announced the reduction from integer factorization to the two-item aperiodic JRP (Theorem 1(a)) in 2011. Cohen-Hillel and Yedidsion (2018) then proved that the aperiodic JRP with an arbitrary number of items is strongly NP-hard (they call it the periodic JRP). The 2020 preprint adds the reduction for the two-item periodic JRP (Theorem 1(b)) and, under the Riemann hypothesis, a randomized reduction from Partition to it (Theorem 2).

Setting

For an item with fixed ordering cost $K$ and holding cost rate $H$ , replenished every $q$ time units, the long-run cost per unit time is

\mathrm{EOQ}_{K,H}(q) = \frac{K}{q} + Hq .

Reorder cycles are positive integers $q \in \mathbb Z^+$ . In the aperiodic two-item JRP (objective (1) of the paper) items 1 and 2 have data $(K_1,H_1)$ and $(K_2,H_2)$ , and every joint replenishment earns a discount $K_0 \le K_1, K_2$ . With cycles $q_1, q_2$ , joint replenishments happen every $\mathrm{lcm}(q_1,q_2)$ time units, so the discount per unit time is $\mathrm{DC}(q_1,q_2;K_0) = K_0/\mathrm{lcm}(q_1,q_2)$ and the problem is

\min\left\{\mathrm{JRP}(q_1,q_2) = \mathrm{EOQ}_{K_1,H_1}(q_1) + \mathrm{EOQ}_{K_2,H_2}(q_2) - \frac{K_0}{\mathrm{lcm}(q_1,q_2)} \ :\ q_1,q_2 \in \mathbb Z^+\right\}.

For an integer $M$ , the instance of Lemma 1 has

K_1 = K_0 = M(M-1),\qquad H_1 = 4,\qquad K_2 = M^3(M^2-1),\qquad H_2 = M(M^2-1).

Item 2's own EOQ optimum is $q_2 = M$ . Fixing $q_2 = M$ leaves the one-variable problem (2) with objective

\mathrm{JRP}^{\mathrm{red}}(q_1) = M(M-1)\left(\frac{1}{q_1} - \frac{1}{\mathrm{lcm}(q_1,M)}\right) + 4q_1 .

In Lean these are eoq, aperiodicCost, lemma1Cost, eoq2 (item 2's cost) and jrpRed, and an optimal solution (IsOptimal) is a pair of positive integers whose value is no larger than that of any other pair of positive integers.

Formalization targets

Goal: Lemma 1

For every odd composite number $M$ , the instance above satisfies $K_0 \le K_1$ , $K_0 \le K_2$ , has all coefficients at most $M^5$ , has an optimal solution, and

\text{every optimal } (q_1,q_2) \text{ satisfies } \quad q_2 = M \quad\text{and}\quad 1 < \gcd(q_1,M) < M .

So $\gcd(q_1, M)$ is a non-trivial divisor of $M$ .

Milestones (the steps of the paper's proof, pp. 9–10)

$\mathrm{EOQ}_{K_2,H_2}(M\pm1) = \mathrm{EOQ}_{K_2,H_2}(M) + H_2/(M\pm1) \ge \mathrm{EOQ}_{K_2,H_2}(M) + K_0$ .
For $q_2 \ne M$ : $\mathrm{JRP}(q_1,q_2) \ge \mathrm{EOQ}_{K_2,H_2}(M) + K_0 + 4 > \mathrm{JRP}(1,M)$ .
$\mathrm{JRP}(q_1, M) = \mathrm{EOQ}_{K_2,H_2}(M) + \mathrm{JRP}^{\mathrm{red}}(q_1)$ .
For $q_1$ coprime with $M$ : $\mathrm{JRP}^{\mathrm{red}}(q_1) \ge 4(M-1)$ .
For a divisor $p$ of $M$ with $3 \le p < M$ and a multiple $q$ of $p$ : $\mathrm{JRP}^{\mathrm{red}}(q) \le (M-1)(M-p)/q + 4q$ .
Some multiple $q$ of $p$ in $\left[\frac{M-1}{2} - \frac{p-1}{2}, \frac{M-1}{2} + \frac{p-1}{2}\right]$ has $\mathrm{JRP}^{\mathrm{red}}(q) < 4(M-1)$ .
Multiples $q_1$ of $M$ have $\mathrm{JRP}^{\mathrm{red}}(q_1) = 4q_1 \ge 4M$ , while $\mathrm{JRP}^{\mathrm{red}}((M-1)/2) \le 4(M-1)$ .

Significance

The result. Lemma 1 turns any exact algorithm for the two-item aperiodic JRP into a factoring algorithm: solve the instance, read off $\gcd(q_1, M)$ , and recurse on the two factors. Since the instance's coefficients have size $O(\log M)$ , a polynomial-time JRP algorithm would factor integers in polynomial time (Theorem 1(a)). This explains, in a precise sense, why the many exact and approximation methods for the JRP never produced a provably polynomial exact algorithm even for two items, and why the problem's difficulty is number-theoretic rather than combinatorial.

Formalizing it. The lemma has a complete, elementary proof in the paper; it has not been machine-checked. The formalization pins down every quantifier the prose leaves loose: that optimal solutions exist, that the claim is about every optimum, which coefficients are used, and that periods range over positive integers only. The proof steps (the item-2 pin, the coprime bound, the interval argument) are stated as separate milestones so they can be checked individually.

Difficulty

Each step is elementary, but the argument mixes discrete and continuous reasoning. The objective is not convex in $q_1$ : the term $-K_0/\mathrm{lcm}(q_1,M)$ jumps down at every period sharing a factor with $M$ . The obvious approach, comparing against the continuous EOQ minimizer, gives the right threshold $4(M-1)$ for coprime periods but says nothing about where a cheaper non-coprime period sits. The interval step needs the exact size of a window of integers around $(M-1)/2$ , that $p$ consecutive integers contain a multiple of $p$ , and a strict inequality between a quadratic's roots and that window. The existence of an optimum is not stated in the paper and needs a coercivity argument over $\mathbb Z^+ \times \mathbb Z^+$ .

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 1(a); polynomial running time is not formalized, and neither are Theorem 1 as a statement about algorithms, the recursion to a full factorization, nor primality testing.

Conventions: periods are natural numbers, and every quantification over a period requires it to be positive, because Lean evaluates $K/0 = 0$ , $\mathrm{lcm}(0,M) = 0$ and $\gcd(0,M) = M$ . Costs are real numbers. Coefficients are natural numbers cast to $\mathbb R$ . "Odd composite" is Odd M ∧ 1 < M ∧ ¬ M.Prime. "Size at most $5\log M$ " is stated as "every coefficient is at most $M^5$ ", equivalent in any logarithm base.

Two additions relative to the printed statement are disclosed in the goal's Formalization Note. The goal states the explicit instance of the proof (p. 9) rather than "there is an instance", since an existential instance could be chosen to make the claim easy and loses the polynomial-size construction the reduction needs. The goal also asserts that an optimal solution exists, so that "every optimal solution satisfies …" is not vacuously true. Neither periods equal to zero nor junk values of division can satisfy the optimality predicate.

All objects are defined in one file, JRPHard.Aperiodic.Setting; nothing beyond Mathlib's Nat.gcd, Nat.lcm, Nat.Prime and real arithmetic is needed. Proofs of any milestone, or alternative proofs of the goal, are welcome.

Selected references

A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, 2020; published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024. https://arxiv.org/abs/2007.09045
F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2), 1913; reprinted in Operations Research 38(6), 1990. https://doi.org/10.1287/opre.38.6.947
E. Porras and R. Dekker, A solution method for the joint replenishment problem with correction factor, International Journal of Production Economics 113(2), 834–851, 2008. https://doi.org/10.1016/j.ijpe.2007.11.008
M. Khouja and S. Goyal, A review of the joint replenishment problem literature: 1989–2005, European Journal of Operational Research 186(1), 2008. https://doi.org/10.1016/j.ejor.2007.03.007
M. Cohen-Hillel and L. Yedidsion, The periodic joint replenishment problem is strongly NP-hard, Mathematics of Operations Research 43(4), 2018. https://doi.org/10.1287/moor.2017.0904

9 thms2 active usersReviewed

Algorithmic Game Theory Economics Optimization·Captain: mikedeng1

Marketplace Leakage 3: The Marketplace Bans Buyer–Seller Communication Above Π/(v − c), Below η_L When q > c/(v − Π), and Always When q Is Close to OneResearch Paper

Motivation

Online marketplaces match buyers with sellers and charge a fee per transaction. Once a buyer has found a seller on the platform, both have an incentive to complete the sale off the platform and split the fee they save. This leakage (also called disintermediation) is a central concern for service marketplaces such as Upwork, Thumbtack or AngelList, and several of them respond by hiding the identity of the parties and blocking direct messages until a transaction is committed.

A. Hagiu and J. Wright, Marketplace Leakage (Management Science, 2023; doi:10.1287/mnsc.2023.4757), build a model of a marketplace that cannot prevent leakage by contract and study six strategies against it. Section 5.2 studies the bluntest of them: banning buyer–seller communication. A ban stops leakage, but it also prevents buyers from learning whether the product suits them. Proposition 3 says exactly when the marketplace gains from the ban. This mission formalizes that proposition and the lemmas of its proof (Appendix §8.4).

Setting

There is one marketplace $M$ , one seller $S$ and a unit mass of buyers with unit demand. The product has value $v$ for buyers who want it and marginal cost $c<v$ ; the outside option is worth $0$ .

Allowing communication (the baseline). $M$ sets a fee $f$ per transaction. $S$ sets the on-platform price $p_m=v$ and a direct price $p_d\le v$ . A buyer who buys directly bears a switching cost $s$ with distribution $G$ ; with the uniform distribution of the paper,

G(s)=\min\{\max\{s/\mu,0\},1\},\qquad \mu>0 .

The seller maximizes its profit (1),

\pi(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),

and $M$ earns $f\,(1-G(v-p_d))$ , choosing $f\le v-c$ . The equilibrium profit of $M$ is $\Pi^*$ . With communication allowed, a buyer values the product at $v$ only with probability $q\in(0,1)$ , but learns their valuation; every payoff is multiplied by $q$ , so $M$ earns $q\Pi^*$ .

Banning communication. Under a ban there is no leakage, but a buyer learns their valuation only with probability $\eta\in[0,1]$ . Facing the fee $f$ , the seller has two options: the high price $p_m=v$ , selling to the fraction $\eta q$ of informed high-value buyers and earning $\eta q\,(v-c-f)$ ; and the low price $p_m=qv$ , selling also to the $1-\eta$ uninformed buyers and earning $(1-\eta+\eta q)(qv-c-f)$ . It takes the better option (ties to the low price) and lists if that option pays at least $0$ . $M$ earns $f$ per transaction and chooses $f\in\mathbb R$ . Its maximal revenue is the ban value $V(\eta)$ . Two closed forms appear:

\Pi_H(\eta)=\eta q(v-c),\qquad \Pi_L(\eta)=(1-\eta+\eta q)\Bigl(\frac{(1-(2-q)\eta)qv}{1-\eta}-c\Bigr).

$M$ prefers to ban if $V(\eta)>q\Pi^*$ and prefers to allow if $V(\eta)<q\Pi^*$ .

Formalization targets

Goal: Proposition 3 (pp. 15–16)

For $0<\Pi^*<v-c$ :

$M$ prefers to ban for every $\eta$ with $\Pi^*/(v-c)<\eta\le 1$ ;
if $q>c/(v-\Pi^*)$ , there is a unique $\eta_L\in[0,1)$ with $\Pi_L(\eta_L)=q\Pi^*$ , it is positive, and $M$ prefers to ban for every $\eta\in[0,\eta_L)$ ;
there is $q_0<1$ such that for $q\in(q_0,1)$ , $M$ prefers to ban for every $\eta\in[0,1]$ ;
with uniform switching costs, $c\ge 0$ , and $\Pi^*=\Pi^*(\mu)$ the baseline equilibrium profit: for each $\eta\in(0,1)$ , $M$ prefers to ban for all sufficiently small $\mu>0$ and prefers to allow for all sufficiently large $\mu$ .

Milestones

f>\frac{(1-(2-q)\eta)qv}{1-\eta}-c\iff \text{the seller prefers the high price}\qquad(\text{p. 15})

V(\eta)=\max\{\Pi_H(\eta),\Pi_L(\eta)\}\qquad(\text{p. 15})

\frac{d\Pi_L}{d\eta}=-\frac{(1-q)qv}{(1-\eta)^2}\bigl((2-\eta)q\eta+2(1-\eta)^2\bigr)+c(1-q)<0\ \text{ when } qv>c\qquad(\text{p. 38})

\Pi_L(\eta)\le\Pi_H(\eta)\iff\eta\ge\eta^*,\quad \eta^*=\frac{qv(2-q)-c-q\sqrt{(1-q)v(v-c)}}{qv(3(1-q)+q^2)-c}\in(0,1)\qquad(\text{p. 38})

\lim_{q\to1^-}\eta^*=1\qquad(\text{p. 38})

Significance

The proposition separates three regimes. When information loss is small ( $\eta$ near $1$ ) a ban costs almost nothing and removes leakage, so the marketplace bans. When information loss is large and buyers are a priori likely to value the product, the marketplace can induce the low price $qv$ and sell to everyone, so a ban pays again. In between, allowing communication can win. With uniform switching costs, the comparison turns on how much leakage costs: when switching is cheap (small $\mu$ ) the baseline profit $\mu/2$ is small and the ban wins; when it is expensive, leakage is rare and allowing communication wins. The result is proved in the paper by an informal appendix argument. No part of it has been machine-checked. A formal version pins down what the paper leaves implicit: the seller's tie-breaking, the domain of $\eta$ on which $\Pi_L$ is defined, which endpoints the strict preferences hold at, and the order of the quantifiers in "sufficiently close to zero (sufficiently large)".

Difficulty

The obvious argument compares two closed forms, but the ban value is not a closed form: it is a maximum over a fee that switches the seller's option and its listing decision. Showing that the maximum is $\max\{\Pi_H,\Pi_L\}$ requires checking that the threshold fee keeps the seller listing, and that fees above the threshold earn at most $\Pi_H$ . The second obstacle is the shape of $\Pi_L$ : it is a rational function with a pole at $\eta=1$ , and its monotonicity rests on the sign of the printed derivative. The comparison point $\eta^*$ involves a square root, so the equivalence $\Pi_L\le\Pi_H\iff\eta\ge\eta^*$ is a quadratic-root argument rather than a one-line inequality. Finally, part 4 needs the baseline equilibrium profit $\Pi^*(\mu)$ from the full baseline game, i.e. a solution of the seller's problem (1) and the marketplace's problem (3) under uniform $G$ .

Formalization scope

All objects are real-valued, with the paper's letters: v c μ q η f; PiStar stands for $\Pi^*$ . The standing assumptions $c<v$ , $0<q<1$ and $0\le\eta\le 1$ are explicit hypotheses. The statements use the reduced seller problem (1) with $p_m=v$ , as the paper does after its Lemma 1; Lemma 1 itself is not posed. The uniform $G$ is the clamped CDF. Seller optimality, the baseline equilibrium and the ban value are optimality predicates (IsGreatest over the fees), never sSup or a chosen maximizer.

Conventions and disclosed additions:

In parts 1–3, $\Pi^*$ is any real in $(0,v-c)$ , a generalization of the paper's $\Pi^*$ for a general "well behaved" $G$ ; the proof uses nothing else.
Part 4 is posed for each fixed $\eta\in(0,1)$ : it fails at $\eta=0$ (ban) when $qv\le c$ and at $\eta=1$ (allow). It adds $c\ge 0$ , without which the marketplace bans for every $\mu$ at small $\eta$ .
The milestones on the ban value, the derivative's sign and $\eta^*$ add $v>0$ , which the proof uses without stating; each is false for some $v\le 0$ .
$\Pi_L$ and the threshold divide by $1-\eta$ and are stated only for $\eta<1$ ; the game itself has no division.
"Prefers" is strict in both directions.

Trivializing formalizations are ruled out: the ban value is not defined as $\max\{\Pi_H,\Pi_L\}$ , the thresholds in $\mu$ are quantified after $\eta$ and not before, $\Pi^*$ is constrained to $(0,v-c)$ , and preferences are strict.

A complete development needs elementary real analysis only: derivatives of rational functions, the intermediate value theorem on $[0,1)$ , limits at $1$ , and the baseline solution of (1) and (3) under uniform switching costs. That baseline solution is reusable for the other missions of this series. Proofs of individual milestones are welcome independently.

Selected references

A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023. Authors' manuscript dated March 2023. doi:10.1287/mnsc.2023.4757
A. Piolatto, F. Schuett, Information vs Competition: How Platform Design Affects Profits and Surplus, TILEC Discussion Paper DP2022-002, 2022 (cited in footnote 8 of the paper for the idea that limiting information exchange reduces transaction value on a platform).

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Optimization·Captain: mikedeng1

Marketplace Leakage 4: The Marketplace Prefers Not to Impose a Price-Parity Clause If and Only If q < 1/2 and μ > (v − c)/2Research Paper

Motivation

Online marketplaces (Amazon, Booking.com, Airbnb, Upwork) charge sellers a fee on every transaction they intermediate. Once a buyer has found a seller on the marketplace, both have an incentive to complete the sale off the platform and split the fee they save. This is leakage (also called disintermediation or showrooming), and it limits the fees a marketplace can sustain. Hagiu and Wright, Marketplace Leakage (Management Science, 2023, doi:10.1287/mnsc.2023.4757), build a minimal model of leakage and compare the strategies a marketplace can use against it.

One of these strategies is contractual: a price-parity clause (PPC), under which the seller must not charge less in its direct channel than on the marketplace, on pain of being delisted. The paper notes that such clauses have been used by hotel-booking platforms, price-comparison platforms and Amazon (p. 22). The paper's Proposition 4 asks when a marketplace that cannot observe how easily buyers switch actually wants such a clause. This mission formalizes that proposition and the profit formulas behind it.

Setting

A marketplace $M$ , a seller $S$ and a unit mass of buyers with unit demand. Every buyer values $S$ 's product at $v$ ; $S$ 's marginal cost is $c<v$ ; the outside option is worth $0$ . $S$ sells on $M$ at price $p_m$ , paying $M$ a fee $f$ per transaction, or directly at price $p_d$ with no fee. A buyer who buys directly bears a switching cost $s$ . In the baseline state switching costs are uniform on $[0,\mu]$ , $\mu>0$ , with clamped distribution function $G(s)=\min\{\max\{s/\mu,0\},1\}$ . In the no-switching state switching costs are infinite and nobody buys directly. The baseline state occurs with probability $q$ . $S$ knows the state when it decides; $M$ does not when it sets $f$ .

Without a PPC, $S$ always lists, sets $p_m=v$ , and in the baseline state picks $p_d\le v$ to maximize

\pi(f,p_d)=(p_d-c)G(v-p_d)+(v-c-f)\big(1-G(v-p_d)\big).

A maximizer is a seller-optimal price $p_d^*(f)$ . $M$ 's value is

\Pi^*=\max_{f\le v-c} f\big(1-q\,G(v-p_d^*(f))\big).

With a PPC, a listed seller must set $p_d=p_m=v$ and earns $v-c-f$ . A seller that delists earns $\max_{c\le p_d\le v}(p_d-c)G(v-p_d)$ in the baseline state and $0$ in the no-switching state. It accepts $M$ 's offer when listing pays at least as much, so $M$ 's value $\Pi^*_{PPC}$ is the largest expected revenue $f\cdot\Pr[\text{accept}]$ over all fees $f$ .

Formalization targets

Goal: Proposition 4 (p. 23)

For $c<v$ , $\mu>0$ and $0<q\le 1$ , both values exist, and

\Pi^*>\Pi^*_{PPC}\iff q<\tfrac12\ \text{ and }\ \mu>\tfrac{v-c}{2},\qquad\text{otherwise}\quad \Pi^*_{PPC}\ge\Pi^* .

The goal states the comparison for any values satisfying the optimality predicates, so it is insensitive to how either value is later computed.

Milestones

$\Pi^*_{PPC}=\max\{v-c-D,\ (1-q)(v-c)\}$ , where $D=\max_{c\le p_d\le v}(p_d-c)G(v-p_d)$ (p. 23).
$D=\dfrac{(v-c)^2}{4\mu}$ if $\mu\ge\frac{v-c}{2}$ and $D=v-c-\mu$ otherwise, so $\Pi^*_{PPC}$ has a closed form (p. 39).
For $q<\tfrac12$ : $\displaystyle\Pi^*=(v-c)\Big(1-q\min\Big\{\frac{v-c}{2\mu},1\Big\}\Big)$ (p. 39).

Significance

Proposition 4 identifies a trade-off. A PPC removes leakage entirely, but it also takes away the seller's ability to divert some buyers when the fee turns out to be too high, so the seller may refuse to participate. When the baseline state is unlikely and switching costs in it are high, the marketplace earns more by tolerating leakage and charging the full surplus $v-c$ . In every other case the clause pays. This makes the welfare and competition-policy debate about parity clauses explicit in a two-parameter region. It also contrasts with the case without uncertainty, where a PPC is always better for the marketplace.

The paper's proof (§8.5, pp. 39–40) is a short case comparison between closed forms. It has not been machine-checked. The printed formula for $\Pi^*$ when $q\ge 1/2$ omits the corner fee $f=v-c$ and is wrong for small $\mu$ . The conclusion $\Pi^*_{PPC}\ge\Pi^*$ still holds there, but by a different comparison. A formal proof pins down which steps survive.

Difficulty

Two optimizations are nested. The seller's optimal direct price changes regime at $f=2\mu$ , where the uniform distribution's kink binds. The marketplace's revenue without a PPC is therefore piecewise in $f$ , with an interior candidate $\mu/q$ that is feasible only when $q\ge 1/2$ . Under a PPC, revenue is discontinuous in $f$ because acceptance switches on and off. Its maximum is attained only because acceptance is weak. Comparing the two values requires a case split over $q\gtrless\tfrac12$ and $\mu$ against $(v-c)/2$ and $q(v-c)$ , and the boundary cases include genuine ties ( $\Pi^*=\Pi^*_{PPC}$ for $q<\tfrac12$ , $\mu\le\frac{v-c}{2}$ ). Reading off a single printed closed form for $\Pi^*$ fails in part of the $q\ge 1/2$ region.

Formalization scope

All objects are in one definitions file in namespace MarketplaceLeakage.Parity. The parameters are real numbers v c μ q, with standing hypotheses c < v, 0 < μ, 0 < q, q ≤ 1 on every theorem. The paper states $v>c$ (p. 5) and $\mu>0$ (p. 9). $q\in(0,1]$ is added: $q$ is a probability, and at $q=0$ both values equal $v-c$ , so the "if" direction of the goal fails. $q=1$ is allowed. The statements use the reduced seller problem (1), as the paper does after its Lemma 1 (p. 7), with $p_m=v$ . Lemma 1 itself is not posed.

Committed conventions:

$G$ is the clamped uniform CDF.
Seller-optimality is a predicate (IsSOpt), not a formula.
$\Pi^*_{PPC}$ (IsPPCValue) is the attained maximum of $f\cdot(q\,\mathbf 1[\text{accept}_B]+(1-q)\,\mathbf 1[\text{accept}_N])$ over all $f\in\mathbb R$ . Acceptance is weak and is stated against every delisting price $c\le p_d\le v$ .
$\Pi^*$ (IsNoPPCValue) is the attained maximum of $f(1-qG(v-p_d))$ over $f\le v-c$ and seller-optimal $p_d$ .
"Prefers not to impose" is strict; "otherwise prefers to impose" is weak.

These choices rule out the trivializing formalizations. Neither value is defined by its printed max-expression, which would make the milestones definitional. Strict acceptance would leave the PPC optimum unattained. A value given by sSup would be meaningless off its domain. Reading "prefers to impose" strictly would make the statement false at the ties.

No published platform definitions are reused. A complete development needs only elementary real analysis: maximizing piecewise-quadratic functions, attainment on compact intervals, and case analysis over min/max. The lemmas on the seller's best response under the uniform $G$ are reusable in the companion missions on Propositions 1–3 of the same paper. Proofs of any milestone are welcome independently.

Selected references

A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023 (authors' manuscript dated March 2023). https://doi.org/10.1287/mnsc.2023.4757

6 thms2 active usersReviewed

Probability·Captain: mikedeng1

Lightning Network Economics: Channels I: The Expected Discounted Cost of a Bidirectional Payment Channel in Closed FormResearch Paper

Payment channels and the cost of locked capital

Blockchains such as Bitcoin settle every transaction on a public ledger. Each on-chain transaction pays a fee and waits for confirmation, so frequent small payments are expensive. The Lightning Network moves such payments off-chain: two parties lock funds in a shared payment channel and pay each other by updating the channel's balance, touching the blockchain only to open, close or re-fund it. A channel is not free either. The locked funds cannot be used elsewhere, and once one side's balance is exhausted the channel has to be reset on-chain.

Guasoni, Huberman and Shikhelman (Lightning Network Economics: Channels, Management Science, 2023) quantify this trade-off in a stochastic model and compare three ways of settling two opposite streams of payments: on-chain transactions, unidirectional channels, and one bidirectional channel. Their comparisons all rest on a single computation, the expected discounted cost of a channel in closed form (Theorem 1). This mission formalizes that computation.

The model

Two nodes exchange unit payments. Node 1 pays node 2 one unit at each jump of a Poisson process $N^{\lambda_1}_t$ with rate $\lambda_1$ ; node 2 pays node 1 one unit at each jump of an independent Poisson process $N^{\lambda_2}_t$ with rate $\lambda_2$ . The paper normalizes $\lambda_1\le\lambda_2$ . The net balance of node 1 is

X_t=N^{\lambda_2}_t-N^{\lambda_1}_t,\qquad X_0=0 .

In a bidirectional channel node 1 commits $l_1$ units and node 2 commits $l_2$ units. The money is the channel's capacity: the channel works as long as $-l_1<X_t<l_2$ . Locked capital has an opportunity cost of $r(l_1+l_2)$ per unit of time, where $r>0$ is the continuously compounded interest rate, and all costs are discounted at rate $r$ . When the balance reaches $-l_1$ (node 1 is exhausted) or $+l_2$ (node 2 is exhausted), the channel is reset at cost $B$ and the balance restarts at $0$ with the same commitments.

Let $J(n)$ be the expected total future cost when the balance equals $n$ . Conditioning on the first payment, which arrives after an exponential time with rate $\lambda_1+\lambda_2$ , gives the first-step equation (15)

J(n)=(l_1+l_2)\frac{r}{r+\lambda_2+\lambda_1}+J(n+1)\frac{\lambda_2}{r+\lambda_2+\lambda_1}+J(n-1)\frac{\lambda_1}{r+\lambda_2+\lambda_1},\qquad -l_1<n<l_2,

with the reset conditions $J(-l_1)=J(0)+B$ and $J(+l_2)=J(0)+B$ . The cost of the channel is $c^{l_1,l_2}(\lambda_1,\lambda_2)=J(0)$ .

In a unidirectional channel only node 2 pays (rate $\lambda_2$ ) and only node 2 commits capital ( $l_2$ units). The cost satisfies $J(n)=l_2\frac{r}{r+\lambda_2}+J(n+1)\frac{\lambda_2}{r+\lambda_2}$ for $0\le n<l_2$ with $J(l_2)=J(0)+B$ , and $c^{0,l_2}(0,\lambda_2)=J(0)$ .

The roots of the characteristic equation $\lambda_2\alpha^2-(\lambda_1+\lambda_2+r)\alpha+\lambda_1=0$ are

\alpha_\pm=\frac{\lambda_1+\lambda_2+r\pm\sqrt{(\lambda_2-\lambda_1)^2+r^2+2r(\lambda_2+\lambda_1)}}{2\lambda_2}. \tag{4}

Formalization targets

Goal: Theorem 1 (ii)

For $0<\lambda_1\le\lambda_2$ , $r>0$ , any $B$ and natural commitments $l_1,l_2\ge1$ , the bidirectional cost system has a solution, and every solution satisfies

c^{l_1,l_2}(\lambda_1,\lambda_2)=l_1+l_2-B\,\frac{\alpha_-^{l_1}(1-\alpha_+^{l_1+l_2})-\alpha_+^{l_1}(1-\alpha_-^{l_1+l_2})}{\alpha_-^{l_1}(1-\alpha_+^{l_1+l_2})-\alpha_+^{l_1}(1-\alpha_-^{l_1+l_2})+\alpha_+^{l_1+l_2}-\alpha_-^{l_1+l_2}}. \tag{3}

Milestones

Competing exponential clocks (proof of Theorem 1, p. 10): the minimum $\tau$ of independent exponential times with rates $\lambda_2,\lambda_1$ is exponential with rate $\lambda_2+\lambda_1$ , and $\tau^{\lambda_2}$ rings first with probability $\lambda_2/(\lambda_2+\lambda_1)$ . This is a published, proved platform theorem, reused as is.
The first term (p. 10): $E[e^{-r\tau}]=(\lambda_2+\lambda_1)/(\lambda_2+\lambda_1+r)$ and $E[\int_0^\tau e^{-rs}r(l_1+l_2)\,ds]=(l_1+l_2)\,r/(r+\lambda_2+\lambda_1)$ .
The last term (p. 10): $E[e^{-r\tau}J(X_{t+\tau})\mid X_t=n]=J(n+1)\frac{\lambda_2}{r+\lambda_2+\lambda_1}+J(n-1)\frac{\lambda_1}{r+\lambda_2+\lambda_1}$ .
General solution of (15) (§5.1): on the lattice $-l_1\le n\le l_2$ , (15) holds at the interior points if and only if $J(n)=l_1+l_2+k_1\alpha_-^n+k_2\alpha_+^n$ for constants $k_1,k_2$ .
The cost function (§5.1): the closed form of $J(n)$ at every balance $n$ , which gives (3) at $n=0$ .
Theorem 1 (i), (1): $c^{0,l_2}(0,\lambda_2)=l_2+B\big(((r+\lambda_2)/\lambda_2)^{l_2}-1\big)^{-1}$ .
Theorem 1 (i), (2): with $k=B\log(1+r/\lambda_2)$ and $B>0$ , the minimum of (1) over real sizes is $\frac{B}{2k}\big(-k+\sqrt{k(k+4)}+2\log(\tfrac12(k+\sqrt{k(k+4)}+2))\big)$ , attained at $l_2=\frac Bk\log(\tfrac12(k+\sqrt{k(k+4)}+2))$ .

What the closed form gives

Formula (3) is what the rest of the paper works with. Lemma 1 prices on-chain settlement of a stream of rate $\lambda$ at $C\lambda/r$ . Comparing that price with (1) and (3) yields the paper's thresholds on the on-chain fee below which no channel pays off (Theorem 2), the small-interest-rate asymptotics of the optimal symmetric channel, whose minimal cost scales like $3(2B\lambda/r)^{1/3}$ (Theorem 3), and the long-run number of channel payments per on-chain transaction (Proposition 2). Without an exact expression for the cost these comparisons would rest on simulation.

The paper proves Theorem 1 by a first-step argument and the solution of a linear difference equation. No part of it has been machine-checked. A formal proof would supply what the published argument passes over: that the first-step equation (15) and the reset conditions together have a unique solution on the lattice, that the denominator of (3) does not vanish, and the measure-theoretic computation of the coefficients of (15) from the exponential clocks. The later missions of this series (rate bounds, small-rate asymptotics, the balance walk) build on the same model.

Where the difficulty lies

The algebra of solving a second-order linear recurrence is routine. Two points are not. First, the solution has to be shown to exist and to be unique for every admissible set of parameters. This requires $\alpha_-\ne\alpha_+$ and a non-singular $2\times 2$ system for $k_1,k_2$ , whose determinant is the denominator of (3), and the paper does not discuss when that determinant vanishes. Second, the coefficients of (15) come from expectations over exponential times: the joint expectation of the discount factor $e^{-r\tau}$ and the indicator of which clock rang first. The paper factors it as $E[e^{-r\tau}]\,P(\tau=\tau^{\lambda_2})$ , which uses that the minimum is independent of the identity of the first clock, a fact it does not state.

Formalization scope

The rates are written lam₁, lam₂; the sizes $l_1,l_2$ are natural numbers with $l_1,l_2\ge1$ , because payments are of one unit and the balance lives on the lattice $\{-l_1,\dots,l_2\}$ . The cost function is a map $J:\mathbb Z\to\mathbb R$ whose values off the lattice are unconstrained.
The cost is defined by its equations, (15) with the reset conditions (IsBiCostFn) and the §5.2 system (IsUniCostFn), never by (3) or (1). Every statement about "the cost" asserts both that a solution exists and that every solution takes the stated value, so it is neither vacuous nor dependent on a choice of solution.
The unidirectional system is a separate definition: the bidirectional one at $l_1=0$ would force $B=0$ . For the same reason the Remark after Theorem 1 ("(1) follows from (3) by substituting $\lambda_1=l_1=0$ ") is not posed: with $\alpha_-=0$ and $l_1=0$ the denominator of (3) vanishes.
Powers are natural powers in (1) and (3), integer powers (zpow) in the general solution and in $J(n)$ , and real powers (Real.rpow) in the minimization (2), which is over real sizes $m>0$ as in the paper's proof.
The paper prints the exponent in the numerator of the $J(n)$ display as $l+n$ ; the statement uses $l_1+n$ , which is what the derivation gives and what reduces to (3) at $n=0$ .
The probabilistic milestones use Mathlib's expMeasure for the laws (through push-forward measures of measurable random variables) and IndepFun. Integrability is part of what is to be proved.
The hypothesis $\lambda_1\le\lambda_2$ is kept in the goal as printed. No sign of $B$ is assumed except $B>0$ in (2), without which the infimum is not attained.
Ruled out as trivializing: defining the cost as its closed form (which turns the goal into a definitional equality), fixing numerical parameters, restricting to $\lambda_1=\lambda_2$ , and treating the sizes as real numbers in the cost system.

Contributions welcome: proofs of the milestones in any order, and reusable lemmas on linear difference equations with constant coefficients and on Laplace transforms of exponential laws, neither of which Mathlib currently has in this form.

Selected references

P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2022.01664
J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, technical report, 2015 (as cited by Guasoni et al.). https://lightning.network/lightning-network-paper.pdf

13 thms2 active usersReviewed

Algorithmic Game Theory Economics Optimization·Captain: mikedeng1

Quality Strategies in Network Markets: Under Potential Maximization the Equilibrium Quality Equates Marginal Cost to n Times the Harmonic-Mean Valuation Times the Uniform Average of ∂f(i,q)/∂qResearch Paper

Motivation

A firm that sells a network good (a platform, a communication service, a standard) faces consumers whose benefit from buying grows with the number of other buyers. When these network effects are strong, the buying decisions form a coordination game: everybody buying and nobody buying can both be equilibria at the same price and quality. The firm's choice of quality then depends on which equilibrium it expects consumers to play.

The classical answer, going back to Spence's analysis of monopoly quality (Spence 1975), is that a monopolist sets quality for the marginal consumer. Under the usual equilibrium-selection criteria (Pareto dominance, focality) the network-good monopolist inherits this logic. L. T. Chan, Quality Strategies in Network Markets (Management Science, 2023; SSRN copy 4203818), asks what happens when the firm instead anticipates potential maximization, a generalization of risk dominance to many players introduced through the potential games of Monderer and Shapley (1996). The answer is a different first-order condition for quality, in which every consumer's valuation and every possible number of buyers matter. This mission formalizes that condition, Proposition 5 of the paper, together with the chain of results in §3 that leads to it.

Setting

There are $n\ge 1$ consumers $N=\{1,\dots,n\}$ . Consumer $i$ has a valuation $v_i>0$ , labelled so that $v_1\ge\dots\ge v_n$ . The benefit $f(k,q)\ge 0$ of the good when $k$ consumers buy at quality $q$ is weakly increasing in $k$ and, in $q$ , weakly increasing and differentiable. The firm's cost of quality $c(q)\ge 0$ is weakly increasing and differentiable.

In stage 1 the firm chooses a price $p\ge 0$ and a quality $q\ge 0$ . In stage 2 consumers simultaneously decide whether to buy. If $B\subseteq N$ is the set of buyers, consumer $i$ receives the payoff (7)

u_i(B,p,q)=v_if(|B|,q)-p\ \text{ if } i\in B,\qquad u_i(B,p,q)=0\ \text{ if } i\notin B,

and the firm earns $|B|p-c(q)$ . A buyer set $B$ is a Nash equilibrium of stage 2 if no buyer gains by leaving and no non-buyer gains by joining. The market has strong network effects at $q$ when $v_if(i,q)$ is strictly increasing in $i$ .

The potential (10) of a buyer set is

\Phi(B,p,q)=\sum_{i=1}^{|B|}f(i,q)-p\sum_{i\in B}\frac1{v_i}.

A potential maximizer is a buyer set maximizing $\Phi(\cdot,p,q)$ over all subsets of $N$ . A firm that anticipates potential maximization earns $\Pi(p,q)=np-c(q)$ when all consumers buying is a potential maximizer, and $-c(q)$ otherwise. In Lean these objects are Market, Market.Standing, Market.StrongNE, Market.u, Market.IsNash, Market.pot, Market.IsPotMax and Market.profitPM in the namespace NetworkQuality.PotentialMax.

Formalization targets

Goal: Proposition 5 (p. 15)

Assume the standing assumptions and strong network effects at every $q\ge 0$ . If $(p^*,q^*)$ maximizes $\Pi$ over $p\ge 0$ , $q\ge 0$ and $q^*>0$ , then

c'(q^*)=n\Big(\frac1n\sum_{i=1}^n\frac1{v_i}\Big)^{-1}\frac1n\sum_{i=1}^n\frac{\partial f(i,q^*)}{\partial q}.

The statement is the necessary first-order condition. It fixes no functional form for $f$ or $c$ .

Milestones

(11), p. 13. For $i\notin B_{-i}$ : $u_i(B_{-i}\cup\{i\})-u_i(B_{-i})=v_i[\Phi(B_{-i}\cup\{i\})-\Phi(B_{-i})]$ , so stage 2 is a weighted potential game.
§3.5, p. 14. Every potential maximizer is a Nash equilibrium.
Proposition 1, p. 10. Under strong network effects the equilibria are exactly $\{N\}$ for $p<v_1f(1,q)$ , $\{\emptyset\}$ for $p>v_nf(n,q)$ , and $\{N,\emptyset\}$ in between.
(12), p. 14. Under strong network effects every potential maximizer is $N$ or $\emptyset$ , and $N$ is one iff $p\le\big(\frac1n\sum_i\frac1{v_i}\big)^{-1}\frac1n\sum_i f(i,q)=:p(q)$ .
(13), p. 14. $v_1f(1,q)\sum_i\frac1{v_i}\le\sum_i f(i,q)\le v_nf(n,q)\sum_i\frac1{v_i}$ .
(14), p. 15. At each quality the maximal profit over prices $p\ge0$ is $n\,p(q)-c(q)$ , attained at $p(q)$ .

Significance

The result. Proposition 5 replaces the Spence condition $c'(q)=n\,v_n\,\partial f(n,q)/\partial q$ (Proposition 4 of the paper) by one in which the marginal consumer's valuation $v_n$ is replaced by the harmonic mean of all valuations, and the equilibrium benefit $f(n,q)$ by its uniform average over the number of buyers. Comparing it with the social optimum (Proposition 3, arithmetic mean of valuations) shows that a firm worried about miscoordination underprovides quality relative to the planner, increasingly so as valuations become more dispersed, and that it tends to undersupply (oversupply) quality when the number of buyers and quality are complements (substitutes) in the benefit $f$ (p. 15).

Formalizing it. The paper's arguments are in the main text (§3.2 and §3.5) and are short; some steps are only sketched: Proposition 1's proof treats only buyer sets of the form $\{1,\dots,k\}$ , and (12) is derived only in the price range with two equilibria. A machine-checked development makes these steps complete, fixes the tie-breaking convention of the selection, and isolates exactly which assumptions the first-order condition uses (none of the convexity the paper assumes). No part of this result has a machine-checked proof at the time of writing.

Difficulty

The objects are finite and the algebra is elementary, so the difficulty lies in bookkeeping that the paper leaves implicit. The obvious reading of Proposition 1, "consumers $1$ to $k$ buy", is not forced when valuations tie; excluding an arbitrary buyer set of intermediate size needs a comparison between its weakest buyer and its strongest non-buyer, using the ordering of valuations and nonnegativity of $f$ . The characterization (12) is a statement about maximizers over all $2^n$ buyer sets, not just about the two candidates the text compares, so it rests on the reduction "potential maximizer ⇒ Nash equilibrium ⇒ $N$ or $\emptyset$ ". Finally the firm optimizes jointly over price and quality against a discontinuous profit function; the first-order condition only appears after the price has been optimized out at each quality, and it needs differentiability at an interior optimum.

Formalization scope

Consumers are Fin n; the paper's consumer $i$ is Lean index $i-1$ , while the first argument of $f$ is a number of buyers in ℕ, so $\sum_{i=1}^n f(i,q)$ is ∑ i : Fin n, M.f (i.val + 1) q. $v_1$ and $v_n$ are M.v ⟨0, _⟩ and M.v ⟨n - 1, _⟩. $f$ and $c$ are total functions on ℝ.

The standing assumptions (Market.Standing, pp. 4 and 9) are: $n\ge1$ ; $v_i>0$ and $v$ antitone; for $k\ge1$ and $q\ge0$ , $f(k,q)\ge0$ , $f$ weakly increasing in $k$ and in $q$ on $[0,\infty)$ , $f(k,\cdot)$ differentiable on $(0,\infty)$ ; $c\ge0$ on $[0,\infty)$ , weakly increasing there and differentiable on $(0,\infty)$ . Statements about a single quality add $q\ge0$ , the paper's domain.

Added hypotheses, each disclosed in the items: equilibria are pure (buyer sets); the goal assumes an interior quality $q^*>0$ and strong network effects at every $q\ge0$ ; the "sufficiently convex" cost of p. 4 is dropped, so the goal is the necessary condition only. The profit under potential maximization selects "all buy" at the tie $\Phi(N)=\Phi(\emptyset)$ , as the paper's "if and only if $p\le\dots$ " does.

The profit is defined through the selection (IsPotMax over all buyer sets), not as the reduced formula (14), and the goal's optimality hypothesis ranges over price and quality jointly; defining the profit by (14), or restricting maximizers to $\{N,\emptyset\}$ , would trivialize the mission and is ruled out. Derivatives are deriv, and the standing assumptions guarantee they are genuine at $q^*>0$ .

Everything needed beyond Mathlib (Finset, deriv, IsLocalMax) is in the single definition file. Proofs of the milestones in any order are welcome, as are proofs of the goal that use the milestones as stepping stones.

Selected references

L. T. Chan, Quality Strategies in Network Markets, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4792 (SSRN version of April 2023: https://ssrn.com/abstract=4203818)
D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
A. M. Spence, Monopoly, Quality, and Regulation, Bell Journal of Economics 6 (1975), 417–429. https://www.jstor.org/stable/3003302

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Optimization·Captain: mikedeng1

Marketplace Leakage 1: With Uniform Switching Costs the Equilibrium Fee Is min{μ, v − c}, Leakage Is Positive but Partial, and the Marketplace's Profit Increases in μResearch Paper

Motivation

Online marketplaces such as Airbnb, Amazon, eBay, Preply or Upwork earn most of their revenue from transaction fees: a seller who sells through the marketplace pays a fee on every sale. Many of these sellers also run their own sales channel, and a buyer who discovers a seller on the marketplace can often complete the purchase directly with that seller, avoiding the fee. This is marketplace leakage (also called disintermediation or showrooming of the platform). Marketplaces respond with measures the paper lists on its first pages: bundling transaction-related services, restricting buyer–seller communication before a transaction, and penalizing sellers caught taking clients off the platform.

Hagiu and Wright (Marketplace Leakage, Management Science, 2023) build a minimal model of this tension. Their baseline analysis answers the first question any of the later strategies depends on: if the marketplace can only choose its fee, what fee does it set, how much leakage remains in equilibrium, and how do these respond when buying directly becomes more costly for buyers? This mission formalizes that baseline result, Proposition 1 of the paper, for uniformly distributed switching costs.

Setting

There is one marketplace $M$ , one seller $S$ and a unit mass of buyers, each wanting one unit of $S$ 's product. Every buyer values the product at $v$ ; $S$ 's marginal cost is $c$ , with $c<v$ ; the outside option is worth $0$ .

$S$ can sell through $M$ , paying $M$ a fee $f$ per transaction, or through its direct channel, which carries no fee. It sets a price $p_m$ on $M$ and a direct price $p_d$ . A buyer who buys directly bears a switching cost $s$ ; in this mission $s$ is uniformly distributed on $[0,\mu]$ with $\mu>0$ , so its CDF is

G(s)=\min\Bigl\{\max\Bigl\{\frac s\mu,0\Bigr\},1\Bigr\}.

The timing is: $M$ sets $f$ ; observing $f$ , $S$ sets its prices; buyers then choose. The paper's Lemma 1 lets one fix $p_m=v$ , so $S$ only chooses $p_d\le v$ . A buyer buys directly iff $s\le v-p_d$ , so a share $G(v-p_d)$ of buyers — the leakage — buys directly. $S$ 's profit at fee $f$ is

\pi_f(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),

and $M$ earns $\Pi=f\,(1-G(v-p_d))$ . A direct price is seller-optimal at $f$ if it maximizes $\pi_f$ over $p_d\le v$ . An equilibrium outcome is a pair $(f,p_d)$ with $f\le v-c$ , $p_d$ seller-optimal at $f$ , such that no other fee $f'\le v-c$ , followed by a seller-optimal response, gives $M$ more.

Formalization targets

Goal: Proposition 1

For every $\mu>0$ an equilibrium outcome exists, and every equilibrium outcome $(f^*,p_d^*)$ satisfies

f^*(\mu)=\min\{\mu,v-c\},\qquad p_d^*(\mu)=v-\min\Bigl\{\frac\mu2,\frac{v-c}2\Bigr\},\qquad \Pi^*(\mu)=\begin{cases}\mu/2 & \mu\le v-c,\\ (v-c)\bigl(1-\frac{v-c}{2\mu}\bigr) & \mu\ge v-c,\end{cases}

with leakage $G(v-p_d^*)=\frac1\mu(v-p_d^*)\in(0,1)$ . As $\mu$ increases, the fee weakly increases, the direct price and the leakage weakly decrease, and the marketplace's profit strictly increases.

Milestones

(4): for every fee $f\ge0$ the seller's optimal direct price is unique and equals $v-f/2$ if $f\le2\mu$ and $v-\mu$ if $f\ge2\mu$ .
(5): at such a response the marketplace earns $f(1-f/(2\mu))$ if $f\le 2\mu$ and $0$ if $f\ge2\mu$ .
The optimal fee (proof of Proposition 1): $(f,p_d)$ is an equilibrium outcome iff $f=\min\{\mu,v-c\}$ and $p_d$ is seller-optimal at $f$ .
Equilibrium leakage (proof of Proposition 1): $G(v-p_d^*)=f^*/(2\mu)=\min\{1/2,(v-c)/(2\mu)\}$ .

Significance

Proposition 1 is the baseline against which the paper measures every anti-leakage strategy: investment in transaction benefits, communication bans, referral fees and price-parity clauses are each compared with the fee-only outcome $\Pi^*(\mu)$ , and Proposition 3 of the paper uses the closed form (6) directly. The result also has a substantive message: a fee-setting marketplace never eliminates leakage, but never lets it become total, and it gains from higher switching costs even though its own fee response offsets part of their effect on leakage.

The proposition is proved in the paper by elementary calculus. To our knowledge it has no machine-checked proof. Formalizing it produces a checked version of the baseline game, a verified statement of the seller's best response and the marketplace's value as functions of the fee, and a template that the companion missions on this paper reuse.

Difficulty

The seller's problem is not a smooth concave program: the clamped distribution $G$ creates a kink at $v-p_d=\mu$ , below which every buyer switches and the profit is linear in $p_d$ . The first-order condition $p_d=v-f/2$ is the optimum only while $f\le2\mu$ ; above that the optimum sits at the kink. The marketplace's objective inherits a kink at $f=2\mu$ , and its feasible set $f\le v-c$ adds a corner that binds exactly when $\mu>v-c$ . Negative fees are feasible and must be ruled out. The comparative statics compare equilibrium objects across two parameter values that may lie in different regimes, so the statement cannot be read off one formula.

Formalization scope

All parameters are real numbers, with the standing assumptions $c<v$ and $\mu>0$ as explicit hypotheses. $G$ is the clamped uniform CDF above. The statements use the reduced seller problem (1) with $p_m=v$ , as the paper does after Lemma 1; Lemma 1 itself, which concerns the full game in which $S$ also chooses $p_m$ , is not posed. Seller-optimality is an optimality predicate over $p_d\le v$ , and the equilibrium is an optimality predicate over feasible fees $f\le v-c$ (negative fees included); "max" is attained, not a supremum. The displays (4) and (5) are stated for $f\ge0$ , which is what they require; the paper's preface "Assuming $f\le v-c$ " is not needed and does not exclude $f<0$ .

Trivializing formalizations are ruled out: the seller's response and the marketplace's profit are not defined by the closed forms (4)–(5), the marketplace's value is not an unattained sSup, the equilibrium fee is not selected by Classical.choose, and the comparative statics are stated about equilibrium outcomes at two values of $\mu$ , not about the formulas alone.

The development needs only Mathlib's real arithmetic, min/max and order lemmas. A proof of the seller's best response for a clamped uniform distribution is reusable in the companion missions on transaction benefits, communication bans and price parity, which restate the same model. Proofs of any milestone are welcome independently.

Selected references

A. Hagiu and J. Wright, Marketplace Leakage, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4757 (formalized from the authors' manuscript dated March 2023; Proposition 1 on pp. 9–10, proof in §8.2, p. 34).

6 thms2 active usersReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Fair and Consistent Prize Allocation in Competitions 3: Anonymity, Order Preservation, Winner Strict Endowment Monotonicity and Top Consistency Characterize Parametric RulesResearch Paper

Motivation

Rank-order competitions — sports tournaments, poker final tables, golf tours, crowdsourcing contests, sales leagues — end with a ranking of the participants and a pot of prize money that has to be split according to that ranking. Organisers publish prize tables that change with the number of entrants and with the size of the purse, and these tables are usually justified only by tradition. Dietzenbacher and Kondratev (arXiv:2008.08985v2, published in Management Science 2023, doi:10.1287/mnsc.2022.4520) take the axiomatic approach of fair-division theory and ask which prize allocation rules are characterised by natural requirements of fairness and coherence across competitions of different sizes.

Consistency — invariance of a rule under "re-running the allocation" for a subgroup with the money it collectively received — has a long history in axiomatic allocation: bankruptcy problems (Aumann and Maschler 1985), taxation (Young 1987), bargaining (Lensberg 1987, 1988) and cooperative games (Peleg 1986; Hart and Mas-Colell 1989). The paper applies it to competitions. Full consistency together with order preservation and endowment monotonicity yields the interval rules (Theorem 1); weakening consistency to local consistency yields the single-parametric rules (Theorem 2). This mission concerns the weakest version, top consistency, which only constrains the top segment of the ranking and describes real prize schemes such as the golf tournament of Table 1(b) of the paper. It is the third mission of a series on this paper; the first two treat Theorems 1 and 2.

Setting

Fix a countable set $U$ of at least three potential competitors. A competition $(N,\mathcal R,E)$ consists of a finite nonempty set $N\subseteq U$ , a ranking $\mathcal R:N\to\{1,\dots,|N|\}$ (a bijection; competitor $i$ is ranked above $j$ when $\mathcal R(i)<\mathcal R(j)$ ), and a prize endowment $E\ge0$ . For $S\subseteq N$ the subranking $\mathcal R_S:S\to\{1,\dots,|S|\}$ orders $S$ as $\mathcal R$ does.

A prize allocation rule $\varphi$ assigns to each competition a vector $\varphi(N,\mathcal R,E)\in\mathbb R_+^N$ with $\sum_{i\in N}\varphi_i(N,\mathcal R,E)=E$ . The axioms are:

anonymity: $\varphi_i(N,\mathcal R,E)=\varphi_j(N',\mathcal R',E)$ whenever $|N|=|N'|$ and $\mathcal R(i)=\mathcal R'(j)$ ;
order preservation: $\mathcal R(i)<\mathcal R(j)$ implies $\varphi_i\ge\varphi_j$ ;
winner strict endowment monotonicity: if $E<E'$ then $\varphi_i(N,\mathcal R,E)\le\varphi_i(N,\mathcal R,E')$ for all $i$ , strictly for the winner $\mathcal R(i)=1$ ;
top consistency: for each $S\subseteq N$ with $\mathcal R(i)\le|S|$ for every $i\in S$ , and each $i\in S$ ,

\varphi_i(N,\mathcal R,E)=\varphi_i\Big(S,\mathcal R_S,\sum_{j\in S}\varphi_j(N,\mathcal R,E)\Big).

A rule is parametric if there are continuous non-decreasing $f_1,f_2,\dots:\mathbb R_+\to\mathbb R_+$ with $f_1(x)=x$ and $f_{k+1}(x)\le f_k(x)$ such that $\varphi_i(N,\mathcal R,E)=f_{\mathcal R(i)}(x)$ , where $x\ge0$ solves $\sum_{k=1}^{|N|}f_k(x)=E$ . The winner gets $x$ and position $k$ gets $f_k(x)$ . Equal Division ( $f_k(x)=x$ ) and Winner-Takes-All ( $f_k=0$ for $k\ge2$ ) are parametric.

Formalization targets

Goal: Theorem 3 (p. 22)

\varphi \text{ is anonymous, order preserving, winner strictly endowment monotonic and top consistent}\iff\varphi\text{ is a parametric rule.}

Both directions are part of the goal.

Milestones (proof of Theorem 3, pp. 32–33)

Every parametric rule satisfies the four axioms (the "readily checked" direction).
Under order preservation, endowment continuity and winner strict endowment monotonicity, the winner's prize $E\mapsto\varphi_1(N,\mathcal R,E)$ is strictly increasing, continuous and unbounded on $\mathbb R_+$ , so each $x\ge0$ is the winner's prize for exactly one $E$ .
The induction step: a representation $f_1,\dots,f_n$ valid on all competitions with at most $n$ competitors extends, by a new continuous non-decreasing $f_{n+1}\le f_n$ , to all competitions with $n+1$ competitors.

Lemma 1 of the paper (endowment monotonicity implies endowment continuity, p. 10) is used in the proof; it is formalized in the first mission of this series and will be referenced from there.

Companion: Corollary 8 (p. 22)

Replacing winner strict endowment monotonicity by endowment additivity (equivalently scale invariance) characterises the proportional rules $\varphi_i=\lambda_{\mathcal R(i)}E/\sum_{k\le|N|}\lambda_k$ with $\lambda_1>0$ and $\lambda_{k+1}\le\lambda_k$ .

Significance

Theorem 3 says that the four axioms leave exactly one degree of freedom per position: a monotone function of the winner's prize. This gives organisers a complete menu of prize schemes that are fair in the anonymous, order-preserving sense and that keep the top of the table unchanged when lower-ranked entrants leave — the property that matters when competitors are eliminated one at a time and paid at the moment of elimination. It contains the single-parametric rules of Theorem 2, the Winner-Takes-Surplus rules, the geometric rules and the proportional rules (Corollary 8) as special cases, and the paper shows in a Remark (p. 33) that the four axioms are logically independent.

The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. The formalization adds a reusable layer for variable-population allocation problems — rankings of finite subsets of a fixed universe, subrankings, and consistency axioms restricted to families of subsets — that is not in Mathlib. Formal proofs of both directions, of the milestones, and of Corollary 8 are all welcome.

Difficulty

The "if" direction is a computation, but it requires showing that the parameter $x$ is well defined and moves monotonically with $E$ , which uses $f_1(x)=x$ and the intermediate value theorem. The "only if" direction must construct the functions $f_k$ from an abstract rule. The natural first idea — define $f_k(x)$ as the prize of position $k$ when the winner receives $x$ — needs the winner's prize to be invertible as a function of $E$ , which uses continuity (supplied by Lemma 1, not assumed), strict monotonicity only for the winner, and unboundedness, which comes from order preservation together with exhaustion of the endowment. Top consistency then has to transfer the representation from competitions of size $n$ to size $n+1$ , and anonymity has to transfer it from one ranked set to every other one of the same size; the induction over the number of competitors must keep all smaller sizes, since top consistency reduces to every top segment.

Formalization scope

A ranked set $(N,\mathcal R)$ is a duplicate-free nonempty List U, best competitor first; $\mathcal R(i)$ is the 1-based index pos l i, and $\mathcal R_S$ is the sublist of entries in $S$ . $U$ is an arbitrary type with decidable equality; the paper's standing assumptions (countable, at least three elements) are hypotheses of the goal and of Corollary 8, and are omitted from milestones that do not use them.
A rule is a function φ : List U → ℝ → U → ℝ; it is required to be a prize allocation rule (nonnegative prizes summing to $E$ ) on rankings and $E\ge0$ , and every axiom quantifies only over that domain. Endowments are reals with $E\ge0$ .
The representation $f_1,f_2,\dots$ is f : ℕ → ℝ → ℝ, indexed from 1 as on the page ( $f_0$ unused); continuity, monotonicity, nonnegativity and $f_1(x)=x$ are required on $[0,\infty)$ . The parameter $x$ is given existentially; it is unique, so this is the page's "where $x\in\mathbb R_+$ is such that".
Endowment continuity is coordinatewise continuity on $[0,\infty)$ .

Trivializing formalizations are ruled out: rules act on every finite ranked subset of $U$ , not on a fixed competitor set; top consistency quantifies over exactly the top segments (full or local consistency would change the theorem — the rule of Example 6 is parametric but not locally consistent); the goal is a biconditional; the parametric family includes $f_1=\mathrm{id}$ , the decreasing chain $f_{k+1}\le f_k$ , and continuity of every $f_k$ .

Corollary 7 of the paper is not included: its "only if" parts ("for each $k$ ") fail as written when $U$ is finite, since $f_k$ for $k>|U|$ is not determined by the rule.

Selected references

B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science, 2023. https://arxiv.org/abs/2008.08985v2, https://doi.org/10.1287/mnsc.2022.4520
R. J. Aumann and M. Maschler, Game theoretic analysis of a bankruptcy problem from the Talmud, Journal of Economic Theory 36(2):195–213, 1985. https://doi.org/10.1016/0022-0531(85)90102-4
S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57(3):589–614, 1989. https://doi.org/10.2307/1911054

8 thms2 active usersReviewed

Completed

Economics Optimization·Captain: mikedeng1

Digital Privacy II: Against the Social Optimum, a Business Never Under-Collects While Over-Protecting Data, and a Purely Usage-Driven One Under-Collects and Under-ProtectsResearch Paper

Motivation

Digital businesses (search engines, social networks, marketplaces) record what their users do and decide how well to protect what they record. Both choices affect users: stored data can improve the service, and it can also be accessed by adversaries such as hackers, fraudsters or data brokers, whose activity harms users. Regulation of data collection and data protection (the GDPR, the CCPA, liability rules for breaches) presupposes an answer to a basic question: in which direction does a profit-maximizing business's data strategy deviate from the one a benevolent planner would choose?

I. P. Fainmesser, A. Galeotti and R. Momot, Digital Privacy (Management Science 69(6), 2023; author manuscript SSRN 3459274), answer it in a model where users, adversaries and the business all respond to each other. Their Theorem 2 shows that the deviation is not arbitrary: one combination of errors never occurs, and the sign of the error is pinned down completely for a business whose revenue depends only on usage. This mission formalizes those two claims.

Setting

A data strategy is a pair $(\xi, C)$ : the share $\xi \in [0,1]$ of each user's activity that the business stores, and a protection level $C \ge 0$ , which costs $\psi C$ . The parameters are real numbers: a network effect $\beta \in [0,1)$ , the users' marginal benefit from stored data $\rho \in [0,1)$ , the cost $\psi$ , the revenue model $P \in [0,1]$ , and the planner's weight $\alpha \in [0,1]$ .

Given $(\xi, C)$ , a unit mass of identical users choose activity levels and a large population of adversaries decide whether to access the stored data. The resulting equilibrium (Proposition 1 of the paper, display (3)) has average user activity

\bar a^*(\xi, C) = \frac{C(1+\rho\xi)}{C(1-\beta)+\xi^2}, \qquad \bar a^*(0, C) = \frac{1}{1-\beta}.

The value at $\xi = 0$ is the activity when nothing is stored, the value the paper uses where (3) reads $0/0$ . From $\bar a^*$ one builds the consumer surplus (4), the business's profit (2) and the planner's objective (7):

\mathrm{CS}(\xi,C) = \tfrac12 \bar a^*(\xi,C)^2, \qquad \Pi(\xi,C) = (1-P)\,\bar a^*(\xi,C) + P\,\xi\,\bar a^*(\xi,C) - \psi C, \qquad W(\xi,C) = \alpha\,\mathrm{CS}(\xi,C) + (1-\alpha)\,\Pi(\xi,C).

The revenue model $P$ interpolates between a purely usage-driven business ( $P = 0$ , revenue proportional to activity) and a purely data-driven one ( $P = 1$ , revenue proportional to stored data $\xi \bar a^*$ ). A business optimum $(\xi^*, C^*)$ maximizes $\Pi$ over the feasible set $[0,1] \times [0,\infty)$ ; a social optimum $(\xi^W, C^W)$ maximizes $W$ over the same set. The business under-collects if $\xi^* \le \xi^W$ and over-protects if $C^* \ge C^W$ , and so on.

Formalization targets

Goal: Theorem 2, first two sentences

The paper's Theorem 2 (p. 13) reads:

Relative to the socially optimal strategy, the equilibrium data strategy of a purely usage-driven business (P = 0) prescribes under-collection and under-protection of users' data, i.e., ξ* ≤ ξ^W and C* ≤ C^W. The equilibrium data strategy of a business with any data-driven component in its revenue model (P > 0) never prescribes under-collection and over-protection of users' data i.e., it is never the case that ξ* ≤ ξ^W and C* ≥ C^W with at least one of the inequalities being strict. Any other direction in which the optimal business's data strategy deviates from the socially optimal strategy is the outcome for some specification of the business's revenue model and values of other model parameters.

The goal is its first two sentences, for every business optimum and every social optimum:

P = 0 \;\Longrightarrow\; \xi^* \le \xi^W \text{ and } C^* \le C^W,

P > 0 \;\Longrightarrow\; \neg\bigl(\xi^* \le \xi^W,\ C^* \ge C^W,\ \text{at least one strict}\bigr).

The third sentence is established numerically in the paper (Figure 3) and is not a target.

Milestones

Display (11), p. 34: under $\xi^* \le \xi^W$ and $C^* \ge C^W$ , the social optimum has weakly higher activity, $\bar a^*(\xi^W, C^W) \ge \bar a^*(\xi^*, C^*)$ .
Display (12), p. 34: under the same assumptions, $\bar a^*(\xi^W,C^W)\,\xi^W \ge \bar a^*(\xi^*,C^*)\,\xi^*$ .
Proposition 5(i), first claim (Online App. p. 8): for fixed $C$ and $P = 0$ , a collection level maximizes $\Pi(\cdot, C)$ on $[0,1]$ if and only if it maximizes $W(\cdot, C)$ .
The $P = 0$ step of the proof (App. A.4, p. 34): if $P = 0$ and $\xi^* > \xi^W$ , then $C^* > C^W$ .

Significance

The result. Theorem 2 identifies the one inefficiency that no revenue model produces: a business never stores too little data while protecting it too much. All other combinations occur for some parameters, so a regulator cannot infer the direction of a business's error without knowing its revenue model; but for a purely usage-driven business the direction is known, and it is too little protection. This underlies the paper's discussion of policy in §6, where the instruments considered (liability for data breaches, taxes on data) are compared by how they move $(\xi^*, C^*)$ towards $(\xi^W, C^W)$ .

The formalization. The result is proved in the paper (App. A.4, with Proposition 5 in Online App. C.5); it has not been machine-checked. The paper's argument for the purely usage-driven case refers to first-order conditions and does not treat the boundary strategies ( $\xi = 0$ , $C = 0$ ) or parameter corners ( $\rho = 0$ ) separately; a formal proof has to handle them. A complete development also yields reusable facts about the equilibrium activity $\bar a^*$ : its sign, its behaviour in $\xi$ for fixed $C$ , and the monotonicity in $C$ of the activity-maximizing collection level.

Difficulty

Both optima are defined only implicitly, as maximizers over a non-compact feasible set of a non-concave objective, and neither has a closed form that this mission may use. The comparison must therefore work from the optimality inequalities alone. The tempting approach, comparing first-order conditions, does not give a global statement: $\Pi$ and $W$ may have several local maxima, the maximizers need not be unique (both optima are $(0,0)$ in a whole region of parameters), and the constraint $\xi \le 1$ binds for large protection. In the purely usage-driven case the profit and welfare share their maximizers in $\xi$ for each fixed $C$ , but turning that into a comparison of $C^*$ with $C^W$ requires control of how the maximizing $\xi$ moves with $C$ , including at $C = 0$ .

Formalization scope

All objects are real-valued functions of explicit real parameters $\beta, \rho, \psi, P, \alpha$ and of the strategy $(\xi, C)$ , in the namespace DigitalPrivacy.Welfare, which imports $\bar a^*$ , CS, the feasible set and the business optimum from the shared module DigitalPrivacy.Strategy.Setting. The equilibrium activity takes the value $1/(1-\beta)$ at $\xi = 0$ for every $C$ , as in the paper; Lean's default $0/0 = 0$ is not used. Optima are predicates (IsBusinessOpt, IsSocialOpt): a feasible point at which the objective is at least its value at every feasible point. Theorem 2 quantifies over every pair of optima and asserts neither existence nor uniqueness. The P > 0 clause keeps the "at least one strict" condition; without it the clause is false, because both optima coincide at $(0,0)$ in part of the parameter space.

The standing assumptions are the paper's ranges $0 \le \beta < 1$ , $0 \le \rho < 1$ , $0 \le P \le 1$ , $\alpha \le 1$ , with two disclosed strengthenings: $\psi > 0$ (with $\psi = 0$ , $\rho = 0$ , $P = 0$ , every $(0, C)$ is both a business and a social optimum and the $P = 0$ sentence fails) and $\alpha > 0$ (with $\alpha = 0$ the planner's problem is the business's, and step (11) does not hold). Proposition 5(i) is stated with the printed ranges, $\alpha = 0$ included. No other hypothesis is added, so the hypotheses on the optima cannot be made vacuous by the encoding; a sanity check exhibits parameters at which $(0,0)$ is both a business and a social optimum.

A complete development needs elementary real analysis of the rational function $\bar a^*$ on $[0,1] \times [0,\infty)$ and nothing beyond Mathlib. Proofs of the milestones, of lemmas about $\bar a^*$ , and alternative arguments for the goal are all welcome. The paper's proofs are in App. A.4 (pp. 33–35) and Online App. C.5 (Online pp. 8–9).

Selected references

I. P. Fainmesser, A. Galeotti, R. Momot, Digital Privacy, Management Science 69(6):3157–3173, 2023. https://doi.org/10.1287/mnsc.2022.4513. Author manuscript, This Draft: April 2022, https://ssrn.com/abstract=3459274 (the version cited for all page and display numbers).

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Mechanism Design·Captain: mikedeng1

Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail I: Under Centralized Dispute Resolution the Equilibrium Ransom Is Not Monotonically Decreasing in Efficiency γδResearch Paper

Review blackmail on online platforms

Online marketplaces depend on consumer reviews, and a single negative review can move a seller's future sales. Review blackmail exploits this: a consumer buys a product, posts a negative review, and offers to remove it in exchange for a payment. Platforms such as Amazon, eBay, Taobao and TripAdvisor respond with dispute resolution mechanisms that let sellers contest reviews. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) build a game-theoretic model of the seller, the blackmailer and the market's belief about product quality, and ask how the design of such a mechanism changes the blackmailer's leverage. Their first finding concerns a centralized mechanism, where the seller reports the review and the platform judges it: making the platform faster or more accurate does not always lower the ransom the blackmailer can extract. This mission formalizes that result together with the equilibrium analysis it rests on.

The model

A monopolist sells a product of unobservable quality $q\in\{l,h\}$ ; the market's prior that quality is high is $a\in(0,1)$ . A buyer of a high-quality product has gross utility $v_j$ with probability $\theta\in(0,1)$ and $0$ otherwise, with $v_j$ standard uniform; a low-quality product always gives $0$ . One consumer arrives.

With probability $\beta\in(0,1)$ he is malicious: he buys, posts a negative review $N$ , and demands a ransom $r$ for removing it.
Otherwise he is regular: at price $p$ he buys iff $a\theta v_j-p\ge0$ , which happens with probability $\rho=1-p/(a\theta)$ , and posts a truthful review, positive ( $P$ ) or negative ( $N$ ). No purchase means no review, written $R=0$ .

The market sees the review $R\in\{N,0,P\}$ , updates its belief to a posterior $a'$ by Bayes' rule, and the seller then earns a continuation payoff $\pi(a')$ , with $\pi$ nonnegative, convex and strictly increasing on $[0,1]$ .

Facing a ransom demand the seller can settle ( $s$ : pay $r$ , the review disappears), do nothing ( $n$ : the review stays), or report ( $c$ ) the review to the platform's centralized mechanism at a hassle cost $c\ge0$ . The platform investigates immediately with probability $\gamma\in[0,1]$ (timeliness) and identifies a malicious review correctly with probability $\delta\in[0,1]$ (accuracy); the review is removed with probability $\gamma\delta$ , the mechanism efficiency.

The market cannot observe the seller's interaction with the blackmailer. It holds a belief $i\in\{s,n,c\}$ about the seller's response, and this belief determines the posteriors: under belief $i$ a malicious review stays visible with probability $m_s=0$ , $m_n=1$ or $m_c=1-\gamma\delta$ , and $a^i_R$ is the Bayes posterior computed from the resulting review likelihoods. When the market believes $i$ and the seller plays $j$ , his payoff is $\pi(a^i_0)-r$ ( $j=s$ ), $\pi(a^i_N)$ ( $j=n$ ), or $\gamma\delta\,\pi(a^i_0)+(1-\gamma\delta)\pi(a^i_N)-c$ ( $j=c$ ). A response $i$ is an equilibrium if it is a best response to the belief $i$ ; among several equilibria, the seller-preferred one prevails. The malicious consumer buys iff some ransom $r>p$ is accepted in the prevailing equilibrium, and the equilibrium ransom $r^*$ is the greatest ransom at which settling prevails.

Formalization targets

Goal: Corollary 1 (p. 14)

If $c>0$ and $p<\pi(a)-\pi(a^n_N)-c$ , there are efficiencies $0\le e_1<e_2\le1$ at both of which the malicious consumer purchases, with

r^*(e_1)<r^*(e_2).

The equilibrium ransom is not monotonically decreasing in the efficiency $\gamma\delta$ .

Milestones

Lemma 2 (p. 11): $a^i_P=1$ , $a^i_0=a$ , $a^i_N\in[0,a]$ , and closed forms of $a^n_N$ , $a^c_N$ , $a^s_N$ .
Ordering (§4.1, p. 11): $a^s_N<a^c_N<a^n_N$ for $0<\gamma\delta<1$ .
Proposition 1(1)–(3) (p. 13): the exact conditions under which $n$ , $s$ and $c$ are equilibria, e.g.

i=n\ \text{is an equilibrium}\iff \pi(a^n_N)\ge\max\{\pi(a)-r,\ \pi(a)-c/\gamma\delta\}.

Proposition 2(1)–(2) (p. 13): the equilibrium ransom

r^*=\begin{cases}\pi(a)-\pi(a^n_N), & c\ge\gamma\delta(\pi(a)-\pi(a^n_N)),\\ (1-\gamma\delta)[\pi(a)-\pi(a^c_N)]+c, & c<\gamma\delta(\pi(a)-\pi(a^n_N)),\end{cases}

and the malicious consumer purchases iff $p<r^*$ .

Significance

Corollary 1 is the paper's headline message about centralized dispute resolution: improving the mechanism's timeliness or accuracy can raise the ransom. Below an efficiency threshold the mechanism is never used and the ransom equals the seller's loss from a visible negative review; just above it, the market expects the seller to report blackmail, which softens how it reads a negative review, and the blackmailer can ask for more. This is the motivation for the paper's second design, semi-decentralized dispute resolution, analysed in a companion mission. Proposition 2 is the complete characterization of the blackmailer's equilibrium behaviour under the centralized mechanism and is used again in the paper's pricing analysis (§4.4).

The results are proved in the paper (Appendix C). No machine-checked version exists. This mission produces Lean statements of the model, of the Bayes posteriors, of the equilibrium conditions, of the seller-preferred selection and of the ransom characterization, all derived from the primitive game rather than from the paper's closed forms.

Difficulty

Each step is elementary, but the chain is long and sign-sensitive. The equilibrium conditions require handling a belief-dependent payoff (the posterior depends on what the market believes, not on what the seller does), so a deviation changes the action without changing the posteriors. The ransom characterization needs a three-way comparison of equilibria and the tie-breaking in favour of settling at the boundary, where two equilibria give the same payoff. The corollary needs the jump at the threshold efficiency $c/(\pi(a)-\pi(a^n_N))$ to be strictly positive and to survive a small increase of the efficiency: the posterior $a^c_N$ moves with the efficiency, so a continuity argument for $\pi$ composed with the posterior is required, and $\pi$ is only assumed convex and strictly increasing on $[0,1]$ . The natural first idea, comparing the two closed forms of Proposition 2 at a single point, does not suffice, since at the threshold itself the two regimes coincide in value.

Formalization scope

Representation. One structure Model with fields $a,\theta,\beta,p,c$ and $\pi:\mathbb R\to\mathbb R$ ; inductive types for quality, reviews ( $N$ , Z for $R=0$ , $P$ ) and responses. The posterior post m R is Bayes' rule over the likelihood table with visibility probability $m$ of a malicious review; $a^i_R$ is post (keep (γ*δ) i) R.
Standing assumptions (Standing): $a,\theta,\beta\in(0,1)$ ; $\pi\ge0$ , convex and strictly increasing on $[0,1]$ ; $c\ge0$ ; and $0<p<a\theta$ . The last is implicit in the paper: it makes the purchase probability $1-p/(a\theta)$ that of a standard uniform valuation and keeps the event $R=0$ of positive probability. Every theorem also assumes $\gamma,\delta\in[0,1]$ .
Added hypotheses. $0<\gamma\delta<1$ in the ordering (strictness) and in Proposition 1 (the page divides by $\gamma\delta$ and $1-\gamma\delta$ ). $c>0$ in Corollary 1: at $c=0$ the corollary is false. Corollary 1's hypothesis, printed with a varying $\gamma\delta$ , is assumed at the threshold efficiency and required at both exhibited efficiencies.
Conventions. "Settling prevails" means settling is an equilibrium and no equilibrium pays the seller strictly more (ties go to settling, as in the paper's proof). $r^*$ is stated with IsGreatest of the set of ransoms at which settling prevails; purchase means some such ransom exceeds $p$ . "Not monotonically decreasing" means not nonincreasing.
Ruled out. Defining the posteriors by Lemma 2's closed forms, or $r^*$ by Proposition 2's formulas, would make the milestones definitional; both are defined from the game instead.
Infrastructure. Only Mathlib (ConvexOn, StrictMonoOn, IsGreatest). Proofs of the milestones in order, and reusable lemmas on the monotonicity of the posterior in the visibility probability, are welcome.

Selected references

Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (accepted manuscript: LBS Research Online, eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/)

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Mechanism Design·Captain: mikedeng1

Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail II: Under Semi-Decentralized Dispute Resolution with Penalty b the Equilibrium Ransom Has a Two-Regime Closed FormResearch Paper

Motivation

Online marketplaces rely on consumer reviews, and a negative review lowers what future buyers believe about a product. Review blackmail exploits this: a consumer buys, posts a negative review, and offers to remove it for a ransom. Platforms counter with dispute-resolution mechanisms. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) compare two of them in a Bayesian game between a seller, one consumer and the market. Under the centralized mechanism the seller reports the review and the platform decides whether to remove it. Under the semi-decentralized mechanism the seller removes the review himself, and the platform checks afterwards. If it judges the removal wrongful, it reinstates the review and fines the seller a penalty $b$ .

This mission covers the semi-decentralized mechanism. Its main result, Proposition 5, gives the ransom a blackmailer can extract in equilibrium in closed form and says when blackmail pays at all. A platform needs that answer when it chooses the penalty. Mission I of this series treats the centralized mechanism.

Setting

A product has quality $q\in\{l,h\}$ . The prior that $q=h$ is $a\in(0,1)$ . A buyer of a high-quality product gets a positive experience with probability $\theta\in(0,1)$ ; a low-quality product never gives one. With probability $\beta\in(0,1)$ the consumer is malicious. A malicious consumer buys at price $p$ , posts a negative review $N$ and demands a ransom $r$ . Otherwise the consumer is regular. A regular consumer buys with probability $\rho=1-p/(a\theta)$ (valuation $v_j$ uniform on $[0,1]$ ) and reviews truthfully: positive ( $P$ ) or negative ( $N$ ). No purchase means no review, written $R=0$ ; a removed review is also seen as $R=0$ .

The market observes $R\in\{N,0,P\}$ and forms the posterior $a'$ by Bayes' rule. The seller then earns $\pi(a')$ , where $\pi$ is nonnegative, convex and strictly increasing on $[0,1]$ .

Facing a ransom demand, the seller can settle ( $s$ : pay $r$ , review removed), do nothing ( $n$ ), or use the mechanism ( $d$ ). Under $d$ the platform judges immediately with probability $\gamma\in[0,1]$ (timeliness). It recognises a malicious review with probability $\delta\in[0,1]$ (accuracy). The review is therefore reinstated with probability $\gamma(1-\delta)$ , and the penalty $b\ge0$ is paid with probability $1-\delta$ . Write $a^i_R$ for the posterior after review $R$ when the market believes the seller's response is $i$ . The payoffs of the three responses are then

\pi(a^i_0)-r,\qquad \pi(a^i_N),\qquad (1-\gamma(1-\delta))\pi(a^i_0)+\gamma(1-\delta)\pi(a^i_N)-(1-\delta)b.

The market cannot see the interaction, so $i$ is an equilibrium at $r$ if no response pays more given the belief $i$ . The equilibrium ransom $r^*$ is the largest $r$ at which settling is an equilibrium and no equilibrium pays the seller more. The malicious consumer buys iff $p<r^*$ .

A seller could also use the mechanism against genuine negative reviews. Proposition 4 shows that this is deterred exactly when $b\ge\underline b:=(1-\gamma)[\pi(a)-\pi(a^s_N)]$ .

Formalization targets

Goal: Proposition 5 (p. 21)

Let $\delta<1$ and $T=\frac{1-\gamma(1-\delta)}{1-\delta}\big(\pi(a)-\pi(a^n_N)\big)$ .

If $b\ge T>\underline b$ :

r^*=\pi(a)-\pi(a^n_N),\qquad\text{and the malicious consumer buys iff } p<r^*.

If $\underline b\le b<T$ :

r^*=(1-\delta)\big(\gamma(\pi(a)-\pi(a^d_N))+b\big),\qquad\text{and the malicious consumer buys iff } p<r^*.

Milestones

(5), p. 21: the closed form of $a^d_N$ , together with $a^i_0=a$ .
§5.1, p. 21: the ordering $a^s_N<a^d_N<a^n_N$ .
Proposition 4, p. 20: genuine negative reviews are kept iff $b\ge\underline b$ .
Proof of Proposition 5, Step 1, pp. 41–42: the conditions under which $s$ , $n$ and $d$ are equilibria, one milestone each.

Significance

Proposition 5 has two regimes. If the penalty is high, the mechanism plays no part in blackmail: the seller would never use it, and the ransom equals the one with no mechanism at all. Below the threshold, the ransom is the seller's expected loss from using the mechanism. A lower ransom then means less blackmail, and it pushes the price at which blackmail stops paying downward. The threshold $T$ rises with the accuracy $\delta$ and falls with the timeliness $\gamma$ . The paper's later results on pricing and on the platform's penalty build on this characterization.

The result is proved in the paper (Appendix C, pp. 41–43). It has no machine-checked proof. Formalizing it pins down the equilibrium concept, including the selection among multiple equilibria. It also corrects a printed slip in the proof: the simplified condition for the mechanism to be an equilibrium drops a factor $1-\delta$ .

Difficulty

Each individual equilibrium condition is a rearrangement of payoff inequalities. The difficulty lies in selecting among equilibria. Several responses can be equilibria at the same ransom. Settling prevails only if no other equilibrium pays more, and the equilibria themselves depend on $r$ . So the set of ransoms at which settling prevails is not given by one inequality. Its greatest element must be found across three scenarios, comparing three thresholds that involve three different posteriors. Those comparisons require the posterior ordering $a^s_N<a^d_N<a^n_N$ , which comes from Bayes' rule and not from the payoff algebra. Reading the equilibrium condition for $s$ alone as the answer gives the wrong ransom in case 1.

Formalization scope

Everything lives in the namespace ReviewBlackmail.SemiDec, with one structure Model holding $a,\theta,\beta,p,\gamma,\delta,b$ and the payoff fut (the paper's $\pi$ ; Real.pi is never used). The predicate Standing collects the standing assumptions: $a,\theta,\beta\in(0,1)$ ; $\pi$ nonnegative, convex and strictly increasing on $[0,1]$ ; $\gamma,\delta\in[0,1]$ ; $b\ge0$ ; and the disclosed addition $0<p<a\theta$ , which makes the purchase probability $\rho$ lie in $(0,1)$ . Per-statement additions, each disclosed in the item:

$\delta<1$ on the goal and on Step 1 for $n$ and $d$ , which divide by $1-\delta$ ;
$0<\gamma(1-\delta)<1$ on the strict ordering;
$0<\gamma<1$ on the second half of Proposition 4.

Posteriors are defined by Bayes' rule over an explicit likelihood table with two visibility probabilities: $m$ for malicious and $g$ for genuine negative reviews. Proposition 4 needs beliefs in which genuine reviews are removed. The payoffs of Proposition 5 keep genuine reviews ( $g=1$ ), the case the paper reduces to via Proposition 4. Ties in the selection rule go to settling.

The posteriors $a^i_R$ are never defined by their closed forms, and $r^*$ is never defined by (6) or (7). The goal is stated with IsGreatest on the set of ransoms at which settling prevails, not with sSup, so neither the closed forms nor junk values of a supremum can make the goal trivial.

A complete development needs only Mathlib's ConvexOn, StrictMonoOn and IsGreatest and real-field algebra. The algebra of Bayes posteriors with two-point priors may be reusable. Proofs of the milestones and the goal are welcome, in any order.

Selected references

Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (cited from the accepted manuscript, LBS Research Online eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/).

8 thms2 active usersReviewed

Completed

Economics Optimization·Captain: mikedeng1

Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition III: Without Accelerability a Financially Constrained Monopoly Invests Less Than an Unconstrained OneResearch Paper

Motivation

Young innovative firms often fund research out of internal cash flow rather than external capital. Whether such financial constraints make firms invest less in research and development (R&D) is a long-standing question in corporate finance and the economics of innovation. Myers (1977) showed that the possibility of default leads to under-investment in growth options. Danmo Lin (Management Science, 2022) separates two ways in which spending more on a project can pay off: it can make the payoff larger (scalability) or make the discovery arrive sooner (accelerability). The paper's Corollary 1 says that the classical under-investment result holds exactly when the project is scalable but not accelerable, while acceleration can reverse it. This mission formalizes the under-investment half of that corollary.

Setting

A firm faces a one-time R&D opportunity. It chooses an investment intensity $R$ , a spending rate per unit of time, and pays it until discovery. Discovery is the first arrival of a Poisson process of rate $\lambda(R)$ , and on discovery the firm receives a payoff with mean $u(R)$ . As in the paper's equation (2),

u(R)=A\,R^{\beta},\qquad \lambda(R)=\eta\,R^{\gamma},\qquad A>0,\ \eta>0,\ \beta,\gamma\in[0,1),\ \beta+\gamma<1,

and intensities are at least $\underline R=1$ . The project is scalable if $u'>0$ (here $\beta>0$ ) and accelerable if $\lambda'>0$ (here $\gamma>0$ ). Future cash is discounted at rate $r>0$ .

An unconstrained (UC) firm can always pay $R$ . By the paper's Lemma 1, equation (5), its project value at intensity $R$ is the perpetuity

V_{uc}(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}.

A financially constrained (FC) firm pays $R$ out of an asset-in-place (AIP) cash flow $X_t$ , a geometric Brownian motion with drift $\mu$ and volatility $\sigma$ that starts at $X$ . It must abandon the project once $X_t<R$ . Lemma 1, equation (6), gives its project value as

V_{fc}(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}\Big(1-\big(\tfrac{X}{R}\big)^{\alpha}\Big),\qquad \alpha=\tfrac12-\tfrac{\mu}{\sigma^2}-\sqrt{\big(\tfrac12-\tfrac{\mu}{\sigma^2}\big)^2+\tfrac{2(\lambda(R)+r)}{\sigma^2}}.

The ranges of intensities are those of (7): $[1,\bar R]$ for the UC firm and $[1,\min\{\bar R,X\}]$ for the FC firm, with $\bar R=(A\eta)^{1/(1-(\beta+\gamma))}$ . The optimal intensities $R^*_{uc}$ and $R^*_{fc}$ are the sets of maximizers of $V_{uc}$ and $V_{fc}$ over these ranges.

Formalization targets

Goal: Corollary 1, first statement (p. 6)

If $\lambda'=0$ and $u'>0$ , then $R^*_{fc}<R^*_{uc}$ . Formally: under the standing assumptions, $r>0$ , $\sigma>0$ , $X\ge1$ , $\gamma=0$ , $\beta>0$ and $A\beta\eta>1$ , both optimal sets are nonempty and

x<y\qquad\text{for every } x\in R^*_{fc}\text{ and every } y\in R^*_{uc}.

Milestones (Appendix A.4, p. 20)

Without accelerability, every interior FC optimum ( $1<R<\min\{\bar R,X\}$ ) satisfies $u'(R)\lambda-1>0$ . This is the paper's consequence of the first-order condition (A.25).
Without accelerability and with $A\beta\eta>1$ , every UC optimum satisfies $u'(R)\lambda-1=0$ (in particular it is interior).

Significance

The statement pins down when the textbook under-investment effect of financing frictions holds: exactly when extra spending scales the prize but cannot speed it up. The paper contrasts it with the possibility of over-investment on accelerable projects (Corollary 1's second statement, supported by numerical exercises). Taken together, the two statements show that the R&D technology, not only the severity of the constraint, decides the direction of the distortion.

The result is proved in the paper (Appendix A.4); it has no machine-checked proof. A formal proof certifies the comparison for every pair of optima, without the paper's tacit assumption that optima are unique. It also makes explicit the interior-optimum condition $A\beta\eta>1$ under which the inequality is strict. The resulting facts about maximizers of products of a concave power-law profit and a decreasing survival factor are reusable for other real-options models with a survival discount.

Difficulty

The first idea is to compare the two first-order conditions. The UC optimum solves $u'\lambda=1$ , and at an interior FC optimum the derivative of the survival factor pushes $u'\lambda-1$ to be positive. Concavity of $f(R)=u(R)\lambda-R$ then orders the two. Turning this into a theorem about sets of maximizers needs more. The FC optimum can sit at a corner, either $R=1$ or the right end $\min\{\bar R,X\}$ , where no first-order condition holds, and the corners must be ruled out or handled separately. The survival factor $1-(X/R)^\alpha$ vanishes at $R=X$ . The UC value vanishes at $\bar R$ . When $X\le R^*_{uc}$ , the comparison is settled by the range rather than by the first-order condition. The strict inequality is false without an interior UC optimum: if $A\beta\eta\le1$ , both optimal sets equal $\{1\}$ .

Formalization scope

All objects are in the namespace AccelScal.FCMonopoly, in one definition file. It holds the parameter structure Tech $(A,\beta,\eta,\gamma)$ , the predicate Standing, $u$ , $\lambda$ , $\bar R$ , $\alpha$ , $V_{uc}$ (5), $V_{fc}$ (6), and the maximizer sets RstarUC, RstarFC over the ranges (7). Powers are Real.rpow, and $u'$ is Mathlib's deriv.

Committed conventions:

The reduced problems are the definitions. The FC firm's original problem (3) is an expectation over a geometric Brownian motion and its first-passage time below $R$ . That its value is (6) is the paper's Lemma 1 (Appendix A.12), which needs first-passage machinery absent from Mathlib, and it is not posed. The mission takes (6), and for symmetry (5), as the definitions of the two firms' problems, exactly as the paper's proof of Corollary 1 does. $V_{fc}$ is "the value of problem (3)" only through Lemma 1.
The random payoff is replaced by its mean $u(R)$ , and the AIP term of (3)/(4), which does not depend on $R$ , is dropped.
Standing assumptions: (2), plus the added condition $A\eta>1$ (investment takes place, so $V_{uc}(1)>0$ ). The goal adds $A\beta\eta>1$ , which is necessary for the strict inequality (the UC optimum is interior), and $X\ge1$ , which keeps the FC range nonempty. " $\lambda'=0$ , $u'>0$ " is encoded as $\gamma=0$ , $\beta>0$ , which is equivalent under (2). No sign condition on $\mu$ is imposed, and $\sigma>0$ .
The paper's single-valued $R^*$ is read as a set of maximizers. The inequality is claimed for every pair of optima.

Trivializing formalizations are ruled out. $R^*_{uc}$ is never defined by its closed form, and neither optimum is a selected value. The goal asserts that both optimal sets are nonempty. The FC range depends on $X$ through $\min\{\bar R,X\}$ . The conclusion is the strict " $<$ ", not " $\le$ ".

The paper's second and third statements of Corollary 1 (over-investment when $\lambda'>0$ , and when it is "more likely") are numerical or informal and are not posed. Contributions are welcome on both milestones and on the goal. Also welcome: general lemmas on the maximizers of a positive concave function times a decreasing positive factor, and a future formalization of Lemma 1 (6) from a geometric Brownian first-passage Laplace transform.

Selected references

D. Lin, Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition, Management Science, Articles in Advance, 2022. https://doi.org/10.1287/mnsc.2022.4503
S. C. Myers, Determinants of Corporate Borrowing, Journal of Financial Economics 5(2), 147–175, 1977. https://doi.org/10.1016/0304-405X(77)90015-0

4 thms2 active usersReviewed

Operations Research

Missions

Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations I: The Rationally Inattentive Decision-Maker's Optimal Choice Probability in Closed FormResearch Paper

Motivation

Setting

Formalization targets

Optimal choice probability

Significance

Difficulty

Formalization scope

Selected references

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 3: The Price of Anarchy Is Locally Lipschitz at Games with Constant Costs or Strictly Increasing C¹ CostsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 1: The Price of Anarchy Is Hölder Continuous with Exponent 1/2 at Every Game with Costs Lipschitz on [0, T(d)]Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9 (p. 26)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 4: The Price of Anarchy Is Not Uniformly Hölder Continuous and No Game Has the Whole Space as a Hölder NeighborhoodResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8b)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 5: For Small Total Demand the Price of Anarchy Exceeds 1 by at Most an Explicit Multiple of the Total DemandResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 5.1 (p. 43)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 2: The Social Optimum Cost, the Wardrop Equilibrium Cost and the Price of Anarchy Are Continuous on the Game SpaceResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 4: For Every τ ∈ (0, 1) Some τ-Bounded Instance Gives No Value-Ordered Policy More Than (β^τ_k + ε) Times the OptimumResearch Paper

Why offer sets with overbooking matter

Setting

Formalization targets

Goal: Theorem 4 (p. 30)

Milestones on the hard instance (App. D.7)

Companions: the maximisers (App. D.8)

Significance

Difficulty

Formalization scope

Selected references

Designing Approximately Optimal Search on Matching Platforms 2: Every Set of Assortments Has a Unique Profile of Thresholds Equal to Expected UtilitiesResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1, item 1 (fixed-point form)

Milestones

Significance

Difficulty

Formalization scope

Selected references