All missions

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors, choosing the $k$ that minimize the residual sum of squares. Mixed-integer optimization made it computable at moderate scale (Bertsimas, King & Mazumder, 2016), which reopened the statistical question of when it should be used. Empirical comparisons (Hastie, Tibshirani & Tibshirani, 2020) found that best subsets predicts poorly when the signal-to-noise ratio (SNR) is low: by fitting the noise exactly within its chosen support it overfits, and shrinkage methods such as the Lasso do better there.

Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty to the cardinality-constrained problem. Their Theorem 2 quantifies the effect of an $\ell_2$ (Euclidean-norm) penalty: it proves prediction-error bounds that are linear in the penalty level and therefore remain small in the low-SNR regime where best subsets fails. This mission formalizes that theorem.

Setting

The data follow the model

$$y=f^*+\epsilon,$$

where $y,f^*,\epsilon\in\mathbb R^n$, $f^*$ is an unknown deterministic mean and $\epsilon$ is a noise vector (in the paper, with independent $N(0,\sigma^2)$ entries, $\sigma>0$). The design $X\in\mathbb R^{n\times p}$ is deterministic and its columns have unit Euclidean norm. Write $\|\cdot\|$ for the Euclidean norm, $\|\beta\|_0$ for the number of nonzero coordinates of $\beta$, and $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$.

For a model size $k$ and a penalty level $\lambda\ge0$, the $\ell_2$-regularized best-subsets estimator is any solution

$$\hat\beta_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|\quad\text{s.t.}\quad\|\beta\|_0\le k.$$

The penalty is the norm $\|\beta\|$, not its square, and the loss carries no factor $1/2$. The quantity of interest is the prediction error $\|f^*-X\hat\beta_2\|^2$.

The minimal $s$-sparse eigenvalue of $X$ is $\gamma_s=\min_{u\neq0,\,u\in B_0(s)}\|Xu\|/\|u\|$. For $u\in\mathbb R^p$, $u^\sharp_1\ge\dots\ge u^\sharp_p$ is the non-increasing rearrangement of $|u_1|,\dots,|u_p|$. Given $\delta_0\in(0,1]$, three noise events are sets of noise vectors:

$$\mathcal E_s=\big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\big\},$$ $$\mathcal F=\Big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\max\Big(\textstyle\sum_{j=1}^p u^\sharp_j\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|\Big),\ \forall u\in\mathbb R^p\Big\},$$ $$\mathcal G_s=\big\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\big\}.$$

The paper's Theorem 1 shows these events have high probability; Theorem 2 is a deterministic statement on each of them. The symbol $\lesssim$ means "up to a positive universal multiplicative constant", one that does not depend on $n,p,k,X,f^*,\sigma,\lambda$ or $\delta_0$.

Formalization targets

Goal: Theorem 2 (p. 14)

Let $1\le k\le p$.

(A) Slow rate. If $\lambda\ge[8+2\sqrt2]\sigma\sqrt{2k\log(ep/k)}$, then on $\mathcal E_{2k}$

$$\|f^*-X\hat\beta_2\|^2\le\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+2\lambda\|\beta\|\big],$$

and on $\mathcal F$

$$\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+\lambda\|\beta\|\big]+\sigma^2\log(1/\delta_0).$$

(B) Fast rate. For every $\lambda\ge0$, on $\mathcal G_{2k}$

$$\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\|f^*-X\beta\|^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2+\sigma^2\log(1/\delta_0).$$

The bounds hold for every minimizer $\hat\beta_2$ and for misspecified models: $f^*$ need not lie in the column span of $X$.

Milestones

The steps of the printed proof (Supplement B.2, pp. 39–40), in the order the proof uses them: the basic inequality (29); the bound (30) on $\mathcal E_{2k}$ and its consequence (31); the dichotomy on $\mathcal F$, where (30) implies (31) and (32) implies (33); the elementary inequality (34); the basic inequality on $\mathcal G_{2k}$ (p. 40); and the bound of $\lambda\|\beta-\hat\beta_2\|$ through $\gamma_{2k}$ (p. 40).

Significance

The result. The slow-rate bound of part (A) is linear in $\lambda$. When the signal $\|\beta^*\|$ is small compared with $\sigma$, the term $\lambda\|\beta^*\|$ is smaller than the rate $\sigma^2 k\log(ep/k)$ that best subsets attains, and the paper's Theorem 4 shows that in this regime the prediction error of best subsets is at least of order $\sigma^2\gamma_k^2k\log(ep/k)$. Together the two results explain the empirical finding that shrinkage helps best subsets at low SNR. Part (B) shows nothing is lost at high SNR: the fast rate is the minimax rate $\sigma^2k\log(ep/k)$ over $k$-sparse vectors plus the shrinkage term $\gamma_{2k}^{-2}\lambda^2$. Combined with Theorem 1, the bounds give the high-probability statements of the paper's Corollaries 1 and 3.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist. The mission produces a checked deterministic core: once the events are granted, every constant ($8+2\sqrt2$, the factor $2\lambda$, the threshold $2k\log(ep/k)$) is verified exactly. Together with the companion mission on Theorem 1 it would yield fully checked high-probability oracle inequalities for a cardinality-constrained estimator, which no current formal library contains.

Difficulty

Every step is elementary, but the bookkeeping is exact. The obvious reading "insert the event's inequality into (29)" does not by itself work on $\mathcal F$: the event's right-hand side is a maximum of a sorted weighted sum and a prediction-norm term, and the first branch has to be compared with $\sqrt{2k\log(ep/k)}\,\|u\|$ for the $2k$-sparse difference $u=\hat\beta_2-\beta$, including when $2k$ exceeds $p$. That comparison is a combinatorial estimate on sorted sums, not a substitution. On $\mathcal G_{2k}$, the penalty difference $\lambda(\|\beta\|-\|\hat\beta_2\|)$ is not controlled by the event at all and has to be converted into prediction errors through $\gamma_{2k}$. In both parts the final constant must not depend on $k$, $p$ or $\delta_0$.

Formalization scope

All objects are explicit Lean definitions in the namespace SubsetShrink.L2:

• vectors are functions on Fin n and Fin p with 0-based indices, and $X$ is a real Matrix (Fin n) (Fin p);
• the Euclidean norm, $\|\cdot\|_0$ and the inner product are explicit finite sums, since Mathlib's norm on Fin m → ℝ is the sup norm;
• $\sum_j u^\sharp_j\sqrt{\log(2p/j)}$ is encoded as a maximum over permutations, which equals the sorted sum by the rearrangement inequality;
• $\gamma_s$ is a real infimum over the nonzero vectors of $B_0(s)$, a nonempty set when $p,s\ge1$.

The model consists of $X$ with unit columns, $f^*$, $\epsilon$, $\sigma>0$ and $y=f^*+\epsilon$. The estimator is a predicate that every minimizer satisfies; no minimizer is chosen and existence is not assumed. "On the event" is a hypothesis that the noise vector satisfies the event's printed inequality, so no probability measure appears. $\mathcal G_{2k}$ is the event as printed on p. 13; the correction of its probability bound belongs to the mission on Theorem 1 and does not affect these deterministic statements.

Committed conventions:

• each $\lesssim$ is an existential constant $C>0$ quantified before all other data;
• an infimum over $B_0(k)$ is stated as a bound for every $\beta\in B_0(k)$;
• $\delta_0\in(0,1]$ is universally quantified;
• the model size satisfies $1\le k\le p$.

Part (B) assumes $\gamma_{2k}>0$ or $\lambda=0$. When $\gamma_{2k}=0<\lambda$ the paper's bound is vacuous ($\gamma_{2k}^{-2}\lambda^2=+\infty$), but Lean's $0^{-1}=0$ would turn it into a false claim.

A formalization that lets the constant depend on $k$, $p$ or $\delta_0$, fixes a particular minimizer, weakens an event (for example drops "for all $u\in B_0(s)$"), or computes the infimum as a real ⨅ over an unbounded set would trivialize the theorem and is ruled out.

Not formalized here: the probability bounds of Theorem 1, the $\ell_1$-penalized Theorem 3, the lower bound of Theorem 4, the data-driven choice of $k$ (Theorem 5), and the corollaries and numerical experiments. These are separate missions or follow-ups. Contributions of reusable lemmas (the rearrangement bound for the sorted sum, properties of $\gamma_s$, the elementary absorption inequality (34)) are welcome.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
• 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

Motivation

Best subset selection fits a linear model $y\approx X\beta$ using at most $k$ of the $p$ available features: it minimizes the residual sum of squares subject to the sparsity constraint $\|\beta\|_0\le k$, where $\|\beta\|_0$ counts the nonzero coordinates of $\beta$. Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) show that best subsets overfits when the signal-to-noise ratio is low, and propose adding a shrinkage penalty $\lambda\|\beta\|_q$ with $q\in\{1,2\}$ to the same constrained problem. Their statistical results (oracle inequalities, a lower bound for best subsets, a BIC-type choice of $k$) are the subject of the companion missions II–VI of this series.

The estimator is a mixed-integer program. To compute it in practice, and to warm-start the mixed-integer solver that certifies optimality, the paper uses a discrete first-order (DFO) method: a proximal-gradient iteration in which the proximal step is a projection-like operation onto the set of $k$-sparse vectors with a norm penalty. The method descends from iterative hard thresholding (Blumensath & Davies, 2009), from proximal gradient methods for composite problems (Nesterov, 2013), and from the discrete first-order algorithms of Bertsimas, King and Mazumder (Annals of Statistics, 2016). This mission formalizes the paper's convergence guarantee for it, Proposition 2.

Setting

Vectors live in $\mathbb R^p$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. Write $\|\beta\|_0$ for the number of nonzero coordinates and $\|\beta\|_1=\sum_i|\beta_i|$. For $q\in\{1,2\}$ the penalty is the norm $\|\beta\|_q$ itself, not its $q$-th power.

Let $f:\mathbb R^p\to\mathbb R$ be a differentiable convex function whose gradient is $L_0$-Lipschitz:

$$\|\nabla f(\beta)-\nabla f(\alpha)\|_2\le L_0\|\beta-\alpha\|_2\qquad\forall\,\beta,\alpha .$$

The motivating case is $f(\beta)=\tfrac12\|y-X\beta\|_2^2$ with $L_0=\sigma_{\max}(X)^2$. The composite problem (7) is

$$\text{minimize}\quad F(\beta):=f(\beta)+\lambda\|\beta\|_q\quad\text{s.t.}\quad\|\beta\|_0\le k .$$

For $L\in\mathbb R$ the quadratic model of $f$ around $\alpha$ is

$$Q_L(\beta;\alpha)=f(\alpha)+\langle\nabla f(\alpha),\beta-\alpha\rangle+\tfrac L2\|\beta-\alpha\|_2^2 ,$$

and the thresholding operator is the set of minimizers

$$\mathrm S(u;k;\mu\ell_q)=\operatorname*{arg\,min}_{\|b\|_0\le k}\ \tfrac12\|b-u\|_2^2+\mu\|b\|_q ,$$

which can contain several points when the $|u_j|$ have ties. A DFO sequence with constant $L>0$ starts at a $k$-sparse $\beta^{(1)}$ and, for $m\ge1$, picks any

$$\beta^{(m+1)}\in\mathrm S\Big(\beta^{(m)}-\tfrac1L\nabla f(\beta^{(m)});\,k;\,\tfrac\lambda L\ell_q\Big).$$

Formalization targets

Goal: Proposition 2 (p. 10)

Assume in addition $f\ge0$ and $\lambda\ge0$. For every DFO sequence:

(a) if $L\ge L_0$, then $F(\beta^{(m)})$ is non-increasing in $m\ge1$ and converges to some $F^*\ge0$;

(b) if $L>L_0$, then for every $M\ge1$

$$\min_{1\le m\le M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2\le\frac{2\big(F(\beta^{(1)})-F^*\big)}{M(L-L_0)} .$$

The statement holds for any $f$ of the stated class and any choice in the set-valued operator; nothing about least squares is assumed.

Milestones (proof in Supplement A.1, p. 35)

1. (9), p. 8: $f(\beta)\le Q_L(\beta;\alpha)$ for all $\alpha,\beta$ and every $L\ge L_0$, the bound the paper takes from Nesterov (2004).
2. (20)–(21), p. 35: completing the square, $Q_L(\eta,\beta)+\lambda\|\eta\|_q=\tfrac L2\|\eta-(\beta-\tfrac1L\nabla f(\beta))\|_2^2-\tfrac1{2L}\|\nabla f(\beta)\|_2^2+f(\beta)+\lambda\|\eta\|_q$. Hence the minimizers of $Q_L(\cdot,\beta)+\lambda\|\cdot\|_q$ over $\|\eta\|_0\le k$ are exactly $\mathrm S(\beta-\tfrac1L\nabla f(\beta);k;\tfrac\lambda L\ell_q)$.
3. (22), p. 35: for $\|\beta\|_0\le k$ and $\hat\eta$ in that set, $F(\beta)\ge\tfrac{L-L_0}2\|\hat\eta-\beta\|_2^2+F(\hat\eta)$.
4. (23) and the next display, p. 35: summed over $m=1,\dots,M$,

$$F(\beta^{(1)})-F(\beta^{(M+1)})\ge\tfrac{M(L-L_0)}2\min_{m\le M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2 .$$

5. Proposition 1, p. 9 (companion, not used by the goal): every $\hat\beta\in\mathrm S(u;k;\lambda\ell_q)$ keeps the $k$ largest entries of $u$ in magnitude, for some ordering of ties. For $q=1$ it soft-thresholds them coordinatewise, and for $q=2$ it shrinks them as a group by $\max\{\tau_u-\lambda,0\}/\tau_u$, with $\tau_u$ the norm of those $k$ entries.

Significance

Proposition 2 is what makes the DFO method a sound component of the paper's computational pipeline. The objective values never increase, so every iterate is a feasible point at least as good as the warm start. Part (b) says that the step length $\|\beta^{(m+1)}-\beta^{(m)}\|_2^2$ is small after $O(1/\epsilon)$ iterations. A point whose step vanishes is a fixed point of the update, which the paper calls a first-order stationary point (Definition 1). The stopping rule of the algorithm ($\|\beta^{(m+1)}-\beta^{(m)}\|_2^2\le\tau$) is therefore reached in at most $\lceil 2(F(\beta^{(1)})-F^*)/(\tau(L-L_0))\rceil$ steps.

The result is proved in the paper, in half a page that defers its central inequality (22) to Proposition 6 of Bertsimas, King & Mazumder (2016). It has not been formalized. A machine-checked version produces three reusable pieces: a descent lemma for functions with Lipschitz gradient on $\mathbb R^p$, the variational characterization of the sparse proximal step, and a sufficient-decrease-to-rate argument for any descent method. These are the same pieces that iterative hard thresholding, proximal gradient, and block-coordinate methods for $\ell_0$ problems need.

Difficulty

The difficulty is moderate, and it lies in the infrastructure rather than in any single step. The descent lemma (9) needs the fundamental theorem of calculus along a segment for a function on a Euclidean space, combined with the Lipschitz bound on the gradient. The feasible set $\{\|\beta\|_0\le k\}$ is not convex, so no convex-analysis argument (subgradient optimality, firm nonexpansiveness of a proximal map) applies to the thresholding step. Inequality (22) must instead be obtained by comparing the minimizer $\hat\eta$ with the feasible competitor $\beta$ itself, which is why the hypothesis $\|\beta\|_0\le k$ appears. Part (a) also needs a lower bound on $F$ for its limit to exist and be nonnegative, which the general class of $f$ does not provide on its own.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p), the gradient is Mathlib's gradient f, and coordinates are $0$-based. Membership in $\mathrm S(u;k;\mu\ell_q)$ is a predicate: feasibility plus minimality against every $k$-sparse competitor. No selection from the set is fixed, and existence of minimizers is not assumed. A DFO sequence is any β : ℕ → ℝᵖ satisfying the update for every $m\ge1$, indexed from $1$ as printed. The stopping rule and the support-restricted polishing Step 2 are not part of it. The penalty is $\|\cdot\|_1$ for $q=1$ and the Euclidean norm for $q=2$, and every theorem assumes $q\in\{1,2\}$ and $k\ge1$. The minimum over $1\le m\le M$ is a finite infimum over a nonempty index set.

Three hypotheses are added to Proposition 2 as printed, each disclosed in the item. The proof's claim "$F(\beta)\ge0$" is false for a general convex $f$ with Lipschitz gradient ($f(\beta)=-\beta_1$ sends $F$ to $-\infty$), so $f\ge0$ and $\lambda\ge0$ are assumed. The update divides by $L$, and $L\ge L_0$ allows $L=0$, so $L>0$ is assumed. "Decreasing" is read as non-increasing. Convexity of $f$ is kept as in the paper's setting (7)–(8), though only the gradient bound is used. Proposition 1 is stated with an existential ordering: for a fixed sorting permutation the printed claim fails under ties.

The statement cannot be trivialized by restricting $f$ or the run. The goal quantifies over every $f$ of the class and every sequence obeying the update, the limit $F^*$ in (b) is the actual limit of the objective values, and the rate holds for every $M\ge1$. Not formalized here: the mixed-integer formulations, the continuation and local-search heuristics of §2.4, Definition 1, and the paper's statistical results (missions II–VI). Contributions of reusable infrastructure, such as a general descent lemma or a lemma turning summed decrease into a $1/M$ rate, are welcome as separate theorems.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research 71(1), 2023. 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
• Y. Nesterov, Gradient Methods for Minimizing Composite Functions, Mathematical Programming 140, 2013. https://doi.org/10.1007/s10107-012-0629-5
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• T. Blumensath, M. E. Davies, Iterative Hard Thresholding for Compressed Sensing, Applied and Computational Harmonic Analysis 27(3), 2009. https://doi.org/10.1016/j.acha.2009.04.002

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.

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Optimal choice probability

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Certify the separation exponent $\alpha\ge2.000252407$ using OpenAI's construction. Sensitivity $s(f)$ counts individual bit flips that change the output; block sensitivity $bs(f)$ counts disjoint sensitive blocks. Both are maximized over inputs. The notation $bs(f,x)$ fixes one input, and $0$ denotes the all-zero input.

The goal requires arbitrarily large sensitivity and $bs(f)\ge s(f)^{2.000252407-\varepsilon}$ for every $\varepsilon>0$. OpenAI's depth-nine seed, with $M=9^{10}$, supplies a slightly larger exponent; the displayed decimal must be certified exactly.

This mission is the campaign's foundation. Its central reusable milestone turns a finite certificate $s(f)\le A$, $bs(f,x)\ge B$, $A,B>1$, and $A^a\le B$ into the asymptotic claim at exponent $a\ge0$. Normalization and sensitivity growth are proof obligations. Later missions import this theorem and the shared definitions.

OpenAI's quantitative separation is already proved on Prove2Me. This mission certifies the numerical exponent and the reusable bridge; its goal remains Open until all required proofs are accepted.

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 12

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

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

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

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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