All missions

Motivation

Digital services are paid for with attention: an ad-financed platform earns more the longer its users stay. Policy reports on digital markets (Crémer, de Montjoye and Schweitzer, 2019; the U.K. Digital Competition Expert Panel, 2019; Scott Morton et al., 2019) worry that such firms degrade their services with features that capture attention at the user's expense, and they usually recommend more competition. Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16; Management Science, 2023), ask whether competition actually helps. Their answer depends on how scarce attention is. When attention is scarce, platforms compete by making their services more addictive rather than better, and a monopoly serves the consumer better than a duopoly. This mission formalizes that comparison, the paper's headline result, together with the two equilibrium characterizations it rests on.

Setting

There are $K$ platforms and a single consumer. Each platform $k$ chooses an addictiveness $d_k \ge 0$. The consumer observes $d = (d_1, \dots, d_K)$, joins a set $J$ of platforms and allocates attention $a_k \ge 0$ to each $k \in J$. She receives $0$ if $J = \emptyset$, and otherwise

$$\sum_{k\in J} u(a_k, d_k) - C\Big(\sum_{k\in J} a_k\Big),$$

subject to the attention cap $\sum_{k\in J} a_k \le \overline{A}$, where $\overline{A} \in \mathbb{R}_+ \cup \{\infty\}$. Platform $k$ earns the attention $a_k$ if the consumer joins it and $0$ otherwise.

The service utility $u(a, d)$ is twice differentiable, strictly increasing and concave in attention $a$, and strictly decreasing in $d$. The marginal utility $u_1(a, d) = \partial u/\partial a$ is strictly increasing in $d$, so a more addictive service is worse to join but harder to stop using. There is some $d$ at which no amount of attention makes the service worth joining, and $u(0,0) \ge 0$. The attention cost $C : \mathbb{R}_+ \to \mathbb{R}_+$ is strictly increasing, convex and twice differentiable, with $\lim_{a\to0}[u_1(a,0) - C'(a)] > 0$. These are Assumptions 1 and 2 of the paper.

Platforms choose addictiveness simultaneously, and then the consumer chooses $J$ and $a$. The solution concept is pure-strategy subgame perfect equilibrium: the consumer chooses optimally at every profile $d$, and no platform gains by changing its own $d_k$. A monopolist ($K = 1$) breaks ties in the consumer's favour. Consumer surplus is the consumer's payoff in the equilibrium outcome.

The monopoly benchmark uses three quantities. The first is $A(d) = \arg\max_{A\ge0} u(A,d) - C(A)$, the consumer's attention on one platform when there is no cap. The second is $d^A(\overline{A}) = \min\{d \in [0,\infty] : A(d) \ge \overline{A}\}$, the lowest addictiveness at which she exhausts her attention. The third is $d^P(\overline{A})$, the addictiveness at which her best capped payoff from one platform falls to zero. Under competition, $A_K(d) = \arg\max_{A\in[0,\overline{A}]} K\,u(A/K, d) - C(A)$ is the total attention she spends on $K$ platforms of common addictiveness $d$.

Formalization targets

Goal: Proposition 3 (monopoly versus duopoly)

Let $\overline{A}^M$ be the least cap from which on monopoly consumer surplus is zero. For every monopoly equilibrium with addictiveness $d^M$ and every duopoly equilibrium with $(d_1, d_2)$:

$$0 < \overline{A} \le A(0) \;\Longrightarrow\; d^M < d_1,\ d^M < d_2,\ CS^{\mathrm{duo}} < CS^{\mathrm{mono}},$$ $$\overline{A} \ge \overline{A}^M \;\Longrightarrow\; d_1 \le d^M,\ d_2 \le d^M,\ CS^{\mathrm{mono}} \le CS^{\mathrm{duo}}.$$

The proposition is silent about intermediate caps, and so is the goal.

Milestones

1. Proposition 1 (monopoly). The monopolist sets $\min\{d^A(\overline{A}), d^P(\overline{A})\}$, which is increasing in $\overline{A}$. The consumer's payoff rises on $[0, A(0)]$, falls on $[A(0), \overline{A}^M]$ and is zero from some $\overline{A}^M > A(0)$ on.
2. Lemmas B.1–B.4. These are comparative statics of the consumer's problem: the tangent intercept $u(x) - xu'(x)$ is increasing, the value of spreading attention over $y$ platforms is concave in $y$, and the incremental gain from one more platform falls with the addictiveness and the number of the platforms already joined.
3. Step 1 of the proof of Proposition 2. For $K \ge 2$ there is a unique $d^* > 0$ solving the indifference condition (3) between joining $K$ and $K - 1$ platforms.
4. Proposition 2 (competition). For $K \ge 2$, every platform chooses $d^*$ in the unique equilibrium.

Significance

Proposition 3 separates two effects of competition. Business stealing pushes duopolists to raise addictiveness, because a more addictive service captures a larger share of a fixed attention budget. Competition for participation restrains them, because a consumer can drop a platform and spend her time on its rival. When attention is scarce the first effect dominates and the consumer is strictly worse off under duopoly. When it is abundant the monopolist extracts the whole surplus and duopoly cannot be worse. The result is the basis of the paper's policy discussion: digital curfews and the comparison between the equilibrium and the joint-profit outcome (Propositions 4 and 6). Propositions 1 and 2 are used throughout the paper.

The paper proves these results on paper. No machine-checked proof exists. A formal proof would check several delicate points. One is the role of the monopolist's tie-break, without which every $d \in [0, d^P]$ is a monopoly equilibrium when attention is scarce. Another is that the uniqueness argument for the duopoly needs a consumer who best-responds off the equilibrium path. The appendix also asserts a few claims without argument or slightly too strongly, recorded below. Verifying them is part of the work.

Difficulty

The obvious argument for Proposition 3 compares equilibrium payoffs through the closed forms of Figure 3, and closed forms do not exist in general. Every object is defined by an optimization problem whose maximizer has no formula. The value functions are concave but need not be differentiable, so the envelope-theorem steps of Appendix B cannot be applied as written; they have to be replaced by monotone comparative statics or one-sided derivatives. Proposition 2's uniqueness is the hardest part. It rules out asymmetric equilibria by a deviation argument that controls which platforms the consumer joins after a small change in one platform's addictiveness (Lemma B.4). It also needs the consumer's whole strategy, not only her choice on the path.

Formalization scope

Platforms are Fin K; the paper's platform 1 is the index 0. Addictiveness and attention are real numbers restricted to $[0,\infty)$, and only the values of $u$ and $C$ there matter. The cap $\overline{A}$ is an extended nonnegative real (ℝ≥0∞), so $\overline{A} = \infty$ is a genuine case and "$\overline{A} \ge \overline{A}^M$" includes it. Derivatives on $[0,\infty)$ are one-sided at $0$.

The definition file states the paper's Assumptions 1–2 as printed and adds disclosed pins:

• $u(\cdot, d)$ is strictly concave. The page says "concave", but Lemma B.1 needs strict concavity and Lemma B.2 applies Lemma B.1 to $u(\cdot,d)$.
• $C(0) = 0$. Without it $d^P$ need not exist.
• The uncapped consumer problem has an optimal attention profile for every profile and every nonempty $J$. The page (p. 6) assumes this for $\overline{A} = \infty$, and $A(d)$ presupposes it.
• $\overline{A} > 0$ where the result needs it: Proposition 1's characterization, Step 1, Proposition 2 and the first half of Proposition 3. At $\overline{A} = 0$ every profile is an equilibrium.

"Increasing" and "decreasing" are weak unless the page says "strictly". The one exception is "higher addictiveness" in the first half of Proposition 3, which is stated strictly because the proof gives $d^M = 0 < d^*$.

Three statements differ from the printed text. Lemma B.2's "$V^*$ is strictly concave" is false on the paper's own Figure 3 instance and is stated as concavity. The strict clause of Lemma B.4 fails when $C$ is linear and is not posed. The derivative claims of Lemmas B.2–B.4 are stated as decreasing differences of value functions.

Several trivializing formalizations are excluded:

• An equilibrium requires the consumer to best-respond at every profile, not only at the equilibrium one.
• The tie-break is part of the monopoly equilibrium.
• Equilibria exist (Propositions 1 and 2 assert existence), and a sanity file checks the standing hypotheses on $u(a,d) = 1 - e^{-(a-d)}$, $C(a) = a/2$.
• No value function is a real supremum; maxima enter through maximizers.

Not posed: Proposition 4 and later results, and the side models of Remarks 2–3. A complete development needs maximizers of concave problems on intervals and simplices, monotone comparative statics (Topkis, Milgrom–Shannon), and envelope arguments for concave value functions. These pieces are reusable well beyond this paper, and contributions of them as separate lemmas are welcome.

Selected references

• S. Ichihashi and B.-C. Kim, Addictive Platforms, Bank of Canada Staff Working Paper 2022-16, 2022. https://doi.org/10.34989/swp-2022-16. Published in Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4392
• P. Milgrom and I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• J. Crémer, Y.-A. de Montjoye and H. Schweitzer, Competition Policy for the Digital Era, report for the European Commission, 2019. https://doi.org/10.2763/407537

Motivation

Clustering points drawn from a mixture of well-separated distributions is a basic problem of unsupervised learning. Practical data sets also contain outliers, points that belong to no cluster and may be placed anywhere. Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) propose a robust spectral clustering algorithm. It thresholds a Gaussian kernel matrix through a linear program, then applies spectral clustering to the result, and they prove that its error decays exponentially in the squared signal-to-noise ratio when the outliers, placed arbitrarily, are a small fraction of the points. The authors report that their bound is tighter than those obtained for related semidefinite relaxations, for example by Mixon, Villar and Ward (arXiv:1602.06612), which use a reference matrix in a similar way (pp. 10–11). This mission formalizes the first of the paper's two main results: the estimation error of the thresholded kernel matrix.

Setting

There are $N = n + m$ points in $\mathbb R^d$: $n$ inliers and $m$ outliers. Each inlier $i$ has a label $\varphi_i \in \{1,\dots,r\}$, and the clusters are $\mathcal C_k = \{i : \varphi_i = k\}$ with sizes $n_k$ and $n_{\min} = \min_k n_k$. The inlier observation is

$$y_i = \mu_{\varphi_i} + \xi_i ,$$

where $\mu_1,\dots,\mu_r$ are the cluster centres and the noise vectors $\xi_i$ are independent, identically distributed within each cluster, and sub-gaussian with parameter $\sigma_{\varphi_i}$: for every $\nu \in \mathbb R^d$, $\mathbb E[e^{\nu^\top\xi_i}] \le e^{\sigma_{\varphi_i}^2\|\nu\|^2/2}$ (Definition 3). The outliers $z_1,\dots,z_m$ are arbitrary random vectors, with no independence or distributional assumption. Write $\Delta_{kl} = \|\mu_k - \mu_l\|$, $\Delta_{\min} = \min_{k\ne l}\Delta_{kl}$ and $\sigma_{\max} = \max_k\sigma_k$.

The algorithm forms the Gaussian kernel $K_{ij} = \exp(-\|y_i - y_j\|^2/2\theta^2)$ over all $N$ points and solves the Robust-LP

$$\max_X\ \langle K - \gamma E_N, X\rangle \quad\text{subject to}\quad 0 \le X_{ij} \le 1 ,$$

where $\langle A, B\rangle = \sum_{ij}A_{ij}B_{ij}$ and $E_N$ is the all-ones matrix. Its solution has the closed form $\hat X_{ij} = 1$ if $K_{ij} > \gamma$ and $0$ otherwise. The true clustering matrix $X^0$ has $X^0_{ij} = 1$ exactly when $i$ and $j$ are inliers with the same label. The error is measured in the entrywise norm $\|A\|_1 = \sum_{ij}|A_{ij}|$, and $A_{\mathcal I}$ denotes the inlier block.

Formalization targets

Goal: Theorem 1 (with corrected thresholds)

Fix $\kappa > 0$ and $\upsilon \in (0,1)$, and set $\theta = \kappa\Delta_{\min}$, $\tau_{\mathrm{in}} = e^{-5\Delta_{\min}^2/64\theta^2}$, $\tau_{\mathrm{out}} = e^{-\Delta_{\min}^2/4\theta^2}$ and $\gamma = \upsilon\tau_{\mathrm{in}} + (1-\upsilon)\tau_{\mathrm{out}}$. There are constants $C, C', C'' > 0$, depending only on $\kappa$ and $\upsilon$, such that if $n_{\min} > r$, $\Delta_{\min} \ge 8\sigma_{\max}\sqrt d$ and $m < n$, then with probability at least $1 - 2r/n_{\min}$,

$$\|\hat X_{\mathcal I} - X^0_{\mathcal I}\|_1 \le Cn^2\max\Big\{e^{-\Delta^2_{\min}/64\sigma^2_{\max}}, \frac{\log n_{\min}}{n_{\min}}\Big\}$$

and

$$\frac{\|\hat X - X^0\|_1}{\|X^0\|_1} \le C'r\,e^{-\Delta^2_{\min}/64\sigma^2_{\max}} + C''r\max\Big\{\frac{\log n_{\min}}{n_{\min}}, \frac{m}{n}\Big\}.$$

The constants are left existential, as on the page.

Milestones

The milestones follow the structure of the paper's proof:

• the closed form of $\hat X$ (§3);
• Lemmas 1–3, which compare Robust-LP with a reference problem built from the reference matrix $R$ of display (6);
• the counting bound (E.2);
• the sub-gaussian tail bounds (E.5), (E.6), (E.7)–(E.8) and (E.9)–(E.10);
• the Bernstein inequalities for one- and two-sample U-statistics (E.11) and (E.14), and their consequences (E.13) and (E.15);
• the threshold gap (E.18).

Significance

Theorem 1 is the quantitative core of the paper. It says that thresholding a Gaussian kernel at a level between two explicit values recovers the cluster structure among the inliers up to an error that is exponentially small in $\Delta^2_{\min}/\sigma^2_{\max}$, plus a sampling term of order $\log n_{\min}/n_{\min}$, whatever the outliers do. The paper's Theorem 2 feeds this bound into Davis–Kahan perturbation theory to bound the fraction of misclassified points after spectral rounding, and Proposition 2 uses it to identify the outliers.

Formalizing it produces more than the theorem. As printed, Theorem 1 is false: the kernel uses $2\theta^2$ while the thresholds use $\theta^2$, a factor-two mismatch that the proof silently drops. A mechanically checked statement settles the corrected thresholds. The proof also rests on three cited probabilistic results that are not proved in the paper and are not in Mathlib: the Hsu–Kakade–Zhang tail bound for quadratic forms of sub-gaussian vectors, and Bernstein inequalities for one- and two-sample U-statistics (the two-sample version is asserted "following the arguments" of earlier work, with no proof). None of these results has a machine-checked proof at present.

Difficulty

The deterministic part (Lemmas 1–3, (E.2), (E.18)) is elementary linear algebra on $[0,1]$-matrices. The difficulty is probabilistic. The kernel entries $K_{ij}$ are not independent: each point appears in $n - 1$ entries. So the natural first idea, a Chernoff or Hoeffding bound on the number of threshold violations treated as a sum of independent indicators, does not apply. The paper handles the dependence by writing the counts of violations as U-statistics and invoking Bernstein-type bounds for them. Those bounds need Hoeffding's representation of a U-statistic as an average of sums of independent terms, which is not available in Mathlib. A second obstacle is the Hsu–Kakade–Zhang inequality: the norm of a sub-gaussian vector whose coordinates may be dependent concentrates at the scale $d$, not $d^2$, and the coordinate-independent Hanson–Wright inequality does not give it.

Formalization scope

• Points and labels. Points are indexed by Fin n ⊕ Fin m (inliers, then outliers) and vectors live in EuclideanSpace ℝ (Fin d). The labels $\varphi$ are fixed. The paper draws them from a multinomial distribution, but its proof conditions on them, and $n_{\min}$ appears in the probability bound.
• Sub-gaussian parameter. $\sigma_k$ is the Definition 3 parameter, encoded through Mathlib's HasSubgaussianMGF of every projection $\nu^\top\xi$. The proof uses this parameter, not the "largest eigenvalue of the second moment matrix" mentioned in §2.2.
• Minima and maxima. $\Delta_{\min}$, $n_{\min}$, $\sigma_{\max}$ and $\tau_{\mathrm{out}}$ are finite minima or maxima over nonempty index sets; $r \ge 2$ and $d \ge 1$ are hypotheses.
• Corrections and additions. The thresholds are corrected from the printed $e^{-5\Delta^2_{\min}/32\theta^2}$ and $e^{-\Delta^2_{kl}/2\theta^2}$ to $e^{-5\Delta^2_{\min}/64\theta^2}$ and $e^{-\Delta^2_{kl}/4\theta^2}$, which are the values for which (E.7)–(E.10) hold. "$\theta = \Theta(\Delta_{\min})$" is read as $\theta = \kappa\Delta_{\min}$, as on p. 42. $m < n$ is added for (12), as the proof uses it at (E.20).
• Probability. The failure event's outer measure is bounded, and outliers need not be measurable.
• Ruling out trivial statements. The goal does not mention the reference matrix, the corruption counts, U-statistics or $\rho_{\min}$, and its constants are quantified before every model datum. With $C$ fixed, letting $n_{\min}$ and the signal-to-noise ratio grow forces $\|\hat X_{\mathcal I} - X^0_{\mathcal I}\|_1/n^2 \to 0$, so (11) is not implied by the trivial bound $\|\hat X_{\mathcal I} - X^0_{\mathcal I}\|_1 \le n^2$.
• Reusable work. Proofs of the sub-gaussian tail bounds and the U-statistic Bernstein inequalities are welcome as standalone developments. They are reusable well beyond this mission, for example in kernel methods, random geometric graphs and two-sample testing.

Selected references

• P. R. Srivastava, P. Sarkar, G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, Operations Research 71(1), 2023; arXiv:1912.07546v3, 2021. https://arxiv.org/abs/1912.07546
• D. Hsu, S. Kakade, T. Zhang, A tail inequality for quadratic forms of subgaussian random vectors, Electronic Communications in Probability 17, 2012. https://doi.org/10.1214/ECP.v17-2079
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
• M. A. Arcones, A Bernstein-type inequality for U-statistics and U-processes, Statistics & Probability Letters 22(3):239–247, 1995 (as cited in arXiv:1912.07546v3, reference list). https://arxiv.org/abs/1912.07546
• Y. Pitcan, A note on concentration inequalities for U-statistics, arXiv:1712.06160, 2017. https://arxiv.org/abs/1712.06160
• D. G. Mixon, S. Villar, R. Ward, Clustering subgaussian mixtures by semidefinite programming, Information and Inference 6(4), 2017; arXiv:1602.06612. https://arxiv.org/abs/1602.06612

Why out-of-sample utility risk matters

A portfolio chosen from historical returns can look attractive in the data used to construct it and deliver a different result when evaluated under the population return distribution. The gap is driven by estimation error in both the mean return and covariance matrix. A mean of future utility values describes average performance, but it does not describe how much that utility varies across possible estimation samples. Lassance, Martín-Utrera and Simaan study this variation for a portfolio that blends an estimated mean-variance choice with an estimated global-minimum-variance choice. Their closed-form variance makes the sampling risk of that blend an explicit function of market and sample parameters. The source for this mission is the authors’ SSRN manuscript, version dated August 18, 2023, including its Internet Appendix; appendix pages are cited as IA pages.

The market and the estimated portfolio

There are $N$ risky stocks. Their excess-return vector has population mean $\mu\in\mathbb R^N$ and positive-definite population covariance $\Sigma\in\mathbb R^{N\times N}$. The investor has risk aversion $\gamma>0$. A portfolio is a vector of weights $w$ whose entries sum to one. Its population mean-variance utility is

$$U(w)=w^\top\mu-\frac{\gamma}{2}w^\top\Sigma w.$$

Write $e$ for the vector of ones. The global-minimum-variance portfolio and its variance are $w_g=\Sigma^{-1}e(e^\top\Sigma^{-1}e)^{-1}$ and $\sigma_g^2=(e^\top\Sigma^{-1}e)^{-1}$. Its mean is $\mu_g=\mu^\top\Sigma^{-1}e\,\sigma_g^2$. The population matrix $B=\Sigma^{-1}(I-ew_g^\top)$ maps the mean vector to a zero-cost portfolio. The variance of that portfolio is $\psi^2=\mu^\top\Sigma^{-1}\mu-\mu_g^2/\sigma_g^2$. These quantities are computed from $\mu$ and $\Sigma$; they are not independent inputs. These definitions are equations (3)–(7) of the manuscript.

The investor observes $T$ independent return vectors $r_1,\ldots,r_T$, each with multivariate Gaussian law $\mathcal N(\mu,\Sigma)$. The sample mean is $\hat\mu=T^{-1}\sum_t r_t$, and the sample covariance is $\hat\Sigma=T^{-1}\sum_t(r_t-\hat\mu)(r_t-\hat\mu)^\top$. Replacing the population parameters in $w_g$ and $B$ by these estimates gives the sample GMV portfolio $\hat w_g$ and the sample zero-cost portfolio $\hat w_z=\hat B\hat\mu$. The estimated mean-variance portfolio is $\hat w^\star=\hat w_g+\gamma^{-1}\hat w_z$. At shrinkage intensity $\kappa\in[0,1]$, the portfolio under study is $\hat w^\star(\kappa)=(1-\kappa)\hat w_g+\kappa\hat w^\star$. Its out-of-sample utility, $U(\hat w^\star(\kappa))$, is evaluated using population $\mu$ and $\Sigma$. It is random because the weights depend on the sample. These choices are fixed by equations (9)–(12) and Assumption 2 of the manuscript.

Formalization targets

The goal is Proposition 1, equations (13)–(19). Under $N\ge2$ and $T>N+7$, it asserts that the utility has a finite second moment and that

$$\mathbb V[U(\hat w^\star(\kappa))] =\mathbb V[U(\hat w_g)]+\Delta(\kappa),\qquad \Delta(\kappa)=a_1\kappa^4+a_2\kappa^3+a_3\kappa^2+a_4\kappa.$$

The coefficients $a_1,\ldots,a_4$ and $\mathbb V[U(\hat w_g)]$ are the exact rational expressions in $T,N,\gamma,\sigma_g^2,\psi^2$ on pp. 14–15 of the manuscript. In particular, the result covers every $\kappa\in[0,1]$, including the sample GMV portfolio at $\kappa=0$ and the sample mean-variance portfolio at $\kappa=1$.

The milestones follow the quantities named in the authors’ proof, Section IA.10. Equation (IA43) gives the covariance matrix of the random weights, and (IA44) gives the variance of their population mean return. The jointly distributed mean-return and return-variance pair in (IA45)–(IA48) supplies the setting for two auxiliary moment identities, (IA53) and (IA57). Equations (IA49), (IA59), and (IA60) give the first and second moments needed for return variance and mean return; (IA68) gives their covariance. All are statements from the Internet Appendix, pp. IA35–IA39.

What the result supplies

The expression tells an investor how the sampling risk of utility changes with the shrinkage intensity, sample size, stock count, risk aversion, and the two population variance parameters. The later comparison of variance-minimizing, mean-maximizing, and robustness-maximizing intensities uses this formula. Without Proposition 1, those comparisons have no explicit OOSU risk function to analyze. The result is already proved in the paper; this mission asks for its Lean proof and for reusable formal statements of the associated Gaussian portfolio and moment identities. No machine-checked proof of this paper’s proposition is included in the draft.

Where the difficulty lies

The sample covariance is random and its inverse appears in the estimated weights. Taking the variance of utility therefore involves inverse-covariance terms and moments beyond those needed for expected utility. The requirement $T>N+7$ is tied to existence of the fourth negative moment of a chi-squared variable in (IA57). A direct calculation that replaces random weights by their population counterparts loses the dependence on the estimation sample. A calculation from separate marginal laws also does not determine the covariance between mean return and return variance; the representation in (IA47)–(IA48) describes them jointly.

Formalization scope

The Lean market uses vectors Fin N → ℝ, matrices indexed by Fin N, and returns in EuclideanSpace ℝ (Fin N) to use Mathlib’s multivariate Gaussian law. The sample has Fin T observations on a probability space. Its covariance divisor is exactly $T$, as in (9). The standing assumptions are $N\ge2$, $T>N+7$, $\Sigma\succ0$, $\gamma>0$, and independent, identically distributed Gaussian returns. Every theorem about a variance or covariance explicitly asserts finite second moments; expectation statements explicitly assert integrability. The source’s finite-variance convention is thereby represented without Lean’s default value for a nonintegrable variance.

The left side of the goal is the probability-theory variance of utility under the sampling law. It is not defined by the closed formula. Likewise $\sigma_g^2$, $\mu_g$, and $\psi^2$ are computed from the market; independence is part of the sampling hypothesis. In the auxiliary representation, the chi-squared law is the squared norm of independent standard normals. The zero-degree cases and footnote 6’s $N=2,3$ rules are encoded explicitly. Mathlib’s matrix inverse and real division are total operations; their values on singular sample covariances or zero denominators do not alter the distributions because those events have probability zero under the stated assumptions. Contributions establishing the sample-covariance distribution, the joint representation, the negative moments, and the final variance identity are within scope and can support other Gaussian portfolio results.

Selected references

• N. Lassance, A. Martín-Utrera, and M. Simaan, The Risk of Expected Utility under Parameter Uncertainty, authors’ SSRN manuscript dated August 18, 2023, subsequently in Management Science (2024). SSRN 3855546; DOI 10.1287/mnsc.2023.00178.

Motivation

A Fisher market allocates a common supply of items among buyers with separate budgets. When the items form a continuum, such as positions in a measurable interval, a buyer's valuation and the market price are functions rather than finite lists. This is a useful model for divisible resources and for settings in which an allocation can be described as a measurable subset of a continuous item space. Gao and Kroer develop equilibrium and convex-programming results for this setting in Infinite-Dimensional Fisher Markets and Tractable Fair Division. Their Section 6 extends the analysis from linear utility to quasilinear utility, where the buyer subtracts the cost of the allocated bundle from its value.

Quasilinear utility changes the role of money. A buyer can retain an unspent part of the budget and value it outside the market. Consequently, normalizing each buyer's valuation independently, which is harmless for linear demand, changes quasilinear demand. The extension therefore needs its own equilibrium definition and its own pair of optimization programs. This mission concerns the existence and exact equilibrium characterization stated in Theorem 10 of the cited preprint, rather than the numerical algorithms discussed elsewhere in that paper.

Setting

There are $n$ buyers and an item space $\Theta$, a compact subset of $\mathbb R^d$, with restricted Lebesgue measure $\mu$. Buyer $i$ has an integrable, nonnegative valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$, and a strictly positive budget $B_i$. A bundle is an essentially bounded, nonnegative measurable function $x_i$ on $\Theta$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. A pure allocation assigns almost disjoint measurable sets $\Theta_i$ to buyers, so $x_i=\mathbf1_{\Theta_i}$ almost everywhere; some items may remain unallocated.

A price density $p$ is nonnegative and integrable. The pairing $\langle f,g\rangle=\int_\Theta f(\theta)g(\theta)\,d\mu(\theta)$ gives the value of a bundle and its cost. At price $p$, buyer $i$ chooses an affordable bundle maximizing $\langle v_i-p,x_i\rangle$, with affordability $\langle p,x_i\rangle\le B_i$. A quasilinear market equilibrium (QLME) is a feasible allocation and price at which every buyer makes such a choice and unsold items have zero total price: $\langle p,1-\sum_i x_i\rangle=0$.

The quasilinear Eisenberg–Gale primal program uses a nonnegative variable $\delta_i$ for each buyer and maximizes $\sum_i(B_i\log u_i-\delta_i)$, where $u_i\le\langle v_i,x_i\rangle+\delta_i$. Its dual program minimizes $\langle p,1\rangle-\sum_i B_i\log\beta_i$ subject to $p\ge\beta_i v_i$ and $0\le\beta_i\le1$. The primal is represented by $(x,\delta)$ with $u_i=\langle v_i,x_i\rangle+\delta_i$ at an optimum. This saturated form has the same optimum as the displayed program and makes the optimality conditions unambiguous.

Formalization targets

Theorem 10: attainment and equilibrium

The goal is the full four-part statement. The primal attains its maximum at a pure allocation. The dual attains its minimum with a unique vector $\beta^*$ and price density $p^*=\max_i\beta_i^*v_i$ almost everywhere. For feasible primal and dual points, simultaneous optimality is equivalent to market clearance and

$$\beta_i(\langle v_i,x_i\rangle+\delta_i)=B_i,\qquad \delta_i(1-\beta_i)=0,\qquad \langle p-\beta_i v_i,x_i\rangle=0 \quad\text{for every }i.$$

Finally, $(x,p)$ is a QLME exactly when there are $\delta$ and $\beta$ for which $(x,\delta)$ and $(p,\beta)$ are optimal in the two programs. The same given $p$ must appear on both sides of this equivalence.

Milestone results

The milestones follow the statements in the proof of Theorem 10: attainment of the utility-space program (A.14), uniqueness of the minimizer in the reduced dual program, weak duality (A.15) with its additive constant $\sum_iB_i(\log B_i-1)$, the KKT characterization, and each direction of the QLME equivalence. The earlier paper's Lemma 1 identifies the feasible utility set with utilities of pure allocations and supplies the compactness used here. It belongs to the first mission of this series and is not duplicated as a target in this one.

Significance

The theorem establishes that the two infinite-dimensional programs describe the quasilinear market exactly. Attainment guarantees actual optimal allocation and price objects rather than only approximating sequences. Pure attainment gives a measurable partition-type allocation. The unique $\beta^*$ pins down each buyer's utility price, while $p^*=\max_i\beta_i^*v_i$ identifies the price density almost everywhere. The KKT equations give precise tests for a candidate optimal pair, and the final equivalence translates between optimization solutions and buyer-level equilibrium behavior. These are the claims made by Theorem 10 and its appendix proof.

The result is proved in the paper; the work here is to formalize its statement and, in later solver contributions, its proof in Lean. A complete development will also provide reusable infrastructure for integrating valuation densities against essentially bounded bundles, representing continuum-item allocations, and relating a finite buyer-indexed vector to pointwise price maxima. No machine-checked proof of this mission's goal is supplied with this draft.

Difficulty

The optimization variables include functions in $L^\infty$ and $L^1$, and the positive cone of $L^1$ has no useful interior for a direct appeal to standard infinite-dimensional convex-duality theorems. The finite-dimensional utility vector is easier to optimize over, but recovering a pure allocation from it requires the measurable-allocation result established earlier in the paper. The dual price is a pointwise maximum of integrable densities, and equality of prices is meaningful almost everywhere. Equilibrium demand compares a buyer's assigned bundle with every affordable essentially bounded bundle, so an optimality statement about program variables must account for that full comparison.

Formalization scope

Lean represents densities and bundles as functions on the ambient Euclidean space, with the measure restricted to $\Theta$; values outside $\Theta$ do not matter. The standing hypotheses are compactness of $\Theta$, integrability and almost-everywhere nonnegativity of every $v_i$, strictly positive total valuation, and strictly positive budgets. There is no assumption that total budgets or total item measure equal one. The buyer type Fin n is zero-based; the paper numbers buyers from one. The empty-buyer case is allowed and has the expected trivial finite-vector interpretation.

The equilibrium predicate includes supply feasibility. The printed QLME definition on page 29 omits it, although the linear-market definition includes it and Theorem 10(d) requires it. Without it, a buyer can receive more than unit supply on part of the item space while buyer optimality and market clearance still hold. The primal uses the saturated value $u_i=\langle v_i,x_i\rangle+\delta_i$; leaving $u$ free below that value makes the printed KKT converse false. These two choices are disclosed in the item descriptions and moderation notes, with concrete counterexamples there.

The paper treats $\log0$ as a limiting infinite cost. Lean's real logarithm is total, so optimality compares only points whose logarithm arguments are positive. The utility KKT equation is multiplied by $\beta_i$ to avoid division by zero. Valuation and price densities are integrable, and bundles are essentially bounded, so pairings are genuine finite integrals. The pointwise maximum over buyers is an indexed supremum; feasibility and uniqueness use almost-everywhere equality for price functions and exact equality for the finite vector $\beta$. These conventions prevent degenerate total-function values from deciding the theorem.

Contributions can address the measurable utility-set and pure-allocation infrastructure, finite-dimensional attainment, weak duality, the equality conditions, or the demand comparison. The intermediate milestones are stated at the strength used in the paper; the goal contains the entire four-part result.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, preprint arXiv:2010.03025v5, 2021; published in Operations Research, 2023. arXiv preprint.

Motivation

Quantum error correction needs families of codes that protect a growing number of logical qubits while using checks that touch few physical qubits. In a quantum Tanner code, the local constraints come from two smaller binary codes. The distance analysis requires those local codes to satisfy a geometric condition called robustness: a low-weight word in a certain sum code must occupy only a controlled number of complete rows and columns. The deterministic distance theorem in Leverrier and Zémor's Quantum Tanner codes assumes this condition; their Theorem 9 supplies it for randomly chosen component codes. Establishing that random codes satisfy the assumption makes the later existence result meaningful rather than conditional on a property with no known examples.

The appendix follows the approach of Panteleev and Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, with a separate treatment of puncturing. The historical relation here is limited: this mission formalizes Leverrier and Zémor's Theorem 9 and its own numbered supporting results, with their hypotheses and constants.

Setting

Fix two coordinate sets $A$ and $B$, each of cardinality $\Delta$. A binary linear code $C_A\subseteq\mathbb F_2^A$ is a vector subspace; similarly $C_B\subseteq\mathbb F_2^B$. Regard a word on $A\times B$ as a matrix $x=(x_{ab})$. The column code contains matrices whose column at every $b\in B$ belongs to $C_A$. The row code contains matrices whose row at every $a\in A$ belongs to $C_B$. Their intersection is the tensor code $C_A\otimes C_B$; their sum is the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$. The Hamming weight $|x|$ counts its nonzero entries. These conventions are those of §3.5 of the source paper.

Write $d_A,d_B$ for the actual minimum distances of the two component codes. The dual tensor code is $w$-robust if every codeword $x$ with $|x|\le w$ vanishes outside the union of some set of at most $|x|/d_B$ rows and some set of at most $|x|/d_A$ columns. Thus a low-weight word cannot be spread thinly across many rows and columns. For retained coordinate sets $A'\subseteq A$ and $B'\subseteq B$, the punctured codes $C_{A'}$ and $C_{B'}$ are the images under restriction. Robustness has $p$-resistance to puncturing when the corresponding dual tensor code remains $w$-robust for every pair $A',B'$ of equal size obtained by removing at most $p$ coordinates from each side. These are Definitions 5 and 8 on pp. 15–16 of the paper.

A uniform generator matrix with $r$ rows and $\Delta$ columns is sampled uniformly from all binary matrices of that shape. Its row span is $C_A$. Independently, a uniform parity-check matrix with $s$ rows and $\Delta$ columns defines $C_B$ as its kernel. Probability is the fraction of matrices, or matrix pairs, satisfying an event. In the asymptotic statement, $\Delta$ tends through natural numbers to infinity.

Formalization targets

Random robustness and resistance

For $0<\rho_A,\rho_B<1$, $0<\varepsilon<1/2$, and $1/2+\varepsilon<\gamma<1$, sample $C_A$ and $C_B$ from the matrix models above, using $\lfloor\rho_A\Delta\rfloor$ generator rows and $\lceil(1-\rho_B)\Delta\rceil$ parity-check rows. The goal, Theorem 9, is

$$\Pr\!\left[C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B\text{ is }\Delta^{3/2-\varepsilon}\text{-robust with }\Delta^\gamma\text{-resistance}\right]\longrightarrow 1.$$

The milestones are the paper's numbered appendix statements: Lemma 31 converts concentration on few rows and columns into Definition 5's sharper weight-based bounds; Lemmas 24–29 address ranks and probabilities for random kernels and punctured kernels; Theorem 30 gives the quantitative high-probability alternative used before the final limit. The goal fixes the exponents and quantifies over the whole uniform matrix experiment.

Significance

Theorem 9 certifies that the robustness hypothesis needed by the paper's distance construction occurs with asymptotic probability one. It covers all allowed puncturings at once, which matters because a later distance argument deletes coordinates selected by the codeword under study. A statement about one fixed puncturing would not provide that guarantee. The result is proved in the 2022 paper; this mission poses its statements for machine-checked proofs and does not claim that those proofs already exist.

Formalizing the result produces reusable finite probability statements for random linear codes, a parity-check treatment of puncturing, and rank bounds for sparse binary matrices. Those ingredients are independent of the group complex used in the paper's other mission. They can support later formalizations of random coding arguments where a union over many coordinate restrictions is necessary.

Difficulty

The evident first check is that one fixed low-weight matrix probably does not belong to a random dual tensor code. That alone does not establish robustness: the statement ranges over all such matrices and, for resistance, over every pair of large retained coordinate sets. The paper's intermediate results control this whole collection using rank information about sparse matrices and the exact probability that independent vectors lie in a random kernel. A further issue is that puncturing a parity-check code does not simply delete columns from its defining matrix; the discarded columns contribute a random subspace. The quantitative event in Theorem 30 and the simultaneous limit in Theorem 9 both have to survive these ranges.

Formalization scope

Lean uses ZMod 2 for $\mathbb F_2$, Fin \Delta for each coordinate set, and functions on $A\times B$ for matrices. Rows are indexed by $A$ and belong to $C_B$; columns are indexed by $B$ and belong to $C_A$. The published TillichZemor.HGP.Setting supplies the parity-check kernel and the extended-natural minimum distance, whose value is infinity for the zero code. CodingTheory is a published prerequisite. Local definitions give the row and column codes, their sum, puncturing, robustness, uniform finite probability, generator row span, and binary entropy in bits.

The printed matrix sizes $\rho_A\Delta$ and $(1-\rho_B)\Delta$ need integer values. The chosen floor and ceiling keep their respective dimensions within the bounds used in the appendix. Every logarithm in the formalized appendix bounds means $\log_2$, including occurrences printed simply as $\log$. Theorem 30 includes an explicit sufficiently-large-$\Delta$ threshold, as its proof's asymptotic count requires, and carries the appendix's preceding entropy condition $\delta<h^{-1}(1-\rho)$ as $\delta<1/2$ and $h_2(\delta)<1-\rho$. Lemmas 25, 26, and 29 use the preceding condition $d>2\alpha\Delta$; the symbol beside $\Delta$ in the scan is ambiguous, and the argument on p. 29 determines this reading. These choices are recorded for audit in MODERATION_NOTES.md.

The probability space is all matrices of each stated size, with the two matrices in Theorem 9 sampled independently. There is no conditioning on a favorable code or an assumed version of Theorem 30 in the goal. The mission does not formalize the later quantum Tanner code construction or the cited Gilbert–Varshamov result as an additional item. Contributions proving the goal, the numbered milestones, or reusable rank and finite-probability facts are within scope.

Selected references

• Anthony Leverrier and Gilles Zémor, Quantum Tanner codes, arXiv:2202.13641v3, 2022. Preprint.
• Pavel Panteleev and Gleb Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv:2111.03654, 2021. Preprint.

Why quantum Tanner codes matter

An error-correcting code protects information by adding redundancy. A quantum code must also account for two kinds of errors, commonly called $X$ and $Z$ errors. Quantum low-density parity-check codes use checks that each touch only a bounded number of qubits, while each qubit participates in only a bounded number of checks. Such locality matters when the number of qubits grows. For years it was difficult to make both the number of encoded qubits and the minimum distance proportional to the block length while retaining bounded-weight checks. Leverrier and Zémor's quantum Tanner construction gives a route through local codes placed on an expanding square complex; its main distance theorem is the target of this mission Leverrier and Zémor, 2022.

The construction combines two earlier ingredients. Left-right Cayley complexes provide the squares and expansion properties used by the code Dinur, Evra, Livne, Lubotzky, and Mozes, 2021. Robustness of a dual tensor code, including after puncturing coordinates, controls local words Panteleev and Kalachev, 2021. The paper states the local reduction property as Theorem 1 and derives the rate and distance bounds as Theorem 17. This mission formalizes that implication under the paper's stated component-code and expansion conditions; the separate random-code result that supplies robust examples belongs to the second mission of this series.

The square complex and its codes

Let $G$ be a finite group and let $A,B\subseteq G$ be inverse-closed sets, each of size $\Delta$. The total no-conjugacy condition says $ag\ne gb$ for every $a\in A$, $b\in B$, and $g\in G$. Vertices are two copies of the group, $V=G\times\{0,1\}$. A square associated with $v=(g,i)$ and $(a,b)\in A\times B$ has vertices $v$, $(ag,1-i)$, $(gb,1-i)$, and $(agb,i)$. The set of squares is $Q$, and a binary word on $Q$ has length $n=|Q|$. At a vertex $v$, the incident squares are indexed by $A\times B$; this indexing makes the local view $x_v$ of a word $x\in\mathbb F_2^Q$ an $A\times B$ matrix Leverrier and Zémor, §§3.2 and 4.1.

A binary linear code $C_A$ has coordinates indexed by $A$, and $C_B$ has coordinates indexed by $B$. Their tensor code $C_A\otimes C_B$ consists of matrices whose columns lie in $C_A$ and whose rows lie in $C_B$. The dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ is the sum of the column and row codes. In Definition 5, it is $w$-robust when every member of weight at most $w$ is supported on a union of few rows and columns, with the bounds determined by the two component minimum distances. Definition 8 requires this property after deleting up to $p$ coordinates from each side. These are conditions on all relevant codewords and all permitted puncturings, including the unpunctured pair Leverrier and Zémor, pp. 15–16.

The two Tanner codes are $\mathcal C_0=T(\mathcal G^\square_0,(C_A\otimes C_B)^\perp)$ and $\mathcal C_1=T(\mathcal G^\square_1,(C_A^\perp\otimes C_B^\perp)^\perp)$. Here $\mathcal G^\square_i$ is the square-adjacency graph on the vertices in copy $i$. Together they define the quantum CSS code $\mathcal Q=(\mathcal C_0,\mathcal C_1)$. Its dimension counts encoded qubits. Its distance is the smaller of the minimum weights in $\mathcal C_0\setminus\mathcal C_1^\perp$ and $\mathcal C_1\setminus\mathcal C_0^\perp$ Leverrier and Zémor, pp. 14, 18.

Formalization targets

The goal is Theorem 17. Fix $0<\rho<1/2$, $0<\varepsilon<1/2$, $1/2+\varepsilon<\gamma<1$, and $\delta>0$. For sufficiently large $\Delta$, take a left-right Cayley complex satisfying total no-conjugacy and the paper's Ramanujan conditions. Require $0<\dim C_A\le\rho\Delta$, $\dim C_B=\Delta-\dim C_A$, minimum distance at least $\delta\Delta$ for $C_A,C_B$ and both duals, and $\Delta^{3/2-\varepsilon/2}$ robustness with $\Delta^\gamma$ resistance to puncturing for both relevant dual tensor codes. The target is

$$k\ge (1-2\rho)^2 n,\qquad d\ge \frac{\delta n}{4\Delta^{3/2+\varepsilon}}.$$

The milestones mirror the paper's route to this result. Lemma 4 bounds the nontrivial eigenvalues of the union and square graphs. Propositions 6 and 7 turn dual-tensor robustness into a decomposition and a $3/2$ closeness bound. Theorem 1 supplies a weight-reducing local codeword for every sufficiently light nonzero Tanner-code word. Display (5) supplies the dimension lower bound. Theorem 17 combines the two distance directions with that rate estimate Leverrier and Zémor, pp. 12, 15–16, 18–23.

What the result supplies

The lower bound on $k$ ensures a positive fraction of qubits can carry logical information when $\rho<1/2$. The lower bound on $d$ rules out small undetectable logical errors. For a fixed allowable degree $\Delta$, both bounds scale linearly with $n$. The paper also shows that random component codes can satisfy the robustness assumptions; that probabilistic result is a separate formalization target Leverrier and Zémor, Theorems 9 and 17.

A checked development would make explicit how the square indexing, duals, punctured codes, and CSS quotient fit together. The source proves the mathematical result; the statements here remain open Lean theorems. Reusable contributions include the tensor-code interface, spectral bounds for the graph construction, and lemmas connecting local views to the global Tanner codes. A proof of the existence of infinite Ramanujan complex families is outside this mission's stated target.

Where the proof is difficult

A light global codeword need not have a local view that is itself close to a tensor-code word. Some square-graph vertices have unusually large local weight, and puncturing is needed to isolate coordinates shared with those exceptional vertices. The paper's small-set expansion estimates and robustness conditions control those interactions. Simply averaging local weights does not yield the weight-reducing local codeword asserted by Theorem 1 Leverrier and Zémor, §4.2.

Formalization scope

Words are functions into ZMod 2, codes are submodules, and a matrix is a function on $A\times B$ with $A$ indexing rows. The square coordinates are four-element vertex sets. The construction uses $V=G\times\operatorname{Fin}(2)$ and counts $n$ as the number of squares rather than building $n=\Delta^2|G|/2$ into a definition. The minimum distance of the zero code is infinity, and robustness uses inequalities involving that extended value. Powers of $\Delta$ and the parameters $w,p$ are real; the paper uses integer $w,p$ in Definition 8, while the theorem's power thresholds need real comparisons. The formal robustness predicate includes Definition 5's range $0\le w\le\Delta^2$; the theorem thresholds satisfy it for sufficiently large $\Delta$. These conventions are recorded with each item.

The goal quantifies over every finite complex satisfying inverse closure, total no-conjugacy, and Ramanujan conditions, with a uniform threshold $\Delta_0$ chosen before the group and codes. This pins the complexes in the cited infinite family without formalizing their existence. In particular, the goal contains no auxiliary set or local reduction assumption that could make the distance bound immediate. The published CodingTheory and TillichZemor.HGP.Setting definitions supply dual codes and CSS dimension; the paper-specific setting supplies the square complex, local views, Tanner codes, and robustness. Contributions that keep these conventions and close any milestone theorem are welcome.

Selected references

• A. Leverrier and G. Zémor, Quantum Tanner codes, arXiv preprint, 2022. arXiv:2202.13641v3.
• I. Dinur, S. Evra, R. Livne, A. Lubotzky, and S. Mozes, Locally Testable Codes with constant rate, distance, and locality, arXiv preprint, 2021. arXiv:2111.04808.
• P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv preprint, 2021. arXiv:2111.03654.

Why spatial pricing needs a dynamic control

A ride-hailing firm chooses prices while drivers move through a city. A trip from one region uses a driver immediately and returns that driver at another region only after a travel delay. Prices affect which trips are requested, but the actual requests fluctuate. A plan that ignores these fluctuations can run out of available drivers at a busy origin even when its average flows fit the fleet. Chen, Lei, and Jasin study how closely a feasible pricing control can approach a deterministic revenue benchmark in this setting (accepted manuscript, published article).

Their Arc Balancing Control (ABC) responds to realized trips. It groups each directed arc's periods into batches and adjusts the next batch's demand rates according to the previous batch's cumulative surplus or deficit. The paper proves a loss rate for ABC that is smaller than the rate established there for its Static Price Control. The target here is the paper's Theorem 3, with the model and parameters of its authors' accepted manuscript. Its e-companion contains the paper's proofs.

The pricing network and benchmark

The network has $N\ge1$ regions and a horizon of $T\ge1$ periods. Every ordered pair $i\to j$, including $i=j$, is an arc. At most one customer can request an arc's trip in a period. A served trip takes one server from region $i$ for $\tau_{ij}\ge1$ periods, then returns it at $j$. Region $i$ starts with $C_i\ge N$ servers. A control must respect the available server count before it serves each period's realized requests.

The decision is a demand rate $\lambda_{t,ij}\in[0,1]$ rather than its inverse price. The expected revenue from that arc and period is $r_{t,ij}(\lambda_{t,ij})$. The revenue functions are nonnegative and strongly concave, vanish at zero, and have bounded first and second derivatives. The bound on those derivatives is $\Psi_3>0$. The paper's price-side assumptions imply these rate-side conditions; the Lean model states the conditions directly.

The deterministic convex program $\mathrm{DCP}(\zeta)$ chooses rates to maximize the sum of expected revenues. Its flow constraints replace realized trips with their rates, while its cushion requires $\zeta\le\lambda_{t,ij}\le1-\zeta$. Write $J(\zeta)$ for its value and $\lambda^{\zeta,D}$ for an optimal schedule. In the $n$th system, the fleet, horizon, and travel times are multiplied by $n$; each original period's revenue curve is used for $n$ consecutive scaled periods. Thus $T^n=nT$ and $\underline\tau^n=n\min_{i,j}\tau_{ij}$. For a control $\pi$, the per-period benchmark loss is

$$L^\pi(n)=\frac{J(n,0)-\mathbb E^\pi[R^\pi(n)]}{T^n}.$$

ABC uses $\lambda^{n,\zeta,D}$ as its baseline. Its batches have a target sum $b$ of the baseline variance weights $\lambda^{n,\zeta,D}_{t,ij}(1-\lambda^{n,\zeta,D}_{t,ij})$. Within a batch, the control subtracts a weighted share of the preceding batch's realized surplus $\bar\delta^k_{ij}=\sum_{t\in\mathcal T^k_{ij}}(D_{t,ij}-\lambda^{ABC}_{t,ij})$. A rate is projected to $[0,1]$, and an origin with too few available servers is turned off. The finite path law uses the rates posted along each path.

Formalization targets

The principal target is Theorem 3. With $b_n=(\underline\tau^n)^{2/3}$ and

$$\epsilon_n=(\underline\tau^n)^{-1}\left(1+16\sqrt{2(b_n+1)\log T^n}\right),\qquad \zeta_n=2\epsilon_n,$$

there is a constant $\widetilde\Psi_2$, independent of $n$, for which every integer $n\ge1$ satisfies

$$L^{ABC}(n)\le\widetilde\Psi_2\frac{\log(1+n)^{3/2}}{n^{2/3}}.$$

The milestone list follows the source results used in the analysis: Lemma 2 bounds the deterministic cost of a small cushion and gives feasibility; Lemma EC.1 bounds a maximal cumulative Bernoulli deviation; and the two parts of Lemma 4 characterize ABC on a batchwise good event $\mathcal A$ and bound that event's probability. Theorem 3 fixes the complete control and these exact parameters; its constant may depend on the fixed network instance and $\Psi_3$.

What the result establishes

The theorem gives a finite-$n$ loss bound relative to $J(n,0)$, with the stated $n^{-2/3}$ rate and logarithmic factor. In the paper, Lemma 1 shows that $J(n,0)$ bounds the optimal admissible policy's revenue. Theorem 3 therefore bounds ABC's distance from a benchmark that is at least as high as the unknown stochastic optimum. The paper compares this rate with its $n^{-1/2}$ result for Static Price Control and explains the resulting value of adapting prices to realized demand (Theorems 2–3).

The published mathematical result and its manuscript proof are known; the statements in this mission are Lean targets with proofs still to be formalized. A complete development would also make reusable definitions for finite controlled path laws, delayed network flow balance, and cushioned deterministic relaxations. The batch and feedback definitions isolate the paper-specific control from that general infrastructure.

Main difficulty

The deterministic program controls expected flows, while ABC must keep every realized path feasible. An unadjusted baseline can accumulate demand fluctuations over the whole horizon; bounding those fluctuations alone does not describe the effect of ABC's feedback. The control's posted rate in a period depends on earlier realized requests, which changes the distribution of later requests. The manuscript's proof of Lemma 4 bounds a variance proxy from its deterministic baseline when treating the adaptive posted rates; that step needs separate justification in a formal proof. Lemma EC.1, as posed here, covers deterministic Bernoulli rates and does not by itself close that gap. The finite-horizon claim, including small scaling factors for which the cushioned DCP may be infeasible, must still be established.

Formalization scope

Lean represents regions by Fin N, periods by natural numbers $1,\ldots,T$, travel times and server counts by naturals, demand by Boolean paths, and revenue and rates by real numbers. The $\mathrm{DCP}(n,\zeta)$ program uses a real supremum; statements involving positive $\zeta$ assert feasibility, and $J(n,0)$ has the zero schedule as a feasible point. ABC's path law is the product of sequential Bernoulli factors at its own posted rates. Its rate history is built by structural recursion, and the event $\mathcal A$ checks every nonempty batch and all its partial sums.

The accepted manuscript leaves the final incomplete batch unspecified, so the last short batch is merged with its predecessor. The printed ABC box turns an origin off at $C_{t,i}\le N$, while Lemma 4 and its base case require service when $C_{t,i}=N$; the formal control uses $C_{t,i}\ge N$. If the cushioned DCP has no optimum, the baseline is zero. The sample-path part of Lemma 4 adds the hypothesis $\underline\tau\le T$, which the manuscript does not print. Without it the part is false: when the horizon is shorter than every travel time, no server returns, and a single realized trip can leave a region below $N$ servers on the good event. These conventions are recorded with the source discrepancies in the moderation notes. The rate model drops assumptions A1 and A3(i), which concern only the price parametrization, and writes A2, A3(ii), $r\ge0$, and $r(0)=0$ directly. It assumes a twice continuously differentiable extension of revenue to $\mathbb R$. No statement substitutes expected demand for the realized batch surplus or lets the theorem's parameters depend on $n$ by existential choice. Contributions toward the source milestones, the adaptive concentration step, and the reusable model definitions are all within scope.

Selected references

• Q. Chen, Y. Lei, and S. Jasin, Real-Time Spatial-Intertemporal Pricing and Relocation in a Ride-Hailing Network: Near Optimal Heuristics and The Value of Dynamic Pricing, authors' accepted manuscript, LBS Research Online eprint 2845, pp. 7–25 and ec2–ec6; published as Real-Time Spatial–Intertemporal Pricing and Relocation in a Ride-Hailing Network: Near-Optimal Policies and the Value of Dynamic Pricing, Operations Research 72(5):2097–2118, 2024. Manuscript, DOI.

Motivation

Many problems in signal processing, statistics and engineering design have the form of a nonconvex, possibly nonsmooth objective subject to nonlinear equality constraints. Zhu, Zhao and Zhang (arXiv:2007.12219v1, 2020; published in Mathematics of Operations Research, 2024) propose NAPP-AL, a first-order primal-dual method that takes one linearized step on the augmented Lagrangian per iteration. Their analysis has three layers: subsequential convergence with an $o(1/\sqrt k)$ stationarity rate (§4), linear convergence under a new value proximity error bound (VP-EB, §5), and sufficient conditions for VP-EB (§6).

This mission formalizes the second sufficient condition: metric subregularity of the stationarity map, together with a local value condition on nearby stationary points, implies VP-EB. Metric subregularity is a standard regularity notion of variational analysis (Dontchev–Rockafellar), and error bounds of this kind are the classical route to linear convergence (Luo–Tseng). The paper attributes the cost-to-go inequality it relies on to Tseng and Yun [18]. A companion mission treats the KL-property route (Proposition 6.1); a third proves linear convergence from VP-EB (Theorem 5.1).

Setting

Write $w=(u,v,p)\in\mathbb R^n\times\mathbb R^d\times\mathbb R^m$ with the Euclidean norm of the stacked vector, $\|w\|=\sqrt{\|u\|^2+\|v\|^2+\|p\|^2}$, and $\mathbb B(\bar w;\eta)$ the open ball. The problem (P) is

$$\min_{u\in U,\,v\in\mathbb R^d}\ F(u,v)=G(u,v)+J(u)+H(v)\quad\text{s.t.}\quad \Theta(u)+Bv=0,\qquad \Theta=\Omega+\Phi,$$

with $G,H$ smooth with Lipschitz gradients, $J$ lower semicontinuous and locally Lipschitz near $U$, $U$ closed and convex, $\Theta$ Lipschitz, each component of $\Omega$ with Lipschitz gradient, and $B$ an $m\times d$ matrix of full column rank with $\mathrm{Im}\,\Theta\subseteq\mathrm{Im}\,B$; $F$ is bounded below and coercive on the feasible set (Assumption 1).

The augmented Lagrangian is $\mathcal L_\gamma(w)=F(u,v)+\langle p,\Theta(u)+Bv\rangle+\tfrac\gamma2\|\Theta(u)+Bv\|^2$. The set $\partial\mathcal L_\gamma(w)$ is the KKT display of p. 6: with $r=\Theta(u)+Bv$, it collects the triples

$$\big(\nabla_uG+\partial J(u)+N_U(u)+(\nabla\Theta(u))^\top[p+\gamma r],\ \ \nabla_vG+\nabla H(v)+B^\top[p+\gamma r],\ \ r\big),$$

with $\partial J$ the limiting subdifferential and $N_U$ the normal cone. A point is stationary if $0\in\partial\mathcal L_\gamma(w)$; $\bar{\mathbf W}$ is the set of stationary points. Distances follow the paper's convention: $\mathrm{dist}(x,C)=\inf_{z\in C}\|x-z\|$, and $\mathrm{dist}(x,\emptyset)=+\infty$.

NAPP-AL keeps $q^k=p^k+\gamma(\Theta(u^k)+Bv^k)$, takes $u^{k+1}$ as a global minimizer over $U$ of a linearized model with a Bregman term $D(u,u^k)/\epsilon^k$, $v^{k+1}$ as the minimizer of a strongly convex quadratic, and sets $p^{k+1}=p^k+\gamma(\Theta(u^{k+1})+Bv^{k+1})$. The step $\epsilon^k$ lies in $[\sigma\delta_k,\delta_k]$ with $\delta_k$ given explicitly by (8), and $\gamma>(\sqrt{57}+1)(L_G+L_H)/(2\lambda_{\min}(B^\top B))$ (Assumption 2).

VP-EB at $\bar w$ (Definition 5.1): there are $\kappa_1,\eta,\nu>0$ such that $\mathcal L_\gamma(w^{k+1})-\mathcal L_\gamma(\bar w)\le\kappa_1\|w^k-w^{k+1}\|^2$ whenever $w^{k+1}\in\mathbb B(\bar w;\eta)$ and $\mathcal L_\gamma(w^{k+1})<\mathcal L_\gamma(\bar w)+\nu$.

Metric subregularity (Definition 6.2): $\partial\mathcal L_\gamma$ is metrically subregular around $(\bar w,0)$ if, for some $\eta,\kappa_3>0$, $\mathrm{dist}(w,\bar{\mathbf W})\le\kappa_3\,\mathrm{dist}(0,\partial\mathcal L_\gamma(w))$ for all $w\in\mathbb B(\bar w;\eta)$. Assumption 3 at a stationary $\bar w\in\bar{\mathbf W}$: for some $\delta>0$, $\mathcal L_\gamma(w)\le\mathcal L_\gamma(\bar w)$ for all $w\in\bar{\mathbf W}$ with $\|w-\bar w\|\le\delta$.

Formalization targets

Goal: Proposition 6.2 (p. 26)

Let $\{w^k\}$ be generated by NAPP-AL in the standing setting and let $\bar w$ be a cluster point. If Assumption 3 holds at $\bar w$ with $\delta$, and $\partial\mathcal L_\gamma$ is metrically subregular around $(\bar w,0)$ with $\kappa_3>0$ and $\eta>0$, $\eta<\delta$, then

$$\exists\,\kappa_1,\eta',\nu>0:\quad w^{k+1}\in\mathbb B(\bar w;\eta'),\ \mathcal L_\gamma(w^{k+1})<\mathcal L_\gamma(\bar w)+\nu\ \Longrightarrow\ \mathcal L_\gamma(w^{k+1})-\mathcal L_\gamma(\bar w)\le\kappa_1\|w^k-w^{k+1}\|^2 .$$

The constants are existential, as in Definition 5.1, so the statement survives any improvement of them.

Milestone: Lemma 6.1 (p. 23), the cost-to-go inequality

$$\forall\bar w\in\bar{\mathbf W}\ \ \exists\,c_6>0\ \ \forall k:\quad \mathcal L_\gamma(w^{k+1})-\mathcal L_\gamma(\bar w)\le c_6\big(\|\bar w-w^{k+1}\|^2+\|w^k-w^{k+1}\|^2\big).$$

Significance

The result. Combined with Theorem 5.1 of the paper, Proposition 6.2 gives finite length, convergence of the whole sequence, Q-linear convergence of the potential and R-linear convergence of the iterates whenever the stationarity map is metrically subregular at the limit and Assumption 3 holds there. Metric subregularity is known for broad classes, such as piecewise linear-quadratic problems and polyhedral multifunctions, so the proposition turns a structural property of the problem into a rate for this algorithm.

Formalizing it. The proposition is proved on paper; nothing about NAPP-AL has a machine-checked proof. The formalization makes two things exact that the paper leaves loose. First, the proposition’s proof needs a cost-to-go constant independent of the stationary point, and the proof of Lemma 6.1 supplies one even though the lemma’s printed statement fixes the point first. Second, the proposition's proof places the nearest stationary point $w_p^{k+1}$ in $\mathbb B(\bar w;\eta)$, while only $\|w_p^{k+1}-\bar w\|\le 2\eta$ follows from its steps; the existential conclusion leaves room to shrink the radius. A formal proof settles both, and the general facts it needs (metric subregularity in $[0,+\infty]$, closedness of limiting-subdifferential graphs) are reusable.

Difficulty

The obvious route is to combine subregularity with the residual bound of Theorem 4.1(iv), $\mathrm{dist}(0,\partial\mathcal L_\gamma(w^{k+1}))\le c_5\|w^k-w^{k+1}\|$, which bounds the distance from $w^{k+1}$ to $\bar{\mathbf W}$ by the step. The difficulty is transferring a distance bound into a value bound of second order: local Lipschitz continuity of $\mathcal L_\gamma$ would bound $\mathcal L_\gamma(w^{k+1})-\mathcal L_\gamma(w_p)$ only by a multiple of $\|w^{k+1}-w_p\|$, which is first order in the step, while VP-EB asks for the square; and $J$ is nonsmooth and nonconvex, so no Taylor expansion at the stationary point is available. Moreover, the stationary point closest to $w^{k+1}$ changes with $k$. The proposition’s proof needs a cost-to-go inequality with a constant uniform over stationary points, which in turn rests on the boundedness of the iterates and on the lower bound for $\epsilon^k$ coming from (8). The radius bookkeeping between the subregularity ball, Assumption 3's radius and the VP-EB ball is a second, smaller obstacle.

Formalization scope

$\mathbb R^k$ is EuclideanSpace ℝ (Fin k) and points are triples E n × E d × E m; every norm and ball uses the stacked Euclidean norm tnorm, never Lean's product (sup) norm. $B$ is a continuous linear map with its operator norm (the spectral norm), never a Matrix with the entrywise norm; $\lambda_{\min}(B^\top B)$ is the Rayleigh minimum over the unit sphere. Distances $\mathrm{dist}(0,S)$ and $\mathrm{dist}(w,S)$ are infima in $[0,+\infty]$, equal to $+\infty$ on the empty set; Metric.infDist, which returns $0$ on $\emptyset$ and would make subregularity and the residual bounds trivial, is not used. The normal cone $N_U(u)$ is empty for $u\notin U$, so a nonempty normal cone off $U$ cannot manufacture stationary points. (H3)'s local Lipschitz continuity is read on neighbourhoods in $\mathbb R^n$ of points of $U$, not Mathlib's relative LocallyLipschitzOn.

Disclosed readings of the arXiv v1 text: $G,J,H$ are real-valued with globally Lipschitz gradients; $\lambda_{\min}(B^\top B)>0$; NAPP-AL is a relation on given sequences (any global minimizer may be selected; existence is not asserted); VP-EB is the inequality alone, without Definition 5.1's presupposition that the sequence converges to $\bar w$; "generated by NAPP-AL" in Lemma 6.1 and Proposition 6.2 carries the standing setting of Theorem 4.1 (Assumptions 1–2 and rule (8)); Lemma 6.1 follows the printed quantifier order; its proof supplies the uniform constant needed by Proposition 6.2. The radius of Assumption 3 is δ3 in Lean, distinct from the step sequence $\delta_k$.

Welcome contributions: a proof of Lemma 6.1 from the optimality of (5)–(6), Lipschitz estimates and the bounds of Theorem 4.1(ii); the boundedness and residual results of Theorem 4.1 (formalized in the companion mission on the $o(1/\sqrt k)$ rate); closedness of $\bar{\mathbf W}$; and the radius argument of Proposition 6.2. The source is arXiv:2007.12219v1; numbering and constants of the published version are not used.

Selected references

• D. Zhu, L. Zhao, S. Zhang, A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian, arXiv:2007.12219v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2007.12219v1
• P. Tseng, S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming 117, 2009. https://doi.org/10.1007/s10107-007-0170-0
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46, 1993. https://doi.org/10.1007/BF02096261
• A. L. Dontchev, R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3