All missions

Motivation

A Nash equilibrium is a feasible choice of strategies at which no player can lower her own cost by changing her strategy alone. A Pareto minimizer is a feasible point that cannot be improved under a specified comparison of vector outcomes. These ideas usually select different points: a change that helps several players at once is relevant to ordinary Pareto comparison, while Nash stability holds the other players' strategies fixed. Feinstein and Rudloff ask whether a suitable vector comparison can recover all equilibria, including when the equilibrium set has several points or is empty. Their answer for games with one shared feasibility constraint is Theorem 2.6 of the pinned preprint. The result addresses the full equilibrium set rather than the existence or computation of a single point.

The paper places this characterization alongside vector optimization methods that can compute solution sets for some structured games. It also extends the framework to generalized Nash games and vector-valued costs. This mission concentrates on the shared-constraint, scalar-cost statement on which those later sections build. The formal target is a known theorem from the paper, not a claim that the game always has an equilibrium or that a particular numerical algorithm finds one.

Setting

Let $I$ be a finite set of at least two players. Player $i$ chooses a strategy in a real linear space $\mathcal X_i$; the spaces may differ. A joint strategy $x$ is a member of $\prod_{i\in I}\mathcal X_i$. Player $i$ has an arbitrary real-valued cost function $f_i$ on joint strategies. A set $\mathbb X\subseteq\prod_i\mathcal X_i$ specifies the shared constraint: only joint strategies in $\mathbb X$ are feasible. No continuity, convexity, boundedness, or nonemptiness condition is imposed on the costs or on $\mathbb X$.

For a joint strategy $x^*$, write $(x_i,x^*_{-i})$ for the strategy obtained by replacing only player $i$'s coordinate. The set $\mathrm{NE}(f,\mathbb X)$ consists of feasible $x^*$ such that every feasible replacement obeys $f_i(x^*)\le f_i(x_i,x^*_{-i})$. The feasibility condition applies to the whole replacement; it cannot be replaced by membership of $x_i$ in a coordinate projection of $\mathbb X$. This is Definition 2.2 in the source.

For a vector space $Z$ and a cone $K\subseteq Z$, define $a\le_K b$ when $b-a\in K$. For a domain $D$, feasible set $A\subseteq D$, and objective $g:D\to Z$, the paper calls $x^*$ a $K$-minimizer if it is feasible and every feasible $x$ satisfying $g(x)\le_K g(x^*)$ also satisfies $g(x^*)\le_K g(x)$. This permits equivalent outcomes and does not require a convex cone. The mission restricts comparisons to feasible points, matching Definition 2.3.

The objective for the game is $g(x)=(x,f(x))$, where $f(x)=(f_i(x))_{i\in I}$. Its target space is $\bigl(\prod_i\mathcal X_i\bigr)\times\mathbb R^I$. For each player $i$, the cone $C_i$ permits any change in strategy coordinate $i$ and in the other players' cost coordinates, requires zero change in every other strategy coordinate, and requires a nonnegative change in cost coordinate $i$. The paper's ordering cone is $C=\{(u,v):\exists i,\ u_j=0\text{ for }j\ne i,\ v_i\ge0\}$. Equation (7) gives $C_i$ as an explicit product; equation (6) gives $C$ directly. The resulting relation compares costs only while other players' strategies remain fixed.

Formalization targets

Player-cone structure

The paper states that $C=\bigcup_{i\in I}C_i$ and that each $C_i$ is a convex cone. It then characterizes comparisons by $C_i$ and $C$ in terms of fixed strategy coordinates and a player's cost. These are the first two milestones, from §2.2, pages 6–7 of the preprint.

Minimizer decomposition

Lemma 2.7 is the third milestone:

$$C\text{-argmin}\{(x,f(x)):x\in\mathbb X\} =\bigcap_{i\in I} C_i\text{-argmin}\{(x,f(x)):x\in\mathbb X\}.$$

Main equality

The goal is Theorem 2.6, an equality of complete solution sets:

$$\mathrm{NE}(f,\mathbb X) = C\text{-argmin}\{(x,f(x)):x\in\mathbb X\}.$$

The equality covers an empty equilibrium set as well as games with one, several, or infinitely many equilibria. It asserts neither existence nor uniqueness.

Significance

The theorem gives a vector optimization description of every stable joint strategy in a shared-constraint game. Because the objective retains the strategy vector, the cone can express which coordinates remain fixed during a unilateral deviation. The decomposition into player cones also identifies separate convex comparisons inside a potentially nonconvex overall preference. In settings where suitable vector optimization methods are available, the paper uses this characterization as a route toward finding full equilibrium sets; it does not claim a universal exact algorithm for arbitrary games §1 and §2.2.

Formalization adds a reusable generic cone-induced relation and vector-minimizer definition, plus a shared-constraint game interface that later results can import. It pins down the direction of comparison, the feasible deviation set, and the product-coordinate constraints in the cones. The source proves the goal and its supporting statements on paper. The local Prove2Me prior-art search found no published machine-checked statement with this exact shared-constraint model and cone; the mission asks solvers to supply proofs of the drafted statements.

Difficulty

Applying the ordinary coordinatewise order to the cost vector $f(x)$ compares outcomes from arbitrary simultaneous changes of strategy. It therefore does not encode the unilateral test in the Nash definition. Including the strategy vector in the objective and using $C$ makes the relevant changes comparable, but $C$ is a union of player cones and need not be convex. A proof must respect the paper's minimizer definition for this relation and establish the set equality in both directions. Restricting the theorem to smooth or convex games would miss the generality of Theorem 2.6.

Formalization scope

Lean represents $I$ by a finite type $\iota$ with decidable equality and states $2\le|I|$, the paper's standing convention. Each $\mathcal X_i$ is a possibly different type carrying an additive commutative group and a real module structure. Joint strategies are dependent functions $\forall i,\mathcal X_i$; feasible deviations use Function.update. The shared constraint is an arbitrary set of joint strategies, and each cost is an arbitrary real-valued function. An empty feasible set remains permitted. The objective space is the product of joint strategies with real cost profiles, and $C_i$ is built as the product of the coordinate sets in equation (7). The condition $x_{-i}=0$ in equation (6) means that every coordinate other than $i$ equals its vector-space zero.

The generic vector-minimizer definition, the Nash equilibrium definition, and the two cones are independent. In particular, Nash equilibrium is defined directly by unilateral feasible deviations; $C$ is defined directly by the existential condition in (6); and vector minimization is generic in its cone, objective, and feasible domain. This rules out a definition that makes the main equality true by construction. The $|I|\ge2$ hypothesis is copied from the paper, although these particular equalities also hold with fewer players. Contributions to the cone comparison lemmas, the minimizer decomposition, and the full set equality are welcome. Later generalized Nash and vector-valued results, numerical examples, and Corollary 2.8 lie outside this mission.

Selected references

• Zachary Feinstein and Birgit Rudloff, Characterizing and Computing the Set of Nash Equilibria via Vector Optimization, arXiv:2109.14932v5, 2022; published as an Operations Research technical note, 2024. Pinned preprint

Why compare a clustering SDP with an oracle?

Clustering methods must infer a partition from noisy observations, while the quality of a partition is usually judged against labels that the method cannot see. Fei and Chen study a balanced sub-Gaussian mixture model in which a semidefinite program (SDP) estimates a cluster matrix from pairwise distances. Their Theorem 1 relates its error to a simpler integer program allowed to know the true cluster centers. This comparison makes the SDP's error interpretable through an explicit benchmark, even when exact recovery is unavailable. The paper also investigates semi-random perturbations, but this mission targets the Model 1 comparison on which that broader discussion builds.

The tension is that an SDP solution may be fractional. Its entries express pairwise affinities, whereas an assignment matrix places each point in exactly one cluster. The result bounds the fractional matrix's entrywise error by an integer assignment error without assuming that the SDP solution itself is integral. That is the hidden-integrality claim relevant to this mission.

The model and the two optimization problems

There are $n\ge4$ observations in $\mathbb R^d$ and $k\ge2$ clusters. The true label of point $i$ is $\sigma^*(i)\in[k]$, and every cluster contains exactly $\ell=n/k$ points. For unknown centers $\mu_1,\ldots,\mu_k$, the observations have the form

$$h_i=\mu_{\sigma^*(i)}+g_i.$$

The noise vectors $g_i$ are independent, measurable, zero-mean, and sub-Gaussian. Their vector sub-Gaussian norms are at most $\tau>0$. The minimum center separation and signal-to-noise ratio are

$$\Delta=\min_{a\ne b}\|\mu_a-\mu_b\|_2,\qquad s=\Delta/\tau.$$

The SDP uses the squared-distance matrix $A_{ij}=\|h_i-h_j\|_2^2$. It minimizes $\langle Y,A\rangle=\sum_{i,j}Y_{ij}A_{ij}$ over real $n\times n$ matrices with row sums $n/k$, diagonal entries one, nonnegative entries, and symmetric positive semidefiniteness. Write $\widehat Y$ for any optimum. The true cluster matrix is $Y^*_{ij}=1$ when $\sigma^*(i)=\sigma^*(j)$ and $0$ otherwise. Its error is measured by the entrywise norm $\|\widehat Y-Y^*\|_1=\sum_{i,j}|\widehat Y_{ij}-Y^*_{ij}|$.

The benchmark is an Oracle Integer Program. An assignment matrix $F\in\mathcal F$ has zero-one entries and exactly one one in each row. The true assignment is $F^*_{ja}=\mathbf1\{\sigma^*(j)=a\}$. The oracle sees the centers and augmented observations $\bar h_j=\mu_{\sigma^*(j)}+(2\kappa)^{-1}g_j$ with the fixed $\kappa=1/8$, so its noise is four times the realized noise in $h_j$. It minimizes

$$\eta(F)=\sum_{j,a}\|\bar h_j-\mu_a\|_2^2F_{ja}.$$

The Oracle error is the largest $\tfrac12\|F-F^*\|_1$ among assignments satisfying $\eta(F)\le\eta(F^*)$. The Oracle feasible set has no balance constraint. In contrast, the SDP retains the row-sum constraint inherited from balanced clustering.

Formalization targets

Main goal: Theorem 1

The goal is the paper's quantitative comparison. It asserts that universal constants $C_s>0$ and $C\ge1$ exist such that, when

$$s^2\ge C_s\left(\sqrt{\frac{kd}{n}\log n}+\frac{kd}{n}+k\right),$$

an event of probability at least $1-n^{-C}-2e^{-n}$ has, for every realized SDP optimum $\widehat Y$, the bound

$$\frac{\|\widehat Y-Y^*\|_1}{\|Y^*\|_1} \le 2\max_{\substack{F\in\mathcal F\\\eta(F)\le\eta(F^*)}} \frac{\|F-F^*\|_1}{\|F^*\|_1}.$$

The constants are independent of $n,k,d$, the centers, the labels, and the noise law. The event and the SDP optimum are chosen after the random observations are realized. The theorem fixes the factor two and the failure-probability expression exactly as printed.

Milestone results

The eight milestones follow the statements in Section 5: the six structural properties of the SDP error matrix (Fact 2), the basic inequality (16), the signal estimate (Proposition 3), the two noise estimates (Propositions 1 and 2), the representation of the remaining term (Lemma 1), the identity between the integer program and Oracle error (Lemma 2), and the final deterministic bound. Each milestone keeps the paper's constants and its own hypotheses. Together they expose the interfaces needed to close Theorem 1.

What the comparison gives

Theorem 1 transfers a question about a real matrix optimum to a finite assignment benchmark. The Oracle benchmark can itself be bounded under additional assumptions, as Fei and Chen do in their separate Theorem 2. The present target preserves the comparison even in regimes where the benchmark does not vanish. It therefore expresses an error guarantee rather than an exact-recovery assertion.

A complete Lean proof would connect a probability model, finite-dimensional semidefinite feasibility, and the paper's integer assignment comparison. At present these mission statements are draft proof obligations: compiling a statement with sorry checks its formulation but does not prove the result. The development reuses published definitions of scalar and vector sub-Gaussian norms; proving the new lemmas and the main theorem remains open within this mission.

Where the difficulty lies

SDP optimality gives an inequality for the squared-distance objective, but it does not directly bound the entrywise difference from $Y^*$. Noise enters that objective through both a Gram matrix and mixed center-noise terms. A direct entrywise comparison also ignores the row-sum and positive-semidefinite structure that constrains the SDP error.

On the benchmark side, replacing a fractional matrix error by an arbitrary rounded assignment would not retain the stated factor. The paper identifies an intermediate linear program whose value can be controlled at integer cardinalities. Formalizing the result requires preserving that cardinality constraint, the exact coefficient $\kappa=1/8$, and the distinction between the observed points and the oracle's augmented points.

Formalization scope

Points, clusters, and coordinates use finite index types; Lean indices start at zero while the paper's $[n]$ and $[k]$ start at one. All matrices are real. The trace inner product is represented by a double sum, the matrix $\ell_1$ norm is entrywise, and the spectral norm in Proposition 2 uses the $L^2$ operator norm. The minimum separation ranges over distinct center pairs, which is nonempty when $k\ge2$. Oracle maxima are finite, nonempty, bounded sets; the true assignment is a feasible candidate. The normalized denominators are nonzero under $n\ge4$ and $k\ge2$ with balanced labels.

The random model uses one probability space and the same noise realization in both $h$ and $\bar h$. Measurability, zero mean, independence, and the extended-nonnegative vector sub-Gaussian norm bound are explicit. High-probability conclusions use measurable events and quantify over every optimum at each realized data set. Deterministic milestones take a fixed realization and do not add a probability space. The universal constants occur before all model parameters. These choices rule out a vacuous instance-dependent SNR constant, a norm that assigns zero to heavy-tailed noise, and an SDP optimum chosen before observing the noise.

The scope is Theorem 1 and its selected Section 5 statements. Theorem 2's separate Oracle-error rate, the rounding algorithm, semi-random Model 2, and the stochastic-ball special case are outside this proposal. Reusable work includes the SDP and assignment interfaces, matrix-error identities, and finite integer-program comparisons. Contributions that prove the eight source milestones or establish their supporting concentration and finite-dimensional optimization results are welcome.

Selected references

• Y. Fei and Y. Chen, Hidden Integrality and Semi-Random Robustness of SDP Relaxation for Sub-Gaussian Mixture Model, Mathematics of Operations Research, 2022. arXiv:1803.06510v2, the version and pagination used here.

Why SRPT in many-server queues with abandonment

Shortest remaining processing time first (SRPT) is the scheduling rule that always works on the jobs closest to completion. For a single server it minimizes the number of jobs in the system at every time, on every sample path (Schrage 1968). Service systems with many parallel servers and customers who leave when they wait too long, such as call centers, hospital wards and cloud platforms, are a different setting. There an overloaded system must turn customers away somehow, and the scheduling rule decides who. How SRPT behaves in such systems had resisted analysis: the state of the queue is a vector of remaining service and patience times of unbounded dimension, and preemptions couple all customers together.

Dong and Ibrahim (2021) analyze SRPT in the $M/GI/s+GI$ queue in the overloaded many-server regime. They show that SRPT asymptotically behaves like a two-class priority system with a sharp threshold $\tau$ on the service time. Short jobs are served with vanishing delay, long jobs almost all abandon, and the resulting waiting-time measures depend on the patience distribution only through its mean. Under first-come-first-served, by contrast, performance depends on the whole patience distribution (Whitt 2006).

Setting

Customers arrive according to a Poisson process of rate $\lambda$ to $s$ identical servers. Customer $n$ brings a service time $S_n$ and a patience time $T_n$. The $S_n$ are i.i.d. with a continuous law $\nu_S$, density $g$, cdf $G$ and mean $1/\mu$; the $T_n$ are i.i.d. with a continuous law $\nu_T$ and mean $1/\theta$. Arrivals, services and patience times are mutually independent.

A schedule says which customers occupy the servers at each time. From it one reads off each customer's remaining processing time $R_n(t)$ and cumulative time in queue $Q_n(t)$. Customer $n$ abandons when $Q_n(t)$ reaches $T_n$. Her patience clock keeps running across preemptions and is not reset. Under SRPT, at every time the servers are busy whenever customers are waiting, and every customer in service has remaining work no larger than that of any waiting customer. Customer $n$ is served ($\mathrm{Serv}$) if she completes service and abandons ($\mathrm{Ab}$) otherwise. Her waiting time $W_n$ is the total time she is present but not in service.

The traffic intensity is $\rho = \lambda/(s\mu)$. The paper fixes $\rho > 1$ and lets $\lambda$ and $s$ grow together, with $s = \lambda/(\rho\mu)$. The threshold $\tau$ is defined by equation (1),

$$\lambda\,\mathbb E[S\,\mathbf 1(S \le \tau)] = s, \qquad\text{equivalently}\qquad \mathbb E[S\,\mathbf 1(S\le\tau)] = \frac{1}{\rho\mu},$$

so the work brought by jobs shorter than $\tau$ exactly matches capacity. Class 1 consists of the customers with $S \le \tau$ and class 2 of those with $S > \tau$.

The analysis couples the SRPT queue with a loss system $L$. This system has the same customers and $s$ servers but no waiting room. Class 1 customers preempt class 2 customers, and a class 1 customer who finds all servers busy with class 1 work is lost. Its class 1 throughput is $\mathrm{Th}_{L,1}$.

Formalization targets

Goal: Theorem 2 (p. 10)

As $s \to \infty$, under SRPT and for a tagged customer $c$ in steady state:

$$\text{(a)}\quad P(\mathrm{Serv}_c \mid S_c\le\tau)\to 1,\qquad P(\mathrm{Serv}_c\mid S_c>\tau)\to 0;$$ $$\text{(b)}\quad \mathbb E[W_c\mid\mathrm{Serv}_c]\to 0,\qquad \mathbb E[W_c\mid S_c\le\tau]\to 0;$$ $$\text{(c)}\quad \mathbb E[W_c\mid\mathrm{Ab}_c]\to 1/\theta,\qquad \mathbb E[W_c\mid S_c>\tau]\to 1/\theta;$$ $$\text{(d)}\quad \mathbb E[W_c]\to \frac{1-G(\tau)}{\theta}.$$

The goal states all four parts. The constants $1$, $0$, $1/\theta$ and $(1-G(\tau))/\theta$ are those of the paper.

Milestones

Proposition 1 (p. 8) is the coupling inequality $\mathrm{Th}_{L,1}\le\mathrm{Th}_O$, where $\mathrm{Th}_O$ is the throughput of the SRPT queue. The capacity constraint (5) (p. 16) says that work is completed at rate at most $s$. Two steps in the proof of Lemma 4 (p. 17) concern Erlang's loss formula. The first is the identity $E(r,C) = \bigl(\int_0^\infty(1+t/r)^C e^{-t}dt\bigr)^{-1}$. The second is the limit $E(s,s)\to 0$. Lemma 4 (p. 16) gives $\mathrm{Th}^\lambda_{L,1}/\lambda\to G(\tau)$. Problem (7) (p. 18) is a linear program over service-probability profiles. Lemma 5 (p. 17) says the limiting service probability is $\bar\gamma(x) = \mathbf 1\{x\le\tau\}$; the mission states the analytic step that concludes its proof (p. 18), not Lemma 5 itself. Theorem 2(a) is the goal's first part.

Significance

Theorem 2 is a state-space collapse: an infinite-dimensional preemptive system becomes, in the limit, a two-class priority rule with an explicit threshold. Several consequences follow from it. SRPT asymptotically minimizes the waiting time of served customers and maximizes that of abandoning ones (Corollary 1). It also asymptotically maximizes throughput among all disciplines (Proposition 3). Its performance measures are insensitive to the patience law beyond its mean.

The paper proves Theorem 2 on paper. To our knowledge none of it is machine-checked. The mission asks for a formal model of a multi-server preemptive queue with abandonment and a formal proof of the coupling. It also asks for the Erlang-formula asymptotics and the variational step that pins down $\bar\gamma$. Two parts of the published argument need care in a formal proof. The proof of (b) switches to patience laws with $f(0)>0$, while the statement is for general patience laws. The proof of Lemma 5 presupposes that $\bar\gamma = \lim \gamma^\lambda$ exists. A complete development must close both points or replace them with arguments that avoid them.

Difficulty

The SRPT queue has no finite-dimensional Markov description. Preemptions mean that the order in which customers are served is not their arrival order, and a preempted customer's patience keeps running. Standard fluid or diffusion limits for many-server queues track the number of customers, or a measure-valued state under first-come-first-served, and SRPT fits neither. The coupling with the loss system avoids this, but proving it requires a matching argument along the sample path that survives every preemption. Converting throughput bounds into statements about conditional waiting times then requires control of steady-state quantities that the model does not provide in closed form.

Formalization scope

The model is a single definitions file in the namespace SRPTManyServer.Collapse, with these conventions.

• Sample paths. A path lists arrival, service and patience times $(A_n, S_n, T_n)_{n\ge 0}$. It is admissible if arrivals are strictly increasing from time $\ge 0$ and tend to infinity, and if $S_n, T_n > 0$; this holds almost surely.
• Schedules. A schedule is a measurable $\{0,1\}$-valued $\delta_n(t)$. SRPT is the relational predicate "only present customers are served; $\min(s, \#\text{present})$ are in service; those in service have remaining work no larger than any waiting customer". Ties are broken arbitrarily. The page describes preemption at arrivals, and the predicate also fixes who takes a freed server.
• The loss system. It is defined by recursion over arrivals.
• The probability model. The seeds are i.i.d. $\mathrm{Exp}(1)$ variables $E_n$, and system $s$ has arrivals $A_n = (E_0+\dots+E_n)/(\rho\mu s)$. All systems share the service and patience times. The sequence is indexed by $s\in\mathbb N$ in place of $\lambda$.
• Standing assumptions. Both laws are carried by $[0,\infty)$ and have densities. The means are $1/\mu$ and $1/\theta$, $\rho>1$, and $\tau$ satisfies (1).
• Steady state. Steady-state tagged-customer quantities are read as almost-sure customer long-run averages, for example the fraction served among customers $0,\dots,N-1$ with $S_n\le\tau$ as $N\to\infty$. Their existence for each $s$ is a hypothesis, standing for the paper's assumption of a steady state. The theorems are about these limits as $s\to\infty$.
• Pathwise and analytic forms. Proposition 1 is stated for one deterministic admissible path and every SRPT schedule of it. The capacity constraint (5) is stated pathwise: completed work by time $t$ is at most $s t$. Lemma 5 itself is not stated; the final step of its proof is, analytically and $g$-almost everywhere: if $\int g\bar\gamma \ge G(\tau)$ and $\int xg\bar\gamma \le \mathbb E[S\mathbf 1\{S\le\tau\}]$, then $\bar\gamma = \mathbf 1\{\cdot\le\tau\}$ a.e. where $g>0$. Problem (7) is an IsLeast statement over measurable $\gamma$.

The discipline in the goal is SRPT on the actual arrival stream. It is not the two-class priority system, the threshold $\tau$ does not appear in the scheduling predicate, and the throughputs and service probabilities are not free parameters: a statement in which they were would reduce the goal to Lemma 5. The non-idling clause is part of the SRPT predicate, so the empty schedule does not qualify.

A complete development needs a sample-path theory of preemptive multi-server queues with abandonment. It also needs renewal or regenerative arguments that connect time averages with customer averages, and the insensitivity of the $M/G/s/s$ blocking probability, which the paper cites from the literature and does not prove. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The Erlang identities, problem (7) and the final step of the proof of Lemma 5 are self-contained analysis.

Not formalized here: Corollary 1, Proposition 3 (Appendix B), inequality (4), and the numerical comparisons of §4.

Selected references

• J. Dong and R. Ibrahim, On the SRPT scheduling discipline in many-server queues with impatient customers, arXiv:2102.05789v1, 2021 (published in Management Science). https://arxiv.org/abs/2102.05789
• L. Schrage, A proof of the optimality of the shortest remaining processing time discipline, Operations Research 16(3), 687–690, 1968. https://doi.org/10.1287/opre.16.3.687
• W. Whitt, Fluid models for multiserver queues with abandonments, Operations Research 54(1), 37–54, 2006. https://doi.org/10.1287/opre.1050.0227
• O. Garnett, A. Mandelbaum and M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4(3), 208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753

Motivation

Firms that advertise online choose whom to target from the customer data they hold, and the industry's working assumption is that more granular data can only help: a firm that knows more about each consumer can at worst ignore the extra information. Despotakis and Yu (SSRN 3900394; Management Science, 2022, doi:10.1287/mnsc.2022.4604) show that this fails once consumers draw inferences from being targeted. A consumer who receives an ad learns something about how well the product suits her, and she decides whether to spend effort clicking on that basis. When the firm uses more dimensions of data, the set of consumers it targets changes shape, and the signal that being targeted conveys becomes weaker. In equilibrium the firm can then earn strictly less with more data than with less.

The result belongs to a line of work on targeted advertising as a signal, and on the value of customer data to a firm whose actions consumers observe and interpret. It is a commitment problem: the firm would like to promise to use less information, but cannot.

Setting

A unit mass of consumers is interested in a product sold at an exogenous price $p\in(0,1)$. A consumer's utility from the product is

$$u=\omega\alpha+(1-\omega)\beta,$$

where $\alpha,\beta\in[0,1]$ are her matching values on two components of the product and $\omega\in[0,1]$ is her private weight on the first. The three are independent and uniform on $[0,1]$. The consumer does not know $\alpha$ and $\beta$ until she clicks.

The firm sends ads at unit ad cost $c_{ad}>0$. Under single-dimensional (sd) targeting it observes $\alpha$ and chooses a targeting set $\Sigma\subseteq[0,1]$; under multidimensional (md) targeting it observes $(\alpha,\beta)$ and chooses $\Sigma\subseteq[0,1]^2$.

A targeted consumer does not see $\Sigma$ but expects a set $\widetilde\Sigma$. Her posterior is uniform: under sd targeting $\alpha$ is uniform on $\widetilde\Sigma$ and $\beta$ uniform on $[0,1]$; under md targeting $(\alpha,\beta)$ is uniform on $\widetilde\Sigma$. She clicks at click cost $c_{click}>0$ if and only if her posterior expected surplus $E[\max\{u-p,0\};\widetilde\Sigma]$ is at least $c_{click}$; the weights that click form the click set $\Omega(\widetilde\Sigma)\subseteq[0,1]$. After clicking she learns $u$ and buys if and only if $u\ge p$.

Against a click set $\Omega$, the ad value of a consumer is $p$ times the probability that she clicks and buys, minus $c_{ad}$; under md targeting $\pi^{md}(\alpha,\beta;\Omega)=p\,|\{\omega\in\Omega:\omega\alpha+(1-\omega)\beta\ge p\}|-c_{ad}$. The firm's profit from targeting $T$ is the integral of the ad value over $T$.

A non-trivial equilibrium is a targeting set $\Sigma$ of positive measure that maximizes the firm's profit over all targeting sets, against the click set $\Omega(\Sigma)$ that consumers who correctly expect $\Sigma$ produce. An md equilibrium is symmetric if $\Sigma$ is symmetric about the 45-degree line. $\Pi^{*sd}$ and $\Pi^{*md}$ denote equilibrium profits. Two thresholds from the paper enter the statements: the click-cost threshold $c^{max}_{click}(c_{ad},p)$ of Equation (7), above which no non-trivial symmetric md equilibrium exists, and the ad-cost threshold $\overline{c_{ad}}(c_{click},p)$ from the proof of Proposition 1.

Formalization targets

Goal: Proposition 3

For every $p\in(0,1)$ there is $\delta>0$ such that for every $c_{ad}\in(0,\delta)$ there is $c_1<c^{max}_{click}(c_{ad},p)$ such that for every $c_{click}\in(c_1,c^{max}_{click}(c_{ad},p)]$ both a non-trivial sd equilibrium and a non-trivial symmetric md equilibrium exist, and

$$\Pi^{*md}<\Pi^{*sd}$$

for every such pair. The goal fixes neither $\delta$ nor $c_1$; the right end of the click-cost interval is the explicit threshold of Equation (7).

Milestones

1. Lemmas 1 and 3: the click set is $[0,1]$ minus an interval, $[0,\underline\omega]\cup[\overline\omega,1]$, in both environments; for a symmetric md strategy it is symmetric about $\omega=1/2$.
2. Claim 3 (first case): against $\Omega=[0,\underline\omega]\cup[\overline\omega,1]$ with $c_{ad}\le p\underline\omega$ and $c_{ad}\le p(1-\overline\omega)$, the md best response is the set bounded by two lines through $(p,p)$ with slopes $\gamma_1^*=-c_{ad}/(p-c_{ad})$ and $\gamma_2^*=1/\gamma_1^*$.
3. Proposition 1 (for $(1-p)^2/2<c_{click}<(1-p)/2$): a unique non-trivial sd equilibrium $[\bar\alpha^*,1]$.
4. Proposition 2 (for $c_{ad}<\min\{p^2,p(1-p)\}$): a unique non-trivial symmetric md equilibrium if and only if $c_{click}\le c^{max}_{click}(c_{ad},p)$.
5. Lemma 4: the sd equilibrium profit decreases in $c_{click}$ on $((1-p)^2/2,(1-p)/2)$ and is $0$ at $(1-p)/2$.
6. Lemma 5: near $c^{max}_{click}$ the symmetric md profit tends to $0$ as $c_{ad}\to0$.
7. Lemma 6: $(1-p)^2/2<c^{max}_{click}(c_{ad},p)<(1-p)/2$ for $c_{ad}<\min\{p^2,p(1-p)\}$.

Significance

The result is a clean counterexample to the monotonicity of the value of information for a firm whose actions are observed by strategic receivers. It isolates a mechanism, inference from being targeted, that does not need competition, price discrimination or privacy costs to make extra data harmful. The paper uses it to explain why firms might coarsen the data they act on, and §5 revisits the comparison with endogenous pricing and with consumers who do not know which dimension the firm targets on.

On the platform this mission is the first model of targeting with consumer inference. The model layer, uniform posteriors on an expected targeting set, click sets defined by posterior expected surplus, and equilibria defined as fixed points over arbitrary measurable targeting sets, is reusable for other signalling-through-targeting results. The result is proved on paper, with Lemmas 4 and 5 argued in sketch form; to our knowledge no part of it has a machine-checked proof.

Difficulty

Both equilibria are fixed points: the firm's best response depends on the click set, and the click set depends on the expected targeting set through a posterior average. The md firm may choose any measurable subset of the square, so the reduction to the two-line class $\mathcal S$ of Equation (6) is part of the work, and Proposition 2 asks for uniqueness among all symmetric measurable equilibria, not only within $\mathcal S$.

The comparison itself is not a monotonicity argument. As $c_{click}$ approaches $c^{max}_{click}$, the md click set shrinks to the threshold where the md equilibrium disappears, while the sd profit stays positive only because $c^{max}_{click}$ lies strictly below $(1-p)/2$, where the sd profit vanishes. Making this precise requires the piecewise closed forms of the expected surplus (with logarithms) and control of both profits uniformly as $c_{ad}\to0$, which the page leaves implicit. Comparing the closed forms at a single numerical point does not give the statement for every price.

Formalization scope

All quantities are real numbers. Consumer populations are Lebesgue measure on $[0,1]$ and $[0,1]^2$, so probabilities are lengths and areas. Targeting sets are measurable subsets of the unit interval or square, "non-trivial" means positive measure, "symmetric" means invariance under $(\alpha,\beta)\mapsto(\beta,\alpha)$, and "unique" means unique up to a null set. The tie-breaks follow the page: buy at $u=p$, click at equality, and indifference is allowed in the firm's optimization. Click thresholds are arbitrary reals, so an empty click set is expressible.

Equilibria are defined as fixed points, never by the paper's closed forms $[\bar\alpha^*,1]$ and $\Sigma^{md}(\gamma_1^*,1/\gamma_1^*)$; otherwise Propositions 1 and 2 would be definitional and the goal a comparison of two formulas. The paper's $c^{min}_{click}$ is defined as the least click cost at which $\Pi^{*sd}\ge\Pi^{*md}$, which would make a literal statement nearly true by definition; the goal therefore asserts the existence of the region instead, and it includes existence of both equilibria so that the comparison is not vacuous.

Added or restricted hypotheses: Propositions 1 and 2 are stated only in the regimes Proposition 3 uses; Proposition 1 uses $c_{ad}<\overline{c_{ad}}$ strictly (at equality the cutoff is $1$ and the targeting set is null); Lemma 4 adds $c_{ad}<p(1-p)$; Lemma 5 is stated in $\varepsilon$–$\delta$ form because its limit is not shown to exist; and the price is $p\in(0,1)$ throughout.

A complete development needs set integrals and product measures from Mathlib, convexity of the expected surplus in $\omega$, and real analysis of the piecewise closed forms. Proofs of any milestone, and alternative arguments for Lemmas 4 and 5, are welcome.

Selected references

• S. Despotakis and J. Yu, Multidimensional Targeting and Consumer Response, SSRN working paper 3900394 (version of October 11, 2022). https://ssrn.com/abstract=3900394
• S. Despotakis and J. Yu, Multidimensional Targeting and Consumer Response, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4604

Motivation

Interior-point methods solve a conic optimization problem by following the minimizers of a barrier function for the cone. Their iteration count is governed by the barrier's parameter $\nu$: the best known algorithms need $O(\sqrt\nu\log(1/\varepsilon))$ iterations to reach accuracy $\varepsilon$ (Nesterov and Todd, 1997). A cone can be used natively by a solver only once a logarithmically homogeneous self-concordant barrier (LHSCB) with a small parameter is known for it, together with efficient oracles for its derivatives.

Coey, Kapelevich and Vielma (arXiv:2103.04104v2; Mathematics of Operations Research, 2022) study cones defined by spectral functions on Euclidean Jordan algebras. This framework covers vectors, real symmetric matrices and complex Hermitian matrices at once. The paper implements the resulting cones in the solver Hypatia. One of its two new barrier results concerns the root-determinant cone, the hypograph of the geometric mean of the eigenvalues. For symmetric matrices this is the hypograph of $\det(W)^{1/d}$ over the positive semidefinite cone, a standard modelling device for D-optimal experimental design and for determinant maximization. Before this paper, the usual way to represent it was an extended formulation with auxiliary variables and a semidefinite constraint.

Setting

A Jordan algebra is a real vector space $V$ with a bilinear product $\circ$ that is commutative and satisfies the Jordan identity $w_a\circ(w_a^2\circ w_b)=w_a^2\circ(w_a\circ w_b)$, where $w^2:=w\circ w$. It has a multiplicative identity $e$. It is Euclidean if $\langle w_a\circ w_b,w_c\rangle=\langle w_b,w_a\circ w_c\rangle$. An idempotent is a $c$ with $c^2=c$. It is primitive if it is non-zero and is not the sum of two orthogonal non-zero idempotents. A Jordan frame is a family $c_1,\dots,c_d$ of pairwise orthogonal primitive idempotents summing to $e$. Every Jordan frame of $V$ has the same size $d$, the rank of $V$.

Every $w\in V$ has a spectral decomposition $w=\sum_{i\in[\![d]\!]}w_ic_i$ over a Jordan frame, with real eigenvalues $w_1,\dots,w_d$. From these, $\det(w)=\prod_iw_i$, $\operatorname{tr}(w)=\sum_iw_i$, and a real function $f$ acts by $f(w)=\sum_if(w_i)c_i$. The inner product is the trace form $\langle w_a,w_b\rangle=\operatorname{tr}(w_a\circ w_b)$. The cone of squares is $\mathcal Q=\{w\circ w:w\in V\}$; $w\succ0$ means $w\in\operatorname{int}(\mathcal Q)$. The quadratic representation is $P(w)=2L(w)^2-L(w^2)$, where $L(w)v=w\circ v$.

The root-determinant is $\varphi(w)=\det(w)^{1/d}$ on $\mathcal Q$. With $\mathcal E=\mathbb R\times\mathcal Q$ and $\zeta(u,w)=\varphi(w)-u$, the root-determinant cone and its candidate barrier are

$$\mathcal K_{\mathrm{rtdet}}=\{(u,w)\in\mathbb R\times\mathcal Q:\ u\le\det(w)^{1/d}\},\qquad \Gamma(u,w)=-\log\zeta(u,w)-\log\det(w).$$

A function $\Gamma$ is a $\nu$-LHSCB for a cone $\mathcal K$ if it is $C^3$ and convex on $\operatorname{int}(\mathcal K)$ and tends to $+\infty$ at the boundary. It must also satisfy $\Gamma(\theta\tilde u)=\Gamma(\tilde u)-\nu\log\theta$ and $|\nabla^3\Gamma(\tilde u)[\tilde p,\tilde p,\tilde p]|\le2(\nabla^2\Gamma(\tilde u)[\tilde p,\tilde p])^{3/2}$, and the parameter satisfies $\nu\ge1$.

Formalization targets

Goal: Proposition 7.1 (p. 24)

$$\mathcal K_{\mathrm{rtdet}}\ \text{is a proper cone, and}\ \ \Gamma\ \text{is a}\ (1+d)\text{-LHSCB for}\ \mathcal K_{\mathrm{rtdet}}.$$

The goal holds for every finite-dimensional Euclidean Jordan algebra of rank $d\ge1$, not for one matrix algebra.

Milestones, in proof order

1. $\mathcal K_{\mathrm{rtdet}}$ is proper (p. 23).
2. $\Psi(u,w)=-\log\det(w)$ is a $d$-LHSCB for $\mathcal E$ (p. 24).
3. $\varphi$ is nonnegative, concave and homogeneous on $\mathcal Q$ ((96), p. 23).
4. $\zeta$ is concave and $C^3$ on $\operatorname{int}(\mathcal E)$ (p. 24).
5. The derivative identities, with $\hat r=P(w^{-1/2})r$, $\sigma$ the eigenvalues of $\hat r$, $m_1=d^{-1}\sum_i\sigma_i$ and $\delta_i=\sigma_i-m_1$:

$$\nabla^2\Psi(\tilde u)[\tilde p,\tilde p]=\operatorname{tr}(\hat r^2)=\|\sigma\|^2,\quad \nabla^2\varphi(w)[r,r]=-d^{-1}\varphi\textstyle\sum_i\delta_i^2,\quad \nabla^3\varphi(w)[r,r,r]=d^{-1}\varphi\sum_i\delta_i^2(m_1+2\sigma_i),$$

which are (105), (107) and (108). 6. The scalar inequality (109c): $\ d^{-1}\varphi\sum_i\delta_i^2(\|\sigma\|-m_1+2(\|\sigma\|-\sigma_i))\ge0$ for every $\sigma\in\mathbb R^d$. 7. The compatibility inequality (103) on $\operatorname{int}(\mathcal K_{\mathrm{rtdet}})$:

$$\nabla^3\zeta(\tilde u)[\tilde p,\tilde p,\tilde p]\le-3\big(\nabla^2\Psi(\tilde u)[\tilde p,\tilde p]\big)^{1/2}\nabla^2\zeta(\tilde u)[\tilde p,\tilde p].$$

8. The reduction: if $\Psi$ is a $d$-LHSCB, $\zeta$ is $C^3$ and concave, and (103) holds, then $\Gamma$ is a $(1+d)$-LHSCB. This is the paper's application of Nesterov–Nemirovskii Proposition 5.1.7.

Significance

The result gives the root-determinant cone a barrier whose parameter $1+d$ is one more than the optimal parameter $d$ of its domain $\mathbb R\times\mathcal Q$, so it cannot be improved by more than one (p. 24). It also removes the extended formulation: a solver works with the cone in its natural dimension. The paper pairs the barrier with closed-form oracles for the gradient, Hessian product and inverse Hessian product (§7.4, Lemma 7.1), and reports computational gains in Hypatia. Because the statement is uniform over Euclidean Jordan algebras, it covers the vector, real symmetric and complex Hermitian cases at once.

The result is proved in the paper; this mission formalizes it. To the best of the curators' knowledge, it has no machine-checked proof, and Lean's Mathlib has no theory of Euclidean Jordan algebras, spectral decompositions in them, or barrier functions for their cones. Formalizing Proposition 7.1 therefore also yields a reusable layer: the Jordan-algebraic setting, the cone of squares, the quadratic representation, and an LHSCB predicate on arbitrary normed spaces.

Difficulty

The obvious route checks self-concordance of $\Gamma$ directly. That requires bounding the third derivative of $-\log(\det(w)^{1/d}-u)-\log\det(w)$ by the $3/2$-power of its Hessian in every direction. The two logarithmic terms interact, and no simple direct estimate is available. The paper instead uses a compatibility criterion of Nesterov and Nemirovskii, which reduces the barrier property to the single inequality (103) between derivatives of $\zeta$ and $\Psi$. In Lean that criterion is not available and must be established for this cone; it is the deepest milestone.

The derivative identities (105), (107) and (108) require differential calculus of spectral functions on a Jordan algebra: derivatives of $\det$, of $w\mapsto w^{-1}$, and of $P(w^{-1/2})$, expressed through the eigenvalues of the scaled direction $\hat r$. Deriving them from the structure axioms needs, among other things, the fact that the eigenvalues of $\theta w$ and $w^2$ are those of $w$ scaled and squared, uniqueness of the spectral decomposition, and positivity of the eigenvalues on $\operatorname{int}(\mathcal Q)$. Only the final scalar inequality (109c) is elementary.

Formalization scope

$V$ is a real finite-dimensional inner product space carrying a structure EJA V d. The structure bundles the Jordan product (bilinear, commutative, Jordan identity), the unit $e$ and the Euclidean property. It also bundles, for every $w$, eigenvalues and a Jordan frame of primitive idempotents with $w=\sum_iw_ic_i$, and the identity $\langle a,b\rangle=\operatorname{tr}(a\circ b)$. The spectral theorem (Faraut–Korányi III.1.2) says such data exist for every Euclidean Jordan algebra of rank $d$, so this is the paper's setting. Primitivity forces $d$ to be the rank: without it, a frame could be padded with zeros and $\det$ would change.

The ambient space is $\mathbb R\times V$. Directional derivatives are iterated Fréchet derivatives on the diagonal, and "boundary" is the topological frontier. The barrier limit is taken within the interior at every frontier point.

The following conventions are fixed:

• the rank satisfies $d\ge1$, since the paper divides by $d$ and the goal is false at $d=0$;
• self-concordance includes convexity, as in Nesterov–Nemirovskii Definition 2.1.1;
• logarithmic homogeneity (38) is required for $\tilde u\in\operatorname{int}(\mathcal K)$ and $\theta>0$;
• $\|\sigma\|$ is the Euclidean norm;
• $(\cdot)^{1/2}$ in (103) is the real square root;
• (105) is stated in squared form;
• $\varphi$, $\zeta$, $\Gamma$, $\Psi$ and $\hat r$ are total functions that are only evaluated on the relevant interiors.

Properness is a separate predicate from LHSCB, because $\mathcal E$ is not pointed.

A trivializing formalization is ruled out by these choices. Specializing $V$ to $\mathbb R^d$ or $\mathbb S^d$, dropping primitivity, allowing $d=0$, dropping convexity, or imposing the barrier limit at only some boundary points would each prove a different, weaker or vacuous statement.

Proposition 6.1 (the $(2+d)$-LHSCB for the matrix monotone derivative cones) and Lemma 7.1 (the inverse Hessian oracle) are deliberately absent. The first needs matrix monotonicity and Löwner's integral representation and is independent of Proposition 7.1. The second is an oracle formula that the goal does not use.

Contributions are welcome at every level: the scalar inequality (109c); the cone and homogeneity facts; the spectral calculus behind (105)–(108); and the compatibility reduction. The Jordan-algebraic infrastructure and the LHSCB predicate are reusable beyond this mission.

Selected references

• C. Coey, L. Kapelevich, J. P. Vielma, Conic optimization with spectral functions on Euclidean Jordan algebras, Mathematics of Operations Research, 2022. https://arxiv.org/abs/2103.04104v2
• Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• J. Faraut, A. Korányi, Analysis on Symmetric Cones, Oxford University Press, 1994 (cited in the paper as Faraut and Koranyi, 1998).
• Y. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1), 1997. https://doi.org/10.1287/moor.22.1.1

Motivation

Whether more competition among banks makes the financial system safer or more fragile is a long-running question in banking theory and regulation. The competition-fragility view holds that competition erodes bank margins and charter values and so encourages risk-taking; the competition-stability view, formalized by Boyd and De Nicolò (2005), holds that competition lowers loan rates, which reduces the incentive of borrowers to choose risky projects. Empirical studies of deregulation episodes, such as the removal of interstate branching restrictions in the United States, have found evidence for both views.

Dam and Sengupta (2024) point out that such episodes do not merely add competitors to a single market: they integrate previously separate markets with different customer compositions. In their model integration changes both the number of competing banks and the ratio of borrowers to depositors each bank faces, and the second channel can reverse the conventional prediction in one of the integrating markets. This mission formalizes that result, Proposition 2 of the paper, together with the equilibrium characterizations it rests on.

Setting

There are two banking markets $j=1,2$. Market $j$ has $a_j>0$ depositors, $b_j>0$ borrowers (entrepreneurs) and $n\ge1$ banks, and $\lambda>1$ is a model constant. A borrower chooses the risk $\theta\in[0,\lambda]$ of a unit-size project, which returns $\theta$ with probability $1-\theta/\lambda$ and $0$ otherwise. At loan rate $r$ the borrower maximizes $(1-\theta/\lambda)(\theta-r)$; a maximizer is a borrower-optimal risk.

Inverse deposit supply and inverse loan demand in market $j$ are $R_j=D_j/a_j$ and $r_j=\lambda-L_j/b_j$, where $D_j$ and $L_j$ are aggregate deposits and loans. Banks are financed by deposits only, so $D_j=L_j$. Each bank $i$ chooses a loan volume $L_{ij}\ge0$ to maximize its expected profit, display (2),

$$\frac{L_j}{2\lambda b_j}\Big(\lambda-\frac{L_j}{b_j}-\frac{L_j}{a_j}\Big)L_{ij},\qquad L_j=\sum_i L_{ij}.$$

A Cournot equilibrium is a profile of volumes from which no bank gains by changing its own volume. The segmented market equilibrium (SME) of market $j$ is the Cournot equilibrium of this game; its loan rate is $r_j$ and its borrower-optimal risk $\theta_j$.

The integrated market has $a_1+a_2$ depositors, $b_1+b_2$ borrowers and $2n$ banks, with profit (7) of the same form. Its Cournot equilibrium is the integrated market equilibrium (IME), with loan rate $r^*$ and risk $\theta^*$. The customer composition of a market is the ratio of borrowers to depositors, $\xi_j=b_j/a_j$ and $\xi^*=(b_1+b_2)/(a_1+a_2)$. Market 2 is labelled as the borrower-heavy one, $\xi_1<\xi_2$.

The comparison is organized by the two terms of display (11):

$$C=-\lambda\cdot\frac{1}{1+\xi^*}\Big(\frac{2n+1}{2n+2}-\frac{n+1}{n+2}\Big),\qquad B_j=\lambda\cdot\frac{n+1}{n+2}\Big(\frac{1}{1+\xi_j}-\frac{1}{1+\xi^*}\Big),$$

the bank-competitor effect (more banks) and the bank-customer effect with respect to market $j$ (a different customer composition).

Formalization targets

Goal: Proposition 2

If $\xi_1<\xi_2$, then for all Cournot equilibria of the three markets and all borrower-optimal risks at their loan rates,

$$\text{(a)}\quad r^*<r_2,\ \ \theta^*<\theta_2;\qquad \text{(b-i)}\quad B_1<-C\ \Rightarrow\ r^*<r_1,\ \theta^*<\theta_1;\qquad \text{(b-ii)}\quad B_1>-C\ \Rightarrow\ r^*>r_1,\ \theta^*>\theta_1 .$$

Milestones

1. Equation (1): the borrower-optimal risk is unique and equals $\theta(r)=(\lambda+r)/2$.
2. Lemma 6(a): with marginal cost $c$ the Cournot game has a unique equilibrium, symmetric, with deposit rate, loan rate and risk (A.4)–(A.6).
3. Lemma 1: the SME, with (3)–(5).
4. Lemma 2: the IME, with (8)–(10), and $\xi_1<\xi^*<\xi_2$.
5. Display (11): $r^*-r_j=C+B_j$ for $j=1,2$.
6. The bank-competitor effect is negative, $C<0$.
7. The bank-customer effects have opposite signs, $B_2<0<B_1$.

Significance

Proposition 2 shows that a single deregulation episode can lower loan rates and borrower risk-taking in one integrating market while raising them in the other, even though the number of competing banks doubles. Its consequence for empirical work is that the competition-fragility and competition-stability views can both be consistent with the same episode, depending on each market's initial customer composition; it also separates within-market competition (captured by $C$, which reproduces the classical Boyd–De Nicolò prediction) from across-market competition. Corollary 1 and the bank-merger analysis of §3 build on the same equilibria.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The formal work this mission adds is the Cournot layer: the paper's proof of Lemma 6 argues only through the first-order condition, whereas the formal statements require that the closed-form profile is a global best response for every bank and that no other equilibrium, symmetric or not, exists.

Difficulty

The algebra of (11) and of the sign comparisons is elementary once the equilibrium rates are known. The substantive step is the equilibrium characterization. A bank's profit is a cubic in its own volume, so the first-order condition is necessary only at an interior choice and is not sufficient. A complete argument must rule out corner equilibria in which some banks lend nothing, show that every equilibrium is symmetric, and show that the stationary point is a global maximum over all nonnegative volumes. The integrated market has $2n$ banks indexed by Fin (2 * n), so the cast from $2n$ to the real number $2n$ enters every closed form.

Formalization scope

All quantities are real numbers, the number of banks is a natural number, and banks are indexed by Fin n (segmented) and Fin (2 * n) (integrated). A Cournot equilibrium is the published feasible pure-strategy Nash equilibrium CarbonDoubleCount.Planner.IsPureNash, with feasible set $[0,\infty)$ for each bank and payoff given by display (2)/(7). The loan and deposit rates are functions of the aggregate equilibrium volume. A borrower-optimal risk is a maximizer of $(1-\theta/\lambda)(\theta-r)$ over $[0,\lambda]$; it is never defined by a closed form. The standing assumptions $\lambda>1$, $a_j,b_j>0$, $n\ge1$ of p. 6 are bundled in one predicate, and $\xi_1<\xi_2$ is a separate hypothesis.

Added or chosen conventions: the volumes are nonnegative; equation (1) is stated for $-\lambda\le r\le\lambda$; Lemma 6(a) assumes $c<\lambda$ and is stated for $m\ge1$ banks (the appendix prints $n\ge2$, while Lemma 1 needs $n\ge1$); "sufficiently weak/strong" in Proposition 2 is the strict comparison of $B_1$ with $-C$, and the tie $B_1=-C$ is not covered, as on the page.

A trivializing formalization would define $r_j$, $r^*$, $\theta_j$, $\theta^*$ by the closed forms (4), (5), (9), (10), which reduces the goal to arithmetic; the goal instead quantifies over all Cournot equilibria and all borrower-optimal risks, and the weak/strong conditions are stated through the defined effect terms, not through $r^*$ and $r_1$. All hypotheses are satisfiable: the parameters $\lambda=3/2$, $n=3$, $a_1=a_2=4$, $b_1=1$, $b_2=6/5$ satisfy the premise of (b-i), and $\lambda=2$, $n=1$, $a_1=a_2=1$, $b_1=1$, $b_2=2$ that of (b-ii).

Contributions welcome: proofs of the milestones, in particular a reusable characterization of symmetric Cournot equilibria for cubic profits of this form, which also covers the merger analysis of §3.

Selected references

• K. Dam and R. Sengupta, Bank competition and risk-taking under market integration, Management Science, 2024 (doi:10.1287/mnsc.2022.03495); cited here from Federal Reserve Bank of Kansas City Research Working Paper RWP 20-21, updated October 2024. https://doi.org/10.18651/RWP2020-21
• J. H. Boyd and G. De Nicolò, The theory of bank risk taking and competition revisited, Journal of Finance 60(3), 2005. https://doi.org/10.1111/j.1540-6261.2005.00763.x
• J. E. Stiglitz and A. Weiss, Credit rationing in markets with imperfect information, American Economic Review 71(3), 1981. https://www.jstor.org/stable/1802787
• F. Allen and D. Gale, Competition and financial stability, Journal of Money, Credit and Banking 36(3), 2004. https://doi.org/10.1353/mcb.2004.0038

Motivation

Many assets, such as corporate and municipal bonds, securitized products and new issues, trade over the counter: there is no central exchange, and an asset reaches its final buyers through a sequence of bilateral trades between dealers. Empirical work on these markets documents intermediation chains, in which a block of securities passes through several dealers, each of whom keeps part of it for her own customers and sells the rest onwards: in US municipal bonds, Li and Schürhoff (2019) find that chains account for 82% of the trades that start with a customer selling to a dealer, and in registered securitizations Hollifield, Neklyudov and Spatt (2017) find that about 27% of customer sales give rise to a sequence involving more than one dealer (figures as reported by Colliard and Demange, p. 1). Colliard and Demange (SSRN 3244321, forthcoming in Management Science) build a model of this process in which the length of the chain, the prices and the quantities are all equilibrium outcomes, and the friction that makes the chain finite is asymmetric information about how much each dealer's customers want to buy.

The equilibrium of that model rests on one object, the collected demand $\Omega$, defined by a functional equation. This mission formalizes the existence and properties of $\Omega$ and the theorem that the strategies built from it form an equilibrium of the dealer game.

Setting

An asset pays a sure return $\rho>0$ per unit. Dealers $D_1,D_2,\dots$ arrive in sequence. Each is available to trade with probability $q\in(0,1)$, independently. Dealer $D_n$'s customers buy up to $v^C_n$ units at price $\rho$; the customer demand $\omega_n=\rho v^C_n$ is private information of $D_n$ and is drawn i.i.d. from a distribution $G$ on $\mathbb R_+$ with finite mean. Write $H(\omega)=\Pr(\tilde\omega\ge\omega)$. $G$ may have atoms. Dealers borrow cash at the funding spread $r>0$.

A dealer of type $\omega$ who accepts a take-it-or-leave-it offer $(p,v)$ (volume $v$ at unit price $p$) sells to her customers and has financing needs $y=\max(pv-\omega,0)$, which she covers by borrowing or by making a new offer $(p_n,v_n)$ to the next dealer, with $0\le v_n\le v$. If the next dealer accepts with probability $\Phi(p_n,v_n)$, her expected profit (5) is

$$\pi=(\rho-p)v-ry+q\,\Phi(p_n,v_n)\bigl[r\min(p_nv_n,y)-(\rho-p_n)v_n\bigr].$$

A rank-free equilibrium (Definition 1) is a strategy (an acceptance rule $A(p,v,\omega)$ and a new-offer rule $(P,V)$) that does not depend on the dealer's position in the chain, such that $\Phi$ is the acceptance probability induced by $A$, the new offer maximizes $\pi$ over all feasible offers, and a dealer accepts exactly when this maximal profit is non-negative.

The collected demand is the function $\Omega$ on $\mathbb R_+$ solving

$$\Omega(0)=0,\qquad \Omega(y)=\sup_{0\le\omega\le y} qH(\omega)\bigl(\omega+\Omega(y-\omega)\bigr)\quad(y>0).\tag{9}$$

The maximizers form the set $\mathcal T(y)$ of targeted values (10); a selection is a function $T$ with $T(y)\in\mathcal T(y)$ for all $y\ge0$.

Formalization targets

Goal: Theorem 2

For $\Omega$ bounded, continuous and solving (9), and any selection $T$, put $\pi^*(p,v,y)=(\rho-p)v-ry+r\Omega(y)$. The strategy "accept $(p,v)$ iff $\pi^*(p,v,y)\ge0$; on acceptance with $y>0$ offer $(P(y),V(y))$ with

$$P(y)V(y)=y,\qquad (\rho-P(y))V(y)-ry+r\bigl(T(y)+\Omega(y-T(y))\bigr)=0\tag{14}$$

(and no offer when $y=0$)" is a rank-free equilibrium. Moreover $P(y)\le\rho$, $0\le V(y)\le v-\omega/\rho$, the offer's expected transaction payoff is $r\Omega(y)$, and the dealer's profit is $\pi^*(p,v,y)$.

Milestones

1. $\Psi(\beta)(y)=\max_{0\le\omega\le y}qH(\omega)(\omega+\beta(y-\omega))$ maps bounded continuous non-negative $\beta$ with $\beta(0)=0$ to such functions and is a $q$-contraction in sup-norm (proof of Theorem 1).
2. Theorem 1: a unique bounded continuous solution of (9) exists; the supremum in (9) is reached; $\Omega$ is $q$-Lipschitz and non-decreasing; hence $\Omega(z)\le qz$ and $z\mapsto z-\Omega(z)$ is non-negative and increasing.
3. Lemma A.2: for $f$ non-decreasing and $q$-Lipschitz on $\mathbb R_+$, $\min(pv,y)+f(pv-\omega)\le pv+f(y-\omega)$ whenever $\omega\le pv$, $\omega\le y$.
4. The three points of the proof of Theorem 2: the offer is feasible; no offer yields a transaction payoff above $r\Omega(y)$; the offer $(P(y),V(y))$ is accepted exactly by types $\omega\ge T(y)$ and achieves $r\Omega(y)$.

Significance

Theorem 2 is the existence result on which the rest of the paper is built. The comparative statics of dissemination length, customer purchases and prices along the chain (Propositions 1–4, Implications 1–6) are all statements about this equilibrium. It shows that the infinite-horizon screening problem of each dealer, against a chain of unknown length, reduces to the one-dimensional equation (9), and that the reduction is exact: the expected transaction payoff from the new offer is $r\Omega(y)$.

The paper proves Theorem 2 in Appendix A; Lemma A.2 is proved in an Online Appendix that is not part of the source. To the knowledge of this mission, none of these results has a machine-checked proof. The mission's output is a checked existence-and-optimality argument for a dynamic screening game with a discontinuous survival function, together with the fixed-point theory of the operator $\Psi$, which is not an expectation operator and does not fall under standard Bellman-operator results.

Difficulty

The operator $\Psi$ takes a supremum over the moving interval $[0,y]$ of a product with the survival function $H$, which jumps downward at every atom of $G$. Standard dynamic-programming theorems assume a continuous kernel or a finite state space; here attainment of the supremum and continuity of $\Psi(\beta)$ rely on $H$ being left-continuous and non-increasing, and on $\omega+\beta(y-\omega)\ge0$. In the equilibrium part, the natural first step, verifying optimality only against the strategy's own offer or against offers accepted with a fixed probability, does not work: a deviation changes the set of types that accept it, so the acceptance probability must be recomputed from the acceptance rule for every candidate offer. The deviation can change both its unit margin and its probability of acceptance, making a uniform payoff bound the central difficulty.

Formalization scope

All objects live in the namespace DealerDissem.RankFree, in one definitions file. Parameters $\rho,r,q$ are bundled with $\rho>0$, $r>0$, $0<q<1$. $G$ is a Measure ℝ that is a probability measure, gives no mass to $(-\infty,0)$ and has an integrable identity; $H(\omega)$ is the measure of $[\omega,\infty)$ (closed, so acceptance probabilities are exact at atoms). $\Omega$, $T$, $P$, $V$ are functions ℝ → ℝ; every hypothesis and conclusion about them is restricted to $[0,\infty)$, and uniqueness in Theorem 1 is equality on $[0,\infty)$. Suprema in (9) and (46) range over $0\le\omega\le y$. Acceptance rules are predicates $A(p,v,\omega)$, and $\Phi$ is computed as the $G$-measure of the acceptance set. $V(y)$ is (14) solved for $V$ (the paper's (16)), and $P(y)=y/V(y)$; at $y=0$, $V=0$ and Lean's value $P(0)=0/0=0$ is irrelevant.

Definition 1 (ii) is encoded as: after acceptance the strategy's offer is feasible and maximizes (5) over every feasible offer; and acceptance holds iff some feasible offer gives a non-negative profit. The equilibrium predicate requires measurable acceptance events for feasible offers, so the quantity called a probability in Definition 1 (i) has that meaning. Added hypotheses, each where the printed sentence is false otherwise: $v>0$ in "this case surely occurs for $p>\rho$"; $y>0$ for the bound $0\le V(y)\le v-\omega/\rho$; non-negative $\beta$ in the contraction milestone.

A trivializing formalization is ruled out: $\Phi$ is never a free parameter, optimality is against all feasible offers rather than the strategy's own, $\Omega$ must solve (9) at every $y>0$, and $T(y)$ must be a maximizer, not merely a point of $[0,y]$.

A complete development needs suprema over compact intervals of upper semicontinuous functions, the Banach fixed-point theorem on bounded continuous functions on $\mathbb R_+$, and Markov's inequality for $\omega H(\omega)\le\mathbb E\tilde\omega$. The fixed-point machinery for sup-over-interval operators is reusable for other sequential search and screening models. Proofs of any milestone are welcome, as is a proof of Theorem 2 from the milestones.

Selected references

• J.-E. Colliard and G. Demange, Asset Dissemination through Dealer Markets, Management Science (forthcoming; authors' version of September 17, 2020), SSRN 3244321. https://ssrn.com/abstract=3244321 — published version: https://doi.org/10.1287/mnsc.2020.3779
• D. Li and N. Schürhoff, Dealer Networks, The Journal of Finance 74(1), 91–144, 2019. https://doi.org/10.1111/jofi.12728
• B. Hollifield, A. Neklyudov and C. Spatt, Bid-Ask Spreads, Trading Networks, and the Pricing of Securitizations, The Review of Financial Studies 30(9), 2017. https://doi.org/10.1093/rfs/hhx027
• N. L. Stokey and R. E. Lucas, with E. C. Prescott, Recursive Methods in Economic Dynamics, Harvard University Press, 1989 (Theorem 3.3, Blackwell's sufficient conditions). https://www.hup.harvard.edu/books/9780674750968