Optimization

Completed

Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low I: The Discrete First-Order Algorithm Is a Descent Method Whose Successive Steps Shrink at Rate O(1/M)Research Paper

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)

(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).
(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)$ .
(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)$ .
(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 .

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

7 thms2 active usersReviewed

Completed

Economics Information Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Optimal choice probability

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

6 thms2 active usersReviewed

Algorithmic Game Theory Analysis Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 12

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

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

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

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

8 thms2 active usersReviewed

Algorithmic Game Theory Analysis Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Games are compared by the distance

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

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

Formalization targets

Goal: Theorem 9 (p. 26)

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

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

The Lean development fixes the following conventions.

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

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

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

Selected references

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

13 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 8b)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

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

Selected references

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

8 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

Games are compared by the distance (3.3),

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

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

Formalization targets

Goal: Corollary 5.1 (p. 43)

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

7 thms2 active usersReviewed

Algorithmic Game Theory Analysis Operations Research+1·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

9 thms2 active usersReviewed

Linear algebra Quantum Information Theoretical Computer Science·Captain: mikedeng1

Optimization by Decoded Quantum Interferometry 2: With an Imperfect Decoder and Uniform v, 𝔼_v⟨f⟩ ≥ wᵀ[A − 2ε(m+1)]w / Σ_k w_k²(1 − ε_k) for max-XORSATResearch Paper

Motivation

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective value is also a good approximate solution. Jordan and coauthors study decoded quantum interferometry (DQI), a way to sample candidate assignments by encoding a weighted superposition of error patterns and then decoding their syndromes. Their ideal-state analysis assumes that low-weight errors have distinct syndromes. Real decoders can succeed on many errors even when this uniqueness condition fails, which makes the theorem in this mission relevant to the algorithmic regime beyond the guaranteed decoding radius. Jordan et al., §§8.1 and 10.

The paper's 2024 preprint introduced DQI for linear constraint satisfaction and related optimization problems. Its revised 2025 version studies the effect of decoder failures on the measured objective in Theorem 10.1. This mission uses that revision, arXiv:2408.08292v5, and isolates the first inequality of equation (172). The same section supplies explicit identities for the norm of the postselected state and for its objective matrix, making the theorem a bounded campaign of finite combinatorics and linear algebra. Jordan et al., §10, pp. 35–43.

Setting

Fix integers $m,n\ge0$ and a binary matrix $B\in\mathbb F_2^{m\times n}$ . Its $i$ th row defines a parity $b_i\cdot x$ of an assignment $x\in\mathbb F_2^n$ . For a binary vector $v\in\mathbb F_2^m$ , the objective is

f_v(x)=\sum_{i=1}^{m}(-1)^{b_i\cdot x+v_i}.

An error pattern $y\in\mathbb F_2^m$ has syndrome $B^\top y$ and Hamming weight $|y|$ . The weight- $k$ shell $E_k$ contains all errors with $|y|=k$ . Choose $0\le\ell\le m$ and real weights $w_0,\ldots,w_\ell$ . The ideal syndrome-space state in equation (140) sums $(-1)^{v\cdot y}|B^\top y\rangle$ over each $E_k$ , multiplied by $w_k/\sqrt{\binom m k}$ . Jordan et al., equations (140) and (171).

A deterministic decoder $\mathrm{dec}:\mathbb F_2^n\to\mathbb F_2^m$ guesses an error from its syndrome. It correctly identifies $y$ when $\mathrm{dec}(B^\top y)=y$ . Write $D_k\subseteq E_k$ for the correctly identified errors and $F_k=E_k\setminus D_k$ for the failures. The shell failure rate is $\varepsilon_k=|F_k|/\binom m k$ , and $\varepsilon=\max_{0\le k\le\ell}\varepsilon_k$ . Postselecting successful decoding leaves the unnormalized state $\widetilde P_D(f)$ formed by replacing each $E_k$ in the ideal state with $D_k$ . Apply the binary Hadamard transform, divide by the resulting norm, measure $x$ , and evaluate $f_v(x)$ . Denote this measured expectation by $\langle f_v\rangle$ . Jordan et al., §10.3, pp. 39–40.

Formalization targets

Theorem 10.1: the averaged objective

Let $N=\sum_{k=0}^{\ell}w_k^2(1-\varepsilon_k)$ be the squared norm of the postselected state. The goal, for $N>0$ and uniform $v\in\mathbb F_2^m$ , is

\mathbb E_v\langle f_v\rangle\ge \frac{w^\top A^{(m,\ell,0)}w-2\varepsilon(m+1)w^\top w}{N}.

The matrix $A^{(m,\ell,0)}$ is the symmetric tridiagonal matrix in equation (70): its diagonal is zero and its entries adjacent to the diagonal are $a_k=\sqrt{k(m-k+1)}$ . This is the first inequality of (172), with the decoder's actual failure fractions in $N$ and the worst shell failure rate in the correction. It has no minimum-distance hypothesis. Jordan et al., Theorem 10.1, pp. 39–40.

Supporting targets

The milestone list includes the norm identity of Lemma 10.4, the ideal and postselected objective matrices of Lemmas 10.2 and 10.5, the normalized expectation identity in (179), the averaged matrix identities of Lemmas 10.3 and 10.6, and the error-matrix bound of Lemma 10.7. A separate companion item records the second comparison printed in (172) under an explicit sign condition; without that condition, the printed comparison can fail. Jordan et al., §10, pp. 36–43.

Significance

The result assigns a quantitative cost to decoding errors. It says how the measured max-XORSAT objective changes when some error patterns are lost during postselection, while permitting a code whose low-weight errors share syndromes. Consequently the theorem addresses the setting in which practical decoding succeeds often but exact distance-based uniqueness is unavailable. The denominator also records the survival probability of the weighted state, so the bound keeps the actual normalization visible. Jordan et al., §10, pp. 35 and 39–43.

A complete formalization would provide reusable definitions for binary syndrome decoding, shellwise failure rates, real-amplitude states, normalized measurement expectations, and finite objective matrices. The paper proves the result on paper; this mission asks for machine-checked proofs of the stated goal and its milestones. The formal development would also document exactly which part of equation (172) requires an additional sign assumption. No proof is claimed by the draft statements themselves.

Difficulty

When two errors have the same syndrome, the ideal syndrome state can combine their amplitudes, so its norm need not equal $w^\top w$ . Postselection changes which errors remain, and the measured objective depends on the normalized state for each $v$ . Replacing that normalized expectation with the objective of an average state would change the claim. The proof must keep the decoder fixed while $v$ varies and must control the error matrix uniformly over every real weight vector. The printed second inequality of (172) adds a separate sign issue: a smaller positive denominator reverses the expected comparison when the numerator is negative. Jordan et al., equations (161), (171)–(172), (179)–(182).

Formalization scope

Lean uses ZMod 2 for bits, Fin m and Fin n for zero-based coordinates, functions for binary vectors, and Matrix for $B$ . The decoder is one function of the syndrome, independent of $v$ . Hamming shells, correct and failed decoding sets, and $\varepsilon_k$ are computed from that function. Weights and amplitudes are real. The postselected state uses the factor $1/\sqrt{\binom m k}$ ; the Hadamard transform uses $1/\sqrt{2^n}$ . The average over $v$ is the sum over all $2^m$ vectors divided by $2^m$ . The tridiagonal entries compute $m-k$ in the reals, preserving the square-root formula at the boundary.

Two domain conditions are made explicit. The bound $\ell\le m$ rules out absent weight shells, for which Lean would otherwise assign zero to division by $\binom m k=0$ . The condition $N>0$ rules out a zero postselected state, whose normalized expectation would likewise be assigned a meaningless zero by total real division. The goal ranges over every binary matrix, every fixed deterministic decoder, and every real weight vector satisfying those conditions. It states the expectation of the explicit postselected state after a Hadamard transform, rather than an unconstrained expectation variable.

The supporting development needs finite character sums, Hamming-shell cardinalities, matrix quadratic forms, and an operator bound for a symmetric real matrix. These components can serve other finite decoding and quantum-state calculations. Contributions proving the seven cited milestones or the goal are within scope. The circuit's resource accounting, asymptotic equation (173), and numerical decoder studies are outside this mission.

Selected references

S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, and R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025 revision of the 2024 preprint. arXiv

10 thms2 active usersReviewed

Differential Geometry Machine Learning Probability·Captain: mikedeng1

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 2: ZO-RSGD Has Average Expected Squared Riemannian Gradient Norm at Most 4L(f(x₀) − f(x*))/(N+1) + 2μ²L²(d+6)³ + 16(d+4)σ²/mResearch Paper

Motivation

Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.

In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb R^n$ ), and let $\mathcal M \subseteq E$ be a $C^1$ embedded submanifold of dimension $d$ . The tangent space $T_x\mathcal M$ at $x \in \mathcal M$ is the linear span of the tangent cone of $\mathcal M$ at $x$ . For a submanifold this is the set of velocities $\gamma'(0)$ of curves in $\mathcal M$ through $x$ , and it is a subspace of dimension $d$ . $\mathcal M$ carries the metric induced by the inner product of $E$ , and $P_x$ denotes the orthogonal projection of $E$ onto $T_x\mathcal M$ .

A retraction is a map $R$ , $(x, \eta) \mapsto R_x(\eta)$ . For every $x \in \mathcal M$ it sends all of $T_x\mathcal M$ into $\mathcal M$ and is smooth on $T_x\mathcal M$ , with $R_x(0) = x$ and differential the identity at $0$ . The Riemannian gradient of a differentiable $f$ is $\operatorname{grad} f(x) = P_x \nabla f(x)$ .

The objective is stochastic, $f(x) = \mathbb E_\xi F(x, \xi)$ , with noise $\xi$ distributed according to a probability measure $P_\xi$ . Two assumptions are imposed:

Assumption 2.1 ( $L$ -retraction-smoothness). For almost every $\xi$ , $|F(R_x(\eta),\xi) - F(x,\xi) - \langle \operatorname{grad}F(x,\xi), \eta\rangle| \le \frac L2\|\eta\|^2$ for all $x \in \mathcal M$ and $\eta \in T_x\mathcal M$ .
Assumption 2.3 (unbiased oracle, bounded variance). For every $x \in \mathcal M$ , $\mathbb E_\xi F(x,\xi) = f(x)$ , $\mathbb E_\xi \operatorname{grad}F(x,\xi) = \operatorname{grad}f(x)$ and $\mathbb E_\xi\|\operatorname{grad}F(x,\xi) - \operatorname{grad}f(x)\|^2 \le \sigma^2$ .

Given a smoothing parameter $\mu > 0$ and a batch size $m$ , draw $m$ independent pairs $(u_{0,i}, \xi_i)$ , each with $u_{0,i} \sim \mathcal N(0, I)$ independent of $\xi_i \sim P_\xi$ , and put $u_i = P_x u_{0,i}$ . The mini-batch zeroth-order Riemannian gradient is

\bar g_{\mu,\xi}(x) = \frac1m\sum_{i=1}^m \frac{F(R_x(\mu u_i), \xi_i) - F(x, \xi_i)}{\mu}\,u_i .

ZO-RSGD (Algorithm 2) starts at $x_0 \in \mathcal M$ and iterates $x_{k+1} = R_{x_k}(-\hat\eta\,\bar g_{\mu,\xi}(x_k))$ with step $\hat\eta = 1/L$ and a fresh batch at every step. $x^*$ denotes a minimizer of $f$ over $\mathcal M$ .

Formalization targets

Goal: Theorem 3.2

If $m \ge 16(d+4)$ , then for every $N$

\frac{1}{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2 \le 4L\,\frac{f(x_0) - f(x^*)}{N+1} + 2\mu^2L^2(d+6)^3 + \frac{16(d+4)}{m}\sigma^2 .

The constants are the paper's own. The goal states the rate for every $\mu$ , $m$ and $N$ . It does not state the parameter choices $\mu = O(\epsilon/d^{3/2})$ , $m = O(d\sigma^2/\epsilon^2)$ , $N = O(1/\epsilon^2)$ that follow from it.

Milestones

Lemma 2.1. For a $d$ -dimensional subspace $\mathcal X$ with projection $P$ , $u = Pu_0$ and $x \in \mathcal X$ : $\mathbb E\langle x,u\rangle u = x$ and $\mathbb E\langle x,u\rangle^2 = \|x\|^2$ .
Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p \le (n+p)^{p/2}$ for a standard Gaussian $u$ on $\mathbb R^n$ and $p \ge 2$ . This is already proved on the platform and is reused.
Corollary 2.1. $\mathbb E\|Pu_0\|^p \le (d+p)^{p/2}$ .
Proposition 2.1(a). $\|\mathbb E\,g_\mu(x) - \operatorname{grad}f(x)\| \le \frac{\mu L}{2}(d+3)^{3/2}$ for the single-sample estimator $g_\mu$ .
Lemma 3.1. $\mathbb E\|\bar g_{\mu,\xi}(x) - \operatorname{grad}f(x)\|^2 \le \mu^2L^2(d+6)^3 + \frac{8(d+4)}{m}\sigma^2 + \frac{8(d+4)}{m}\|\operatorname{grad}f(x)\|^2$ .

Significance

Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an $\epsilon$ -stationary point in expectation after $O(d/\epsilon^4)$ noisy function evaluations. The dependence is on the manifold dimension $d$ , not on the ambient dimension $n$ . This matches the Euclidean rate of Ghadimi and Lan with $n$ replaced by $d$ , and it is what makes projected-Gaussian estimators attractive when $d \ll n$ (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).

The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use $x + \mu u$ instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.

Difficulty

The Euclidean argument relies on a smoothed function $f_\mu(x) = \mathbb E f(x + \mu u)$ whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: $R_x(\mu u)$ is not a translate, so $\mathbb E\,g_\mu(x)$ is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.

The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step $k$ is projected onto $T_{x_k}\mathcal M$ , which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, $m \ge 16(d+4)$ .

Formalization scope

$E$ is any finite-dimensional real inner product space with its Borel σ-algebra. The Gaussian is Mathlib's stdGaussian E.
$\mathcal M$ and its dimension are given by the published ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a $C^1$ coordinate-slice submanifold), so $d$ is tied to $\mathcal M$ and is never a free number. $T_x\mathcal M$ is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.
The retraction is defined on all of each tangent space, as the paper requires (Assumption 2.1 holds "for all $\eta \in T_x\mathcal M$ , i.e., $\rho_x = \infty$ "). The objective $f$ and the samples $F(\cdot,\xi)$ are assumed differentiable rather than smooth, which is all the gradient formula (2.3) uses.
Added hypotheses. The goal assumes $m \ge 16(d+4)$ . The paper's proof assumes it explicitly, but the theorem statement omits it. The goal also assumes that $(x,\eta) \mapsto R_x(\eta)$ and $x \mapsto P_x$ are measurable, so that the iterates are random variables; this holds for closed $\mathcal M$ such as spheres and Stiefel manifolds. Lemma 3.1 is stated for every $m \ge 1$ . The paper's last proof step uses $m \ge 2$ , but the bound holds for $m = 1$ as well.
The iterates are defined for every $k$ on the sequence space of i.i.d. batches (the algorithm without a stopping index), so $x_{N+1}$ exists.
No junk expectations. Every expectation of a nonnegative quantity is a lower Lebesgue integral compared with ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of $F(x,\cdot)$ and $\operatorname{grad}F(x,\cdot)$ . So no statement can hold because a Bochner integral defaulted to $0$ .
The $O(\cdot)$ parameter choices (3.10) and the oracle complexity $mN = O(d/\epsilon^4)$ are not formalized.
The development needs projections of Gaussian measures onto subspaces, moments of Gaussian norms, conditional expectation along an i.i.d. sequence of batches, and telescoping. Proofs of any milestone are welcome, as are general lemmas about the push-forward of stdGaussian under an orthogonal projection.

Selected references

J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023. Preprint arXiv:2003.11238v3. https://arxiv.org/abs/2003.11238
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://arxiv.org/abs/1309.5549
K. Balasubramanian, S. Ghadimi, Zeroth-Order Nonconvex Stochastic Optimization: Handling Constraints, High Dimensionality, and Saddle Points, Foundations of Computational Mathematics, 2022. https://arxiv.org/abs/1809.06474
N. Boumal, P.-A. Absil, C. Cartis, Global Rates of Convergence for Nonconvex Optimization on Manifolds, IMA Journal of Numerical Analysis, 2019. https://arxiv.org/abs/1605.08101
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008.

13 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 8(iii)

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

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

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

Milestones

In the order of the attack:

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

The standing assumptions are hypotheses of the statements:

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

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

Disclosed corrections of the printed text:

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

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

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

Selected references

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

13 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem II: For Random Signs the QAOA Expectation Concentrates Above (1/2 + sin γ cos^(3D) γ/2)mResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) prepares a parametrized quantum state whose measurement yields a candidate solution of a combinatorial optimization problem. Its level-one version alternates a single phase operator and a single mixing operator and is simple enough to analyse by hand. In arXiv:1412.6062 the same authors applied it to Max E3LIN2 with bounded occurrence: given linear equations mod 2, each on exactly three bits, with every bit in at most $D+1$ equations, satisfy as many equations as possible. A uniformly random string satisfies half of them in expectation; the question is by how much an algorithm can beat $\tfrac12$ .

Without the occurrence bound no efficient algorithm achieves $\tfrac12+\epsilon$ unless P = NP (Håstad, J. ACM 2001). With every bit in at most $D+1$ equations the history, as recounted on pp. 2–3 of the paper, is:

2000: Håstad gave a classical algorithm with approximation ratio $\tfrac12+\Omega(1/D)$ (Inf. Process. Lett. 74).
2001: Trevisan showed that an efficient algorithm achieving $\tfrac12+c/D^{1/2}$ for a sufficiently large constant $c$ would imply P = NP (STOC).
2014: the first version of this paper showed that the level-one QAOA satisfies at least $\big(\tfrac12+\tfrac1{22D^{3/4}}\big)m$ equations.
2015: Barak et al. gave an efficient classical algorithm reaching $\big(\tfrac12+\Omega(D^{-1/2})\big)m$ on every instance (arXiv:1505.03424); the second version of this paper improved the QAOA worst-case bound to $\big(\tfrac12+\tfrac1{101D^{1/2}\ln D}\big)m$ (Section II).

Section III, formalized here, studies the typical case: it fixes the triples and draws the right-hand sides at random, and shows that the QAOA then reaches an advantage of order $D^{-1/2}$ , the order of the classical algorithm, on all but a vanishing fraction of the instances.

Setting

An instance on $n$ bits with $m$ equations is a list of triples $(a_i,b_i,c_i)$ with $a_i<b_i<c_i$ , no triple repeated, together with right-hand sides $r_i\in\{0,1\}$ ; equation $i$ is $x_{a_i}+x_{b_i}+x_{c_i}\equiv r_i\pmod 2$ . The instance has occurrence at most $D+1$ if every bit lies in at most $D+1$ triples. Write $z_v=(-1)^{x_v}$ and $d_i=(-1)^{r_i}$ ; equation $i$ is satisfied by $x$ exactly when $z_{a_i}z_{b_i}z_{c_i}=d_i$ .

Let $C(x)$ be the number of equations satisfied by $x$ , viewed as a diagonal operator on the $2^n$ -dimensional space spanned by $|x\rangle$ , let $B=\sum_v X_v$ , and let $|s\rangle$ be the uniform superposition. For angles $\gamma,\beta$ the level-one QAOA state is

|\gamma,\beta\rangle=e^{-i\beta B}e^{-i\gamma C}|s\rangle .

Measuring it in the computational basis gives a string; $N(\gamma,\beta)=\sum_x|\langle x|\gamma,\beta\rangle|^2C(x)$ is the expected number of satisfied equations.

In Section III the triples are fixed and the instance is drawn uniformly from the $2^m$ choices of right-hand sides; $\mathbb E_d$ and $\mathrm{Var}_d$ denote the mean and variance over this choice. The mixing angle is $\beta=\pi/4$ and the state analysed is $|-\gamma,\pi/4\rangle$ , following the paper's sign convention.

For an equation with bits $1,2,3$ , the polynomial $c_\rho(z)=\sum d_{\rho ab}z_az_b$ collects the equations that share exactly the bit $\rho$ with it, and $D_\rho$ is its number of terms.

Formalization targets

Goal: concentration above the mean bound

For every E3LIN2 family of $m$ triples with occurrence at most $D+1$ , every $\gamma\in[0,\pi/2]$ and every $t>0$ ,

\Pr_d\Big[N(-\gamma,\pi/4)\le\frac m2+\frac m2\sin\gamma\cos^{3D}\gamma-t\Big]\le\frac{m(6D+3)(D+1)}{4t^2}.

With $t=c\sqrt m$ and $D$ fixed, all but a fraction $(6D+3)(D+1)/(4c^2)$ of the instances reach $\big(\tfrac12+\tfrac12\sin\gamma\cos^{3D}\gamma\big)m-c\sqrt m$ . This is the paper's closing sentence of Section III with an explicit failure probability.

Milestones

(55): $N(-\gamma,\pi/4)=\tfrac m2+\sum_i\tfrac12d_i\langle Z_{a_i}Z_{b_i}Z_{c_i}\rangle$ .
(25): the single-clause term equals $\tfrac18d\,\mathbb E_z\big[\sum_{\pm}\sin(\gamma(d\pm c_1\pm c_2\pm c_3))\big]$ over four sign patterns.
(47): averaging over the clause's own sign gives $\tfrac12\sin\gamma\,\mathbb E_z[\cos\gamma c_1\cos\gamma c_2\cos\gamma c_3]$ .
(48): $\mathbb E_d[\cos\gamma c_\rho(z)]=(\cos\gamma)^{D_\rho}$ for every $z$ .
(49): $\mathbb E_d$ of the clause term is $\tfrac12\sin\gamma(\cos\gamma)^{D_1+D_2+D_3}$ , with $D_1+D_2+D_3\le3D$ .
(50): for $\gamma\in[0,\pi/2]$ , $\tfrac m2\sin\gamma\cos^{3D}\gamma\le\mathbb E_d[N-\tfrac m2]\le\tfrac m2\sin\gamma$ .
(57): clause terms whose (25) expressions share no sign are uncorrelated.
Linked count: each equation is linked to at most $(6D+3)(D+1)$ equations.
Variance: $\mathrm{Var}_d\,N(-\gamma,\pi/4)\le\tfrac14m(6D+3)(D+1)$ .
(51)–(53): $D^{1/2}\sin\gamma_D\cos^{3D}\gamma_D\to1/\sqrt{3e}$ at $\gamma_D=1/\sqrt{3D}$ .

Significance

The result shows that on random-sign instances with any fixed bounded-occurrence structure, a single layer of QAOA beats a random assignment by $\Theta(D^{-1/2})m$ , the same order as the best known classical guarantee and better than the paper's own worst-case bound by a logarithmic factor. It was one of the first concrete performance statements for the QAOA on a problem where its advantage over random guessing could be compared with the best classical guarantee. The average-case technique, an exact single-clause formula followed by an average over independent signs and a dependency count, applies to other local constraint problems.

The statements are proved in the paper by hand; none of them, and no QAOA performance bound, has a machine-checked proof on the platform. The mission produces a verified link from the quantum state to a classical average (25), a finite second-moment method over sign vectors, and an explicit Chebyshev form of the concentration claim.

Difficulty

The central step is (25): turning the expectation of $Z_aZ_bZ_c$ in the state $e^{-i\beta B}e^{-i\gamma C}|s\rangle$ into a classical average over bits. It requires conjugating three Pauli operators through the mixer at $\beta=\pi/4$ , expanding the phase operator around the three bits, and showing that equations sharing two bits with the clause cancel. A direct computation in the $2^n$ -dimensional space does not scale with $n$ and does not give a closed form.

For the variance, the naive bound by $m^2$ pairs gives nothing. The argument needs exact independence of clause terms whose sign dependencies are disjoint, which rests on (25) showing that each term depends only on its own sign and on the signs of the equations sharing exactly one bit with it, and then a combinatorial count of linked pairs.

Formalization scope

Bit strings are Fin n → Bool with true the bit $1$ ; the quantum layer reuses the published QAlgorithms definitions (Qubits, act, prob, uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary). The phase operator is the full count of satisfied equations, which differs from the paper's $C$ of (6) by the constant $m/2$ ; the resulting states differ by a global phase and all probabilities agree. Triples are strictly increasing and pairwise distinct, which encodes "exactly three variables" and $d_{abc}\in\{0,\pm1\}$ . $D$ is a natural number. $\mathbb E_d$ is the uniform average over all $2^m$ right-hand-side vectors, $\mathbb E_z$ over all $2^n$ strings.

Two pins are disclosed. The angle range $0\le\gamma\le\pi/2$ is added to (50) and the goal, since the lower bound needs $\sin\gamma,\cos\gamma\ge0$ . The goal's threshold is (50)'s exact lower bound, not the paper's (54): $\big(\tfrac12+\tfrac1{2\sqrt{3e}D^{1/2}}\big)m$ is the large- $D$ limit and is false at every finite $D$ , so (51)–(53) are stated as a limit instead. The goal is about the expected satisfied count of the measured state; the sampling procedure, circuit size and the search over $\gamma$ are out of scope.

A trivializing reading is excluded: the probability is over the $2^m$ instances on the fixed triples, not over a single instance, and the bound is about the quantum expectation at $|-\gamma,\pi/4\rangle$ (at $+\gamma$ the mean has the opposite sign and the statement would be false).

A complete development needs finite averages over $\{0,1\}^m$ with independence of coordinates, the single-clause formula (25) in the $2^n$ -dimensional Hilbert space, and Chebyshev's inequality on a finite uniform space. The (25) computation and the second-moment count are reusable for other QAOA analyses. Contributions to any milestone are welcome, in any order.

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem, arXiv:1412.6062v2, 2015. https://arxiv.org/abs/1412.6062
E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv:1411.4028, 2014. https://arxiv.org/abs/1411.4028
B. Barak, A. Moitra, R. O'Donnell, P. Raghavendra, O. Regev, D. Steurer, L. Trevisan, A. Vijayaraghavan, D. Witmer, J. Wright, Beating the random assignment on constraint satisfaction problems of bounded degree, APPROX/RANDOM 2015. https://arxiv.org/abs/1505.03424
J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74(1), 2000. (cited as [3] in arXiv:1412.6062v2)
L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. STOC 2001 (cited as [4] in arXiv:1412.6062v2)

17 thms2 active usersReviewed

Differential Geometry Machine Learning Probability·Captain: mikedeng1

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 1: ZO-RGD Has Average Expected Squared Riemannian Gradient Norm at Most 8(d+4)L(f(x₀) − f(x*))/(N+1) + 8(d+4)L·C(μ)Research Paper

Motivation

Many optimization problems in statistics and machine learning constrain the variable to a smooth manifold: orthonormal frames in sparse PCA and dictionary learning (the Stiefel manifold), unit vectors in phase retrieval (the sphere), fixed-rank matrices in matrix completion. Riemannian optimization handles these problems directly on the manifold. A step is taken in the tangent space and mapped back to the manifold by a retraction.

In several applications the objective can be evaluated but not differentiated: black-box adversarial attacks, simulation-based models, and hyperparameter or policy tuning. Zeroth-order (derivative-free) methods replace the gradient by an estimator built from function values. In Euclidean space the standard construction is Gaussian smoothing, analysed by Nesterov and Spokoiny (2017) and Ghadimi and Lan (2013). Li, Balasubramanian and Ma (arXiv:2003.11238; Mathematics of Operations Research, 2023) carry the construction over to embedded submanifolds. They sample a Gaussian vector, project it onto the tangent space, and use the retraction in place of the straight line $x+\mu u$ . This mission formalizes their first optimization guarantee: the convergence rate of zeroth-order Riemannian gradient descent (ZO-RGD).

Setting

Let $E$ be a finite-dimensional real inner product space (the ambient $\mathbb R^n$ ). Let $M\subseteq E$ be a $C^1$ embedded submanifold of dimension $d$ . At each $x\in M$ the tangent space $T_xM$ is a $d$ -dimensional linear subspace of $E$ ; let $P_x$ denote the orthogonal projection onto it. $M$ carries the metric induced by the inner product of $E$ .

A retraction is a map $(x,\eta)\mapsto R_x(\eta)$ such that, for every $x\in M$ , $R_x$ is smooth on $T_xM$ , maps $T_xM$ into $M$ , satisfies $R_x(0)=x$ , and has the identity as its differential at $0$ . In this mission $R_x$ is defined on all of $T_xM$ .

For a differentiable $f:E\to\mathbb R$ the Riemannian gradient is $\operatorname{grad} f(x)=P_x\nabla f(x)$ . Assumption 2.1 (retraction smoothness) asks for a constant $L\ge0$ such that

\big|f(R_x(\eta))-f(x)-\langle \operatorname{grad} f(x),\eta\rangle\big|\le \tfrac L2\|\eta\|^2\qquad(x\in M,\ \eta\in T_xM).

Given $\mu>0$ and a standard Gaussian vector $u_0\sim N(0,I_n)$ of $E$ , set $u=P_xu_0$ . The zeroth-order Riemannian gradient estimator is

g_\mu(x)=\frac{f(R_x(\mu u))-f(x)}{\mu}\,u .

ZO-RGD (Algorithm 1) starts at $x_0\in M$ , draws independent Gaussian vectors $u_0^0,u_0^1,\dots$ , and sets $x_{k+1}=R_{x_k}(-\hat\eta\, g_\mu(x_k))$ , where $g_\mu(x_k)$ uses $u_k=P_{x_k}u_0^k$ . The step size is $\hat\eta=1/(2(d+4)L)$ . Let $x^*\in M$ be a minimizer of $f$ over $M$ .

Formalization targets

Goal: Theorem 3.1

For every $N\ge0$ ,

\frac1{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2\le\frac4{\hat\eta}\left(\frac{f(x_0)-f(x^*)}{N+1}+C(\mu)\right),

where $4/\hat\eta=8(d+4)L$ and

C(\mu)=\frac{\mu^2L}{16}\frac{(d+3)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{(d+4)^2}.

Milestones

These are the paper's own intermediate results (§2.2, p. 8):

Lemma 2.1. For a subspace $\mathcal X$ with projection $P$ , $u=Pu_0$ and $x\in\mathcal X$ : $\mathbb E\langle x,u\rangle u=x$ and $\mathbb E\langle x,u\rangle^2=\|x\|^2$ .
Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p\le(n+p)^{p/2}$ for $p\ge2$ . This result is already on the platform as a proved theorem and is referenced.
Corollary 2.1. If $\dim\mathcal X=d$ , then $\mathbb E\|Pu_0\|^p\le(d+p)^{p/2}$ .
Proposition 2.1(a). $\|\mathbb E g_\mu(x)-\operatorname{grad} f(x)\|\le\frac{\mu L}{2}(d+3)^{3/2}$ .
Proposition 2.1(b). $\|\operatorname{grad} f(x)\|^2\le2\|\mathbb E g_\mu(x)\|^2+\frac{\mu^2}{2}L^2(d+6)^3$ .
Proposition 2.1(c). $\mathbb E\|g_\mu(x)\|^2\le\frac{\mu^2}{2}L^2(d+6)^3+2(d+4)\|\operatorname{grad} f(x)\|^2$ .

Significance

Theorem 3.1 shows that ZO-RGD reaches an $\epsilon$ -stationary point in expectation using $O(d/\epsilon^2)$ function evaluations, provided the smoothing parameter is of order $\epsilon/d^{3/2}$ . The dimension that enters is the intrinsic dimension $d$ of the manifold, not the ambient dimension $n$ . For the Stiefel manifold of $n\times p$ orthonormal frames this is the difference between $np-p(p+1)/2$ and $np$ , and for the sphere between $n-1$ and $n$ . More importantly, the estimator never explores normal directions. The three estimates of Proposition 2.1 are the toolkit that the paper reuses for its stochastic (ZO-RSGD), proximal (ZO-ManPG) and second-order variants.

The paper proves these results on paper; none of them has a machine-checked proof. The mission adds three things. It gives a precise model of a random iterate sequence on a submanifold, driven by the infinite product of Gaussian draws. It formalizes the projected-Gaussian identities, which are reusable for any method that samples in tangent spaces. And it pins down the constants. In checking the constants, the printed Proposition 2.1(b) turned out to be false for large $L$ (its proof yields $L^2$ , not $L$ ), and the middle term of the printed $C(\mu)$ inherits that slip. The statements here carry the constants the proofs actually give.

Difficulty

In Euclidean space, $\mathbb E\,g_\mu(x)$ is exactly the gradient of the Gaussian-smoothed function $f_\mu(x)=\mathbb E f(x+\mu u)$ , and the analysis runs on $f_\mu$ . Once a retraction replaces $x+\mu u$ , no smoothed function has $\mathbb E g_\mu$ as its gradient. The bias must be estimated directly from Assumption 2.1, which controls $f\circ R_x$ only along the tangent space. The moment bounds must then be taken for a Gaussian projected onto a subspace that changes with $x$ .

In the descent argument, the direction $u_k$ is sampled in $T_{x_k}M$ , which depends on all earlier draws. The expectation of step $k$ is therefore conditional on the past. Summing the one-step inequality requires conditional expectations on the product space, together with measurability of the iterate map. Finiteness of $\mathbb E f(x_k)$ is not given and must be handled as well.

Formalization scope

Space. The ambient space is a finite-dimensional real inner product space $E$ . The standard Gaussian is Mathlib's stdGaussian E, so $\kappa^{-1}\int\cdots e^{-\|u_0\|^2/2}du_0$ becomes integration against it.
Manifold and tangent spaces. The manifold is given by the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold 1 d M, which ties $d$ to $M$ . The tangent space is the published ProjLikeRetr.Retractor.tangentSpace M x, the span of Mathlib's tangent cone. Neither $d$ nor the tangent spaces are free parameters.
Retraction. The retraction is global: Assumption 2.1 is required for every $\eta\in T_xM$ (the paper's " $\rho_x=\infty$ "). "Smooth" means $C^\infty$ , not analytic.
Regularity of $f$ . $f$ is assumed differentiable on $E$ , which is what the definition $\operatorname{grad} f=P_x\nabla f$ needs. This is weaker than the paper's "smooth".
Constants. The goal takes $L>0$ , because the step size divides by $L$ . The milestones take $L\ge0$ and $\mu>0$ .
Draws and iterates. The draws live on $E^{\mathbb N}$ with the infinite product of standard Gaussian measures. The iterates are defined for every $k$ : the algorithm runs without a stopping time, so the sum over $k=0,\dots,N$ is meaningful.
Minimizer. $x^*$ is an attained minimizer over $M$ .
Measurability. The goal adds two measurability hypotheses that make the iterates random variables: $(x,\eta)\mapsto R_x(\eta)$ is measurable and $x\mapsto P_x$ is measurable. Both hold for closed manifolds such as spheres and Stiefel manifolds.
Corrected constants. Proposition 2.1(b) carries $L^2$ , and the middle term of $C(\mu)$ carries $L$ . The milestone texts keep the printed forms. Proposition 2.1(a) and (c) are as printed.
Not formalized. The parameter choices $\mu=O(\epsilon/d^{3/2})$ , $N=O(d/\epsilon^2)$ in the theorem's second sentence are an $O(\cdot)$ statement.

Several trivializing formalizations are ruled out. A Bochner integral of a non-integrable function is $0$ , so every expectation in a conclusion is either a lower Lebesgue integral compared with a finite bound or paired with an integrability conjunct. The dimension $d$ comes from the manifold, not from a free natural number. The projection is onto $M$ 's own tangent space, never onto an arbitrary subspace field.

A complete development needs the following infrastructure:

the law of $P u_0$ (a standard Gaussian on the subspace);
Gaussian moment bounds;
conditional expectation along the product filtration;
measurability of the iterate map.

The projected-Gaussian lemmas and the iterate model are reusable for the stochastic variant (ZO-RSGD) in the companion mission. Contributions of proofs for any milestone, and of general lemmas about Gaussian measures restricted to subspaces, are welcome.

Selected references

J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023; preprint arXiv:2003.11238v3, 2021. https://arxiv.org/abs/2003.11238
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17 (2017) 527–566. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23 (2013) 2341–2368. https://doi.org/10.1137/120880811
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

13 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Reinforcement Learning·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 7.1

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

8 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Reinforcement Learning·Captain: mikedeng1

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

Motivation

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6.3 (p. 12)

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

10 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem I: Level-One QAOA Satisfies (1/2 + 1/(101 D^(1/2) ln D))m Equations of Max E3LIN2 for Large DResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) is a family of shallow quantum circuits for combinatorial optimization. At its lowest level, $p = 1$ , the circuit has two real parameters, and its output is a random bit string. The question is how many constraints that string satisfies, compared with the best classical algorithms.

Max E3LIN2 is a natural test problem. Each constraint is a linear equation modulo $2$ on exactly three bits, and the task is to satisfy as many of the $m$ equations as possible. A uniformly random string satisfies $m/2$ in expectation, and for general instances no efficient algorithm does better than $(1/2 + \varepsilon)m$ unless P = NP (Håstad 2001). The interesting regime is bounded occurrence: every bit lies in at most $D + 1$ equations.

Timeline, as recorded on p. 3 of the paper:

2000: Håstad gives a classical algorithm with approximation ratio $1/2 + \mathrm{const}/D$ (doi:10.1016/S0020-0190(00)00032-6).
2001: Trevisan shows that an efficient algorithm with ratio $1/2 + \mathrm{const}/D^{1/2}$ , for a sufficiently large constant, would imply P = NP (doi:10.1145/380752.380839).
December 2014: the first version of this paper shows that the $p = 1$ QAOA yields a string satisfying $(1/2 + 1/(22D^{3/4}))m$ equations. That beat every classical algorithm known at the time.
2015: Barak et al. (arXiv:1505.03424) and Håstad give efficient classical algorithms reaching $(1/2 + \mathrm{const}/D^{1/2})m$ .
June 2015: version 2 of this paper (arXiv:1412.6062v2) improves the QAOA bound to $(1/2 + 1/(101D^{1/2}\ln D))m$ . This mission formalizes that bound.

Setting

An instance on $n$ bits consists of $m$ equations. Equation $i$ is

x_a + x_b + x_c \equiv r_i \pmod 2,

on a triple of distinct bits $a < b < c$ , with right-hand side $r_i \in \{0, 1\}$ , and no triple carries two equations. The instance has occurrence bound $D$ if every bit appears in at most $D + 1$ equations.

Let $C(z)$ be the number of equations satisfied by the string $z$ , viewed as a diagonal operator on the $2^n$ -dimensional space spanned by the basis states $|z\rangle$ . Let $B = X_1 + \dots + X_n$ be the sum of the Pauli $X$ operators, and $|s\rangle$ the uniform superposition of all basis states. For real angles $\gamma, \beta$ the level-one QAOA state is

|\gamma, \beta\rangle = e^{-i\beta B} e^{-i\gamma C} |s\rangle .

Measuring it in the computational basis returns $z$ with probability $|\langle z|\gamma,\beta\rangle|^2$ . The expected satisfied count is

F(\gamma, \beta) = \sum_z |\langle z|\gamma,\beta\rangle|^2\, C(z).

The paper writes the objective as $m/2 + \tfrac12\sum d_{abc} Z_a Z_b Z_c$ , with $d_{abc} = (-1)^{r}$ for the equation on $a, b, c$ . The analysis is phrased through the shifted quantity $\langle\gamma,\beta|\tfrac12\sum d_{abc}Z_aZ_bZ_c|\gamma,\beta\rangle = F(\gamma,\beta) - m/2$ .

The angles used are $\beta = \pi/4$ and, for an odd integer $k$ ,

\gamma_r = \frac{1}{10 D^{1/2}} \cos\frac{\pi r}{k}, \qquad r = 0, 1, \dots, k .

Formalization targets

Goal: (44)–(45), pp. 8–9

There is a threshold $D_0$ such that for every $D \ge D_0$ there is an odd $k$ with $5\ln D \le k \le 5\ln D + 2$ , such that on every instance with occurrence bound $D$ some grid angle satisfies

F(\gamma_r, \pi/4) \ \ge\ \Big(\frac12 + \frac{1}{101\, D^{1/2} \ln D}\Big)\, m .

$D_0$ and $k$ depend on $D$ only, never on the instance. Equivalently, in the paper's form (44), $\max_r \langle\gamma_r,\pi/4|\tfrac12\sum d_{abc}Z_aZ_bZ_c|\gamma_r,\pi/4\rangle \ge m/(101D^{1/2}\ln D)$ .

Milestones

The milestones are the displayed claims of Section II, in the order the argument uses them:

the sum form of $F$ and its oddness in $\gamma$ (p. 4);
the exact single-clause formula (25);
the Taylor remainder bound (28);
hypercontractivity for degree-2 polynomials (29);
the second-moment bounds (31) and (32);
the uniform remainder bound (34) and the triangle-inequality step (37);
the Chebyshev-node inequality (39), and its consequence (41) on the grid;
the numerical threshold (43).

Significance

The theorem shows that a single layer of the QAOA, with fixed $\beta$ and $O(\ln D)$ predetermined angles, beats random guessing by $\Omega(m/(D^{1/2}\ln D))$ on every bounded-occurrence instance. Up to the $\ln D$ factor this matches the $1/2 + \Theta(D^{-1/2})$ threshold that Trevisan's hardness result places on efficient algorithms.

Two ingredients are reusable well beyond this paper. The hypercontractive inequality (29) bounds all moments of a degree-2 polynomial in uniform $\pm1$ variables, at every exponent $q = k + 2$ . The Chebyshev-node inequality (39) bounds from below the maximum of a polynomial with unit linear coefficient over the points $\cos(\pi r/k)$ . Neither is in Mathlib or on the platform in this generality.

The result is proved on paper, with explicit constants, but none of it has been machine-checked. A complete formalization would also pin down two places where the printed argument is loose (see Formalization scope).

Difficulty

The obvious approach is to expand the expected count as a power series in $\gamma$ and keep the linear term $m\gamma/2$ . That fails because the higher-order terms are not small: each clause interacts with up to $3D$ others, so the coefficient of $\gamma^j$ can grow like $D^{j/2}$ , and their signs are uncontrolled. Uniform small-angle estimates therefore lose the linear gain unless $|\gamma| \lesssim D^{-1/2}$ . Even there, the polynomial part of degree up to $k$ can cancel the linear term at any single angle. The step that needs a genuinely new input is showing that some angle of a short fixed grid avoids this cancellation for every instance at once. The remaining difficulty is bookkeeping: the threshold where the explicit constants start to work is enormous ( $\ln D$ of order several hundred), so it has to be existential.

Formalization scope

Representation. Strings are Qubits n = Fin n → Bool, with true the bit $1$ . An instance is tri : Fin m → Fin n × Fin n × Fin n (strictly increasing coordinates, injective) and rhs : Fin m → Bool. Bounded occurrence counts, for each bit, the equations whose triple contains it.
Reused quantum layer. The published QAlgorithms definitions supply act, prob, uniformState, problemHamiltonian, qaoaMixer and qaoaUnitary.
Phase operator. The state uses the full count $C$ as phase operator, not the paper's $C - m/2$ . This changes the state by a global phase only, so every probability is the same.
Averages. $E_z$ is the uniform average over all $2^n$ strings. The paper averages over the bits occurring in $c_1, c_2, c_3$ only, which gives the same number.
Pinned forms. "For large $D$ " is an existential threshold $D_0$ , uniform over instances. " $k = 5\ln D$ " is an odd $k$ with $5\ln D \le k \le 5\ln D + 2$ : the Chebyshev-node step requires $k$ odd, and $5\ln D$ is not an integer. The grid therefore has at most $5\ln D + 3$ angles rather than the printed "no more than $5\ln D$ ".
Added hypothesis. The remainder bound (34) and its consumers assume $D \ge 1$ . The printed last step $e(1+9D)^{1/2} \le 9D^{1/2}$ holds for $D \ge 1$ only, and the printed justification " $e < 3$ " does not by itself give it.
Scope. The goal is about the expected satisfied count of the measured $p = 1$ state, which is what the paper's analysis bounds. Out of scope: the repetition and sampling procedure after (45), running time, circuit size, and the search over angles.
No trivialization. The goal cannot be met by a degenerate encoding: $D_0$ and $k$ precede the instance, the grid angles are fixed by $D$ and $k$ , and the hypotheses on the instance (distinct bits, one equation per triple, occurrence at most $D + 1$ ) are satisfiable for every $D$ .
Infrastructure. A complete development needs moments of polynomials on the Boolean cube (hypercontractivity at general $q$ ), Taylor remainders for $\sin$ , an extremal inequality for polynomials on Chebyshev extreme points, and exponential-of-Pauli computations on $n$ qubits. Hypercontractivity and the Chebyshev-node inequality are stated independently of the QAOA and are the most reusable contributions. Proofs of any milestone are welcome. Platform statements of $L^4$ – $L^2$ Bonami inequalities for bilinear chaos exist, but they cover only $q = 4$ and do not imply (29).

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem, arXiv preprint, v2, 2015. https://arxiv.org/abs/1412.6062v2
E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028
I. Dinur, E. Friedgut, G. Kindler, R. O'Donnell, On the Fourier tails of bounded functions over the discrete cube, Israel Journal of Mathematics 160 (2007), 389–412. https://doi.org/10.1007/s11856-007-0068-z
J. Håstad, Some optimal inapproximability results, Journal of the ACM 48 (2001), 798–859. https://doi.org/10.1145/502090.502098
J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74 (2000), 1–6. https://doi.org/10.1016/S0020-0190(00)00032-6
L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. 33rd ACM STOC (2001), 453–461. https://doi.org/10.1145/380752.380839
B. Barak et al., Beating the random assignment on constraint satisfaction problems of bounded degree, ECCC TR15-082 / arXiv preprint, 2015. https://arxiv.org/abs/1505.03424

18 thms2 active usersReviewed

Number Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Lemma 1

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

9 thms2 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

The seller maximizes its profit (1),

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

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

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

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

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

Formalization targets

Goal: Proposition 3 (pp. 15–16)

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

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

Milestones

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

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Conventions and disclosed additions:

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

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

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

Selected references

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

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Proposition 4 (p. 23)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Committed conventions:

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

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

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

Selected references

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

6 thms2 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

The potential (10) of a buyer set is

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

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

Formalization targets

Goal: Proposition 5 (p. 15)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Proposition 1

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

6 thms2 active usersReviewed

Graph Theory Quantum Information·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm II: On v-Regular Graphs the Variance of the Cut Value in the QAOA State Is at Most 2((v−1)^(2p+2)−1)/(v−2) Times the Number of EdgesResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits for combinatorial optimization, indexed by a depth $p$ and $2p$ real angles. It has become one of the standard candidate algorithms for near-term quantum hardware, and its MaxCut instance is the usual benchmark on which it is analysed.

The algorithm is run by preparing a quantum state, measuring it in the computational basis to obtain a bit string $z$ , and evaluating the classical objective $C(z)$ . Its analysis in the paper bounds the mean $F_p$ of $C(z)$ . A mean alone does not say what a single run returns. Section III of the paper supplies the missing piece for MaxCut on bounded-degree graphs: the variance of $C(z)$ grows at most linearly in the number of edges, so the measured cut values are concentrated around $F_p$ and a modest number of repetitions reproduces the mean. This mission formalizes that variance bound, equation (30) of the paper, together with the locality and counting facts it rests on.

Setting

Let $G$ be a simple graph on vertices $\{0,\dots,n-1\}$ with edge set $\{\langle jk\rangle\}$ of size $m$ , each edge listed once. Vertices are qubits; a computational basis state is a bit string $z\in\{0,1\}^n$ .

The clause operator of an edge is $C_{\langle jk\rangle}=\tfrac12(-\sigma^z_j\sigma^z_k+1)$ . It is diagonal: $C_{\langle jk\rangle}(z)=1$ if $z_j\ne z_k$ and $0$ otherwise.
The MaxCut objective is $C=\sum_{\langle jk\rangle}C_{\langle jk\rangle}$ ; $C(z)$ is the number of edges cut by $z$ .
The mixer is $B=\sum_j\sigma^x_j$ , and $U(C,\gamma)=e^{-i\gamma C}$ , $U(B,\beta)=e^{-i\beta B}$ .
The initial state is $|s\rangle=2^{-n/2}\sum_z|z\rangle$ .
For $p\ge1$ and angles $\boldsymbol\gamma=(\gamma_1,\dots,\gamma_p)$ , $\boldsymbol\beta=(\beta_1,\dots,\beta_p)$ , the QAOA state is

|\boldsymbol\gamma,\boldsymbol\beta\rangle=U(B,\beta_p)\,U(C,\gamma_p)\cdots U(B,\beta_1)\,U(C,\gamma_1)\,|s\rangle .

Measuring it gives $z$ with probability $P(z)=|\langle z|\boldsymbol\gamma,\boldsymbol\beta\rangle|^2$ . The mean is $F_p(\boldsymbol\gamma,\boldsymbol\beta)=\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle=\sum_zP(z)C(z)$ and the variance is

\langle\boldsymbol\gamma,\boldsymbol\beta|C^2|\boldsymbol\gamma,\boldsymbol\beta\rangle-\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle^2 .

The light cone (the paper's subgraph $g(j,k)$ ) of an edge is the set of qubits at graph distance at most $p$ from $j$ or from $k$ .

In Lean these are edgeCut, cutValue, qaoaState, expectCut and edgeTerm in the shared FarhiQAOA.Cubic setting, and edgePairs, cutVariance, edgePairTerm, edgeCov and lightCone in FarhiQAOA.Concentration, all built on the published QAlgorithms definitions of qubit registers, measurement probabilities, the uniform superposition, the problem Hamiltonian and the QAOA unitary.

Formalization targets

Goal: the variance bound (30)

For a $v$ -regular graph with $v\ge3$ , every depth $p\ge1$ and all real angles,

\langle\boldsymbol\gamma,\boldsymbol\beta|C^2|\boldsymbol\gamma,\boldsymbol\beta\rangle-\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle^2\le2\left[\frac{(v-1)^{2p+2}-1}{(v-1)-1}\right]\cdot m .

The constant is the paper's, as printed.

Milestones

(27)–(28). The variance is the double sum, over ordered pairs of edges, of the covariances $\langle C_{\langle jk\rangle}C_{\langle j'k'\rangle}\rangle-\langle C_{\langle jk\rangle}\rangle\langle C_{\langle j'k'\rangle}\rangle$ .
Disjoint light cones. If $g(j,k)$ and $g(j',k')$ share no qubit, the covariance of the two edges is $0$ .
(26). For maximum degree $v\ge3$ , $|g(j,k)|\le2\big[((v-1)^{p+1}-1)/((v-1)-1)\big]$ .
(29). For maximum degree $v\ge3$ , at most $2\big[((v-1)^{2p+2}-1)/((v-1)-1)\big]$ edges $\langle j'k'\rangle$ have $g(j',k')$ meeting $g(j,k)$ .
Summand bound. Each covariance is at most $1$ in absolute value.

Companions, printed in the paper for $v=2$ : $|g(j,k)|\le2p+2$ and at most $4p+4$ meeting edges.

Significance

The result. For fixed $v$ and $p$ the bound makes the standard deviation of the cut value $O(\sqrt m)$ , while the mean is of order $m$ . The algorithm's output is therefore concentrated: a single measurement already returns a cut close to $F_p$ in relative terms, and the paper uses this to argue that the sample mean of polynomially many runs estimates $F_p$ within $1$ . The same locality structure, that each edge term depends only on a bounded neighbourhood, is what makes $F_p$ classically computable for fixed $p$ and underlies later analyses of QAOA on bounded-degree and random regular graphs.

Formalizing it. The bound is proved in the paper in a few lines; none of it is machine-checked. A formal proof has to make the paper's operator locality argument precise (the conjugated clause operator is supported on the light cone, and the initial state is a product state), connect it to the computational-basis probabilities, and carry out the graph counting with explicit constants. The resulting locality lemma for QAOA circuits on graphs is reusable for any statement about QAOA at fixed depth.

Difficulty

The algebra of (28) and the bound by $1$ are routine. The substance is in two places.

The vanishing of a covariance requires showing that $U^\dagger C_{\langle jk\rangle}U$ , for the full depth- $p$ QAOA unitary $U$ , acts only on the qubits of $g(j,k)$ , and that for two operators acting on disjoint sets of qubits the expectation in the product state $|s\rangle$ factorizes. Both are statements about operators on $(\mathbb C^2)^{\otimes n}$ , whereas the objects in the statement are probabilities of computational basis states; the formal proof must pass between the two. Matrix exponentials of commuting sums have to be split into commuting factors, which in Lean means working with NormedSpace.exp on matrices indexed by bit strings.

The counting (26) and (29) is a ball-growth bound in a graph of bounded degree. The paper's count, via (26) with $p$ replaced by $2p+1$ , bounds vertices, while (29) counts edges; the passage between the two, and the extended graph distance on disconnected graphs, must be made exact with the printed constant.

Formalization scope

Qubits are indexed by Fin n, bit strings are Fin n → Bool with true the bit $1$ , and states live in EuclideanSpace ℂ (Fin n → Bool).
All expectations are sums $\sum_zP(z)\,f(z)$ over the computational basis. This equals the operator expectation in the paper because every operator involved is diagonal.
Each edge is counted once (pairs $j<k$ ), in $m$ , in $C$ , in the double sum of (28) and in the count (29).
Graph distance is the extended distance SimpleGraph.edist ( $+\infty$ between components).
The goal is stated for $v$ -regular graphs with $v\ge3$ , the domain of the printed formula. The milestones (26) and (29) assume only maximum degree $\le v$ , as printed there.
The angles range over all of $\mathbb R^p$ . The paper restricts them to $[0,2\pi]$ and $[0,\pi]$ by periodicity; the bound does not depend on that restriction.
The QAOA state is the state itself, not an arbitrary vector: normalisation of the measurement probabilities follows from unitarity and is part of what must be proved.

A variance defined with two different states, or a probability vector that is not normalised, would make the goal vacuous or false; the definitions use the single state $|\boldsymbol\gamma,\boldsymbol\beta\rangle$ throughout.

Out of scope: the $O(\sqrt m)$ standard-deviation reading and the sampling claim after (30), which carry no explicit constant; the measurement-and-repetition procedure, running time, circuit depth and the classical search for the angles.

Welcome contributions: a general light-cone lemma for conjugation by products of exponentials of local Hamiltonians on qubits; factorization of product-state expectations over disjoint qubit sets; ball-size bounds in graphs of bounded degree.

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028 (v1; Section III, pp. 6–7)
E. Farhi, J. Goldstone, S. Gutmann, M. Sipser, Quantum Computation by Adiabatic Evolution, arXiv preprint, 2000. https://arxiv.org/abs/quant-ph/0001106

14 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2, first two sentences

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

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

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

7 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

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

Motivation

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

Milestones (Appendix A.4, p. 20)

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

Significance

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

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

Difficulty

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

Formalization scope

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

Committed conventions:

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

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

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

Selected references

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

4 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Achieving High Individual Service Levels Without Safety Stock? Optimal Rationing Policy of Pooled Resources I: Capacity Is Asymptotically Feasible iff E[max Σ wⱼRⱼ] ≥ Σ wⱼβⱼ for All Weights w ≥ 0Research Paper

Motivation

Firms that serve several customers from shared capacity must decide which demands to fulfil after demand is observed. A customer-level service commitment constrains the allocation policy even when total capacity appears adequate: serving one customer can consume resources that another customer needs. The question in this mission is how to test a fixed capacity vector against all individual service targets without first specifying a particular rationing rule. Jiang, Wang, and Zhang give a characterization for a broad family of pooled-resource models, including inventory pooling, process flexibility, and assemble-to-order systems (SSRN preprint, §§1.1–2).

The authors' model allows service to mean more than the probability of completely filling an order. It can represent the probability of full service, a fulfilled fraction relative to expected demand, or a fulfilled fraction of realized demand. Their Theorem 1 addresses asymptotic feasibility: every target can be met to within any prescribed positive tolerance. It is distinct from exact feasibility, which the paper treats later under stronger conditions (Jiang, Wang, and Zhang, Theorems 1–2).

Setting

There are $n$ customers and $m$ resource types. A nonnegative capacity vector $c$ is fixed before a random, nonnegative demand vector $D$ is observed. The joint law of $D$ is $F$ and has a bounded second moment. After seeing $D$ , a decision consists of a vector $s$ of fulfilled customer demands and an allocation array $y$ recording the amount of each resource assigned to each customer. The paper's set $P(c,D)$ specifies all feasible pairs $(s,y)$ for that capacity and demand. It is a model input: the three operational examples use different feasible sets (§1.1, equations (1)–(4)).

For customer $j$ , a service measure $R_j(s_j,D_j)$ assigns a nonnegative score to fulfilled demand $s_j$ and demand $D_j$ . The customer has a target $\beta_j\in(0,1)$ . A deterministic policy chooses a feasible pair in $P(c,D)$ for each $D$ . A randomized policy chooses among deterministic policies. Its expected service to customer $j$ is denoted $S_j(\lambda)$ . The capacity is asymptotically feasible when, for every $\varepsilon>0$ , some randomized policy $\lambda_\varepsilon$ satisfies $S_j(\lambda_\varepsilon)\ge\beta_j-\varepsilon$ for every customer (Definition 1, equation (8)).

For nonnegative customer weights $w=(w_j)_j$ , define maximum weighted service at a realized demand by

M_w(D)=\max_{(s,y)\in P(c,D)}\sum_j w_jR_j(s_j,D_j).

The maximum uses only service, with zero allocation cost. The paper also introduces a linear allocation cost $f(y)$ , a deterministic Max-Weighted-Service minimization problem, and its expected dual functional; Lemma 1 concerns those general objects (§2, equations (14), (16)–(17)).

Formalization targets

Theorem 1: capacity characterization

Under Assumption 1, the target is the equivalence

c\text{ is asymptotically feasible} \quad\Longleftrightarrow\quad \mathbb E_F[M_w(D)]\ge\sum_jw_j\beta_j \quad\text{for every }w\ge0.

The weights range over the whole nonnegative orthant; they are not restricted to a simplex in the theorem. Assumption 1 requires each $R_j$ to be nondecreasing and upper semicontinuous in fulfilled demand at fixed realized demand, and each $P(c,D)$ to be compact (Theorem 1, equation (18)).

Milestones from the paper

Lemma 1 identifies the value of the pointwise Max-Weighted-Service rule: $\inf_\phi F(w,\phi)=F(w,\phi_w)=\mathbb E_F[g(w,c;D)]$ for a fixed $w\ge0$ . The proof of Theorem 1 then uses a minimax display over $W=\{w\ge0:\sum_jw_j\le1\}$ to obtain, for every $\varepsilon>0$ , a randomized policy whose weighted service shortfall is at most $\varepsilon$ throughout $W$ (equation (21)). Equation (22) gives the corresponding individual service bounds. These three source claims are the mission's milestones (Lemma 1 and proof of Theorem 1, pp. 12–14).

Significance

Theorem 1 supplies a test for a vector of simultaneous service targets using a family of deterministic, weighted allocation problems. It applies to any feasible-set model satisfying the stated assumptions, rather than only to one pooling network. It also delineates the strength of the conclusion: satisfying all weighted tests guarantees arbitrarily close service, while exact attainment requires the additional assumptions in the paper's next result (Theorems 1–2).

The statements in this mission compile as Lean declarations, but their proofs have not yet been machine checked. Completing the mission would provide a reusable formal interface for demand-dependent feasible sets, measurable rationing policies, finite policy randomization, service expectations, and pointwise weighted optimization. Those definitions can also support formal study of the paper's later exact-feasibility and policy-optimality results.

Difficulty

The forward implication compares service under one policy with a maximum over feasible decisions at every demand. The reverse implication is harder: a weighted inequality for each $w$ must yield one policy that serves all customers simultaneously to a common tolerance. A separate policy chosen for each weight does not itself meet the vector of targets. The optimization involves a set of demand-dependent policies, and the source's argument relies on properties of its attainable service vectors that need explicit representation in Lean (proof of Theorem 1, pp. 13–14).

Formalization scope

Customers and resources are Fin n and Fin m, with zero-based indices; the paper numbers them from one. A solution is a pair $(s,y)$ , and $P(c,D)$ remains an arbitrary feasible set. Deterministic policies are measurable functions of $D$ that select from $P(c,D)$ for every demand realization, at the theorem's fixed capacity. Randomized policies are finite probability mixtures of these selectors. Only finitely many expected services and costs occur in the statements, and finite mixtures represent the corresponding finite-dimensional expectation vectors of the paper's policy measures. The definition of asymptotic feasibility is made directly from these policies and their service values. The maximum in the theorem is made directly from $P(c,D)$ and $R$ , so the equivalence cannot follow from defining either side in terms of the other.

The paper defines $R_j$ on nonnegative pairs. Lean uses a total real-valued extension; the theorem requires it to be nonnegative, monotone and upper semicontinuous as specified, and jointly measurable. A common integrable envelope bounds every feasible service value, preventing a nonintegrable Bochner integral from silently taking Lean's default value of zero. A measurable maximizing selector is assumed for every nonnegative $w$ ; it ensures that the expectation of $M_w(D)$ and the policy behind the source's tie-breaking are meaningful. The demand law is a probability measure with bounded second moment and nonnegative demand, capacity is nonnegative, and $\beta_j\in(0,1)$ , matching the section's standing setup. Compactness alone permits an empty feasible set in Lean; the selector assumption ensures nonemptiness at each demand.

The definitions include the linear allocation-cost functional because Lemma 1 is stated with the paper's general $f$ . An integrable envelope also bounds its absolute value in that milestone. Reusable work includes measurable selection for a demand-dependent compact feasible set, integrability of finite policy mixtures, interchange of the pointwise optimum and expectation under the stated bounds, and the finite-dimensional minimax statement. Proofs or improvements to these interfaces are welcome as long as the source claims retain their stated strength.

Selected references

J. Jiang, S. Wang, and J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, SSRN preprint 3385089, version of 31 July 2021. SSRN.
J. Jiang, S. Wang, and J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, Operations Research, 2023. DOI: 10.1287/opre.2022.2386. The mission's labels and pages follow the SSRN preprint.

5 thms2 active usersReviewed

Operations Research Statistics·Captain: mikedeng1

Design and Analysis of Switchback Experiments 1: With m-Period Carryover and T = nm, n ≥ 4, the Unique Minimax-Optimal Regular Design Flips Fair Coins at 1, 2m+1, 3m+1, …, (n−2)m+1Research Paper

Motivation

Online platforms such as ride-hailing, delivery and advertising marketplaces routinely test new pricing or matching policies on a single market. Randomizing over users is often impossible there: every rider and driver in a city shares one supply pool, so treating some users and not others contaminates the control group. The standard alternative is a switchback experiment: the whole market alternates between the new policy (treatment) and the current one (control) over time, and the effect is estimated from the time series of outcomes. Switchbacks are in production use at ride-hailing and delivery firms (see the industry references in Bojinov, Simchi-Levi and Zhao, 2023).

The design question is when to switch. Switching often produces many nearly independent observations, but a policy change has carryover effects: an outcome is affected by the policy of the last few periods, not only the current one, so frequent switching leaves few periods whose recent history is purely treated or purely control. Bojinov, Simchi-Levi and Zhao formalize this trade-off in a design-based, minimax framework and solve it in closed form. This mission formalizes that solution.

Setting

Time is divided into periods $t\in[T]=\{1,\dots,T\}$ . An assignment path is $w_{1:T}\in\{0,1\}^T$ , with $w_t=1$ meaning treatment. For every period $t$ and every path there is a fixed, unknown potential outcome $Y_t(w_{1:T})\in\mathbb R$ ; the collection is $\mathbb Y$ . Randomness comes only from the random path $W_{1:T}$ .

Three assumptions restrict $\mathbb Y$ :

Non-anticipation: $Y_t$ does not depend on $w_{t+1:T}$ .
$m$ -carryover: for $t\ge m+1$ , $Y_t$ does not depend on $w_{1:t-m-1}$ .
Boundedness: $|Y_t(w)|\le B$ for every $t$ and every path, with $B>0$ .

The set of outcomes satisfying all three is $\mathcal Y$ . Under 1–2, $Y_t(\mathbf 1_{m+1})$ and $Y_t(\mathbf 0_{m+1})$ denote the outcome after $m+1$ consecutive treatments, respectively controls. The estimand is the average lag- $m$ effect

\tau_m(\mathbb Y)=\frac1{T-m}\sum_{t=m+1}^T\bigl[Y_t(\mathbf 1_{m+1})-Y_t(\mathbf 0_{m+1})\bigr].

A regular switchback design $(\mathbb T,\mathbb Q)$ fixes randomization points $\mathbb T=\{t_0=1<t_1<\dots<t_K\}\subseteq[T]$ , $K\ge1$ , and probabilities $q_{t_k}\in(0,1)$ . At each $t_k$ an independent coin with success probability $q_{t_k}$ is flipped, and its outcome is applied to the periods $t_k,\dots,t_{k+1}-1$ (with $t_{K+1}=T+1$ ). The Horvitz–Thompson estimator $\hat\tau_m$ weights the outcome of each period whose window $w_{t-m:t}$ is all ones (all zeros) by the inverse probability of that event. Its risk is the mean squared error

r(\eta_{\mathbb T,\mathbb Q},\mathbb Y)=\mathbb E\bigl[(\hat\tau_m-\tau_m(\mathbb Y))^2\bigr],

where the expectation is over the law $\eta_{\mathbb T,\mathbb Q}$ of the path. A design is minimax optimal if it minimizes the worst-case risk $\max_{\mathbb Y\in\mathcal Y}r(\eta_{\mathbb T,\mathbb Q},\mathbb Y)$ over all regular designs.

Formalization targets

Goal: the optimal design (Theorem 2 with Theorem 1)

If $m=0$ and $T\ge2$ , the unique minimax-optimal regular design has $\mathbb T^*=\{1,2,\dots,T\}$ and fair coins.
If $m\ge1$ and $T=nm$ for an integer $n\ge4$ , the unique minimax-optimal regular design is

\mathbb T^*=\{1,\ 2m+1,\ 3m+1,\ \dots,\ (n-2)m+1\},\qquad q_0=\dots=q_K=\tfrac12 .

The goal asserts both existence and uniqueness, and it compares against every regular design with arbitrary probabilities in $(0,1)$ .

Milestones

In attack order:

Unbiasedness of the estimator (Proposition 1).
The moments of the error terms (Lemmas EC.3 and EC.4).
The adversary's best responses $\mathbb Y^\pm\equiv\pm B$ (Lemma 1).
The product inequality

\frac1{\prod_i q_i}+\frac1{\prod_i(1-q_i)}\ge2^{n+1}

(Lemma EC.2), and fair coins (Theorem 1). 5. The fair-coin moments (Lemma EC.6). 6. The structure of optimal point sets (Lemmas EC.7 and EC.8). 7. The closed-form risk (EC.8) (Lemma EC.9). 8. The integer optimum of the subset selection objective (7) at $T=nm$ :

\min_{\mathbb T}\Bigl\{4\sum_{k=0}^{K}(t_{k+1}-t_k)^2+8m(t_K-t_1)+4m^2K-4m^2+4\sum_{k=1}^{K-1}\bigl[(m-t_{k+1}+t_k)^+\bigr]^2\Bigr\}=16mT-32m^2,

attained only at $\mathbb T^*$ .

Companion statements

These are not milestones:

Lemma EC.5 (the moments at $\mathbb Y^\pm$ for general $\mathbb Q$ ).
Theorem 2's equivalence of (6) and (7), restricted to the goal's horizons.
The optimal worst-case risk $(16mT-32m^2)B^2/(T-m)^2$ .
Lemma EC.10 on the gaps of minimizers of (7).

Significance

The result. Theorem 2 turns a design question into a rule: randomize once every $m$ periods, except that the first and the last epoch last $2m$ periods. The rule depends only on the carryover order $m$ , not on $B$ or on the outcome model. A practitioner who chooses the period length close to the carryover duration gets a design that is robust to a short carryover, since the optimal designs for $m=0$ and $m=1$ nearly coincide. The fair-coin result (Theorem 1) keeps the inverse-probability weights at powers of $2$ , which avoids the instability of Horvitz–Thompson estimators with extreme propensities. The same design underlies the paper's asymptotic normality result and its confidence intervals (mission 2 of this series).

Formalizing it. The results are proved in the paper; none of them is machine-checked. The formalization has to make the paper's finite-sample expansion of the risk exact, establish its integer optimum, and connect it to a genuine minimax statement over all regular designs, not only over fair-coin designs. It also pins down where the printed statements need hypotheses. As printed, the first sentence of Theorem 2 and Lemma EC.7 fail for short horizons (at $m=2$ , $T=4$ the minimax-optimal point sets are $\{1,2\}$ and $\{1,4\}$ , while (7) is minimized by $\{1,3\}$ ). Their corrected forms are stated here. The strictness part of Lemma 1 fails at $m=0$ (with $T=2$ , $\mathbb T=\{1,2\}$ , fair coins, outcomes $B$ in period 1 and $-B$ in period 2 tie with $\mathbb Y^+$ ); it is stated for $m\ge1$ .

Difficulty

The risk is a quadratic form in the reduced outcomes whose coefficients depend on the combinatorics of the point set. The coefficients are products of inverse probabilities over the determining randomization points of each window $\{t-m,\dots,t\}$ and over the overlaps of two windows. Writing the risk in closed form requires a case analysis of how windows of length $m+1$ meet the blocks of the design. The paper's closed form (EC.8) holds only under three structural conditions on the points. Showing that every optimal design satisfies them (Lemmas EC.7, EC.8) needs exchange arguments that remove or move a point while keeping the design regular, and these break down at short horizons.

The step from the closed form to the explicit optimum is an integer program. The paper solves its continuous relaxation and observes that the relaxed optimum is integral. A formal proof must handle every point set, including those that violate the structural conditions and for which (EC.8) is not the risk. The obvious approach of minimizing (EC.8) directly is therefore not enough: the minimax optimum must also be compared with designs outside the class where (EC.8) applies.

Formalization scope

Lean represents a path as a function $\mathbb N\to\mathrm{Bool}$ of which only the indices $1,\dots,T$ are read, potential outcomes as a function of the period and the whole path, and the point set as a Finset ℕ. Probabilities are indexed by the randomization point ( $q_{t_k}$ ). The expectation under the law of a regular design is the finite sum over the $2^{K+1}$ coin vectors.

Committed conventions:

the lag of the estimand equals the carryover order ( $p=m$ ), as throughout §3;
$m<T$ ;
every probability lies in $(0,1)$ , so the estimator's denominators are positive;
$t_{K+1}=T+1$ ;
$(a)^+=\max\{a,0\}$ .

Minimax optimality is the statement "for every regular design and every admissible $\mathbb Y$ there is an admissible $\mathbb Y'$ whose risk under the other design is at least the risk of $\mathbb Y$ under this one". No supremum over outcome functions is ever taken. $\mathbb Y^\pm$ are the constant outcome functions $\pm B$ .

Added hypotheses.

The case $m=0$ of the goal requires $T\ge2$ , the page's condition that $K$ be positive.
Lemma EC.7 assumes $m=0$ or $T=nm$ with $n\ge4$ .
The strictness clause of Lemma 1 assumes $m\ge1$ (it is false at $m=0$ ), and its " $\mathbb Y\ne\mathbb Y^\pm$ " is read on the reduced outcomes $(Y_t(\mathbf 1_{m+1}),Y_t(\mathbf 0_{m+1}))_{t\ge m+1}$ .
Lemmas EC.7–EC.9 are stated for fair coins against $\mathbb Y^\pm$ , as in the paper's EC.3.5.
Lemma EC.10 is read for minimizers of (7).

Not a trivialization. The goal mentions neither the objective (7) nor the structural conditions, nor the closed form (EC.8). It is stated against the full class of regular designs and asserts existence. A proof cannot replace it by " $\mathbb T^*$ minimizes (7)" (that is a milestone), and Theorem 1 is not vacuous because the goal asserts that optimal designs exist.

A complete development needs finite expectations over independent coin flips, the risk expansion as a quadratic form, and an integer optimization argument. The first two are reusable for the second mission of this series and for other design-based analyses of Horvitz–Thompson estimators. Proofs of any milestone, and of the companion statements, are welcome independently.

Selected references

I. Bojinov, D. Simchi-Levi, J. Zhao, Design and Analysis of Switchback Experiments, Management Science 69(7), 2023; arXiv:2009.00148v4, 2025. https://arxiv.org/abs/2009.00148
I. Bojinov, N. Shephard, Time Series Experiments and Causal Estimands: Exact Randomization Tests and Trading, Journal of the American Statistical Association 114(528), 2019. https://doi.org/10.1080/01621459.2018.1527225
C.-F. J. Wu, On the Robustness and Efficiency of Some Randomized Designs, Annals of Statistics 9(6), 1981. https://doi.org/10.1214/aos/1176345640
D. G. Horvitz, D. J. Thompson, A Generalization of Sampling Without Replacement from a Finite Universe, Journal of the American Statistical Association 47(260), 1952. https://doi.org/10.1080/01621459.1952.10483446

14 thms2 active usersReviewed

Missions

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low I: The Discrete First-Order Algorithm Is a Descent Method Whose Successive Steps Shrink at Rate O(1/M)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 10)

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

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Optimal choice probability

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 12

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 9 (p. 26)

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 8b)

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Corollary 5.1 (p. 43)

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Optimization by Decoded Quantum Interferometry 2: With an Imperfect Decoder and Uniform v, 𝔼_v⟨f⟩ ≥ wᵀ[A − 2ε(m+1)]w / Σ_k w_k²(1 − ε_k) for max-XORSATResearch Paper

Motivation

Setting

Formalization targets

Theorem 10.1: the averaged objective

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 2: ZO-RSGD Has Average Expected Squared Riemannian Gradient Norm at Most 4L(f(x₀) − f(x*))/(N+1) + 2μ²L²(d+6)³ + 16(d+4)σ²/mResearch Paper