Probability

Motivation

Social services such as public housing, food banks and free clinics are congested: the users who arrive wait in a queue they cannot see, and some of them could do almost as well elsewhere. A provider who sees the queue can decide what to tell arriving users about it. Telling low-need users that the queue is long sends them to their outside option and shortens the wait for everyone else; telling them too much may send away users the provider would rather serve. Information design (Bayesian persuasion, Kamenica and Gentzkow 2011) studies what a sender who commits to a signaling rule in advance can achieve.

Anunrojwong, Iyer and Manshadi (2023) build on the queueing persuasion model of Lingenbrink and Iyer (2019) and ask how much welfare information design can add in a congested service. Their answer depends on whether users are heterogeneous. This mission formalizes the homogeneous case, Proposition 1: when every user is low-need, the simplest policy, full disclosure of the queue length, is already within an explicit factor of the best signaling mechanism.

Setting

A single server with exponential service times of rate one serves users first come, first served. Low-need users (type L) arrive as a Poisson process of rate $\lambda_L > 0$ and may leave for an outside option worth $0$; high-need users (type H, rate $\lambda_H \ge 0$) always join. The total rate is $\lambda = \lambda_L + \lambda_H \le 1$. A type-$i$ user who joins with $n$ users present receives utility $u_i(n)$, where $u_i(0) > 0$, $u_i$ is strictly decreasing, $u_i(k) < 0$ for large $k$, and the increments $u_L(n) - u_L(n+1)$ are non-increasing (Assumption 1).

By Lemma 1 of the paper, an obedient signaling mechanism is described by the stationary distribution $\pi$ of the queue length on $\mathbb N_0$ it induces. The admission policies $\Pi_{AP}$ are the probability distributions with

$$\lambda_H \pi_n \le \pi_{n+1} \le \lambda \pi_n \qquad (n \ge 0),$$

and the signaling mechanisms $\Pi_{SM}$ are those that also satisfy the obedience constraints

$$J(\pi) = \sum_{n\ge0}(\pi_{n+1} - \lambda_H\pi_n)\,u_L(n) \ge 0, \qquad L(\pi) = \sum_{n\ge0}(\lambda\pi_n - \pi_{n+1})\,u_L(n) \le 0 .$$

The welfare of low-need users is $W_L(\pi) = J(\pi)$.

A threshold policy $\pi_x$ with $x = m + a$, $m \in \mathbb N_0$, $a \in [0,1)$, admits L-users below queue length $m$, admits them with probability $a$ at $m$, and turns them away above $m$. $W_L(x)$ denotes $W_L(\pi_x)$. The full-information threshold $m_{fi}$ is the least $k$ with $u_L(k) < 0$, and the full-information mechanism is $\mathrm{fi} = \pi_{m_{fi}}$. The homogeneous setting is $\lambda_H = 0$.

Formalization targets

Goal: Proposition 1 (p. 16)

In the homogeneous setting, with

$$\beta_{fi} = \frac{\sum_{n=0}^{m_{fi}-1}\lambda_L^n}{\sum_{n=0}^{m_{fi}}\lambda_L^n},$$

the goal asserts three facts:

1. every signaling mechanism $\pi \in \Pi_{SM}$ satisfies $W_L(\mathrm{fi}) \ge \beta_{fi}\, W_L(\pi)$;
2. $\beta_{fi} \ge 1 - 1/(m_{fi}+1)$;
3. full information maximizes $W_L$ over $\Pi_{SM}$ if and only if $W_L(m_{fi}) \ge W_L(m_{fi}-1)$.

The paper phrases parts 1 and 3 for "the optimal signaling mechanism sm". They are stated here for every element of $\Pi_{SM}$, which implies the paper's form for any maximizer and requires no existence result.

Milestones

• Lemma 3 (p. 36), the detailed-balance sandwich $\lambda_H^{k-q}\pi_q \le \pi_k \le \lambda^{k-q}\pi_q$.
• Theorem 1 (p. 14): every Pareto-efficient signaling mechanism has a threshold structure with threshold at most $m_{fi}$.
• Lemma 5(2) (p. 37): $W_L(x)$ is monotone between consecutive integers and unimodal on $\mathbb R_+$.
• From the proof of Proposition 1 (p. 40):
  • full information is a feasible signaling mechanism with $W_L(\mathrm{fi}) > 0$;
  • every obedient threshold is at least $m_{fi}-1$;
  • $\beta_{fi}\,W_L(m_{fi}-1) \le W_L(\mathrm{fi})$;
  • $\beta_{fi} \ge 1 - 1/(m_{fi}+1)$ for all $\lambda_L \le 1$.

Significance

Proposition 1 bounds what persuasion can do when users are alike. The ratio $1/\beta_{fi}$ is at most $1 + 1/m_{fi}$, so the gain from optimal signaling is small whenever full information already admits a few users. The paper contrasts this with the heterogeneous setting (§4.2), where information design can Pareto-improve on full information substantially. The homogeneous bound is the baseline for that comparison: it shows that the gains there come from the presence of two types, not from pooling queue states.

The result is proved in the paper. Nothing in this model has been machine-checked so far. A formal proof would check the reduction from an arbitrary signaling mechanism to a threshold mechanism (Theorem 1), the unimodality of threshold welfare (Lemma 5(2)), and the obedience calculation on p. 40. It would also confirm that these hold at $\lambda_L = 1$, where the stationary distribution of the always-join policy no longer exists. The model layer defined here is shared with three sibling missions on Theorems 1 and 6 and Proposition 3 of the same paper.

Difficulty

The two finite inequalities, the bound on $\beta_{fi}$ and the comparison of $W_L(m_{fi}-1)$ with $W_L(\mathrm{fi})$, are elementary. The difficulty lies in part 1 for an arbitrary $\pi \in \Pi_{SM}$, which is a distribution on an infinite state space. Restricting attention to threshold policies is not free: Theorem 1 only says that Pareto-efficient mechanisms are thresholds. An arbitrary obedient $\pi$ must either be shown to be dominated by a threshold mechanism, or bounded directly. The sets $\Pi_{SM}$ are not compact in the obvious topology at $\lambda_L = 1$, so the existence of an optimal mechanism cannot simply be assumed.

Part 3 needs a strict comparison. When $W_L(m_{fi}-1) > W_L(m_{fi})$, the proof must exhibit an obedient threshold policy strictly better than full information, which requires the obedience constraint to hold for thresholds slightly below $m_{fi}$.

Formalization scope

Lean represents queue lengths as ℕ and distributions as functions ℕ → ℝ, inside the namespace NeedPersuasion.Homog. Every statement carries the standing assumptions M.Standing: $\lambda_L > 0$, $\lambda_H \ge 0$, $\lambda \le 1$, $u_i(0) > 0$, $u_i(k) < 0$ for some $k$, $u_i$ strictly decreasing, and $u_L(n) - u_L(n+1)$ non-increasing. The homogeneous statements add $\lambda_H = 0$. The type-H utility $u_H$ stays a field of the model so that the definitions coincide with those of the sibling missions; with $\lambda_H = 0$ it does not enter $W_L$.

Conventions the formalization commits to:

• Membership in $\Pi_{AP}$ includes summability of $\pi_n u_L(n)$ and $\pi_n u_H(n)$. The paper treats welfare as finite, and Lean's infinite sum of a non-summable series is $0$.
• $W_L$ is the series $\sum_n (\pi_{n+1} - \lambda_H\pi_n) u_L(n)$, not the form of (2) that divides by $\lambda_L\pi_n$.
• The threshold policy $\pi_x$ is defined by its unnormalized weights and normalized by their sum. $W_L(\mathrm{fi})$ and $W_L(x)$ are computed from these distributions, never from a closed-form expression.
• $\lambda_L \le 1$ is allowed, as on the page; no $\lambda < 1$ is assumed.

The following trivializations are excluded: defining "sm" as $\mathrm{fi}$, defining it through sSup of an unbounded set or Classical.choose, computing $W_L(\mathrm{fi})$ from Lemma 5's closed form, or stating part 3 with both sides about the same threshold. A sorry-free sanity check exhibits a model satisfying all hypotheses ($\lambda_L = 1/2$, $u_L(k) = 1 - 3(k+1)/10$, $m_{fi} = 3$, $\beta_{fi} = 14/15$) with $\mathrm{fi} \in \Pi_{SM}$.

A complete development needs:

• finite geometric sums and ratios of affine functions, which are in Mathlib;
• monotonicity of ratios of affine functions;
• summation arguments for distributions on ℕ.

The perturbation arguments behind Theorem 1 and the lemmas about threshold policies are reusable in the sibling missions. Proofs of any milestone are welcome. So are intermediate lemmas, such as closed forms for $W_L(x)$ and $L(x)$ of a threshold policy in the homogeneous case.

Selected references

• J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; read as arXiv:2005.07253v3 (2022). https://arxiv.org/abs/2005.07253
• B. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5), 2019. https://doi.org/10.1287/opre.2019.1856
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200

Motivation

Social services such as public health clinics, legal aid offices and food banks are congested: users wait in a queue whose length they cannot see. Some users have no alternative (high need) and others have an outside option (low need). A provider cannot price access, but can decide what to tell arriving users about the queue. Anunrojwong, Iyer and Manshadi (Management Science, 2023; read as arXiv:2005.07253v3) study how far such information design can raise the welfare of both groups. Their model builds on the obedient signaling framework of Lingenbrink and Iyer (Operations Research 67(5), 2019). This mission formalizes their Section 5. It compares the best signaling mechanism with the first-best: the admission policy a provider would choose if it could see user types and order users to join or leave.

Setting

A single server with exponential service times of rate one serves an unobservable first-come-first-served queue. High-need users (type H) arrive at Poisson rate $\lambda_H\ge0$ and always join. Low-need users (type L) arrive at rate $\lambda_L>0$ and either join or take an outside option worth $0$. Write $\lambda=\lambda_L+\lambda_H\le1$. A type-$i$ user who joins behind $n$ users gets utility $u_i(n)$. The standing assumptions are $u_i(0)>0$, $\lim_k u_i(k)<0$, each $u_i$ strictly decreasing, and the increments $u_L(n)-u_L(n+1)$ non-increasing (Assumption 1).

An admission policy is a distribution $\pi$ on $\mathbb N_0$ with

$$\lambda_H\pi_n\le\pi_{n+1}\le\lambda\pi_n\qquad(n\ge0);$$

their set is $\Pi_{AP}$. It is the steady state of a queue in which a low-need user arriving at length $n$ is admitted with probability $(\pi_{n+1}-\lambda_H\pi_n)/(\lambda_L\pi_n)$. A signaling mechanism is an admission policy that low-need users obey when it is announced as a join/leave recommendation. The obedience constraints are

$$J(\pi)=\sum_n(\pi_{n+1}-\lambda_H\pi_n)u_L(n)\ge0,\qquad L(\pi)=\sum_n(\lambda\pi_n-\pi_{n+1})u_L(n)\le0,$$

and the signaling mechanisms form $\Pi_{SM}\subseteq\Pi_{AP}$. The welfares are $W_L(\pi)=J(\pi)$ and $W_H(\pi)=\lambda_H\sum_n\pi_nu_H(n)$. For a weight $\theta\in[0,1]$, $W(\pi,\theta)=\theta W_L(\pi)+(1-\theta)W_H(\pi)$. Then $\mathrm{sm}(\theta)$ is the set of maximizers of $W(\cdot,\theta)$ over $\Pi_{SM}$, and $\mathrm{ap}(\theta)$ the set of maximizers over $\Pi_{AP}$. Under no information (ni) every low-need user joins with the same equilibrium probability $p^{ni}$. Finally,

$$g(x)=\sum_{k\ge0}(1-x)x^ku_L(k)$$

is a low-need user's expected utility in an M/M/1 queue with load $x$. It has a unique root $\bar\Lambda_H\in(0,1)$.

Formalization targets

Goal: Theorem 6 (Achieving first-best)

1. If $\lambda_H\ge\bar\Lambda_H$, then $\mathrm{sm}(\theta)=\mathrm{ap}(\theta)$ for every $\theta\in[0,1]$.
2. If $\lambda_H<\bar\Lambda_H$, there is $\bar\theta=\theta(\lambda_L,\lambda_H)\in(0,1]$ with

$$\mathrm{sm}(\theta)=\mathrm{ap}(\theta)\quad(\theta>\bar\theta),\qquad \mathrm{sm}(\theta)=\mathrm{sm}(\theta')\quad(\theta,\theta'<\bar\theta).$$

The goal does not fix $\bar\theta$ or give it in closed form. It asserts only that $\bar\theta$ exists, that $\bar\theta$ is positive, and that the optimal signaling mechanism splits into these two regimes.

Milestones

In the order the proof in Appendix D uses them:

• Lemma 3, the detailed-balance sandwich $\lambda_H^{k-q}\pi_q\le\pi_k\le\lambda^{k-q}\pi_q$.
• Theorems 1 and 2: every Pareto-efficient signaling mechanism or admission policy has a threshold structure with threshold at most $m_{fi}$.
• Lemma 2, existence of maximizers.
• Lemma 4, the no-information equilibrium.
• $g$ strictly decreasing with a unique root.
• Theorem 5 and Proposition 3(3): ni is Pareto-dominated by a signaling mechanism iff $\lambda_H<\bar\Lambda_H$.
• Lemma 5(1): $W_H$ of the threshold policy decreases in the threshold.
• Theorem 3: when (LEAVE) is slack, efficiency in $\Pi_{SM}$ and in $\Pi_{AP}$ coincide.
• Lemma 6, the shape of $L$ along threshold policies.

Significance

Theorem 6 says that over a large range of weights the obedience constraints cost nothing. The optimal signaling mechanism coincides with the first-best admission policy, even though that benchmark presumes the provider sees user types and can enforce decisions. In that range the signal acts only as a coordination device, and no user is indifferent between the recommended action and the alternative. This differs from typical Bayesian persuasion, where optimal schemes make some receiver indifferent. The two regimes of the theorem coincide with those of Theorem 5. Where no information is already Pareto-efficient, efficient signaling and efficient admission agree for all weights. Elsewhere, signaling falls short of the first-best only for weights that favour high-need users.

The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. The mission produces a formal model of obedient binary signaling in an unobservable queue, with admission policies, obedience constraints, welfare and Pareto efficiency within a class. It also formalizes the structural theorems and the first-best comparison. Formal proofs would also check the steps the paper calls "straightforward" or leaves out, such as Theorem 2's omitted proof and the coupling arguments.

Difficulty

Each step of the proof uses a different tool. The threshold monotonicity in $\theta$ is a revealed-preference argument, and it needs $W_H$ of threshold policies to be strictly decreasing. Obedience propagates upward only along threshold policies, through the shape of $L$ in Lemma 6. The positivity of $\bar\theta$ needs the optimal admission policy for small $\theta$ to violate (LEAVE). Below $\bar\theta$, the binding (LEAVE) constraint must pin a single threshold. The tempting shortcut is to argue only with the scalarized problem $\max W(\cdot,\theta)$, and it fails for two reasons. At $\theta\in\{0,1\}$ maximizers need not be Pareto-efficient (footnote 12). Also, $\mathrm{sm}(\theta)$ and $\mathrm{ap}(\theta)$ are sets, so set equality needs both inclusions and non-emptiness. Existence (Lemma 2) rests on a weak-compactness argument over distributions on $\mathbb N_0$, which is delicate at $\lambda=1$.

Formalization scope

• A model is a structure with fields $\lambda_L,\lambda_H\in\mathbb R$ and $u_L,u_H:\mathbb N\to\mathbb R$. Queue lengths are natural numbers, and everything is real-valued.
• Membership in $\Pi_{AP}$ requires $\sum_n\pi_nu_L(n)$ and $\sum_n\pi_nu_H(n)$ to converge, since the paper treats welfare as finite.
• $W_L$ is written without the division by $\lambda_L\pi_n$.
• Thresholds are reals $x\ge0$, and threshold $\infty$ is a separate case.
• $\mathrm{sm}(\theta)$ and $\mathrm{ap}(\theta)$ are sets of maximizers (footnote 14). At $\theta=0$ ($\theta=1$) they maximize $W_H$ then $W_L$ ($W_L$ then $W_H$), as in footnote 12.
• The no-information equilibrium is defined by the low-need user's best-response condition, not by a closed form.
• $\bar\Lambda_H$ enters as any root of $g$ in $(0,1)$, which is unique.

Hypotheses added relative to the page, all stated in the items:

• Lemma 2's hypothesis ($\lambda<1$, or $u_L,u_H\to-\infty$) and convergence of $\sum_k\lambda_H^ku_H(k)$ on the goal, so the compared optimizer sets are non-empty.
• Convergence of $\sum_k\lambda_H^ku_H(k)$ on Lemma 2, Lemma 5(1), and the goal, and convergence of $\sum_kr^ku_H(k)$ for every $r\in[0,1)$ on the existence part of Lemma 4. Under the finite-welfare convention, $\Pi_{AP}$ is empty without the first when $\lambda_H>0$ and $u_H$ falls fast enough.
• $\lambda_H>0$ in Lemma 5(1), which is false for $\lambda_H=0$.

Encodings that would trivialize the goal are excluded:

• $\mathrm{sm}(\theta)$ and $\mathrm{ap}(\theta)$ are full sets of maximizers, not single chosen maximizers. The goal's finiteness and existence hypotheses rule out empty optimizer sets.
• Pareto efficiency of ni is tested against all of $\Pi_{AP}$.
• (LEAVE) is never read off a divergent series.

The work needs:

• stochastic-dominance arguments for distributions on $\mathbb N_0$;
• monotonicity of ratios of affine functions;
• a compactness argument for existence.

The model layer and the threshold structural theorems can be reused by the companion missions of this series. Proofs of individual milestones are welcome independently.

Selected references

• J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; preprint arXiv:2005.07253v3, 2022. https://arxiv.org/abs/2005.07253v3
• D. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5):1397–1416, 2019.
• Y.-K. Che, J. Kim, F. Kojima, C. T. Ryan, Characterizing Pareto Optima: Sequential Utilitarian Welfare Maximization, arXiv:2008.10819, 2020. https://arxiv.org/abs/2008.10819

Why information design for congested public services

Many social services are rationed by waiting rather than by price: public health clinics, food banks, shelters, legal aid. Users who need the service most often have no outside option, while users with less need could be served elsewhere but join the queue anyway and lengthen everyone's wait. The provider usually cannot force anyone to leave, and charging money defeats the purpose of the service. What the provider does control is information: it observes the queue and decides what to tell arriving users about it.

Anunrojwong, Iyer and Manshadi (2023) model this as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (2019, Operations Research 67(5):1397–1416). Their first structural result, Theorem 1, says that whatever trade-off the provider makes between the two user groups, the efficient way to signal is a simple threshold rule, and that the threshold never exceeds the one under full information. This mission formalizes Theorem 1 and the steps of its proof.

Setting

A single server serves users first-come-first-served; service times are exponential with rate one. Users of two types arrive by independent Poisson processes: low-need users (type $\mathsf L$) at rate $\lambda_{\mathsf L}>0$ and high-need users (type $\mathsf H$) at rate $\lambda_{\mathsf H}\ge0$, with total rate $\lambda=\lambda_{\mathsf L}+\lambda_{\mathsf H}\le 1$. A type-$i$ user who joins with $n\in\mathbb N_0$ users already present receives utility $u_i(n)$, where $u_i(0)>0$, $u_i(n)<0$ for large $n$, $u_i$ is strictly decreasing, and the increments $u_{\mathsf L}(n)-u_{\mathsf L}(n+1)$ are non-increasing (Assumption 1). High-need users always join; low-need users take an outside option worth $0$ unless joining is at least as good in expectation.

By the revelation principle and Lemma 1 of the paper, an obedient binary signaling mechanism is identified with its steady-state distribution $\pi=(\pi_n)_{n\ge0}$ of the queue length. The admission policies $\Pi_{\mathsf{AP}}$ are the probability distributions on $\mathbb N_0$ satisfying the detailed-balance constraints

$$\lambda_{\mathsf H}\pi_n\le\pi_{n+1}\le\lambda\pi_n\qquad(n\ge0).$$

The signaling mechanisms $\Pi_{\mathsf{SM}}\subseteq\Pi_{\mathsf{AP}}$ additionally satisfy the obedience constraints

$$J(\pi)=\sum_{n\ge0}(\pi_{n+1}-\lambda_{\mathsf H}\pi_n)\,u_{\mathsf L}(n)\ge0,\qquad L(\pi)=\sum_{n\ge0}(\lambda\pi_n-\pi_{n+1})\,u_{\mathsf L}(n)\le0 .$$

The welfare of the two groups is $W_{\mathsf L}(\pi)=J(\pi)$ and $W_{\mathsf H}(\pi)=\lambda_{\mathsf H}\sum_n\pi_nu_{\mathsf H}(n)$. A mechanism $\hat\pi$ Pareto-dominates $\pi$ if $W_i(\hat\pi)\ge W_i(\pi)$ for both $i$, with at least one strict inequality; $\pi\in\Pi_{\mathsf{SM}}$ is Pareto-efficient within $\Pi_{\mathsf{SM}}$ if no $\hat\pi\in\Pi_{\mathsf{SM}}$ dominates it (Definition 1).

A distribution has a threshold structure (Definition 2) if for some $m\in\mathbb N_0\cup\{\infty\}$, $\pi_{k+1}=\lambda\pi_k$ for $k<m$ and $\pi_{k+1}=\lambda_{\mathsf H}\pi_k$ for $k>m$: low-need users are told to join below $m$, to leave above $m$, and to join with probability $a=(\pi_{m+1}-\lambda_{\mathsf H}\pi_m)/(\lambda_{\mathsf L}\pi_m)\in[0,1]$ at $m$. The threshold is $x=m+a$. The full-information threshold $m_{\mathsf{fi}}$ is the smallest $k$ with $u_{\mathsf L}(k)<0$: when the queue is revealed, low-need users join exactly below it.

Formalization targets

Goal: Theorem 1 (p. 14)

For every $\pi\in\Pi_{\mathsf{SM}}$ that is Pareto-efficient within $\Pi_{\mathsf{SM}}$, there is a finite $m\in\mathbb N_0$ such that

$$\pi_{k+1}=\lambda\pi_k\ (k<m),\qquad \pi_{k+1}=\lambda_{\mathsf H}\pi_k\ (k>m),\qquad m+\frac{\pi_{m+1}-\lambda_{\mathsf H}\pi_m}{\lambda_{\mathsf L}\pi_m}\le m_{\mathsf{fi}} .$$

No weight $\theta$ is fixed: the statement covers the whole Pareto frontier.

Milestones

1. Lemma 3 (p. 36): for $\pi\in\Pi_{\mathsf{AP}}$ and $k>q$, $\lambda_{\mathsf H}^{k-q}\pi_q\le\pi_k\le\lambda^{k-q}\pi_q$; if $\lambda_{\mathsf H}>0$, every $\pi_k\in(0,1)$.
2. Step 1 (App. A, p. 34): if $\pi\in\Pi_{\mathsf{SM}}$ has $\pi_{m+1}<\lambda\pi_m$ and $\lambda_{\mathsf H}\pi_{m+1}<\pi_{m+2}$ for some $m$, some $\hat\pi\in\Pi_{\mathsf{SM}}$ Pareto-dominates $\pi$.
3. Structure dichotomy (App. A, p. 35): if $\pi_{m+1}<\lambda\pi_m$ always forces $\pi_{m+2}=\lambda_{\mathsf H}\pi_{m+1}$, then $\pi$ has threshold $\infty$ or a finite threshold structure.
4. Step 2 (App. A, pp. 35–36): a $\pi\in\Pi_{\mathsf{SM}}$ with a threshold structure whose threshold is $\infty$ or exceeds $m_{\mathsf{fi}}$ is Pareto-dominated within $\Pi_{\mathsf{SM}}$.

Significance

Theorem 1 reduces an infinite-dimensional design problem (a distribution on $\mathbb N_0$ subject to obedience) to a one-parameter family of threshold policies $x\in[0,m_{\mathsf{fi}}]$. Every later result of the paper is computed in that family: the bound of the optimal signaling mechanism against full information when all users are low-need (Proposition 1), the condition under which information design Pareto-dominates full information (Theorem 4 and Proposition 3), and the conditions under which signaling achieves the first-best admission policy (Theorems 5 and 6). The bound $x\le m_{\mathsf{fi}}$ also has a direct reading: efficient persuasion only ever discourages low-need users relative to full information, never encourages them.

The theorem is proved in the paper (App. A). This mission produces a machine-checked version of the proof, on top of a reusable Lean model of obedient signaling in an $M/M/1$-type queue with two user types. To our knowledge no part of this model or of its results has been formalized before.

Difficulty

The statement quantifies over the full Pareto frontier, so it cannot be obtained from first-order conditions of a single weighted objective. Both steps are perturbation arguments on infinite sequences: each must build an explicit competitor, keep it inside the detailed-balance constraints and both obedience constraints at once, and show weak improvement for one group with strict improvement for the other. The obedience constraint (LEAVE) cuts against (JOIN): moving mass toward shorter queues raises $J$ but can raise $L$, and the bound on $L$ is where $\lambda\le1$ is needed. Since $\lambda=1$ is allowed, the geometric tails are not automatically summable and the infinite sums have to be handled with care. The threshold $\infty$ must be excluded explicitly; it is not ruled out by the structure argument alone.

Formalization scope

All definitions live in NeedPersuasion.Threshold (file Def_NeedPersuasion_Threshold_Model). Queue lengths are ℕ, everything else is ℝ; the two types are two fields of a Model structure. The standing assumptions are the predicate Model.Standing: $\lambda_{\mathsf L}>0$, $\lambda_{\mathsf H}\ge0$, $\lambda\le1$, $u_i(0)>0$, $u_i(k)<0$ for some $k$ (equivalent to $\lim u_i<0$ for a strictly decreasing sequence, and allowing $-\infty$), both utilities strictly decreasing, and the $\mathsf L$-increments non-increasing. Every theorem assumes it; no other hypothesis is added, and in particular $\lambda<1$ is not assumed.

Committed conventions:

• $\Pi_{\mathsf{AP}}$ requires $\sum_n\pi_n=1$ as a HasSum, and finite welfare: $(\pi_nu_{\mathsf L}(n))$ and $(\pi_nu_{\mathsf H}(n))$ summable. The paper treats the welfare sums as real numbers; without this, a policy with welfare $-\infty$ (possible at $\lambda=1$) would receive welfare $0$ from Lean's tsum.
• $W_{\mathsf L}$ is the right-hand form of (2), which has no division by $\lambda_{\mathsf L}\pi_n$.
• The threshold $\infty$ is the first disjunct of HasThresholdStructure; HasThresholdAtMost π y asks for a finite $m$ with $m+a\le y$.
• Pareto efficiency is Definition 1 (ParetoEfficientIn), never maximization of $\theta W_{\mathsf L}+(1-\theta)W_{\mathsf H}$.

Trivializing encodings are ruled out: the threshold-structure predicate is not satisfied by every admission policy, efficiency is taken over all of $\Pi_{\mathsf{SM}}$ (including the competitors the proof builds), and no sum whose value is compared can be a divergent tsum. A sorry-free sanity file exhibits a model satisfying Standing whose full-information mechanism lies in $\Pi_{\mathsf{SM}}$, so the hypotheses are not vacuous.

A complete development needs manipulation of tsum over shifted and truncated sequences, geometric tails, and first-order stochastic dominance for sequences on $\mathbb N_0$; these pieces are reusable for the other missions of this series (missions 2–4 restate the same model). Contributions of proofs of individual milestones, or of general lemmas on detailed-balance sequences, are welcome.

Selected references

• J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; read as arXiv:2005.07253v3 (2022). https://arxiv.org/abs/2005.07253
• D. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5):1397–1416, 2019 (cited as reference in arXiv:2005.07253v3, p. 32).
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200

Why estimate a mean with a quantum algorithm?

Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure can be run coherently as a quantum algorithm and its unitary part can also be inverted. The bounded-variance result gives an estimator whose dependence on the requested accuracy is approximately linear in $1/\epsilon$, compared with the quadratic dependence of ordinary sampling, up to logarithmic factors and the paper's model-specific operation counts. The exact asymptotic claims are in Theorem 5 of the pinned preprint, p. 12.

This mission concentrates on the probability and accuracy claim of that theorem. It includes the mean-estimation result for a nonnegative output from Lemma 4, because Algorithm 3 invokes that estimator twice after centering a general real output. The underlying amplitude-estimation theorem is a separate, already posed result, QAmpEst.Est.theorem_12; this mission uses the accuracy guarantee stated in Montanaro's Theorem 3 as the interface to that subroutine.

Outputs, truncations, and estimates

Let $X=v(\mathcal A)$ denote the real output of a quantum algorithm $\mathcal A$ under one run, and let $P$ be its probability law. The mean is $\mathbb E[X]$, and the variance is $\operatorname{Var}(X)=\mathbb E[(X-\mathbb E[X])^2]$. The result assumes a known $\sigma>0$ with $\operatorname{Var}(X)\le\sigma^2$. Although the paper describes a circuit that prepares and measures $X$, its accuracy statements depend on the distribution of $X$; the Lean interface therefore represents a run as a measurable real random variable on a probability space.

For real thresholds $a<b$, the truncation $X_{[a,b)}$ returns $X$ when $a\le X<b$ and zero otherwise. The variants $X_{<a}$ and $X_{\ge b}$ retain the output below $a$ and at or above $b$, respectively. They do not clip a value to a threshold. The $L^2$ size is $\|X\|_2=\sqrt{\mathbb E[X^2]}$. These are the output transformations defined in §2.2, p. 9, and used in Lemma 4, pp. 10–11.

Algorithm 2 estimates a nonnegative mean using the base interval $[0,1)$ and the half-open bands $[2^{\ell-1},2^\ell)$ for $1\le\ell\le k$. It sets $k=\lceil\log_2(1/\epsilon)\rceil$ and $t_0=\lceil D\sqrt{\log_2(1/\epsilon)}/\epsilon\rceil$, then adds the base estimate to $2^\ell$ times each band estimate. A successful Algorithm 1 call means that its estimate of a $[0,1]$-valued output $Y$ differs from $\mathbb E[Y]$ by at most $C(\sqrt{\mathbb E[Y]}/t+1/t^2)$, the accuracy bound of Theorem 3, pp. 8–9.

Algorithm 3 rescales $X$ by $\sigma$, draws one sample $m$ from $X/\sigma$, and centers the rescaled output at $m$. It feeds the negative and nonnegative parts, each divided by four, to Algorithm 2 at accuracy $\epsilon/(32\sigma)$ and recombines their estimates. The two calls are specified to fail with probability at most $1/9$ each; the paper describes boosting Algorithm 2's initial success probability for this use on p. 11.

Formalization targets

Lemma 4: nonnegative mean accuracy

When every Algorithm 1 call satisfies its accuracy bound and $0<\epsilon<1/2$, the output $\widetilde\mu$ of Algorithm 2 obeys

$$|\widetilde\mu-\mathbb E[X]|\le\epsilon(\|X\|_2+1)^2.$$

The constant $D>0$ is chosen once for a fixed positive universal constant $C$ from Theorem 3. It is independent of $X$ and $\epsilon$.

Theorem 5: bounded-variance accuracy

For $\operatorname{Var}(X)\le\sigma^2$, $\sigma>0$, and $0<\epsilon<4\sigma$, Algorithm 3 returns $\widehat\mu$ with

$$\Pr\bigl(|\widehat\mu-\mathbb E[X]|\le\epsilon\bigr)\ge\frac23.$$

This is the mission goal. Its probability is over the preliminary sample and both subsequent estimation runs. The milestone list follows the exact displayed statements used in Lemma 4 and the proof of Theorem 5, with their source pages.

What the result supplies

Theorem 5 turns an estimator for nonnegative outputs with finite second moment into one that handles signed outputs whose variance is bounded, without assuming a bound on the magnitude or mean of the output. That extension matters when the quantity being averaged can be negative or has a large offset: a second-moment bound on $X$ itself would then be much stronger than the paper's variance hypothesis. The stated error and success probability are the mathematical guarantee on which the paper's resource comparison rests; the comparison itself includes quantum operations absent from the measure-theoretic statement.

The formal development supplies reusable definitions of truncations, dyadic estimates, and the centered positive and negative parts, together with precisely quantified probability claims. It leaves Lemma 4 and Theorem 5 as open Lean proof targets. The amplitude-estimation statement behind Theorem 3 is already posed separately on Prove2Me, while the composed bounded-variance result and the displayed intermediate claims are the new targets here.

Where the difficulty lies

A bound for one $[0,1]$-valued call does not directly bound the mean of a signed, unbounded output. Truncating after finitely many bands leaves a tail, and the sum of errors over the retained bands can grow with their weights. The theorem must control both effects while keeping $D$ independent of the output distribution. For the signed case, the initial sample is random; its deviation, the two later failures, and the scale of the centered output all contribute to the final probability. Replacing that sample by the exact mean would remove a substantive part of the claim.

Formalization scope

Lean uses probability measures and measurable real outputs for the laws of $v(\mathcal A)$ and Algorithm 3's preliminary sample. The law of that sample is fixed to the image law of $X/\sigma$, so it cannot be selected arbitrarily. The successful-call predicate names the actual truncated outputs and the paper's $k$ and $t_0$ formulas; it does not assume Lemma 4's final error bound. The sample space carrying the later estimates is allowed to encode their joint dependence on the preliminary sample. Events are measured with extended nonnegative real values.

The $L^2$ hypotheses state that the second moment is finite. In Mathlib the real-valued variance and the integral can return a default value on a nonintegrable input, which would make a bare variance inequality or a bare $\|X\|_2$ bound misleading. The paper implicitly uses finite variance where those quantities occur. The condition $0<\epsilon$ makes the divisions and logarithms in the algorithm parameters meaningful. The natural-number expression $\ell-1$ occurs only on bands indexed by $\ell\ge1$.

The quantum circuit for Algorithm 1, the construction of an inverse unitary, and the $O(\cdot)$ copy and operation counts are outside the formal statements. Their interface is Theorem 3's numerical accuracy event. Contributions to the dyadic inequalities, the finite-variance probability bound, and their composition into the final event are in scope. The definitions are also useful for other mean estimators that split a real output into bounded pieces.

Selected references

• Ashley Montanaro, Quantum speedup of Monte Carlo methods, arXiv:1504.06987v3 [quant-ph], 2017, especially §§2.1–2.3, pp. 8–12. Pinned preprint.
• Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation, Contemporary Mathematics 305, 2002. arXiv preprint.

Why a lower bound for best subsets

Best subset selection fits a linear model by least squares using at most $k$ of $p$ available predictors. It is the classical $\ell_0$-constrained estimator of sparse regression. Mixed-integer optimization now computes it for problems with thousands of variables (Bertsimas, King & Mazumder 2016), so its statistical behaviour matters in practice. Simulations in Hastie, Tibshirani & Tibshirani 2020 found that it predicts worse than shrinkage methods such as the Lasso when the signal-to-noise ratio (SNR) is low.

Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add an $\ell_1$ or $\ell_2$ shrinkage penalty to best subsets. They prove upper bounds of two kinds: slow rates, linear in the tuning parameter $\lambda$, and fast rates, quadratic in $\lambda$. Theorems 2 and 3 of the paper give them for the shrunken estimators. For best subsets, the paper only has a fast-rate bound, of order $\sigma^2 k\log(ep/k)$. When $\|\beta^*\|/\sigma$ is small, the shrunken estimators' slow rate beats that bound. Theorem 4, the goal of this mission, shows that the comparison is meaningful: in that regime best subsets really does incur an error of the order of its upper bound.

Setting

The data follow the linear model

$$y = X\beta^* + \epsilon ,\qquad y,\epsilon\in\mathbb R^n,\ \beta^*\in\mathbb R^p ,$$

where the design $X$ is a deterministic real $n\times p$ matrix whose columns have unit Euclidean norm. The noise $\epsilon$ has independent $N(0,\sigma^2)$ entries, with $\sigma>0$. Write $\|v\|$ for the Euclidean norm, $\|v\|_1=\sum_i|v_i|$, $\operatorname{supp}(v)=\{i:v_i\ne0\}$ and $\|v\|_0=|\operatorname{supp}(v)|$. The $\ell_0$ ball is $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$. The minimal $s$-sparse eigenvalue of $X$ is

$$\gamma_s=\min_{u\ne0,\ u\in B_0(s)}\frac{\|Xu\|}{\|u\|} .$$

A best-subsets solution of size $k$ is any minimizer

$$\hat\beta_{\ell_0}\in\arg\min\ \|y-X\beta\|^2\quad\text{s.t.}\quad\|\beta\|_0\le k .\tag{1}$$

A constant is universal if it does not depend on $n,p,k,X,\sigma,\beta^*$. The symbols $\lesssim$ and $\gtrsim$ mean $\le$ and $\ge$ up to positive universal factors. Logarithms are natural, and $e=\exp(1)$.

Formalization targets

Goal: Theorem 4 (p. 18)

There are universal constants $c_0,c,C>0$ such that the following holds. Suppose $2\le k\le p$, $\|\beta^*\|_0\le k$ and $\|\beta^*\|\le c_0\sigma\gamma_k\sqrt{k\log(ep/k)}$. Then, with probability at least $1-2(ep/k)^{-c\gamma_k^2k}-(ep/k)^{-k}$, every best-subsets solution satisfies

$$\|X\hat\beta_{\ell_0}-X\beta^*\|^2\ \ge\ C\,\sigma^2\gamma_k^2\,k\log(ep/k).$$

The constants are left unfixed, as in the paper. The statement asserts the order of the error, which is what the comparison with the upper bounds needs.

Milestones

1. Maurey approximation (p. 44). For unit columns and every $\beta^*$, some $\tilde\beta^*$ with $\|\tilde\beta^*\|_0\le k/2$ has $\|X\beta^*-X\tilde\beta^*\|^2\le2\|\beta^*\|_1^2/k$.
2. (39) (p. 44). With $\Delta^*=X\beta^*-X\tilde\beta^*$, define $G(\beta)=\|y-X\beta\|^2-\|y-X\tilde\beta^*\|^2$ and $H(u)=\|Xu\|^2-2(\Delta^*+\epsilon)^\top Xu$. Then $G(\beta)$ equals $\|X\beta-X\tilde\beta^*\|^2+2(\Delta^*+\epsilon)^\top(X\tilde\beta^*-X\beta)$, and $\min_{\|\beta\|_0\le k}G\le\min H(u)$ over $u$ supported off $\operatorname{supp}(\tilde\beta^*)$ with $\|u\|_0\le k/2$.
3. (40) (p. 45). $\min_{\|\beta\|_0\le k}G(\beta)\le-\max_{v\in\mathcal V_k}|(\Delta^*+\epsilon)^\top Xv|^2$, where $\mathcal V_k$ is the set of $v$ supported off $\operatorname{supp}(\tilde\beta^*)$ with $\|v\|_0\le k/2$ and $\|Xv\|=1$.
4. Lemma 1 (p. 44). Let $S$ have $q$ elements and let $s\in[1,q]$ be an integer. Then $\max|\epsilon^\top Xv|\gtrsim\sigma\gamma_{2s}\sqrt{s\log(eq/s)}$ over $\operatorname{supp}(v)\subseteq S$, $\|v\|_0\le s$, $\|Xv\|=1$, with probability at least $1-2(eq/s)^{-\tilde c\gamma_{2s}^2s}$.

Significance

Theorem 4 matches the fast-rate upper bound for best subsets from Corollary 1 of the paper. When $\gamma_k$ is bounded below, the prediction error of best subsets is of exact order $\sigma^2k\log(ep/k)$ in the low-SNR regime (Remark 10). This is the theoretical counterpart of the empirical observation that best subsets overfits at low SNR. It is also what makes the paper's case for shrinkage a theorem rather than a comparison of upper bounds. The paper's Proposition 4 applies it to a concrete correlated design, where it gives a ratio of prediction errors between best subsets and its $\ell_2$-shrunken version that grows with $k$.

The result is proved in the paper; this mission formalizes it. No formalization of this result exists on the platform. The mission also produces a reusable Gaussian lower bound on sparse correlations (Lemma 1) and a deterministic reduction of the best-subsets objective, (39)–(40), which are of independent use for $\ell_0$ estimators.

Difficulty

An upper bound on best subsets follows from comparing $\hat\beta_{\ell_0}$ with $\beta^*$ in a basic inequality. A lower bound must hold for every minimizer, and $\beta^*$ itself gives no lower bound. The first idea is to compare with the noiseless fit. It fails because the noise can be fitted by sparse directions, which is exactly the effect to be quantified. The difficult step is Lemma 1. It requires a large set of sparse directions that remain separated after multiplication by $X$, a lower bound on the expected maximum of a Gaussian process over that set, and concentration of that maximum around its mean, with all constants universal. A second subtlety is that the statement is about every minimizer of a nonconvex problem, so the proof has to bound the objective rather than the estimator.

Formalization scope

Vectors are Fin n → ℝ and Fin p → ℝ, with indices starting at 0. The design is X : Matrix (Fin n) (Fin p) ℝ. The Euclidean norm, $\ell_1$ norm, support and $\|\cdot\|_0$ are explicit definitions, since Mathlib's norm on Fin m → ℝ is the sup norm. $\gamma_s$ is an infimum over the nonzero vectors with $\|u\|_0\le s$; this set is nonempty when $p,s\ge1$, and every ratio is $\ge0$. The noise law is the product of $n$ centred Gaussians of variance $\sigma^2$ on $\mathbb R^n$. "With probability at least $1-\eta$" means that a measurable set of noise vectors of probability at least $1-\eta$ exists on which the conclusion holds. Best subsets is an argmin predicate: Theorem 4 quantifies over every minimizer, and existence is neither assumed nor needed. Universal constants are quantified before every other parameter. "$\|\cdot\|_0\le k/2$" is a comparison of real numbers.

The model consists of $X$, $\beta^*$ (with $f^*=X\beta^*$), $\epsilon$ and its Gaussian law, the estimator (1), and the minimal sparse eigenvalue $\gamma_s$.

Two hypotheses are pinned relative to the printed theorem:

• $k\ge2$, because the statement is false for $k=1$. Take every column equal to $e_1$ and $\beta^*=0$: the error is $\epsilon_1^2$, while the bound demands order $\sigma^2\log(ep)$ with probability tending to one.
• $\|\beta^*\|_0\le k$, because the proof uses $\|\beta^*\|_1$, which the printed $\ell_2$ hypothesis controls only for sparse $\beta^*$, and §3.4 places the theorem in Corollary 1's setting $\beta^*\in B_0(k)$.

The milestones carry neither pin. Because the constants are existential, a formalization in which $c_0$, $c$ or $C$ may depend on $p$, $k$ or $X$ would be trivial, and is ruled out by quantifying them first. A version asserting the bound for some minimizer would be weaker than the theorem.

Not formalized here: the upper bounds (Theorems 2, 3, 5), the noise events of Theorem 1, Corollaries 1–6, Propositions 3–4, and the numerical experiments. The proof of the goal also uses Theorem 1's event $\mathcal G_{2k}$, which belongs to a separate mission of this series. Proved platform results that a proof of Lemma 1 can use include Sudakov minoration for separated Gaussian families (HighDimProb.RandomProcesses.sudakov_minoration_finite_separated), Gaussian Lipschitz concentration (HighDimStat.TailBounds.lipschitz_gaussian_concentration) and a lower bound on Gaussian maxima (HighDimProb.RandomProcesses.standard_gaussian_max_lower_bound). Contributions are welcome on any milestone, and on supporting lemmas: a packing of sparse sign vectors (Gilbert–Varshamov type), and the approximation of $\ell_1$-bounded vectors by sparse ones.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research, 2023; preprint arXiv:1708.03288v4, 2022. https://arxiv.org/abs/1708.03288v4
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• T. Hastie, R. Tibshirani, R. Tibshirani, Best Subset, Forward Stepwise or Lasso? Analysis and Recommendations Based on Extensive Comparisons, Statistical Science 35(4), 2020. https://doi.org/10.1214/19-STS733
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. https://doi.org/10.1017/9781108231596

Motivation

Advertising platforms repeatedly sell opportunities to show an advertisement. The opportunity's features, such as audience and placement, affect each advertiser differently, while advertisers limit their average spending. This makes the efficiency of an auction a question about both heterogeneous values and budgets. The paper by Balseiro, Kroer, and Kumar studies this setting with a continuum of buyer types and context-dependent values. It constructs equilibria by value pacing, in which a buyer scales values before bidding. This mission asks how much attainable value those equilibria preserve when budgets cap useful value.

Earlier efficiency bounds for second-price auctions concern a different, non-Bayesian multi-item model. In particular, the half guarantee discussed by Azar and coauthors, as discussed in §5 of the paper uses a no-overbudgeting condition that the present pacing equilibria need not satisfy. Balseiro, Kroer, and Kumar prove their bound under their own contextual and in-expectation budget model; the distinction matters when interpreting the constant. Their existence and revenue-equivalence results also make it possible to speak about the same pacing-based allocation across standard auction payment rules. These claims and the limitation of the earlier assumption are explained in §5 of the paper.

Setting

An item has a context $\alpha\in A\subset\mathbb R^d$, with $d\ge2$. There are $n\ge2$ buyers. Each buyer has a private type $\theta=(w,B)$: the vector $w\in(0,U)^d$ assigns a positive weight to every context feature, and $B\in(B_{\min},U)$ is the buyer's budget, where $0<B_{\min}<U$. The buyer's value for the item is $w^\top\alpha$. A context is drawn from a distribution $F$ and buyers' types are drawn independently from a distribution $G$; both distributions have densities. The context and type ranges are the spaces $A$ and $\Theta=(0,U)^d\times(B_{\min},U)$ of §2. The reserve price is zero throughout the efficiency section.

A pacing function $\mu:\Theta\to\mathbb R_{\ge0}$ scales type $\theta$'s value to $w^\top\alpha/(1+\mu(\theta))$. Let $H^\mu_\alpha(x)$ be the probability that the maximum paced value among $n-1$ independent competitors is at most $x$. The first-price bid $\beta^\mu(\theta,\alpha)$ applies the paper's bid function $\sigma^\mu_\alpha$ to the paced value. A buyer may choose a context-dependent bid, subject to an in-expectation budget: expected payment over contexts and competitors must not exceed $B$. The buyer's dual function $q^\mu(\theta,t)$ is the supremum of its Lagrangian over such bids at multiplier $t\ge0$.

The relevant pacing equilibria are fixed points of the correspondence $C_0^*$. Its domain $X_0$ consists of measurable, integrable pacing functions in $[0,\omega/B_{\min}]$ with total variation at most $V_0=(d+1)U^{d+1}\omega/B_{\min}$, where $\omega$ is the supremum of possible values. For a given $\mu\in X_0$, $C_0^*(\mu)$ minimizes the average dual objective $\mathbb E_{\theta\sim G}[q^\mu(\theta,\widehat\mu(\theta))]$ over $\widehat\mu\in X_0$. These are the objects of §3.3, including its multivariate definition of total variation.

An allocation $x$ assigns nonnegative shares $x_i(\alpha,\theta_1,\ldots,\theta_n)$ summing to one. For buyer $i$, keep $\theta_i=(w_i,B_i)$ fixed while averaging $w_i^\top\alpha\,x_i$ over the context and the other types. The buyer's liquid welfare is the smaller of this interim value and $B_i$; total liquid welfare $\mathrm{LW}(x)$ sums its expectation over each buyer's own type. For an equilibrium pacing function $\mu\in C_0^*(\mu)$, $x^\mu$ allocates to a highest paced bidder. Definitions 5 and 6 use this allocation to define the worst equilibrium liquid welfare relative to the optimal allocation.

Formalization targets

The main target is the Theorem 3 guarantee, stated for every measurable allocation $x$ and every equilibrium pacing function $\mu$:

$$\mathrm{LW}(x^\mu)\ge\tfrac12\,\mathrm{LW}(x).$$

The universal comparison expresses the paper's price-of-anarchy bound $\mathrm{PoA}\ge1/2$. It leaves no optimum or worst equilibrium as an arbitrary variable. The two milestones are the dual derivative identity and the first-order budget and complementary-slackness conditions stated in §3.2:

$$\partial_t q^\mu(\theta,t)=B-\mathrm{payment}(b_t),\qquad \mathrm{payment}(b_{t^*})\le B,\quad t^*(B-\mathrm{payment}(b_{t^*}))=0.$$

Here $b_t(\alpha)=\sigma^\mu_\alpha(w^\top\alpha/(1+t))$ and $t^*$ minimizes $q^\mu(\theta,\cdot)$ over nonnegative multipliers. The milestones are posed in the zero-reserve setting used by the main target.

Significance

The theorem gives an explicit welfare guarantee despite private budgets, correlated values across buyers through a shared context, and equilibrium bidding that depends on those budgets. It applies to the allocation induced by pacing in every standard auction covered by the paper, since those auctions have the same equilibrium allocation even when payment rules differ Balseiro, Kroer, and Kumar, §4–5. Without an efficiency bound, existence of a pacing equilibrium alone would give no quantitative assurance about the allocation it produces.

The result has a mathematical proof in the paper's online appendix; it is an open formalization target here. A complete development would connect measurable Bayesian auctions, the buyer's nonconvex dual problem, the bounded-variation fixed-point domain, and interim liquid welfare. The definitions of interim welfare, dual expenditure, and multivariate variation can support other budgeted auction results. The source PDF held for this mission contains the published main article but not its online appendix, where the proofs and auxiliary lemmas appear.

Difficulty

The expected budget applies to each buyer type after averaging over contexts and opponents, while liquid welfare caps that same type's interim value before averaging over types. Moving the budget cap across the expectation changes the quantity. The natural first-price tie convention also awards the good to every highest bidder for the buyer optimization problem, while a welfare allocation must give total share one. The proof must reconcile the dual account of expenditure with a feasible allocation and preserve these different orders of expectation. The dual objective is a supremum over bids, so its derivative cannot be obtained merely by differentiating a chosen closed formula without justifying that formula and the maximizing bid.

Formalization scope

Lean represents a context by Fin d → ℝ and a buyer type by its weight vector and real budget. Value is the explicit finite sum $\sum_i w_i\alpha_i$. The model requires a nonempty bounded measurable context set in the positive orthant, absolutely continuous probability laws $F$ and $G$ supported on their stated domains, measurable reserves and pacing, $n\ge2$, and $0<B_{\min}<U$. Boundedness of $A$ makes $\omega$ finite; these conditions make the domain and integrals implicit in the article well posed. The welfare target assumes zero reserves as §5 does.

Admissible bids are measurable and nonnegative on $A$, with integrable expected payment. The dual is defined by its supremum over bids. Total variation is extended-real-valued and uses Euclidean lengths of test fields; thus infinite variation cannot satisfy the $X_0$ bound through a real supremum's default value. Allocations are measurable and simplex-valued on the model domain. At a tied highest bid, $x^\mu$ splits the item equally; ties have probability zero under these equilibria, as the paper states by its appendix Lemma 6(d). The closed simplex permits zero shares, correcting the paper's notation $\mathbb R_+$ in Definition 5, which §2.1 otherwise calls strictly positive. The universal welfare inequality avoids default real infimum and supremum values on pathological sets. Contributions to the measurable bidding, variation, duality, and welfare infrastructure are all useful within this scope.

Selected references

• Santiago R. Balseiro, Christian Kroer, and Rachitesh Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees, Management Science, Articles in Advance, 2023. DOI: 10.1287/mnsc.2023.4719.

Motivation

Most online advertising is sold by auction, one impression at a time, to advertisers who manage a budget over many auctions rather than a value for a single one. Since 2019 the major ad exchanges have moved from second price to first price auctions, in which the winner pays its own bid. A budget-constrained advertiser in a first price auction must therefore shade its bids twice: once because of the budget, and once because of the payment rule. Whether these two effects admit a coherent equilibrium, and of what form, is the question behind Balseiro, Kroer and Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees (Management Science, 2023, doi:10.1287/mnsc.2023.4719).

Earlier work on pacing equilibria treated second price auctions, where truthful bidding is dominant without budgets (Balseiro, Besbes and Weintraub 2015; Conitzer et al. 2022). In first price auctions with a single deterministic item, an equilibrium may fail to exist (the paper's Online Appendix A). The paper restores existence by letting items carry a random context and values depend on it linearly. This mission formalizes its first main result, Theorem 1: an equilibrium of a simple, interpretable form exists.

Setting

An item has a context $\alpha\in A\subset\mathbb R^d_{+}$, a feature vector drawn from a law $F$ with a density. There are $n$ buyers. Each buyer has a type $\theta=(w,B)$, a weight vector $w$ and a budget $B$, drawn independently from a law $G$ with a density on

$$\Theta=(0,U)^d\times(B_{\min},U).$$

Buyer $(w,B)$ values item $\alpha$ at $w^T\alpha$, and $\omega:=\sup_{(w,B)\in\Theta,\alpha\in A}w^T\alpha$. The seller reveals $\alpha$, then runs a first price auction with a public reserve price $r(\alpha)$: a bid $b(\alpha)$ wins if $b(\alpha)\ge\max(r(\alpha),\{\beta(\theta_i,\alpha)\}_i)$, where $\beta$ is the strategy of the $n-1$ competitors, and the winner pays its bid. A budget only needs to hold in expectation over $\alpha$ and the competitors' types.

A strategy $\beta^*:\Theta\times A\to\mathbb R_{\ge0}$ is a symmetric first price equilibrium (SFPE, Definition 1) if for $G$-almost every type $(w,B)$ the bid function $\beta^*(w,B,\cdot)$ solves

$$\max_{b:A\to\mathbb R_{\ge0}}\ \mathbb E\big[(w^T\alpha-b(\alpha))\mathbb 1\{b(\alpha)\ge\max(r(\alpha),\{\beta^*(\theta_i,\alpha)\}_i)\}\big]\ \ \text{s.t.}\ \ \mathbb E\big[b(\alpha)\mathbb 1\{\cdots\}\big]\le B .$$

A pacing function $\mu:\Theta\to\mathbb R_{\ge0}$ scales values down to paced values $w^T\alpha/(1+\mu(w,B))$. Let $H^\mu_\alpha$ be the distribution function of the highest of $n-1$ i.i.d. paced values, and for $x\ge r(\alpha)$ let

$$\sigma^\mu_\alpha(x)=x-\int_{r(\alpha)}^x\frac{H^\mu_\alpha(s)}{H^\mu_\alpha(x)}\,ds,$$

with $\sigma^\mu_\alpha(x)=0$ if $H^\mu_\alpha(x)=0$ and $\sigma^\mu_\alpha(x)=x$ if $x<r(\alpha)$. The value pacing–based strategy (Definition 2) is

$$\beta^\mu(w,B,\alpha)=\sigma^\mu_\alpha\Big(\frac{w^T\alpha}{1+\mu(w,B)}\Big).$$

For a buyer facing competitors who use $\beta^\mu$, the dual function is $q^\mu(w,B,t)=\sup_b\mathbb E[(w^T\alpha-(1+t)b(\alpha))\mathbb 1\{\cdots\}]+tB$ for $t\ge0$.

Formalization targets

Goal: Theorem 1 (p. 7)

$$\exists\,\mu:\Theta\to\mathbb R_{\ge0}\quad\text{such that}\quad \beta^\mu\ \text{is an SFPE}.$$

Milestones

• Lemma 1 (p. 8): for every type and every $t\ge0$, $\sigma^\mu_\alpha(w^T\alpha/(1+t))$ maximizes the Lagrangian $\mathbb E[(w^T\alpha/(1+t)-b(\alpha))\mathbb 1\{\cdots\}]$.
• Proposition 1 (p. 8): on a set $\Theta'$ of full $G$-measure, for every $\mu$, a minimizer $t^*$ of $q^\mu(w,B,\cdot)$ over $t\ge0$ makes $\sigma^\mu_\alpha(w^T\alpha/(1+t^*))$ optimal for the budget-constrained problem $Q^\mu(w,B)$.
• Lemma 2 (p. 10): the smallest minimizer $\ell^\mu(w,B)$ of $q^\mu(w,B,\cdot)$ over $[0,\omega/B_{\min}]$ is nondecreasing in each $w_i$ and nonincreasing in $B$.
• Lemma 3 (p. 10): $\ell^\mu\in L_1(\Theta)$ and its total variation is at most $V_0=(d+1)\max(U^d,U^{d+1})\,\omega/B_{\min}$. The paper prints $(d+1)U^{d+1}\omega/B_{\min}$, which agrees when $U\ge1$. For $U<1$ the printed bound fails by a rescaling argument, and the mission corrects the exponent to $d$ there.
• Lemma 4 (p. 10): $\mathcal X_0=\{\mu\in L_1(\Theta):0\le\mu\le\omega/B_{\min},\ V(\mu,\Theta)\le V_0\}$ is nonempty, compact and convex in $L_1(\Theta)$; $f(\mu,\hat\mu)=\mathbb E_G[q^\mu(w,B,\hat\mu(w,B))]$ is continuous; $C^*_0(\mu)=\arg\min_{\hat\mu\in\mathcal X_0}f(\mu,\hat\mu)$ is upper hemicontinuous with nonempty, convex, compact values.
• Lemma 5 (p. 10): a fixed point $\mu\in C^*_0(\mu)$ satisfies $\mu(w,B)\in\arg\min_{t\in[0,\omega/B_{\min}]}q^\mu(w,B,t)$ almost surely.
• Proposition 2 (p. 9): some $\mu$ satisfies $\mu(w,B)\in\arg\min_{t\ge0}q^\mu(w,B,t)$ almost surely.

The paper states that Proposition 2 combined with Proposition 1 implies Theorem 1.

Significance

Theorem 1 says that budget-constrained buyers in contextual first price auctions have an equilibrium that is described by one scalar per type: shade the value by the factor $1/(1+\mu(w,B))$, then bid as an unconstrained buyer would in an i.i.d. first price auction against paced competitors. This is the object on which the rest of the paper is built: revenue equivalence across standard auctions (Theorem 2) and a liquid-welfare price of anarchy of at least $1/2$ (Theorem 3) are both statements about pacing-based equilibria. Practically, it supports the use of pacing for budget management in first price auctions, with pacing multipliers computed as for second price auctions.

The result is proved in the paper; every proof is in its online appendix, which is not part of the source this mission cites. Nothing in the paper is formalized. A formalization would check a strong-duality argument for a non-convex problem and an infinite-dimensional fixed-point argument whose topology the authors chose with care, and it would produce reusable pieces: multivariate total variation, compactness of bounded-variation sets in $L_1$, and the first price equilibrium bid against an arbitrary (possibly atomic) value distribution with a reserve price.

Difficulty

The buyer's problem $Q^\mu(w,B)$ is not convex in the bid function, so standard convex duality does not give strong duality; Proposition 1 needs a direct argument combining Lagrangian optimality (Lemma 1), differentiability of $q^\mu$ in $t$, and complementary slackness. Lemma 1 itself cannot quote the textbook first price equilibrium, because the paced value distribution $\lambda^\mu_\alpha$ may have atoms and the reserve price creates discontinuities.

The fixed point lives in an infinite-dimensional space of pacing functions. The obvious topologies fail: the set $\mathcal X$ of bounded pacing functions is not compact in any $L_p$, and in the weak-* topology of $L_\infty$ upper hemicontinuity of the best-response correspondence is hard to obtain; restricting to Lipschitz functions loses the property that best responses stay in the set. The paper restricts to functions of bounded total variation, which requires the monotonicity of Lemma 2 and the variation bound of Lemma 3.

Formalization scope

Contexts are Fin d → ℝ, types are pairs (w, B) : (Fin d → ℝ) × ℝ, and $w^T\alpha$ is the explicit sum $\sum_i w_i\alpha_i$. A single Model structure holds $d,n,U,B_{\min},A,F,G,r$, and Model.Standing collects the assumptions of §2.2 together with four that the paper uses without stating them: $n\ge2$, $B_{\min}<U$, $A$ nonempty and bounded (so $\omega<\infty$), and measurability of $A$ and $r$. Pacing functions are measurable functions on $\mathbb R^d\times\mathbb R$ that are nonnegative on $\Theta$; values off $\Theta$ are irrelevant since $G(\Theta^c)=0$.

The conventions fixed in Lean:

• Ties win: the indicator is $b(\alpha)\ge\max(\cdots)$, as in the paper's tie-breaking rule.
• An admissible bid function is measurable, nonnegative on $A$, and has an integrable payment integrand. The problem of Definition 1, $Q^\mu$, $q^\mu$ and the Lagrangian of Lemma 1 all range over this class.
• An SFPE is jointly measurable in $(\theta,\alpha)$, so Theorem 1 must produce a measurable strategy.
• $q^\mu$ is the supremum over bids of p. 7, not the closed form of p. 8. $\sigma^\mu_\alpha$ has an explicit branch for $H^\mu_\alpha(x)=0$.
• Argmins are stated as membership plus IsMinOn, over $t\ge0$ in Propositions 1–2 and over $[0,\omega/B_{\min}]$ in Lemma 5 and $\ell^\mu$, as printed.
• $V(u,\Omega)$ takes values in EReal, with Euclidean $\|\phi(x)\|\le1$ and test fields supported in $\Omega$; $L_1(\Theta)$ is with respect to Lebesgue measure. Lemma 4 is stated on the image of $\mathcal X_0$ in Lp ℝ 1 (volume.restrict Θ), in its norm topology.

A formalization in which $q^\mu$ is defined by its closed form, in which non-integrable payments count as zero, or in which the strategy need not be measurable would make the milestones easier without proving the paper's theorem; these readings are excluded by the definitions above.

A complete development needs: first price equilibrium bids for general atomic distributions with reserves; measurability of parametric integrals; a duality argument for one-dimensional Lagrangian relaxations; multivariate bounded variation and its compact embedding in $L_1$ of a box; and the Kakutani–Fan–Glicksberg theorem in a locally convex space. The bounded-variation and fixed-point parts are reusable beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• S. R. Balseiro, C. Kroer, R. Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2023.4719
• S. R. Balseiro, O. Besbes, G. Y. Weintraub, Repeated Auctions with Budgets in Ad Exchanges: Approximations and Design, Management Science 61(4), 2015. https://doi.org/10.1287/mnsc.2014.2022
• V. Conitzer, C. Kroer, E. Sodomka, N. E. Stier-Moses, Multiplicative Pacing Equilibria in Auction Markets, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2167
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., CRC Press, 2015.