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

Information Design for Congested Social Services: Optimal Need-Based Persuasion 4: Signaling Achieves the First-Best Admission Policy for All Welfare Weights Above a ThresholdResearch Paper

Motivation

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6 (Achieving first-best)

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

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

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

Milestones

In the order the proof in Appendix D uses them:

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Encodings that would trivialize the goal are excluded:

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

The work needs:

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

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

Selected references

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

15 thms3 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 2: Under FIFO Issuance the Heuristic Base-Stock Policy's Optimality Gap Decays Exponentially in Demand Population SizeResearch Paper

Motivation

Perishable products (blood platelets, fresh food, pharmaceuticals) have a fixed lifetime: units not sold within $m$ periods expire and are discarded. Managing such inventory well is a classical problem in operations research, going back to Nahmias (1975). The difficulty is that the state of the system is the whole age profile of the stock, so the optimal policy depends on an $(m-1)$ -dimensional state and is intractable for realistic lifetimes. In practice firms use base-stock policies, which raise total stock to a fixed level $S$ every period, but until recently there were no theoretical guarantees for them in the perishable setting.

Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first such guarantees. Under FIFO issuance with zero lead time they define a simple heuristic level $\widetilde S$ and bound its optimality gap explicitly (Theorem 1). This mission formalizes their Theorem 2: when demand is generated by a large population of customers, the optimality gap of the heuristic base-stock policy decays exponentially in the population size $n$ . This regime corresponds to high-volume products, where demand is the sum of many small individual requests.

Setting

The inventory system. Time is divided into periods $t=1,2,\dots$ . The product lasts $m\ge1$ periods. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods. The firm orders $q_t\ge0$ , raising total stock to $x_{t,m}=x_{t,m-1}+q_t$ (zero lead time). Demand $D_t$ is served oldest-first (FIFO); unmet demand is lost. The quantity $o_t=(x_{t,1}-D_t)^+$ expires, and the remaining stock ages by one period:

x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1 .

The system starts empty. Each period costs $h(x_{t,m}-D_t)^++p(D_t-x_{t,m})^++\theta o_t$ with $h>0$ , $p>0$ , $\theta\ge0$ . A policy $\pi$ chooses $q_t=\varphi^\pi_t(x_t)$ by a non-negative measurable function of the current state. Its cost is $C^\pi=\limsup_T\frac1T\sum_{t\le T}\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}=\inf_\pi C^\pi$ . The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ ; its cost is $C(S)$ .

The heuristic level. With $D_1,D_2,\dots$ i.i.d. copies of the one-period demand $D$ , let

\widetilde C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\tfrac{\theta}{m}\,\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big],

and let $\widetilde S$ be any minimizer of $\widetilde C$ over $[0,\infty)$ . $S^{NP}=F^{-1}(p/(p+h))$ is the newsvendor level of $D$ .

Demand population form (7). For a positive integer $n$ , the one-period demand is

D(n)=\sum_{j=1}^{N(n)}\hat D_j,\qquad N(n)=\sup\Big\{N\in\mathbb N:\sum_{k=1}^NX_k/n\le1\Big\},

where the customer demands $\hat D_j$ are i.i.d., non-negative, with mean $\mu>0$ and variance $\sigma^2<\infty$ , and the $X_k$ are i.i.d., non-negative, independent of the $\hat D_j$ , with $\mathbb E[X_1]=1$ , variance $\sigma_X^2<\infty$ , and $\mathbb E[e^{sX_1}]<\infty$ for some $s>0$ . Thus $N(n)$ is the number of renewals in $[0,n]$ ; $N(n)=n$ when $X_k\equiv1$ , and $D(n)$ is compound Poisson with mean $n\mu$ when the $X_k$ are exponential. $C_n$ , $\mathrm{OPT}_n$ , $\widetilde C_n$ , $S^{NP}_n$ denote the objects above for demand $D(n)$ , with $m,h,p,\theta$ fixed.

Formalization targets

Goal: Theorem 2 (p. 12)

There exist constants $K_1>0$ , $K_2>0$ such that, for all sufficiently large $n$ and every minimizer $\widetilde S_n$ of $\widetilde C_n$ ,

C_n(\widetilde S_n)-\mathrm{OPT}_n\le K_1e^{-K_2n}.

The constants may depend on $m,h,p,\theta$ and the laws of $\hat D_1$ and $X_1$ . The goal asserts only the exponential rate, not the explicit constants of the proof.

Milestones (proof order)

(23), p. 23: for every $\lambda>0$ , $C_n(\widetilde S)-\mathrm{OPT}_n\le\frac{(m-1)\theta}{\lambda me}\big(e^{\lambda S^{NP}_n/m}\,\mathbb E[e^{-\lambda D(n)}]\big)^m$ .
(EC.6), p. ec3: $S^{NP}_n\le\mathbb E[D(n)]+\sqrt{p\,\mathrm{Var}[D(n)]/h}$ .
(EC.7), p. ec4: $\mathbb E[D(n)]=\mu\mathbb E[N(n)]$ , $\mathrm{Var}[D(n)]=\sigma^2\mathbb E[N(n)]+\mu^2\mathrm{Var}[N(n)]$ .
Renewal limits, p. ec4: $\mathbb E[N(n)]/n\to1$ and $\mathrm{Var}[N(n)]/n\to\sigma_X^2$ .
Step-1 claim, p. ec3: for every $k>1$ , $S^{NP}_n\le k\mu n$ for all large $n$ .
(EC.10)–(EC.11), pp. ec4–ec5: there is $\nu>0$ , depending only on the law of $X_1$ , with $\mathbb P(N(n)<n/(1+\delta))\le\exp(-\delta^2n/(8(1+\delta)^2\nu^2))$ for $0<\delta<\nu$ , $n\ge2(1+\delta)/\delta$ .
(EC.8), p. ec4: under the same quantifiers, $\mathbb E[e^{-\lambda D(n)}]\le e^{-\delta^2n/(8(1+\delta)^2\nu^2)}+(\mathbb E[e^{-\lambda\hat D_1}])^{n/(1+\delta)}$ .

The proof also uses the FIFO results (Lemmas 1–2, Proposition 2 and inequality (21)) that are posed in mission 1 of this series; they are not restated here, and (23) is their consequence at the population demand.

Significance

The result. Theorem 2 shows that the heuristic base-stock policy, which is computed from a one-dimensional convex function, is nearly optimal for high-volume perishable products: the loss from ignoring the age profile vanishes exponentially as demand scales. Together with Theorem 1 (exponential decay in the lifetime) it explains why simple base-stock rules perform well in practice, and it gives a quantitative criterion for when a firm can stop worrying about the optimal policy.

Formalizing it. The result is proved in the paper; no part of it is machine-checked. A formalization adds a checked perishable inventory model (FIFO dynamics, admissible policies, long-run average cost), a random-sum demand model built on a renewal counting process, and checked versions of three classical probabilistic tools that the proof cites: Scarf's minimax bound for the newsvendor, Wald's identity with the law of total variance for random sums, and a lower-deviation bound for renewal counts from Bernstein's inequality for sub-exponential variables. The paper's justification of $\mathrm{Var}[N(n)]/n\to\sigma_X^2$ cites convergence in distribution, which does not imply convergence of variances; the statement is still true, and a formal proof has to supply the renewal variance argument.

Difficulty

The cost comparison itself is inherited from Theorem 1; what is new is controlling both factors of (23) as $n\to\infty$ . The level $S^{NP}_n$ grows linearly in $n$ , so the factor $e^{\lambda S^{NP}_n/m}$ grows exponentially, and must be beaten by the decay of $\mathbb E[e^{-\lambda D(n)}]$ . Neither factor is explicit: $S^{NP}_n$ is a quantile of a compound distribution, and $D(n)$ has a random number of summands. Simply replacing $N(n)$ by its mean is not possible, because the lower tail of $N(n)$ must be shown to be exponentially small with a rate that does not degrade with $n$ ; this needs a concentration inequality for the renewal count, not only a law of large numbers. When $m=1$ the right side of (23) is zero, so the substantive case is $m\ge2$ , where the constants must be balanced to make the exponent negative. None of the needed tools (renewal theory, sub-exponential Bernstein, Scarf's bound) is in Mathlib.

Formalization scope

Namespace PerishBaseStock.Population. Demand laws are CappedBaseStock.DemandLaw (non-negative, finite positive mean); the newsvendor functions come from LostSalesOrderUpTo.Asymptotic.Backorder; the renewal count is the counting variable N of SmithRenewal.Elementary at time $n$ .
Time is zero-based; levels and orders live in $[0,\infty)$ , truncated subtraction is $(\cdot)^+$ . The state is Fin (m - 1) → ℝ≥0 holding cumulative levels, with $x_{t,0}:=0$ ; $m=1$ is allowed.
Costs are lower Lebesgue expectations in $[0,\infty]$ ; $C^\pi$ is a limsup of Cesàro averages; $\mathrm{OPT}$ is the infimum over all measurable state-feedback policies (the paper's class $\Pi$ ). $C(S)$ is the simulated cost of $\pi_S$ , not a formula.
" $\widetilde S$ is a minimizer" is a predicate, and every statement quantifies over every minimizer. Gaps are stated as $C\le\mathrm{OPT}+B$ .
The demand $D(n)$ lives on the product of two independent i.i.d. sequence spaces. The family of systems is a sequence of demand laws whose $n$ -th law equals that of $D(n)$ for $n\ge1$ ; on the null event $N(n)=\infty$ the sum is $0$ .
$\mathbb E[\hat D_1]>0$ is assumed (the paper's standing $\mathbb E[D]>0$ ).
Trivializing formalizations are ruled out: OPT ranges over all admissible policies, $C(S)$ is the long-run average of the simulated cost, the constants $K_1,K_2$ are required to be positive and to be chosen before $n$ , $m$ and $\theta$ are kept general, and the law of $D(n)$ is a genuine pushforward (its measurability is checked).
Reusable beyond this mission: the compound-renewal demand model and milestones 2–4, 6 and 7, which are statements about random sums and renewal counts independent of inventory. Proofs of any milestone, and of the probabilistic lemmas in isolation, are welcome.

Selected references

J. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022; accepted manuscript SSRN 3724966. https://ssrn.com/abstract=3724966
S. Nahmias, Optimal ordering policies for perishable inventory II, Operations Research 23(4):735–749, 1975. https://doi.org/10.1287/opre.23.4.735
H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
W. L. Smith, Renewal theory and its ramifications, J. R. Statist. Soc. B 20(2), 1958.
P. Rigollet, J.-C. Hütter, High Dimensional Statistics, lecture notes for course 18.S997, MIT, 2015 (Theorem 1.13, Bernstein's inequality for sub-exponential variables).

15 thms3 active usersReviewed

Operations Research Optimization Probability+1·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 3: Under FIFO Issuance the Heuristic Base-Stock Policy Is Asymptotically Optimal as the Unit Penalty Cost GrowsResearch Paper

Motivation

Perishable products, among them fresh food, blood platelets and pharmaceuticals, lose their value after a fixed number of periods. Their inventory control has been studied since the 1970s (Nahmias, Perishable inventory theory: a review, Operations Research 1982). The optimal policy of the standard lost-sales model depends on the whole age profile of the stock and is computationally intractable when the lifetime is long. Practitioners therefore use base-stock policies, which raise the total inventory to a fixed level every period. Before Bu, Gong & Chao (SSRN 3724966, accepted at Management Science, 2022), no guarantee was known on how far the best such policy, or any explicitly computable one, is from optimal.

This mission concerns the regime of a large unit penalty cost. Firms in retail and manufacturing often run at very high service levels (Huh et al. 2009; Wei et al. 2021), which in a cost-based model means that the unit lost-sales penalty $p$ is much larger than the unit holding cost $h$ . The question is whether a simple base-stock policy remains near-optimal as $p$ grows.

Setting

A product has a fixed lifetime of $m\ge1$ periods. Demands $D_1,D_2,\dots$ are i.i.d. copies of a non-negative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F(x)=\mathbb P(D\le x)$ . At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods, and $x_{t,0}:=0$ . The firm orders $q_t\ge0$ and the total level becomes $x_{t,m}=x_{t,m-1}+q_t$ (zero lead time). Demand is served oldest first (FIFO issuance) and unmet demand is lost. The outdated quantity is $o_t=(x_{t,1}-D_t)^+$ , and the dynamics are

x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1,

starting from the empty state $x_1=0$ . The period cost is $C^\pi_t=h(x^\pi_{t,m}-D_t)^++p(D_t-x^\pi_{t,m})^++\theta o^\pi_t$ , with $h>0$ , $p>0$ and an additional outdating cost $\theta\ge0$ . An admissible policy orders $q_t=\varphi^\pi_t(x_t)$ with each $\varphi^\pi_t$ a non-negative measurable function of the state. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}=\inf_\pi C^\pi$ over all admissible policies.

The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ , and $C(S)$ is its average cost. $\mathbb E[O_\infty(S)]$ is its long-run average outdated quantity. The heuristic level $\widetilde S$ is any minimizer over $[0,\infty)$ of

\widetilde C(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac\theta m\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big].

Two further objects appear: the upper support $\bar D=\sup\{x:F(x)<1\}\in[0,\infty]$ (demand is bounded when $\bar D<\infty$ ), and the floor level $\underline S=\arg\min_{S\ge0}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\theta S\}$ . A subscript $p$ marks dependence on the penalty: $C_p$ , $\mathrm{OPT}_p$ , $\widetilde S_p$ .

Formalization targets

Goal: Theorem 3 (p. 13)

\lim_{p\to\infty}\big(C_p(\widetilde S_p)-\mathrm{OPT}_p\big)=0,

with $m$ , $h$ , $\theta$ and the demand law fixed, for every selection $p\mapsto\widetilde S_p$ of minimizers. No boundedness assumption on demand is made.

Milestones

(25), p. 24, for every demand law: $C(\widetilde S)-\mathrm{OPT}\le\theta\big(\mathbb E[(D-\widetilde S/m)^+]-\mathbb E[(\frac1m\sum_{i=1}^mD_i-\widetilde S/m)^+]\big)$ .
Lemma 6, p. 22: if $\bar D<\infty$ , some optimal policy has $x_{t,m}\ge\underline S$ in every period on every demand path.
(20), p. 22: such a policy outdates cumulatively at least as much as $\pi_{\underline S}$ , pathwise.
Proposition 3, p. 22: if $\bar D<\infty$ , $\mathrm{OPT}\ge h\mathbb E[(\underline S-D)^+]+\theta\mathbb E[O_\infty(\underline S)]$ .
(EC.13), p. ec6: if $\bar D<\infty$ , $p\mathbb E[(D-\widetilde S)^+]\le p(\bar D-\widetilde S)\mathbb P(D>\widetilde S)\le(h+\theta)(\bar D-\widetilde S)$ .
(EC.15), p. ec6: $\mathbb E[O_\infty(S_2)]\le\mathbb E[O_\infty(S_1)]+S_2-S_1$ for $0\le S_1\le S_2$ .
(26), p. 24: if $\bar D<\infty$ , $C(\widetilde S)-\mathrm{OPT}\le(h+\theta)(\bar D-\underline S)$ .

Significance

Theorem 3 shows that the explicitly computable policy $\pi_{\widetilde S}$ is asymptotically optimal in the high-service regime. The optimal policy is a function of the whole age vector, whereas $\widetilde S$ is the minimizer of a one-dimensional convex function. Together with the companion results of the paper, in the lifetime $m$ , the demand population and the outdating cost $\theta$ , this gives a uniform picture of when a single stock level suffices for a perishable product. Lemma 6 and Proposition 3 are of independent interest: a uniform floor on the optimal order-up-to level and a lower bound on the optimal average cost that does not require solving the dynamic program.

The result is proved in the paper; it has not been formalized. A machine-checked development requires a perishable inventory model, long-run average costs over an infinite i.i.d. demand path, and, for Lemma 6, the existence of an average-optimal policy. The last step requires a vanishing-discount argument.

Difficulty

The unbounded-demand case rests on (25). The lower bounds it combines (Lemma 2 and Proposition 2 of the paper) are posed in mission 1 of this series and only cited here. The bounded-demand case is harder. One would like to compare $\pi_{\widetilde S}$ with an optimal policy directly, but a priori there is no optimal policy at all: $\mathrm{OPT}$ is an infimum over a large class of state-feedback policies on a continuous state space. Lemma 6 asserts that the infimum is attained, and attained by a policy whose order-up-to level never drops below $\underline S$ . The paper obtains it from the discounted problem (Nandakumar & Morton 1993) and a vanishing-discount limit, verifying the conditions of Schäl (1993, Theorem 3.8) and in particular a uniform bound on relative discounted values (EC.34). Schäl's theorem is posed separately on Prove2Me as a statement (SchalAvg.AvgOpt.theorem_3_8, not proved), which is context and not part of this mission. Bounding the lost-sales term by a quantity independent of $p$ , as (EC.13) does, needs the first-order condition at a minimizer of $\widetilde C$ , which is a non-smooth convex function.

Formalization scope

Time is zero-based: Lean period $t$ is the paper's period $t+1$ .
State: Fin (m - 1) → ℝ of cumulative levels, with $x_{t,0}:=0$ , so $m=1$ (empty state, everything left over outdates) is included, not excluded.
Parameters: a record $(m,h,p,\theta)$ with the standing hypotheses $m\ge1$ , $h>0$ , $p>0$ , $\theta\ge0$ . In Theorem 3 only the field $p$ varies.
Expectations and costs are lower Lebesgue integrals over the i.i.d. path law (CappedBaseStock.demandPathLaw), valued in $[0,\infty]$ . Long-run averages are limsups of Cesàro averages.
Policies: the class $\Pi$ of the paper: time-dependent, deterministic, measurable functions of the current state. $\mathrm{OPT}$ is the infimum over all of $\Pi$ , not over base-stock policies.
$C(S)$ is the simulated long-run average cost of $\pi_S$ , not a formula. $\mathbb E[O_\infty(S)]$ is the long-run average outdating of $\pi_S$ from the empty state.
$\widetilde S$ is any minimizer of $\widetilde C$ ; all statements quantify over every minimizer. $\underline S$ is the least minimizer of its function, the weaker choice for Lemma 6.
Gaps " $A-\mathrm{OPT}\le B$ " are stated as $A\le\mathrm{OPT}+B$ in $[0,\infty]$ . The limit uses real values, which is faithful because $C_p(S)\le hS+p\mathbb E[D]+\theta S<\infty$ .
Lemma 6 requires an exactly optimal policy and a floor on every demand path.

Trivializing formalizations are ruled out. OPT is not restricted to base-stock policies, $C(S)$ is not defined by its formula (3), $\widetilde S$ is not replaced by a closed form, and $m$ , $\theta$ , $h$ and the demand law are kept general.

The FIFO lemmas the proof uses, namely Lemma 1, Lemma 2, Proposition 2 and the recursion (19), are posed in mission 1 of this series and are not restated. The development reuses the published demand layer CappedBaseStock_Model and the newsvendor functions LostSalesOrderUpTo.Asymptotic.Backorder. A general vanishing-discount theorem for Borel-state average-cost control would be reusable well beyond this mission; contributions toward it, and toward the convexity and first-order conditions of newsvendor-type costs, are welcome.

Selected references

X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, Management Science, 2022. SSRN 3724966, https://ssrn.com/abstract=3724966
S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 1982. https://doi.org/10.1287/opre.30.4.680
P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1993. https://doi.org/10.1287/mnsc.39.12.1490
M. Schäl, Average optimality in dynamic programming with general state space, Mathematics of Operations Research 18(1), 1993. https://doi.org/10.1287/moor.18.1.163
W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic optimality of order-up-to policies in lost sales inventory systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945

14 thms3 active usersReviewed

Completed

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

Information Design for Congested Social Services: Optimal Need-Based Persuasion 3: Information Design Pareto-Dominates Full Information Exactly When Low-Need Arrivals Exceed a ThresholdResearch Paper

Motivation

Public and nonprofit services such as food banks, shelters, free clinics and legal aid often run with too little capacity and serve two kinds of users: people with no alternative, and people who have a reasonable outside option. When the queue is long, a user who has an alternative but joins anyway imposes waiting costs on everyone behind them, including the users who cannot go elsewhere. Pricing is usually ruled out in such settings, which leaves the provider one lever: what it tells arriving users about congestion.

Anunrojwong, Iyer and Manshadi (arXiv:2005.07253v3; Management Science, 2023) study this lever as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (Operations Research 67(5):1397–1416, 2019). The natural benchmark is full information: announce the queue length and let users decide. This mission formalizes the paper's answer to when full information can be improved for both user types at once, and by how much.

Setting

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

By a revelation-principle argument (Lemma 1 of the paper, from Lingenbrink and Iyer), a recommendation mechanism that users obey is described by the queue's stationary distribution $\pi=(\pi_n)_{n\ge0}$ . An admission policy is a distribution with $\lambda_H\pi_n\le\pi_{n+1}\le\lambda\pi_n$ for all $n$ ; their set is $\Pi_{AP}$ . A signaling mechanism is an admission policy that also satisfies the obedience constraints

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

called (JOIN) and (LEAVE); their set is $\Pi_{SM}$ . The welfare of the two types is $W_L(\pi)=J(\pi)$ and $W_H(\pi)=\lambda_H\sum_n\pi_nu_H(n)$ . A policy $\hat\pi$ Pareto-dominates $\pi$ if it is at least as good for both types and strictly better for one; $\pi$ is Pareto-efficient within a class if no member of the class dominates it.

A threshold policy $\pi_x$ , $x=m+a\ge0$ , admits L users when fewer than $m$ users are present, admits them with probability $a$ at $m$ , and turns them away above $m$ . Write $W_L(x)$ , $W_H(x)$ and $L(x)$ for its welfare and (LEAVE) value. The full-information threshold $m_{fi}$ is the smallest $k$ with $u_L(k)<0$ , and the full-information mechanism is $\mathsf{fi}=\pi_{m_{fi}}$ .

Formalization targets

Goal: Proposition 3(1)–(2)

For $\lambda_H\in(0,1)$ , with $u_L,u_H$ fixed, there is a threshold $\bar\Lambda_L(\lambda_H)\in(0,1-\lambda_H]$ such that some signaling mechanism Pareto-dominates $\mathsf{fi}$ if and only if $\lambda_L\ge\bar\Lambda_L(\lambda_H)$ , and

\bar\Lambda_L(\lambda_H)\ \ge\ (1-\lambda_H)\,\frac{u_L(m_{fi}-1)}{u_L(0)-\sum_{k=1}^{m_{fi}-1}\lambda_H^k\big(u_L(k-1)-u_L(k)\big)}\ >\ 0 .

If moreover $\lambda<1$ , $u_L(m_{fi}-1)\le W_L(\mathsf{fi})$ , $u_H(m_{fi})\le W_H(\mathsf{fi})$ , $L(m_{fi}-1)\le0$ and $W_H(\mathsf{fi})>0$ , then a signaling mechanism $\mathsf{sm}$ exists with

W_L(\mathsf{sm})\ge\beta_{L,sm}W_L(\mathsf{fi}),\qquad W_H(\mathsf{sm})\ge\beta_{H,sm}W_H(\mathsf{fi}),

where $\beta_{L,sm}=1+\frac{\lambda_H(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ and $\beta_{H,sm}=1+\frac{(1-\lambda_H)(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ .

Milestones

Lemma 3: the geometric sandwich $\lambda_H^{k-q}\pi_q\le\pi_k\le\lambda^{k-q}\pi_q$ on $\Pi_{AP}$ .
Theorems 1 and 2: Pareto-efficient signaling mechanisms and admission policies have a threshold structure with threshold at most $m_{fi}$ .
Lemma 2: maximizers of $\theta W_L+(1-\theta)W_H$ exist.
Theorem 3: when (LEAVE) is slack, efficiency within $\Pi_{SM}$ and within $\Pi_{AP}$ coincide.
Lemma 5(1)–(2): $W_H(x)$ is strictly decreasing, and $W_L(x)$ is unimodal and monotone between consecutive integers.
$\mathsf{fi}\in\Pi_{SM}$ with $L(\mathsf{fi})<0$ .
Theorem 4: exactly one of " $\mathsf{fi}$ is Pareto-efficient among admission policies" and "a signaling mechanism dominates $\mathsf{fi}$ " holds, the first if and only if $W_L(m_{fi})>W_L(m_{fi}-1)$ .
From the proof of Proposition 3: the equivalence of that condition with $f(\lambda_L,\lambda_H)<0$ , an identity for $W_L(m-1)$ and an inequality for $W_H(m-1)$ , for $1\le m\le m_{fi}$ .

Significance

The proposition gives a clean regime split. Full information is already Pareto-efficient when low-need demand is light. Once $\lambda_L$ crosses an explicit level, revealing everything leaves welfare on the table for both types, so a provider who cares about either group has a reason to hide some queue information. The lower bound on $\bar\Lambda_L$ is explicit in the primitives, and the factors $\beta_{L,sm},\beta_{H,sm}$ give a guaranteed improvement, not only an existence statement. Theorem 4, the milestone behind part 1, reduces the comparison to two adjacent thresholds.

The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. A formal development checks the "little algebra" steps that the paper compresses (the equivalence with $f<0$ , the welfare identities of p. 41–42). It also produces a reusable layer for persuasion in birth–death queues: obedient mechanisms as distributions, threshold policies, and Pareto efficiency within a class. The companion missions of this series (threshold structure, the homogeneous case, first-best) are stated over the same layer.

Difficulty

The threshold $\bar\Lambda_L$ comes from analysing the sign of $f(\cdot,\lambda_H)$ on $(0,1-\lambda_H]$ . Translating "fi is not dominated" into that sign condition is where the work lies. The obvious attempt, comparing $\mathsf{fi}$ only with nearby threshold policies, settles one direction: if $W_L(m_{fi}-1)\ge W_L(m_{fi})$ , the threshold $m_{fi}-1$ dominates. The converse needs every competitor in $\Pi_{AP}$ , not just threshold policies. That requires the structure theorem for efficient admission policies, the existence of maximizers, and unimodality of $W_L$ , followed by a transfer from $\Pi_{AP}$ to $\Pi_{SM}$ that only works because (LEAVE) is slack at $\mathsf{fi}$ . The welfare series are infinite, and the threshold family is parametrised by a real $x$ whose fractional part enters nonlinearly, so the comparisons are not finite-dimensional linear algebra.

Formalization scope

Everything is stated over a structure Model with real fields $\lambda_L,\lambda_H$ and utilities $u_L,u_H:\mathbb N\to\mathbb R$ , with a predicate Standing holding the standing assumptions ( $\lim_ku_i(k)<0$ is encoded as $\exists k,\ u_i(k)<0$ ). Queue lengths are natural numbers, and the two types are separate fields. Membership in $\Pi_{AP}$ includes summability of $\pi_nu_L(n)$ and $\pi_nu_H(n)$ : the paper treats all welfare as finite, and an unrestricted tsum would assign $0$ to divergent welfare. $W_L$ is the right-hand form of (2), with no division by $\lambda_L\pi_n$ . A finite threshold requires $\pi\in\Pi_{AP}$ , $\pi_m>0$ and a joining fraction in $[0,1]$ , as in Definition 2. Threshold policies are defined from their unnormalised weights, $\mathsf{fi}$ is $\pi_{m_{fi}}$ as a distribution, and Pareto efficiency is Definition 1 within an explicit class. "Exactly one" is exclusive or.

Added hypotheses, each disclosed in the item that carries it:

Convergence of $\sum_n\lambda_H^nu_H(n)$ . This is the finite-welfare convention, equivalent to $\Pi_{AP}\ne\emptyset$ when $\lambda_H>0$ .
Lemma 2's hypothesis ( $\lambda<1$ , or $u_L,u_H\to-\infty$ ) wherever existence of maximizers is used.
$u_L(m_{fi}-1)\ne0$ in Proposition 3. Without it the claimed $\bar\Lambda_L>0$ is false.
$\lambda_H>0$ in Lemma 5(1) and Theorem 4, as required by §4.2's heterogeneous setting. For $\lambda_H=0$ , $W_H\equiv0$ , and Theorem 4's strict adjacent-threshold comparison can fail at a tie.

The page's range $\lambda_L\in[\bar\Lambda_L,1)$ is intersected with $\lambda\le1$ . In part 2, " $\mathsf{sm}$ " is read existentially.

Ruled out as trivializing: choosing $\bar\Lambda_L$ after $\lambda_L$ (the goal quantifies it once, with $\lambda_H,u_L,u_H$ fixed); defining $\mathsf{fi}$ through its welfare; replacing Pareto efficiency by maximization of a weighted welfare; replacing exclusive or by inclusive or; and any constant that differs from the page's $\beta_{L,sm}$ , $\beta_{H,sm}$ or lower bound symbol for symbol.

A complete development needs geometric and arithmetico-geometric series, rearrangement of infinite sums over $\mathbb N$ , and convexity arguments in the space of summable sequences. Proofs of any milestone are welcome, as are lemmas about threshold policies that the other missions of the series can reuse.

Selected references

J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; read as arXiv:2005.07253v3 (2022). https://arxiv.org/abs/2005.07253
D. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5):1397–1416, 2019.
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 5th ed., Wiley, 2018.

15 thms3 active usersReviewed

Completed

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

Information Design for Congested Social Services: Optimal Need-Based Persuasion 1: Every Pareto-Efficient Signaling Mechanism Has a Threshold Structure at or Below the Full-Information ThresholdResearch Paper

Why information design for congested public services

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1 (p. 14)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Committed conventions:

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

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

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

Selected references

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

6 thms3 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian 1: NAPP-AL Drives the Best Stationarity Residual to Zero at Rate o(1/√k)Research Paper

Motivation

Many models in statistics, machine learning and engineering are nonconvex, nonsmooth and coupled by constraints: a sparsity penalty such as SCAD, MCP or capped- $\ell_1$ on one block of variables, a smooth loss coupling the blocks, and a nonlinear equality constraint tying them together. Augmented-Lagrangian methods and ADMM-type splittings are the workhorses for such problems, but most convergence theory for them assumes linear constraints or convexity. Zhu, Zhao and Zhang (arXiv:2007.12219v1, published in Mathematics of Operations Research, 2024) propose a first-order primal-dual method, NAPP-AL (nonconvex auxiliary problem principle with augmented Lagrangian), for a nonconvex problem with a nonlinear coupling constraint, and prove that it reaches approximate stationarity at a sublinear rate. This mission targets that rate result and the chain of lemmas behind it.

Setting

Fix dimensions $n,d,m$ . Problem (P) is

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

where $G$ and $H$ are differentiable with Lipschitz gradients, $J$ is lower semicontinuous and possibly nonconvex and nonsmooth, $U\subseteq\mathbb R^n$ is closed and convex, $\Theta:\mathbb R^n\to\mathbb R^m$ is Lipschitz with constant $L^0_\Theta$ , each component of $\Omega$ has a Lipschitz gradient (constants $L_{\Omega_j}$ , $L_\Omega=\sum_jL_{\Omega_j}$ ), and $B$ is an $m\times d$ matrix with $\operatorname{Im}\Theta\subseteq\operatorname{Im}B$ . These are Assumption 1 (H1)–(H7); (H7) asks $F$ to be bounded below and coercive on the feasible set $\{(u,v):\Theta(u)+Bv=0\}$ .

The augmented Lagrangian of (P) at $w=(u,v,p)$ is

\mathcal L_\gamma(w)=F(u,v)+\langle p,\Theta(u)+Bv\rangle+\frac\gamma2\|\Theta(u)+Bv\|^2 .

Its stationarity set $\partial\mathcal L_\gamma(w)$ (p. 6) collects the triples $(\xi_u,\xi_v,\xi_p)$ with, for $y=p+\gamma(\Theta(u)+Bv)$ ,

\xi_u\in\nabla_uG(u,v)+\partial J(u)+N_U(u)+(\nabla\Theta(u))^\top y,\quad\xi_v=\nabla_vG(u,v)+\nabla H(v)+B^\top y,\quad\xi_p=\Theta(u)+Bv,

where $\partial J$ is the limiting subdifferential and $N_U$ the normal cone of $U$ . A stationary point is a $w$ with $0\in\partial\mathcal L_\gamma(w)$ , and $\operatorname{dist}(0,S)=\inf_{\xi\in S}\|\xi\|$ , with $\operatorname{dist}(0,\emptyset)=+\infty$ .

NAPP-AL takes a $\beta$ -strongly convex $K$ with Lipschitz gradient (Bregman distance $D(u,u')=K(u)-K(u')-\langle\nabla K(u'),u-u'\rangle$ ), a penalty $\gamma>\frac{\sqrt{57}+1}{2\lambda_{\min}(B^\top B)}(L_G+L_H)$ (Assumption 2) and $0<\sigma<1$ . With $q^k=p^k+\gamma(\Theta(u^k)+Bv^k)$ it sets $u^{k+1}$ to a global minimizer over $U$ of the linearized model

\langle\nabla_uG(u^k,v^k),u\rangle+J(u)+\langle q^k,\nabla\Omega(u^k)u+\Phi(u)\rangle+\tfrac1{\epsilon^k}D(u,u^k),

$v^{k+1}$ to the minimizer of a strongly convex quadratic, and $p^{k+1}=p^k+\gamma(\Theta(u^{k+1})+Bv^{k+1})$ . The step $\epsilon^k$ lies in $[\sigma\delta_k,\delta_k]$ , with $\delta_k$ given by the explicit formula (8), which depends on $\|q^k\|$ . The analysis runs through the potential

\Lambda^k=\mathcal L_\gamma(w^k)+c_1\|u^{k-1}-u^k\|^2+c_2\|v^{k-1}-v^k\|^2+\tfrac1{2\gamma}\|p^{k-1}-p^k\|^2 \tag{18}

with explicit constants $c_1,c_2$ .

Formalization targets

Goal: Proposition 4.1 (p. 18)

Under Assumptions 1 and 2, with $\delta_k$ set by (8),

\min_{1\le j\le k}\operatorname{dist}\big(0,\partial\mathcal L_\gamma(w^j)\big)=o\big(1/\sqrt k\big).

Milestones

Proposition 3.1 (p. 9): $\operatorname{dist}(0,\partial\mathcal L_\gamma(w^{k+1}))\le\sqrt3\,h(u^k,p^k)\|w^k-w^{k+1}\|$ with the paper's explicit $h$ (see the scope section for the factor $\sqrt3$ ).
Lemma 4.1 (p. 11): the dual step $\|p^k-p^{k+1}\|$ is controlled by the primal steps.
Lemma 4.2 (pp. 11–12): one-step change estimates for $\mathcal L_\gamma$ .
Lemma 4.3 (p. 15): sufficient decrease $\Lambda^{k+1}-\Lambda^k\le-c_3\|w^k-w^{k+1}\|^2$ with $c_3=\min\{\frac12,c_4,\frac1{3\gamma}\}>0$ .
Theorem 4.1 (p. 16): $\Lambda^k$ converges, the iterates are bounded with vanishing steps, the residuals vanish, and every cluster point is stationary.

Significance

The result gives NAPP-AL an iteration complexity of $O(1/\varepsilon^2)$ to reach an $\varepsilon$ -stationary point (Remark 4.1), for problems with a nonlinear, nonconvex coupling constraint and a nonsmooth nonconvex regularizer, using only gradient evaluations and one proximal-type subproblem per iteration. It is also the base layer for the paper's later results: linear convergence under an error bound (Theorem 5.1) and the sufficient conditions for that error bound (Propositions 6.1–6.2) all start from Theorem 4.1 and Lemma 4.3.

The result is proved in the paper; nothing here is formalized elsewhere. A formal development adds a machine-checked Lyapunov analysis of an augmented-Lagrangian method with nonlinear constraints, with every constant explicit. It also records a correction: Proposition 3.1 as printed is false by a factor of at most $\sqrt3$ , and the corrected bound is what the paper's proof establishes.

Difficulty

The difficulty is the dual variable. The multiplier update has no step size of its own, so the augmented Lagrangian itself need not decrease along the iterates, and the obvious descent argument for $\mathcal L_\gamma$ fails; the step $\delta_k$ of (8) depends on the current multiplier estimate $\|q^k\|$ , so even the step sizes are not uniformly bounded a priori. Boundedness of the iterates is not a hypothesis, and the iterates are infeasible, so coercivity of $F$ on the feasible set does not apply to them directly. The rate needs the residual bound of Proposition 3.1 with a constant uniform in $k$ , while $h(u^k,p^k)$ depends on $\|q^k\|$ and $\delta_k$ . Passing to cluster points involves the limiting subdifferential of a nonconvex, nonsmooth $J$ , which is not closed under arbitrary convergence of its arguments.

Formalization scope

Spaces and norms. Points are in EuclideanSpace ℝ (Fin k). The norm of a triple $(u,v,p)$ is the Euclidean norm of the stacked vector, defined explicitly; Mathlib's sup norm on products is never used. $B$ is a continuous linear map with its operator (spectral) norm and adjoint; $\lambda_{\min}(B^\top B)$ is the Rayleigh minimum over the unit sphere.
Residual. $\operatorname{dist}(0,\cdot)$ takes values in $[0,+\infty]$ and equals $+\infty$ on the empty set, as on p. 5. Metric.infDist (zero on $\emptyset$ ) is not used; with it, every residual bound would hold whenever $\partial\mathcal L_\gamma$ is empty. The goal is stated as $\sqrt k\cdot\inf_{1\le j\le k}\operatorname{dist}(0,\partial\mathcal L_\gamma(w^j))\to0$ in $[0,+\infty]$ , not as a big-O bound.
Stationarity. $\partial\mathcal L_\gamma$ is the p. 6 display with the limiting subdifferential of $J$ (the published NonconvexSplitting.Shared.LimitingSubdiff) and the normal cone of $U$ , which is empty off $U$ , so that stationarity forces $u\in U$ .
Algorithm. NAPP-AL is a relation on given sequences: $u^{k+1}$ is any global minimizer of the $u$ -subproblem over $U$ , whose existence is assumed by the paper (Remark 3.2), not asserted. The starting point is free.
Standing readings of Assumption 1, disclosed in the items: $G,H,J$ are real valued with gradients Lipschitz on the whole space; " $J$ locally Lipschitz on $\operatorname{dom}J\cap U$ " is read as Lipschitz on a neighbourhood in $\mathbb R^n$ of each point of $U$ (not Mathlib's relative LocallyLipschitzOn); $\lambda_{\min}(B^\top B)>0$ (full column rank, invoked in the proof of Lemma 4.2); (H7) is coercivity on the feasible set only.
Indices. $\Lambda^k$ and the lemmas involving $w^{k-1}$ are stated for $k\ge1$ .
Printed slips. Proposition 3.1 carries the factor $\sqrt3$ (the printed bound fails on a one-dimensional instance with ratio about $1.108$ ). Theorem 4.1(iv) prints " $\partial\mathcal L_\gamma(u^k)$ "; it is stated at $w^{k+1}$ , as Proposition 3.1 and the later sections use it.

Contributions welcome: proofs of the milestones in any order, general facts about limiting subdifferentials and normal cones of convex sets (sum rule with a locally Lipschitz function, closedness under attentive convergence), and the "non-increasing summable sequence is $o(1/k)$ " lemma. These are reusable beyond this mission. The source is the preprint arXiv:2007.12219v1, not the published version; all labels and constants are those of v1.

Selected references

D. Zhu, L. Zhao, S. Zhang, A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian, arXiv:2007.12219v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2007.12219v1
B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
G. Cohen, Auxiliary problem principle and decomposition of optimization problems, Journal of Optimization Theory and Applications 32 (1980) 277–305. https://doi.org/10.1007/BF00934554

9 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand I: The Approximation APT Bounds the Expected Cost-to-Go from Below and Above and Is Exact in the Last PeriodResearch Paper

Motivation

Retailers and restaurants increasingly deliver orders from their own stores within an hour or less. Orders arrive throughout the day, a fixed pool of drivers is based at the store, and in each dispatch wave the operator must decide how many drivers to send out now and along which routes. Sending many drivers now gives short delivery times for the current orders but leaves few drivers for orders that arrive while those drivers are still on the road. Liu and Luo (arXiv:2107.13058, Manufacturing & Service Operations Management, 2023) model this trade-off as a finite-horizon stochastic dynamic program and propose a rollout policy built on a tractable approximation of its cost-to-go. Their Theorem 1 justifies the approximation: with suitable parameters it lies below the true expected cost-to-go, with other parameters it lies between that cost and the cost of any feasible simple policy, and in the last period it is exact. This mission formalizes that theorem.

Setting

A store (the depot $0$ ) serves a finite set $\mathcal I$ of customer locations over $N$ periods with strictly increasing decision epochs $t_1 < \dots < t_N$ . A fleet of $\bar K$ drivers carries at most $Q$ items per trip; travel times $\tau(i,j) \ge 0$ , an on-site service time $s \ge 0$ and a delivery target $L_{\max}$ are given. At epoch $t_n$ the operator observes the demand of period $n$ : the set $\mathcal I^n \subseteq \mathcal I$ of locations with an order and the quantities $q^n_i$ , drawn from a finitely supported law $\mathbb Q^n$ , independently across periods.

The driver status $\zeta^n = (\zeta^n_1,\dots,\zeta^n_N)$ records how many drivers are still en route in each period $n'$ because of earlier dispatches, so $\bar K - \zeta^n_n$ drivers are available at $t_n$ . A decision $Y^n$ is a set of depot-to-depot routes $0 \to i_1 \to \dots \to i_m \to 0$ , one per dispatched driver. It is feasible if it uses at most $\bar K - \zeta^n_n$ drivers, serves every current order exactly once, loads at most $Q$ items per route, and delivers every order within $L_{\max}$ . The delivery times are $u_{i_1} = \tau(0,i_1)$ and $u_{i_{k+1}} = u_{i_k} + s + \tau(i_k,i_{k+1})$ ; the cost of $Y^n$ is $\sum_{i \in \mathcal I^n} u_i(Y^n)$ . A driver whose route lasts longer than $t_{n'} - t_n$ is counted as en route in period $n'$ ; this is the transition (9) from $\zeta^n$ to $\zeta^{n+1}$ .

The cost-to-go $\mathcal H_n(\mathcal I^n, q^n, \zeta^n)$ is the minimum over feasible $Y^n$ of the period's cost plus $\mathbb E_{\mathbb Q^{n+1}}[\mathcal H_{n+1}]$ at the resulting status, with $\mathcal H_N$ the period cost alone ((7)–(8)). The single-period cost $\mathcal H^s(K, \mathcal I^n, q^n)$ is the minimum cost of serving the demand with at most $K$ drivers.

The approximation $\mathbf{APT}^n(\zeta^n)$ (10) replaces the future by single-period problems coupled only through driver counts:

V^n_{APT}(\zeta^n) = \min_{K^{n'} \in \mathbb N} \sum_{n'=n}^{N} \mathbb E_{\mathbb Q^{n'}}\big[\mathcal H^s(K^{n'}, \mathcal I^{n'}, q^{n'})\big] \ \ \text{s.t.}\ \ \sum_{m=n}^{n'} \omega^{n'}_m(K^m) \le \bar K - \zeta^n_{n'},\ \ n' = n,\dots,N,

where $\omega^{n'}_{n'}(K) = K$ and the nonnegative parameters $\omega^{n'}_m(K^m)$ , $m < n'$ , estimate how many of the $K^m$ drivers dispatched in period $m$ are still en route in period $n'$ . A static myopic policy dispatches a state-independent number $K^{n',sm}$ of drivers in each period and routes them to minimize the single-period cost; it is feasible from $(n,\zeta^n)$ if it never asks for more drivers than are available and its single-period problems are always feasible.

Formalization targets

Goal: Theorem 1 (p. 13)

For $1 \le n \le N$ and a status with $\zeta^n_{n'} \le \bar K$ :

\exists\,\omega:\ V^n_{APT}(\zeta^n;\omega) \le \mathbb E_{\mathbb Q^n}[\mathcal H_n], \qquad \forall\,\pi^{sm}\ \text{feasible}\ \exists\,\omega:\ \mathbb E_{\mathbb Q^n}[\mathcal H_n] \le V^n_{APT}(\zeta^n;\omega) \le J_n(\pi^{sm}),

and $V^N_{APT}(\zeta;\omega) = \mathbb E_{\mathbb Q^N}[\mathcal H_N(\cdot,\zeta)]$ for every $\omega$ .

Milestones (Appendix D, pp. 34–35, and Lemma 1, p. 12)

With $\omega^{n'}_m \equiv 0$ for $m < n'$ : $V^n_{APT} = \sum_{n'} \mathbb E[\mathcal H^s(\bar K - \zeta^n_{n'})] \le \mathbb E[\mathcal H_n]$ .
For $n < N$ and a feasible static myopic policy: $\mathbb E[\mathcal H_n] \le J_n(\pi^{sm})$ , and some $\omega$ gives $V^n_{APT} = J_n(\pi^{sm})$ .
At $n = N$ : $\mathbb E[\mathcal H_N] = \min_{K^N \le \bar K - \zeta^N_N} \mathbb E[\mathcal H^s(K^N,\cdot)]$ .
Lemma 1: $\mathcal H_n$ and, for nonnegative $\omega$ , $V^n_{APT}$ are nondecreasing in $\zeta^n$ .

Significance

The rollout policy AJRP of the paper solves, at each epoch, the current routing problem together with $\mathbf{APT}^{n+1}$ as a stand-in for the future. Theorem 1 is what connects that stand-in to the dynamic program: it shows that the en route parameters move the approximation between a valid lower bound and the cost of an implementable policy, and its exactness part yields the paper's Corollary 1 (AJRP is optimal for $N = 2$ ). Lemma 1 shows the approximation keeps the monotonicity of the true value in the driver status.

The paper's proofs are in its Online Appendix (Appendix D). They are short but informal, and the formal statement here differs from the printed one in three pinned-down respects: the single-period cost is read with at most $K$ drivers, as the proofs use it; the upper bound is capped by the policy's cost, since otherwise it is vacuous; and the parameter choice printed for the upper bound has to be corrected in the last period. No part of the result has a machine-checked proof. A formal proof makes these readings definitive, and it produces a reusable Lean model of multi-period dispatching with routes, en route drivers and a Bellman recursion over a random demand.

Difficulty

Every part is a backward induction on the remaining periods, but the inductions run over a state that grows: the status $\zeta^{n+1}$ depends on the durations of the routes chosen in period $n$ , and the infimum in (7) is over finite lists of routes, not over a finite action set. The lower bound needs that a larger status can only raise the cost; the upper bound needs that a policy which is feasible on its reachable states stays feasible after every realized demand. Exchanging the expectation with the minimum over the driver count in the last period is not a general fact and holds only because the single-period cost is nonincreasing in the number of available drivers. The obvious choice of parameters for the upper bound, the one printed in the proof, does not bound the last period's count and fails.

Formalization scope

Locations are a type with the depot as none; periods are 1-based natural numbers and every statement carries $1 \le n \le N$ . Costs and values lie in $[0,\infty]$ ; every minimum is an infimum, equal to $+\infty$ on an empty feasible set; expectations are sums against the probability mass function of $\mathbb Q^n$ . A decision is a list of nonempty routes covering the current orders exactly once. The parameters $\omega$ are nonnegative reals by their type, with the diagonal $\omega^{n'}_{n'}(K) = K$ written into (10). The available drivers in the dynamic program are $\bar K - \zeta^n_n$ in $\mathbb N$ ; in APT the right-hand side is the real $\bar K - \zeta^n_{n'}$ .

Standing assumptions, shared by every statement: $N \ge 1$ ; strictly increasing epochs; finitely supported, period-independent demand laws; $q^n_i = 0$ off $\mathcal I^n$ . Added hypothesis: $\zeta^n_{n'} \le \bar K$ for $n \le n' \le N$ (the en route drivers belong to the fleet). Disclosed readings: travel times do not depend on the period; delivery times follow the recursion of Appendix C with equality, starting from the depot leg; a policy's expected cost is defined recursively along its decisions.

Ruled out: defining $\mathcal H_N$ or $\mathcal H^s$ through the APT objective (exactness would become definitional); decision sets that may leave orders unserved (every cost would vanish); an upper bound without the cap by the policy's cost; negative parameters $\omega$ .

The development needs the model and its recursion (provided as one definition file), monotonicity of $\mathcal H^s$ in $K$ , and induction principles for the well-founded recursions. Proofs of the milestones in any order are welcome; Lemma 1 is not used by the paper's proof of Theorem 1 but is a natural first step.

Selected references

S. Liu, Z. Luo, On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand, Manufacturing & Service Operations Management, 2023; preprint arXiv:2107.13058v3, 2022. https://arxiv.org/abs/2107.13058
W. B. Powell, Approximate Dynamic Programming: Solving the Curses of Dimensionality, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9781118029176
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 4th ed., Athena Scientific, 2017 (rollout policies, Ch. 6).

7 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Right to Repair: Pricing, Welfare, and Environmental Implications: The Manufacturer's Optimal New-Product and Repair Prices and the Resulting No-, Partial- or Full-Repair Equilibrium (Table 1)Research Paper

Motivation

Repair access changes more than the cost of fixing a broken product. It also changes how many used products reach a resale market, what those products sell for, and whether a manufacturer prefers to sell another new unit or earn a repair margin. Jin, Yang, and Zhu study these connected pricing decisions in a two-period durable-goods model in Right to Repair: Pricing, Welfare, and Environmental Implications. Their Proposition 1 identifies the manufacturer's prices and the resulting market outcome when independent and manufacturer repair restore the same product quality. This mission formalizes that proposition, including all seven rows of its Table 1.

The question is relevant to work on durable-goods markets because a repaired product can compete with a new one in the next period. A lower independent-repair cost can affect the manufacturer's behavior even if consumers do not choose independent repair in the final equilibrium. The paper's setting makes that effect precise through the used-product price, new-product demand, and the manufacturer's repair decision.

Setting

A new product provides one period of use and then fails with probability $f\in(0,1)$ . If it remains functional, or if a failed unit is repaired, it can be used for one more period as a used product. After two periods of use it has no value. Consumers have types $\theta$ uniformly distributed on $[0,1]$ . A new product gives per-period gross utility $\theta$ ; a functional used product gives $\delta\theta$ , with $\delta\in(0,1)$ . This mission takes the paper's identical-repair-quality case $\mu=\delta$ and zero resale transaction cost $\tau=0$ .

The manufacturer chooses a new-product price $p_n$ and a manufacturer repair price $p_r$ . Producing a unit costs $c$ and repairing it costs $c_M$ . A consumer can instead pay $c_I\ge c_M$ for independent repair. A manufacturer repair price of $\infty$ means that service is unavailable. The used-product price $p_u$ emerges from the secondary market. Consumers who face a failure repair with probability $\alpha$ : they repair whenever the resale gain exceeds $\min\{c_I,p_r\}$ , do not repair when it falls short, and may mix at equality.

Consumers can be inactive, buy a used unit every period, or buy a new unit every period. Their corresponding per-period utilities are $0$ , $\delta\theta-p_u$ , and

\theta-p_n+(1-f)p_u+f[p_u-\min\{c_I,p_r\}]^+.

The thresholds $\theta_1\le\theta_2$ partition these choices. In a market with a positive used price, used demand equals the supply generated by new buyers: $\theta_2-\theta_1=(1-\theta_2)(1-f+f\alpha)$ . At $p_u=0$ , used supply may exceed demand. The manufacturer's per-period profit combines new-unit margin $(p_n-c)(1-\theta_2)$ with its repair margin on units it actually repairs. These primitives and Assumption 1 appear in §4.1 of the paper.

Formalization targets

Consumer behavior and reduced pricing problems

Lemma 1 states that consumer utility has the three-segment form above. The appendix then compares reduced pricing problems for no repair, full repair, and partial repair. One milestone records the full-repair optimum:

\max\pi_4=\frac{(c-\delta+c_Mf-1)^2}{4(1+3\delta)},\qquad p_n+fp_r=\frac{c+\delta+c_Mf+1}{2}

at a feasible full-repair maximizer. Other milestones record the profit-gap identities, the ordering of two production-cost cutoffs, and the appendix results for the two higher ranges of independent-repair cost. Their statements follow Online Appendix G.

Proposition 1 and Table 1

The goal is the complete equilibrium characterization of Proposition 1 and Table 1. When $c_I\ge(\delta+c_M)/2$ , the optimal outcome changes at $\underline c$ and $\bar c$ from no repair to partial repair to full repair. When $c_I<(\delta+c_M)/2$ , three cutoffs $\hat c_1,\hat c_2,\hat c_3$ give four rows: two no-repair regimes, partial repair, and full repair. Each row specifies $p_n^*$ , $p_r^*$ , $p_u^*$ , and $\alpha^*$ ; the partial-repair rows require $0<\alpha^*<1$ . The target fixes the paper's explicit formulas rather than only the number or order of the regimes.

Significance

The theorem gives a simultaneous answer for manufacturer pricing and the secondary-market outcome. It identifies when manufacturer repair is unused, offered to some consumers, or offered to all consumers facing failure. In the low- $c_I$ case it also distinguishes two no-repair regimes with different used prices. Those distinctions matter for subsequent welfare and environmental comparisons in the paper: a price change can alter new production and resale quantities even when the repair count does not change.

The paper proves Proposition 1 analytically; this mission asks for a machine-checked proof of its exact statement. A complete development would also establish reusable interfaces for a market-clearing equilibrium with a zero-price excess-supply corner, price optimization across several feasible regimes, and comparisons between algebraic cutoff formulas. The draft theorem statements are open Lean goals; the local sanity check proves that one specified market equilibrium is inhabited, not the proposition itself.

Difficulty

The manufacturer's choice affects both the direct repair margin and the resale price that determines demand for new and used goods. Optimizing the new-product price in isolation therefore does not give the global result. The appendix's candidate solutions come from distinct repair and market-clearing regimes, and their feasible sets meet at cutoffs where different prices can tie. A global claim has to compare each candidate against all admissible price pairs and their equilibria. The radical and rational cutoff formulas add boundary cases: a formula may be used only in the regime where its denominator and square-root argument have the intended meaning.

Formalization scope

Lean uses real prices, costs, probabilities, and consumer thresholds. The standing assumptions are $0<f<1$ , $0<\delta<1$ , $c_M\le c_I$ , and the paper's Assumption 1, $c_M<\delta$ and $c<1+\delta-c_Mf$ . It also pins the three unit costs to $c,c_M\ge0$ , consistent with the paper's nonnegative-cost appendix domain. An unavailable manufacturer repair service is represented by none, not by an arbitrary large real number. A real repair price must be nonnegative.

The equilibrium predicate requires actual utility-maximizing consumer segments, the repair rule, and market clearing. It allows excess used-product supply only at $p_u=0$ . It also admits the appendix's zero-demand outcome, in which neither product yields positive utility, no units sell, and profit is zero. An optimal outcome contains an equilibrium and beats every equilibrium at every admissible competing price pair. Thus an empty equilibrium relation cannot make the goal true. At cutoff ties the theorem asserts that the displayed prices are an optimum, without claiming uniqueness. The two partial-repair rows assert strict bounds on $\hat\alpha$ , excluding a vacuous $0/0$ value.

The appendix's Problems 1, 4, and 5 are separate reduced objectives and feasible sets. The rational partial-repair objective is accompanied by its polynomial continuation for the profit-gap identity; that continuation is used only where the printed rational form could produce $0/0$ . The source's second identity in (G.41) omits a factor $\delta$ in its denominator. The Lean statement uses the corrected algebraic identity, while the milestone preserves the printed line. Contributions that prove the consumer, reduced-problem, cutoff, and global-optimality milestones are all within scope. The remaining propositions on welfare, quality differences, and environmental effects are outside this mission.

Selected references

Chenyu Jin, Lihong Yang, and Chen Zhu, Right to Repair: Pricing, Welfare, and Environmental Implications, Management Science, 2022. Authors' manuscript used here, DOI 10.1287/mnsc.2022.4401, PDF SHA-256 b869b33a21376a298a2355fb4de697d59b1362d5895f166f3255348812bc1763.

8 thms3 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

Courier Dispatch in On-Demand Delivery I: With Exogenous Demand, Dedicated Delivery Has the Shorter Wait Exactly Below One Threshold in Demand Rate and in Service RadiusResearch Paper

Motivation

On-demand delivery platforms for meals and groceries promise delivery within minutes, and the main operational lever they control is how a courier is dispatched. A courier can carry each order as soon as it is ready (dedicated delivery), or wait until two orders are available and deliver them in one trip (batch delivery). Batching saves travel per order but makes the first customer wait for a second order to arrive. Which mode gives the shorter wait, and hence the higher revenue, is a question practitioners face daily; it is the subject of M. Chen and M. Hu, Courier Dispatch in On-Demand Delivery (SSRN 3675063; published in Management Science, DOI 10.1287/mnsc.2023.4858).

The paper answers the question in closed form for a stylized disk model. This mission formalizes its first headline result, for the case in which the demand rate is fixed exogenously (for example by a growth target or by kitchen capacity), as stated in Propositions 1 and 2 of the authors' version dated 2022-09-21.

Setting

A vendor sits at the centre of a disk of radius $r>0$ and employs one courier with unit travel speed, so travel time equals travel distance. Customer orders arrive as a Poisson process of rate $\lambda>0$ , the demand rate, and each customer's location is independent and uniformly distributed on the disk.

Under dedicated delivery each trip is a round trip to one customer, of length $X_D=2\|U\|$ with $U$ uniform on the disk. Its moments are $\mathbb E[X_D]=\tfrac43 r$ and $\mathbb E[X_D^2]=2r^2$ , so the courier is an M/G/1 server with

\mu_D=\frac{3}{4r},\qquad C_D=\frac98 ,

where $\mu_D$ is the service rate and $C_D$ the summed coefficients of variation. The paper defines the expected wait under dedicated delivery as the M/G/1 in-line delay

W_D(\lambda,\mu,C)=\frac{\lambda}{\mu(\mu-\lambda)}\cdot\frac C2 .

Under batch delivery the courier leaves only with two orders and visits both, so a trip has length $X_B=\|U\|+\|U-U'\|+\|U'\|$ for two independent uniform points, with $\mathbb E[X_B]=\big(\tfrac{128}{45\pi}+\tfrac43\big)r$ . This gives

\mu_B=\frac{45\pi}{4r(32+15\pi)},

and a variability coefficient $C_B\approx 0.583$ that the paper obtains by numerical integration. The paper defines the batch wait as the time for a second order to arrive, plus Kingman's approximation of the E $_2$ /G/1 in-line delay, plus the expected delay of being second in a batch:

W_B(\lambda,\mu,C)=\frac1{2\lambda}+\frac{\lambda}{\mu(2\mu-\lambda)}\cdot\frac C2+\frac r3 .

Customers have valuations with c.d.f. $F$ on $[0,1]$ and a wait cost $c>0$ per unit time; at price $p$ the potential arrival rate $\Lambda r^2$ thins to $\lambda$ . The vendor's revenue rate at demand rate $\lambda$ and expected wait $w$ is

V(\lambda,w)=\lambda\Big[F^{-1}\Big(1-\frac{\lambda}{\Lambda r^2}\Big)-c\,w\Big].

Dedicated delivery is stable exactly when $\lambda r<\tfrac34$ ; batch delivery when $\lambda r<T_2=\frac{45\pi}{2(32+15\pi)}\approx0.893$ .

Formalization targets

Goal: one threshold in $\lambda r$ (Propositions 1 and 2)

For every $C_B\in[0.58,0.59]$ there is a constant $a_1\in(0,\tfrac34)$ such that for all $r>0$ , $\lambda>0$ with $\lambda r<\tfrac34$ ,

W_D(\lambda,\mu_D,C_D)<W_B(\lambda,\mu_B,C_B)\iff \lambda r<a_1,\qquad W_B(\lambda,\mu_B,C_B)<W_D(\lambda,\mu_D,C_D)\iff \lambda r>a_1,

and the same two equivalences hold for the revenues $V(\lambda,W_D)$ and $V(\lambda,W_B)$ , for every $F^{-1}$ , every $\Lambda>0$ with $\lambda\le\Lambda r^2$ , and every $c>0$ . The paper reports $a_1\approx0.5689$ ; the goal asserts only the existence and the location in $(0,\tfrac34)$ .

Milestones

The dedicated trip moments $\mathbb E[X_D]=\tfrac43r$ , $\mathbb E[X_D^2]=2r^2$ , and the resulting $\mu_D$ , $C_D$ (display (3)).
The mean batch trip $\mathbb E[X_B]=(\tfrac{128}{45\pi}+\tfrac43)r$ and the resulting $\mu_B$ (display (8), first moment).
The reduction (A.1): $W_D(\lambda,\mu_D,C_D)-W_B(\lambda,\mu_B,C_B)=f_A(\lambda r)/\lambda$ for an explicit rational function $f_A$ of one variable.
The single crossing: $f_A$ has exactly one zero $a_1$ on $(0,\tfrac34)$ , negative before and positive after, with $0.56<a_1<0.58$ .
Proposition 1: for each $r$ , a threshold $\lambda_{ex}\in(0,\mu_D)$ in the demand rate.
Proposition 2: for each $\lambda$ , a threshold $r_{ex}\in(0,\tfrac3{4\lambda})$ in the radius.

Significance

The result says that, with demand fixed, the choice between dedicated and batch delivery depends on the market only through the product $\lambda r$ : dedicated delivery is better when demand is low or the area small, batching when demand is high or the area large. The threshold is a single universal number, independent of the valuation distribution and of the wait-cost rate, because at a fixed demand rate the strategy with the shorter wait always earns more. This is the efficiency-driven benchmark against which the paper's second main result (endogenous demand in a crowded market, where the order reverses) is contrasted.

To our knowledge none of this has been machine-checked. The mission produces a checked version of the paper's closed-form comparison and, in milestones 1–2, checked computations of classical geometric-probability moments of the disk (the mean distance $128r/(45\pi)$ between two uniform points). The paper's own argument for the single crossing is numerical ("solved using standard methods"); a formal proof must replace it by an exact argument with rigorous bounds on $\pi$ .

Difficulty

The reduction to one variable is algebra. The difficulty is the sign analysis of $f_A$ on $(0,\tfrac34)$ : it is a difference of two rational functions with poles at $\tfrac34$ and $T_2\approx0.893$ , involving $\pi$ , and clearing denominators gives a cubic whose roots the paper only reports numerically. The natural first idea, showing $f_A$ is monotone on the whole interval, does not apply directly, since $f_A$ starts at $-\tfrac12$ , first decreases, and only later rises to $+\infty$ ; a proof must establish that it crosses zero exactly once. A further point is that $C_B$ is not a closed-form number, so the crossing must be shown uniformly over an interval of values.

The moment milestones need integration in polar coordinates on the plane; the mean distance between two uniform points of a disk is a classical but nontrivial four-dimensional integral.

Formalization scope

All objects live in the namespace CourierDispatch.Exogenous. Real numbers are ℝ, $\lambda$ is lam, $\Lambda$ is Lam, and $F^{-1}$ is an arbitrary function Q : ℝ → ℝ (no property of it is needed, since at equal $\lambda$ the price terms cancel). The plane is EuclideanSpace ℝ (Fin 2) and the uniform law on the disk is Lebesgue measure conditioned on the closed ball.

Committed conventions:

The expected waits are the paper's closed-form formulas (5) and (12): the M/G/1 in-line delay for dedicated delivery and Kingman's approximation for the E $_2$ /G/1 batch queue. The paper introduces them as definitions (" $:=$ "), and the mission does not formalize the queues behind them; no statement here is about the true stationary delay of an E $_2$ /G/1 queue.
$C_B$ is a real parameter with the standing hypothesis $0.58\le C_B\le 0.59$ , which contains the paper's value $0.583$ and a Monte-Carlo estimate $0.58297$ .
Every comparison is restricted to $r>0$ , $\lambda>0$ , $\lambda r<\tfrac34$ , the range where both queues are stable; above it only batch delivery is defined and the paper makes no comparison. This also keeps every formula away from Lean's junk values for division by zero.
Revenue comparisons additionally require $\Lambda>0$ and $\lambda\le\Lambda r^2$ , the effective-demand range in §3, p. 8. The arbitrary function Q stands for $F^{-1}$ ; its properties cancel when the two strategies are compared at the same demand rate.
Both directions of each threshold are stated as strict equivalences, so equality at $\lambda r=a_1$ follows.

The threshold $a_1$ (and $\lambda_{ex}$ , $r_{ex}$ ) is existential in every statement; it is never a definition and never an infimum of a sign set, and $W_D$ , $W_B$ are never defined through $f_A$ , so the goal cannot be made true by construction.

Needed infrastructure: polar-coordinate integration on the plane (Mathlib's integral_comp_polarCoord_symm), and rigorous rational bounds on $\pi$ (Real.pi_gt_d6, Real.pi_lt_d6). The goal does not depend on the moment milestones 1–2, which ground the constants $\mu_D$ , $C_D$ , $\mu_B$ in the geometry of the disk and are welcome as separate contributions.

Selected references

M. Chen, M. Hu, Courier Dispatch in On-Demand Delivery, SSRN 3675063, version of 2022-09-21; Management Science, 2023. https://ssrn.com/abstract=3675063, https://doi.org/10.1287/mnsc.2023.4858
J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24 (1962). https://doi.org/10.1111/j.2517-6161.1962.tb00465.x
H. Solomon, Geometric Probability, SIAM CBMS-NSF Regional Conference Series 28, 1978. https://doi.org/10.1137/1.9781611970418
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

9 thms3 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 1: Under FIFO Issuance the Heuristic Base-Stock Policy's Optimality Gap Decays Exponentially in the Product LifetimeResearch Paper

Perishable inventory and the base-stock question

Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that has not been used within $m$ periods of its arrival must be discarded. Managing such stock is a classical problem of inventory theory, going back to Nahmias (1975), and it remains of practical interest for hospital blood banks and grocery retail. The difficulty is structural. The state of the system is the whole age profile of the stock, a vector of dimension $m-1$ , and the optimal policy depends on all of it. Dynamic programming over this state is intractable even for moderate lifetimes, so practice relies on simple heuristics, above all base-stock policies, which raise the total stock to a fixed level $S$ every period.

For decades the performance of base-stock policies in this system was understood only numerically. Chazan and Gal (1977) and Cooper (2001) bounded the long-run outdating of a base-stock policy; Nandakumar and Morton (1993) built a base-stock policy from bounds on the optimal order-up-to level and showed numerically that it performs close to optimal. Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first theoretical guarantees, comparing a simple base-stock policy with the optimal policy in several asymptotic regimes. This mission formalizes the first of them: the optimality gap decays exponentially in the lifetime $m$ .

Setting

Time is discrete, $t=1,2,\dots$ . Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F(x)=\mathbb P(D\le x)$ ; $F^{-1}(x)=\inf\{y:F(y)\ge x\}$ .

At the start of period $t$ the state is $\mathbf x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods. The firm orders $q_t\ge0$ , which arrives immediately and raises the total level to $x_{t,m}=x_{t,m-1}+q_t$ (with $x_{t,0}=0$ ). Demand is served oldest-first (FIFO issuance) and unmet demand is lost. Stock reaching the end of its life is outdated:

o_t=(x_{t,1}-D_t)^+,\qquad x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\quad i=1,\dots,m-1.

The system starts empty. Each period costs

C^\pi_t=h(x^\pi_{t,m}-D_t)^++p(D_t-x^\pi_{t,m})^++\theta o^\pi_t,

with holding cost $h>0$ , lost-sales penalty $p>0$ and additional outdating cost $\theta\ge0$ . A policy is admissible if each order is a nonnegative measurable function of the current state; $\Pi$ is the set of admissible policies. The long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}=\inf_{\pi\in\Pi}C^\pi$ .

The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ ; its cost is $C(S)$ . The heuristic level $\widetilde S$ is a minimizer over $[0,\infty)$ of

\widetilde C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\frac\theta m\,\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big],

and $S^{NP}=F^{-1}(p/(p+h))$ is the newsvendor level.

Formalization targets

Goal: Theorem 1 (p. 11)

For every $\lambda>0$ and $m\ge1$ ,

C_m(\widetilde S_m)-\mathrm{OPT}_m\le\frac{(m-1)\theta}{\lambda me}\,e^{\lambda S^{NP}}\big(\mathbb E[e^{-\lambda D}]\big)^m .

The bound holds for every minimizer $\widetilde S_m$ and every demand law with positive finite mean. Since $\mathbb E[e^{-\lambda D}]<1$ , the gap decays exponentially in $m$ .

Milestones

(19), the FIFO outdating recursion $o^\pi_{t+m-1}=\big(x^\pi_{t,m}-\sum_{i=t}^{t+m-1}D_i-\sum_{j=t}^{t+m-2}o^\pi_j\big)^+$ , for every admissible policy and every demand path.
Lemma 1: $C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\theta\,\mathbb E[O_\infty(S)]$ , with the long-run average outdating $\mathbb E[O_\infty(S)]$ the same from every initial state.
Lemma 2: $\frac1m\mathbb E[(S-\sum_{i\le m}D_i)^+]\le\mathbb E[O_\infty(S)]\le\min\{\mathbb E[(S/m-D)^+],\mathbb E[(S-\sum_{i\le m}D_i)^+]\}$ .
(5): $F^{-1}(\frac p{p+h+\theta})\le\widetilde S\le F^{-1}(\frac p{p+h})$ .
(15): $\sum_{i=t}^{t+m-1}o^\pi_i\ge(x^\pi_{t,m}-\sum_{i=t}^{t+m-1}D_i)^+$ .
Proposition 2: $\mathrm{OPT}\ge\widetilde C(\widetilde S)$ .
(21): $C(\widetilde S)-\mathrm{OPT}\le\frac{(m-1)\theta}m\,\mathbb E[(\widetilde S-\sum_{i\le m}D_i)^+]$ .

Significance

Theorem 1 says that a single explicit base-stock level, computable from the demand law by a one-dimensional convex search, is nearly optimal once the lifetime is moderately long, with an explicit, distribution-dependent rate. It explains why the non-perishable newsvendor intuition carries over to long-lived products, and it is the first of seven guarantees in the paper. Its ingredients are reused throughout: Lemmas 1 and 2, Proposition 2 and the gap bound (21) are posed in this mission and used, without restatement, by missions 2 to 4 of this series (demand population size, penalty cost, outdating cost).

The result is proved on paper; nothing about perishable inventory has been machine-checked. A formal development would provide a reusable model of FIFO perishable dynamics with long-run average costs, sample-path inequalities for outdating, and the first verified optimality-gap bound for an inventory heuristic in a high-dimensional state space.

Difficulty

Most of the argument is sample-path bookkeeping plus Jensen's inequality, but two steps are not routine. Lemma 1 asserts that the long-run average outdating of $\pi_S$ exists and does not depend on the initial state. The natural route through a stationary distribution fails: when $\mathbb P(D<S/m)=1$ the chain can be periodic and has no steady state, so the identity must hold for Cesàro averages directly; in the aperiodic case the paper uses a minorization condition (Meyn and Tweedie, Theorem 16.0.2). Proposition 2 compares every admissible policy with the heuristic cost, which needs the independence of the order-up-to level $x^\pi_{t,m}$ from current and future demands, and a conditional Jensen step for nonlinear expectations of a policy-dependent quantity.

Formalization scope

The Lean development fixes the following conventions.

Time is zero-based: Lean period $t$ is the paper's period $t+1$ .
The state is Fin (m - 1) → ℝ holding the cumulative levels, with $x_{t,0}=0$ , so $m=1$ (empty state, all leftover stock outdates) is included; $m\ge1$ , $h>0$ , $p>0$ , $\theta\ge0$ are fields of the parameter record.
Base-stock levels range over $[0,\infty)$ (ℝ≥0).
The trajectory is a recursion on the demand path, so the state of period $t$ depends only on $D_1,\dots,D_{t-1}$ .
Costs and averages take values in $[0,\infty]$ ; expectations are lower Lebesgue integrals over the i.i.d. path law; averages run over $T+1$ periods, which has the same limsup.
$\Pi$ is the paper's class: time-dependent measurable state-feedback orders.
$\mathbb E[O_\infty(S)]$ is the long-run average expected outdating of $\pi_S$ from the empty state.
" $\widetilde S$ is a minimizer" is a predicate, and the goal, (21) and Proposition 2 quantify over every minimizer; the upper half of (5) is stated for the least minimizer.
Gaps are written $C(\widetilde S)\le\mathrm{OPT}+B$ , equivalent to the paper's form since $\mathrm{OPT}\le C(0)<\infty$ .
(15) and Proposition 2 are stated for FIFO only, although the paper states them for any issuance policy.
The demand law and the newsvendor functions are the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.

Trivializing readings are excluded: $C(S)$ is the simulated cost of $\pi_S$ , not a formula; $\mathrm{OPT}$ ranges over all admissible policies, not only base-stock ones; $\widetilde S$ is the argmin predicate, not a closed form; $m$ , $\theta$ and the demand law are general; and no gap is stated with truncated subtraction. Contributions of any of the milestones, of general facts about Cesàro limits of Markov chains, or of the convexity of $\widetilde C$ , are welcome.

Selected references

J. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022 (accepted manuscript, SSRN 3724966). https://ssrn.com/abstract=3724966
D. Chazan, S. Gal, A Markovian model for a perishable product inventory, Management Science 23(5), 1977. https://doi.org/10.1287/mnsc.23.5.512
W. L. Cooper, Pathwise properties and performance bounds for a perishable inventory system, Operations Research 49(3), 2001. https://doi.org/10.1287/opre.49.3.455.11221
S. Nahmias, Optimal ordering policies for perishable inventory—II, Operations Research 23(4), 1975. https://doi.org/10.1287/opre.23.4.735
P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1993. https://doi.org/10.1287/mnsc.39.12.1490
S. P. Meyn, R. L. Tweedie, Markov Chains and Stochastic Stability, Springer, 1993. https://doi.org/10.1007/978-1-4471-3267-7

12 thms3 active usersReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian 2: Under the VP-EB Error Bound, NAPP-AL Converges Linearly to a Stationary PointResearch Paper

Motivation

Many problems in machine learning, signal processing and engineering design minimize a nonconvex, possibly nonsmooth objective subject to nonlinear equality constraints. Augmented Lagrangian methods are the standard tool for such constraints, but each classical iteration solves a hard nonconvex subproblem. Zhu, Zhao and Zhang (arXiv:2007.12219v1, published in Mathematics of Operations Research, 2024) propose NAPP-AL, a first-order primal-dual method in which each iteration takes one linearized proximal step in each primal block and one multiplier step. Their §4 shows that the best stationarity residual decays like $o(1/\sqrt k)$ . That rate is sublinear, and the question addressed by §5 is when the same method converges linearly. The answer is a local error bound, the value proximity error bound (VP-EB), under which the iterates have finite length, converge to a stationary point, and do so at a geometric rate. Error-bound conditions of this kind are the usual route from sublinear to linear rates for first-order methods (Luo–Tseng; Attouch–Bolte; Bolte–Nguyen–Peypouquet–Suter), and VP-EB is the paper's version adapted to its potential function.

Setting

The problem (P) is

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

with $\Theta:=\Omega+\Phi:\mathbb R^n\to\mathbb R^m$ , $G$ and $H$ smooth with Lipschitz gradients ( $L_G$ , $L_H$ ), $J$ lower semicontinuous and possibly nonsmooth and nonconvex, $U$ closed and convex, $\Theta$ Lipschitz with constant $L^0_\Theta$ , each component $\Omega_j$ with $L_{\Omega_j}$ -Lipschitz gradient, $L_\Omega:=\sum_j L_{\Omega_j}$ , and $B$ an $m\times d$ matrix with $\operatorname{Im}\Theta\subseteq\operatorname{Im}B$ and $\lambda_{\min}(B^\top B)>0$ (Assumption 1). A point is $w=(u,v,p)$ , with $\|w\|$ the Euclidean norm of the stacked vector.

The augmented Lagrangian is $\mathcal L_\gamma(w)=F(u,v)+\langle p,\Theta(u)+Bv\rangle+\frac\gamma2\|\Theta(u)+Bv\|^2$ . The stationarity set $\partial\mathcal L_\gamma(w)$ (p. 6) collects the triples

\big(\nabla_uG+\partial J(u)+\mathcal N_U(u)+(\nabla\Theta(u))^\top y,\ \nabla_vG+\nabla H(v)+B^\top y,\ \Theta(u)+Bv\big),\quad y=p+\gamma(\Theta(u)+Bv),

with $\partial J$ the limiting subdifferential and $\mathcal N_U$ the normal cone; $w$ is stationary when $0\in\partial\mathcal L_\gamma(w)$ .

NAPP-AL (p. 8) fixes a $\beta$ -strongly convex $K$ with $L_K$ -Lipschitz gradient and its Bregman distance $D$ , and a penalty $\gamma$ above $\frac{\sqrt{57}+1}{2\lambda_{\min}(B^\top B)}(L_G+L_H)$ (Assumption 2). With $q^k=p^k+\gamma(\Theta(u^k)+Bv^k)$ , it sets $u^{k+1}$ to a global minimizer over $U$ of $\langle\nabla_uG(u^k,v^k),u\rangle+J(u)+\langle q^k,\nabla\Omega(u^k)u+\Phi(u)\rangle+D(u,u^k)/\epsilon^k$ , $v^{k+1}$ to the minimizer of a strongly convex quadratic, and $p^{k+1}=p^k+\gamma(\Theta(u^{k+1})+Bv^{k+1})$ . The step $\epsilon^k$ lies in $[\sigma\delta_k,\delta_k]$ , with $\delta_k$ given explicitly by rule (8).

The analysis uses the potential (18)

\Lambda^k=\mathcal L_\gamma(w^k)+c_1\|u^{k-1}-u^k\|^2+c_2\|v^{k-1}-v^k\|^2+\tfrac1{2\gamma}\|p^{k-1}-p^k\|^2,

with explicit $c_1,c_2$ . VP-EB at $\bar w$ with constants $\kappa_1,\eta,\nu>0$ (Definition 5.1) asks that $\mathcal L_\gamma(w^{k+1})-\mathcal L_\gamma(\bar w)\le\kappa_1\|w^k-w^{k+1}\|^2$ whenever $\|w^{k+1}-\bar w\|<\eta$ and $\mathcal L_\gamma(w^{k+1})<\mathcal L_\gamma(\bar w)+\nu$ .

Formalization targets

Goal: Theorem 5.1 (p. 19)

Under Assumptions 1–2 and rule (8), let $\bar w$ be an accumulation point of an NAPP-AL run with $\mathcal L_\gamma(\bar w)=\Lambda^*:=\lim_k\Lambda^k$ , and let VP-EB hold at $\bar w$ with $\kappa_1,\eta,\nu$ . Then (i) eventually $\|w^k-\bar w\|<\eta$ and $\mathcal L_\gamma(w^k)<\Lambda^*+\nu$ ; (ii) $\sum_k\|w^k-w^{k+1}\|<\infty$ ; (iii) $w^k\to\bar w$ and $\bar w$ is stationary; (iv) for some $\alpha\in(0,1)$ and $k_0$ ,

\Lambda^{k+1}-\Lambda^*\le\alpha(\Lambda^k-\Lambda^*)\quad(k\ge k_0);

and the iterates converge R-linearly: $\|w^k-\bar w\|\le C\rho^k$ for some $C\ge0$ , $\rho\in(0,1)$ .

Milestones

Theorem 5.1(i)–(iii): localization, finite length, convergence to a stationary point.
Theorem 5.1(iv): Q-linear convergence of $\Lambda^k$ .

No constant is hard-coded in the conclusions: $\alpha$ , $\rho$ , $C$ and the thresholds $k_0$ are existential.

Significance

The theorem upgrades the method's guarantee from sublinear stationarity to a geometric rate for both the potential and the iterates, and it gives whole-sequence convergence rather than subsequential convergence. VP-EB is checkable through standard conditions: §6 of the paper shows that the Kurdyka–Łojasiewicz property of $\mathcal L_\gamma$ with exponent $1/2$ , and metric subregularity of $\partial\mathcal L_\gamma$ , each imply it; those implications are the companion missions of this series. The result is proved on paper; no machine-checked proof of it or of NAPP-AL's convergence theory is known. Formalizing it produces a checked localization-and-induction argument of the kind that recurs throughout the error-bound literature, written against an explicit potential with explicit constants.

Difficulty

Accumulation alone does not make the iterates stay near $\bar w$ : VP-EB only applies while $w^{k+1}$ is inside the ball and below the level $\Lambda^*+\nu$ , so its use is circular unless one first shows the iterates never leave the region. The obvious argument — apply the error bound at every step — therefore fails; localization (part (i)) is the core of the proof, and it must be carried out with the paper's explicit constants $c_1,c_2,c_3$ and the sufficient decrease of $\Lambda^k$ (Lemma 4.3 and Theorem 4.1, pp. 15–16, milestones of the first mission of this series). A second subtlety is that the page's proof treats $\Lambda^k$ as strictly decreasing, while the sufficient-decrease lemma gives only non-increase; the case where $\Lambda^k$ reaches $\Lambda^*$ in finite time must be handled separately.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin k); triples $w$ use the explicit Euclidean norm tnorm of the stacked vector, never the sup norm of the product type. $B$ is a continuous linear map with its operator (spectral) norm, never a Matrix with the entrywise norm; $\lambda_{\min}(B^\top B)$ is the Rayleigh minimum over the unit sphere. $\operatorname{dist}(0,S)$ is an infimum in $[0,\infty]$ , equal to $+\infty$ on $\emptyset$ , never Metric.infDist. The normal cone is empty off $U$ , so stationary points lie in $U\times\mathbb R^d\times\mathbb R^m$ . NAPP-AL is a relation on given sequences (any global minimizers of (5); existence is not asserted), with arbitrary $u^0$ . $\Lambda^0$ is junk in Lean, so statements about $\Lambda^k$ concern $k\ge1$ .

Disclosed readings of the page: $G,H,J$ are real valued with gradients Lipschitz on the whole space; (H3)'s local Lipschitz clause means each $u\in U$ has a neighbourhood in $\mathbb R^n$ on which $J$ is Lipschitz (not Mathlib's relative LocallyLipschitzOn); $\lambda_{\min}(B^\top B)>0$ ; $\mathcal N_U(u)=\emptyset$ for $u\notin U$ ; Definition 5.1's phrase "which converges to $\bar w$ " is dropped, since Theorem 5.1 proves convergence, and keeping it would assume conclusion (iii); " $\mathcal L_\gamma(\bar w)=\Lambda^*$ " is the hypothesis $\Lambda^k\to\mathcal L_\gamma(\bar w)$ . Using Metric.infDist, the product sup norm, an entrywise matrix norm, a relative local Lipschitz condition, or a normal cone nonempty off $U$ would each change or trivialize the statements and is ruled out.

The source is the preprint arXiv:2007.12219v1, not the published version; all labels, pages and constants are v1's. The definitions are restated in this mission's namespace NAPPAL.Linear and coincide with those of the other missions of the series. A complete development needs the sufficient-decrease lemma and the convergence theorem of the first mission (Lemma 4.3, Theorem 4.1), plus elementary facts on summable sequences and geometric bounds. Contributions to the localization induction, which is reusable for the other error-bound arguments of §6, are welcome.

Selected references

D. Zhu, L. Zhao, S. Zhang, A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian, arXiv:2007.12219v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2007.12219v1
H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Mathematical Programming 116, 2009. https://doi.org/10.1007/s10107-007-0133-5
J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Mathematical Programming 165, 2017. https://doi.org/10.1007/s10107-016-1091-6
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46, 1993. https://doi.org/10.1007/BF02096261

9 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

The Conceptual Flaws of Decentralized Automated Market Making: Constant Product Pricing Admits Profitable Front-Running and Multi-Venue ArbitrageResearch Paper

Why constant product pricing matters

Decentralized exchanges on public blockchains do not match buyers with sellers through an order book. Most of them trade against a liquidity pool: a smart contract that holds reserves of two tokens and quotes a price by a fixed formula. The most widely used formula is the constant product rule of Uniswap (Adams, Zinsmeister and Robinson, 2020), under which a trade must leave the product of the two reserves unchanged. Pools of this kind settle a large share of on-chain token trading, and their pricing rule is fixed in code, visible to every participant, and executed in the order in which transactions are included in a block.

That last feature creates a market-structure question. Pending transactions are public before they execute, so another trader can see an order and place her own trade ahead of it. The empirical literature documents this behaviour at scale (Daian et al., 2020; Zhou et al., 2021). Park's paper asks which properties of the pricing rule itself make such strategies profitable, independently of any information the front-runner has. The paper compares the constant product rule with the cost function of a traditional market maker whose marginal price is linear in quantity, in the tradition of inventory models such as Biais (1993), and then derives four properties of constant product pricing in its Proposition 3.

Timeline:

2018–2020: Uniswap v1 and v2 deploy constant product pools on Ethereum.
2020: Daian et al. measure front-running and transaction reordering on decentralized exchanges.
2021: Park's working paper (June 8, 2021), the source of this mission, states the properties below.
2023: the paper appears in Management Science, retitled; this mission follows the 2021 working paper and its numbering.

The constant product pool

A pool holds $X>0$ units of a token $A$ and $Y>0$ units of a token $B$ . A trader who takes $x$ units of $A$ out of the pool pays $y$ units of $B$ , where $y$ is fixed by the constant product invariant

(X-x)(Y+y)=XY .

A positive $x$ is a buy of $A$ ; a negative $x$ is a sale of $-x$ units of $A$ into the pool, and then $y$ is negative: the trader receives $-y$ . Solving the invariant gives the paper's cost function, equation (3):

p^{\mathrm{cmm}}(x,X,Y)=\frac{xY}{X-x},\qquad x<X .

After a buy of $x$ the pool holds $X-x$ units of $A$ and $Y+p^{\mathrm{cmm}}(x,X,Y)=XY/(X-x)$ units of $B$ . Selling $q>0$ units of $A$ into a pool $(X',Y')$ therefore earns $-p^{\mathrm{cmm}}(-q,X',Y')$ units of $B$ . The paper writes $y(x)$ for $p^{\mathrm{cmm}}(x,X,Y)$ on the current pool.

For the companion comparison the mission also defines the linear market maker's cost $p^{\mathrm{tmm}}(x,I)=x\bigl(V-\tfrac{\ell}{N}I\bigr)+\tfrac{\ell}{2N}x^2$ , where $V$ is the fundamental value, $N$ the number of market makers, $I$ their excess inventory and $\ell>0$ a liquidity factor.

Formalization targets

Goal: Proposition 3

For $x\in(0,X)$ , $\alpha\in(0,1)$ and $k>0$ :

\begin{aligned} &\text{(1)}\quad p^{\mathrm{cmm}}(\alpha x,X,Y)+p^{\mathrm{cmm}}\bigl((1-\alpha)x,\,X-\alpha x,\,Y+y(\alpha x)\bigr)=p^{\mathrm{cmm}}(x,X,Y),\\ &\text{(2)}\quad x<X/2\ \Rightarrow\ -p^{\mathrm{cmm}}(x,X,Y)-p^{\mathrm{cmm}}\bigl(-x,\,X-2x,\,Y+y(2x)\bigr)>0,\\ &\text{(3)}\quad p^{\mathrm{cmm}}(x,X,Y)=k\cdot p^{\mathrm{cmm}}(x/k,\,X/k,\,Y/k),\\ &\text{(4)}\quad -p^{\mathrm{cmm}}\bigl(-\alpha x,\,X-x,\,Y+y(x)\bigr)-p^{\mathrm{cmm}}(\alpha x,X,Y)>0 . \end{aligned}

Part (1) says that splitting an order in time does not change its cost; part (3) that splitting liquidity into $k$ identical pools, with the order split pro rata, does not change it either. Part (2) is the front-runner's profit: she buys $x$ , the victim buys $x$ , and she sells $x$ into the pool left by both buys. Part (4) is the profit of selling $\alpha x$ into a pool just moved by a buy of $x$ and buying $\alpha x$ on an identical untouched pool, for every $\alpha\in(0,1)$ .

Milestones

Lemma 2: for $x<X$ and every real $y$ , $(X-x)(Y+y)=XY$ holds if and only if $y=p^{\mathrm{cmm}}(x,X,Y)$ , and the pool then holds $XY/(X-x)$ of $B$ .
Proposition 3(1), additivity.
Equation (4): for $0<x<X/2$ the front-runner's proceeds are $xXY/((X-x)(X-2x))$ and her profit is

\frac{2x^2Y}{(X-x)(X-2x)}>0 .

Proposition 3(3), split-liquidity invariance.

A companion item poses Proposition 1: with $I=0$ , $N=X$ , $Y=VX$ and $x^*=(X/\ell)(\ell-2V)$ , constant product pricing has a larger signed cost than linear pricing for $x^*<x<X$ , and a smaller one for $x<x^*$ , $x\neq 0$ .

Significance

Parts (1) and (3) are the consistency properties one asks of any market maker: an order's cost does not depend on how it is sliced in time, or on how liquidity is fragmented across identical venues. Parts (2) and (4) show that the constant product rule, despite these properties, rewards anyone who can trade ahead of an observed order or across two identical pools. These are properties of the pricing curve alone, with no informational advantage, which is what makes them relevant to the design of on-chain exchanges, transaction ordering rules and fee schedules.

All statements are proved in the paper by direct algebra, and they are not open. What this mission adds is a machine-checked record of the exact statements, with the paper's printed sign slips resolved explicitly, and a reusable definition of the constant product cost function in Lean on which statements about fees, multi-hop routing or other invariant curves can build. No machine-checked version of Proposition 3 is known.

Difficulty

The mathematics is rational-function algebra; the difficulty is in stating it correctly. Three points need care. First, the sale convention: the paper's cost function returns a negative number for a sale, while the printed statements of parts (2) and (4) add that number as if it were the positive proceeds. Read literally, both printed left-hand sides are negative. Second, the pool after a trade must be tracked exactly: part (4) prints the first pool's $B$ reserve as $Y-y(x)$ , whereas after a buy of $x$ it is $Y+y(x)$ . Third, every quantity is a ratio with a denominator such as $X-x$ , $X-2x$ or $X-\alpha x$ , and the statements hold only on the domain where those are positive. A solver who simplifies before checking signs will prove the wrong inequality.

Formalization scope

Everything lives in the namespace CPAMMFlaws.Properties over the real numbers. The definition pcmm x X Y := x * Y / (X - x) is equation (3) verbatim, argument order $(x,X,Y)$ ; ptmm x V ℓ N I is the printed closed form of $p^{\mathrm{tmm}}$ . Conventions committed to:

Every theorem assumes the deposits are positive, $0<X$ and $0<Y$ (§II.C), although Proposition 3 does not print them; with $Y=0$ every profit vanishes.
Every theorem assumes $x<X$ ; part (2) of the goal and equation (4) assume $x<X/2$ , the paper's restriction for front-running (p. 19). Lean evaluates $a/0$ to $0$ , so these bounds are not optional.
Sale proceeds are written $-p^{\mathrm{cmm}}(-q,\cdot,\cdot)$ , the paper's own sign convention (p. 16). Parts (2) and (4) are posed in this proceeds reading, because the printed signs give false statements; part (4) uses $Y+y(x)$ for the printed $Y-y(x)$ .
Pools after a trade are written in the printed form $Y+p^{\mathrm{cmm}}(\cdot,X,Y)$ , not simplified.

Trivializing formalizations are ruled out: Lemma 2 is the invariant characterization over all $y$ , not the defining equation of pcmm; parts (2), (4) and equation (4) are strict inequalities on the signed proceeds, not $\ge$ and not absolute values; and no statement drops $x<X$ .

Out of scope: the paper's CARA-normal market-maker equilibrium (Lemma 1), its results on the linear market maker (Proposition 2), the fee analysis of §IV and the calibration of §V. The linear cost $p^{\mathrm{tmm}}$ enters only through the companion Proposition 1. Contributions welcome beyond the milestones: proofs of the goal's parts directly, and further invariant-curve properties built on pcmm.

Selected references

A. Park, The Conceptual Flaws of Constant Product Automated Market Making, working paper, June 8, 2021; published as The Conceptual Flaws of Decentralized Automated Market Making, Management Science, 2023. https://doi.org/10.1287/mnsc.2021.02802
H. Adams, N. Zinsmeister, D. Robinson, Uniswap v2 Core, whitepaper, 2020. https://uniswap.org/whitepaper.pdf
P. Daian et al., Flash Boys 2.0: Frontrunning in Decentralized Exchanges, Miner Extractable Value, and Consensus Instability, IEEE Symposium on Security and Privacy, 2020. https://arxiv.org/abs/1904.05234
L. Zhou, K. Qin, C. F. Torres, D. V. Le, A. Gervais, High-Frequency Trading on Decentralized On-Chain Exchanges, IEEE Symposium on Security and Privacy, 2021. https://arxiv.org/abs/2009.14021
B. Biais, Price Formation and Equilibrium Liquidity in Fragmented and Centralized Markets, Journal of Finance 48(1), 1993. https://doi.org/10.1111/j.1540-6261.1993.tb04705.x

6 thms3 active usersReviewed

Completed

Mathematical Physics Probability Quantum Information·Captain: mikedeng1

Quantum Speedup of Monte Carlo Methods 2: Along a B-Chebyshev Cooling Schedule, Consecutive Gibbs Sample States Overlap with |⟨π_i|π_{i+1}⟩|² ≥ 1/BResearch Paper

Motivation

Approximating a partition function $Z(\beta)=\sum_{x\in\Omega}e^{-\beta H(x)}$ is a central task in statistical physics and in counting: it covers the Ising and Potts models, and, at $\beta=\infty$ , counting the zero-energy configurations of a Hamiltonian, for instance the proper $k$ -colourings of a graph. Computing $Z(\infty)$ exactly is #P-complete in many cases, so the goal is an estimate $\widetilde Z$ with $|\widetilde Z-Z(\infty)|\le\epsilon Z(\infty)$ with high probability.

The standard classical approach writes $Z(\infty)$ as a telescoping product of ratios $\alpha_i=Z(\beta_{i+1})/Z(\beta_i)$ along a sequence of inverse temperatures $0=\beta_0<\beta_1<\dots<\beta_\ell=\infty$ , and estimates each ratio by sampling from the Gibbs distribution $\pi_i$ at $\beta_i$ . Dyer and Frieze (1992, as cited on p. 14 of arXiv:1504.06987v3) showed how to bound the number of samples when each estimator has bounded relative second moment; Štefankovič, Vempala and Vigoda (J. ACM 2009) named the resulting condition a Chebyshev cooling schedule and showed that schedules of length $\widetilde O(\sqrt{\log|\Omega|})$ exist and can be found efficiently.

Montanaro (arXiv:1504.06987v3, 2017) gives a quantum algorithm for this problem that improves the dependence on $\epsilon$ and on the relaxation time $\tau$ of the underlying Markov chains quadratically. Its quantum sampling step rests on a theorem of Wocjan and Abeyesinghe (Phys. Rev. A 78, 042336, 2008): a sequence of coherent quantum sample states can be prepared efficiently if consecutive states overlap by at least a constant. This mission formalizes the paper's own link between the two: a Chebyshev cooling schedule produces exactly such overlaps.

Setting

Let $\Omega$ be a finite set of configurations and $H:\Omega\to\{0,1,\dots,n\}$ an integer-valued Hamiltonian. Inverse temperatures range over $[0,\infty]$ . The partition function is

Z(\beta)=\sum_{x\in\Omega}e^{-\beta H(x)},

with the convention $e^{-\infty\cdot h}=1$ if $h=0$ and $0$ otherwise, so that $Z(0)=|\Omega|$ and $Z(\infty)$ counts the configurations with $H(x)=0$ .

A cooling schedule is a sequence $0=\beta_0<\beta_1<\dots<\beta_\ell=\infty$ . Along it, the Gibbs distributions are $\pi_i(x)=e^{-\beta_iH(x)}/Z(\beta_i)$ , the ratios are $\alpha_i=Z(\beta_{i+1})/Z(\beta_i)$ , and the estimators are the random variables $Y_i(x)=e^{-(\beta_{i+1}-\beta_i)H(x)}$ , whose mean under $\pi_i$ is $\alpha_i$ .

Definition 1 (Chebyshev cooling schedule). The schedule is a $B$ -Chebyshev cooling schedule for $Z$ if for every $i=0,\dots,\ell-1$

\frac{Z(2\beta_{i+1}-\beta_i)\,Z(\beta_i)}{Z(\beta_{i+1})^2}\le B.

The chi-squared divergence of $\nu$ from $\pi$ is $\chi^2(\nu,\pi)=\sum_x\pi(x)\big(\nu(x)/\pi(x)-1\big)^2$ , and the quantum sample of a distribution $\pi$ is the unit vector $|\pi\rangle=\sum_{x\in\Omega}\sqrt{\pi(x)}\,|x\rangle$ of $\ell^2(\Omega;\mathbb C)$ . In Lean these are Z, gibbs, alpha, Y, IsCoolingSchedule, IsChebyshevSchedule, chiSq and qsample in the namespace QuantumMC.Cooling.

Formalization targets

Goal: overlap of consecutive quantum samples

For every $B$ -Chebyshev cooling schedule and every $i\in\{0,\dots,\ell-1\}$ ,

|\langle\pi_i|\pi_{i+1}\rangle|^2\ge\frac1B.

The statement fixes no value of $B$ and no length $\ell$ ; it is the shape in which the paper feeds the schedule into the quantum sampling theorem, with overlap parameter $p=1/B$ .

Milestones

The second form of the divergence: $\chi^2(\nu,\pi)=\sum_x\nu(x)^2/\pi(x)-1$ for probability vectors with $\pi>0$ .
Display (1): $\chi^2(\pi_{i+1},\pi_i)=Z(\beta_i)Z(2\beta_{i+1}-\beta_i)/Z(\beta_{i+1})^2-1$ , including the last step $\beta_{i+1}=\infty$ .
Along a $B$ -Chebyshev schedule, $\chi^2(\pi_{i+1},\pi_i)\le B-1$ for all $i$ .
For distributions $\nu$ and $\pi>0$ : $1/\sqrt{\chi^2(\nu,\pi)+1}\le\sum_x\nu(x)\sqrt{\pi(x)/\nu(x)}=\langle\nu|\pi\rangle$ .

Companion statements

The classical facts of §3–3.1 that motivate Definition 1: $\mathbb E_{\pi_i}[Y_i]=\alpha_i$ ; $\mathbb E[Y_i^2]/\mathbb E[Y_i]^2=Z(2\beta_{i+1}-\beta_i)Z(\beta_i)/Z(\beta_{i+1})^2$ ; the telescoping product $Z(\beta_\ell)=Z(\beta_0)\prod_i\alpha_i$ with $Z(\beta_0)=|\Omega|$ ; $\operatorname{Var}(Y_i)/\mathbb E[Y_i]^2\le B$ ; and the accuracy claim that ratio estimates within relative error $\epsilon/(2\ell)$ , each failing with probability at most $1/(4\ell)$ , give $|\widetilde Z-Z(\infty)|\le\epsilon Z(\infty)$ with probability at least $3/4$ for $\epsilon<1$ .

Significance

The result. The overlap bound is the hypothesis of the Wocjan–Abeyesinghe theorem (Theorem 9 of the paper) and is used in the proof of the paper's partition-function theorem (Theorem 11). It explains why a cooling schedule built for a classical estimator, with no reference to quantum states, is also good enough for quantum annealing-style state preparation. The paper remarks that, unlike the classical analysis of Štefankovič, Vempala and Vigoda, which needs the reverse divergence $\chi^2(\pi_i,\pi_{i+1})$ and a reversed schedule, the overlap is symmetric in $i$ and $i+1$ , so no reversal is needed.

Formalizing it. The result is proved on paper; nothing in it has been machine-checked. A formal development pins down the treatment of the endpoint $\beta_\ell=\infty$ , where $\pi_\ell$ is supported on the ground states and is no longer strictly positive, and records exactly which positivity conditions the divergence identities require. The definitions of Gibbs distributions, cooling schedules and $\chi^2$ on a finite space are reusable for other analyses of simulated annealing and of partition-function estimation.

Difficulty

The algebra at finite temperatures is a direct computation. The step that needs care is the last one, $i=\ell-1$ : there $\beta_{i+1}=\infty$ , the weights $e^{-\infty\cdot H(x)}$ are indicator values, $2\beta_{i+1}-\beta_i$ is again $\infty$ , and the divergence identity must hold with $\pi_{i+1}$ vanishing on every configuration of positive energy. A formalization that replaces $\infty$ by a large finite inverse temperature, or that requires both distributions to be strictly positive, does not cover this step. The second point is the passage from a bound on the divergence to a bound on an inner product of quantum states, which must handle the configurations where $\nu(x)=0$ .

Formalization scope

Inverse temperatures are elements of $[0,\infty]$ (ℝ≥0∞); the Boltzmann weight branches on $\beta=\infty$ . The differences $\beta_{i+1}-\beta_i$ and $2\beta_{i+1}-\beta_i$ are truncated subtractions in $[0,\infty]$ , exact on a cooling schedule. A schedule is a map $\mathbb N\to[0,\infty]$ of which only $\beta_0,\dots,\beta_\ell$ matter, and "for all $i$ " ranges over $i=0,\dots,\ell-1$ . $H$ takes values in $\mathbb N$ with $H\le n$ . Quantum samples are vectors of EuclideanSpace ℂ Ω with real amplitudes, and $|\langle\cdot|\cdot\rangle|^2$ is the squared norm of the complex inner product.

Added hypotheses, all disclosed in the statements: some configuration has $H(x)=0$ , so that $Z(\infty)>0$ (without it $\pi_\ell$ and the last ratio of Definition 1 are divisions by zero, which Lean evaluates to $0$ ); the general divergence statements assume $\pi(x)>0$ , which the paper's displays use implicitly by dividing by $\pi(x)$ . No hypothesis is placed on $B$ . In the accuracy companion, the per-ratio guarantee is stated as a bound on the failure probability; neither measurability nor independence is assumed.

A goal that assumes $\chi^2(\pi_{i+1},\pi_i)\le B-1$ , assumes $B>0$ in a way that excludes the endpoint, or drops the step $\beta_\ell=\infty$ would be a different, weaker statement; the goal's only hypothesis on the schedule is Definition 1.

Not formalized: the quantum walk algorithms, the Wocjan–Abeyesinghe theorems (Theorems 9 and 10), the sample and step counts of Theorems 8 and 11 (stated in $O(\cdot)$ notation), and the existence of short Chebyshev cooling schedules.

Contributions welcome: proofs of the milestones and of the companions, and lemmas on Gibbs distributions at $\beta=\infty$ that the companions share.

Selected references

A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471:20150301, 2015; cited here as the preprint arXiv:1504.06987v3, 2017. https://arxiv.org/abs/1504.06987
D. Štefankovič, S. Vempala, E. Vigoda, Adaptive simulated annealing: a new connection between sampling and counting, J. ACM 56(3):18, 2009. https://arxiv.org/abs/cs/0612058
P. Wocjan, A. Abeyesinghe, Speedup via quantum sampling, Phys. Rev. A 78:042336, 2008. https://arxiv.org/abs/0804.4259
P. Wocjan, C.-F. Chang, D. Nagaj, A. Abeyesinghe, Quantum algorithm for approximating partition functions, Phys. Rev. A 80:022340, 2009. https://arxiv.org/abs/0811.0596
M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004, 32–41. https://arxiv.org/abs/quant-ph/0401053

6 thms3 active usersReviewed

Completed

Machine Learning Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low IV: ℓ1-Regularized Best Subset Selection Satisfies Slow-Rate and Fast-Rate Oracle InequalitiesResearch Paper

Why shrink a best subset?

Best subset selection fits a linear predictor using at most $k$ of $p$ available columns. Its explicit limit on the number of selected variables makes the model easy to interpret, but the search can still fit noise: among many subsets of the same size, one can align unusually well with a noisy response. Mazumder, Radchenko and Dedieu study this effect in Subset Selection with Shrinkage. They add a penalty on the size of the selected coefficients and show how this changes prediction error when the signal-to-noise ratio is low.

An $\ell_1$ penalty is familiar from the Lasso. The estimator here also keeps the subset-size constraint, so its comparison class and its tuning parameter have a different role from those in an unconstrained Lasso. The paper's Theorem 3 gives three deterministic error bounds for this estimator, each valid on a specified event of the Gaussian noise. These bounds are the target of this mission. The separate probability estimates for the events are Theorem 1 of the paper and belong to another mission in this series.

Setting

Let $X\in\mathbb R^{n\times p}$ be a fixed design matrix whose columns have Euclidean norm one. The observation is $y=f^*+\epsilon$ , where $f^*\in\mathbb R^n$ is a fixed mean and the coordinates of $\epsilon$ are independent $N(0,\sigma^2)$ random variables, with $\sigma>0$ . The result below fixes one realized noise vector $\epsilon$ and assumes it lies in an event stated below. No assumption that $f^*$ is itself a linear combination of columns of $X$ is required.

For $1\le k\le p$ , write $B_0(k)=\{\beta\in\mathbb R^p:\|\beta\|_0\le k\}$ , where $\|\beta\|_0$ counts nonzero coordinates. An $\ell_1$ -regularized best subset estimator is any minimizer

\hat\beta_1\in\operatorname*{argmin}_{\beta\in B_0(k)}\bigl\{\|y-X\beta\|_2^2+\lambda\|\beta\|_1\bigr\}.\tag{16}

The objective has no factor $1/2$ . The assertion applies to every minimizer, so tied solutions are covered. The sparse minimum singular value is $\gamma_s=\inf\{\|Xu\|_2/\|u\|_2:u\ne0,\ \|u\|_0\le s\}$ . When $p\ge1$ and $s\ge1$ its domain is nonempty. Write $u_1^\sharp,\ldots,u_p^\sharp$ for the decreasing rearrangement of $|u_1|,\ldots,|u_p|$ .

The paper defines three noise events used here. $\mathcal H$ bounds the largest coordinate of $X^\top\epsilon$ by $\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}$ . On $\mathcal F$ , every $u\in\mathbb R^p$ satisfies

\epsilon^\top Xu\le(4+\sqrt2)\sigma\max\left\{\sum_{j=1}^{p}u_j^\sharp\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|_2\right\}.

On $\mathcal G_s$ , every $u\in B_0(s)$ satisfies $\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|_2$ . Here $\delta_0\in(0,1]$ and all logarithms are natural. These definitions, including the constant in $\mathcal G_s$ , are the printed deterministic events of p. 13.

Formalization targets

Exact slow rate on $\mathcal H$

At $\lambda=2\sigma\sqrt{2\log(2p)}+2\sigma\sqrt{2\log(1/\delta_0)}$ , Theorem 3(A) states

\|f^*-X\hat\beta_1\|_2^2\le\inf_{\beta\in B_0(k)}\bigl[\|f^*-X\beta\|_2^2+2\lambda\|\beta\|_1\bigr]\qquad(\epsilon\in\mathcal H).

Slow rate on $\mathcal F$

For $\lambda\ge(8+2\sqrt2)\sigma\sqrt{\log(2p)}$ , a positive universal constant $C_A$ gives

\|f^*-X\hat\beta_1\|_2^2\le C_A\left[\inf_{\beta\in B_0(k)}\bigl(\|f^*-X\beta\|_2^2+\lambda\|\beta\|_1\bigr)+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal F).

Fast rate on $\mathcal G_{2k}$

For every $\lambda\ge0$ , a positive universal constant $C_B$ gives

\|f^*-X\hat\beta_1\|_2^2\le C_B\left[\inf_{\beta\in B_0(k)}\|f^*-X\beta\|_2^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2 k+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal G_{2k}).

The $k$ multiplying $\gamma_{2k}^{-2}\lambda^2$ distinguishes this rate from the $\ell_2$ -penalized estimator's bound. The three claims together, with their separate tuning conditions, are Theorem 3 on p. 16. The milestones follow the displays of its proof in Supplement B.6, pp. 42–43.

What the result provides

Each inequality compares the prediction of any selected minimizer with that of every sparse competitor. The first bound has an exact leading constant and no additive noise term on $\mathcal H$ . The second keeps a linear penalty term when $\lambda$ meets a fixed noise-dependent threshold. The third replaces the linear term with a quadratic $\lambda$ term controlled by the sparse minimum singular value. This distinguishes regimes in which coefficient shrinkage changes the error rate. The paper also combines deterministic bounds with event probabilities in subsequent corollaries; those probability statements are separate from this goal.

The paper proves Theorem 3. The formalization task is to verify its model definitions, event interpretation and all three inequalities in Lean, with the same constants and quantifiers. The milestone statements isolate the basic inequality, the $\mathcal H$ bound, the rearranged-coordinate bound, the $\mathcal F$ case split and the sparse $\ell_1$ step. A complete proof would also provide reusable finite-dimensional norm and matrix estimates. This mission does not include the paper's numerical experiments, data-driven model-size selection, the $\ell_2$ -penalized estimator, or the event-probability theorem.

Difficulty

The constraint $\|\beta\|_0\le k$ makes the estimator a minimizer over a nonconvex set. A standard unconstrained Lasso argument does not directly supply the paper's bound for every feasible sparse comparator. The slow rates rely on two different noise controls: a coordinatewise bound on $\mathcal H$ and a maximum of a sorted-coordinate term and a prediction-norm term on $\mathcal F$ . The fast rate also needs the sparse minimum singular value to relate coefficient error to prediction error. The constants in these steps matter: replacing the exact first tuning equality or dropping the factor $k$ in the fast rate would state a different theorem.

Formalization scope

Lean uses Fin n → ℝ and Fin p → ℝ for vectors and Matrix (Fin n) (Fin p) ℝ for $X$ . Norms are explicit finite sums, rather than the function type's default supremum norm. The paper's one-based sorted index $j$ is j.val + 1; the sum using $u^\sharp$ is encoded as a maximum over coordinate permutations, which agrees with the decreasing rearrangement. The events are predicates on realized noise vectors. The Gaussian law explains the model but is not needed in these deterministic statements. The estimator is an argmin predicate, never a chosen minimizer.

The universal constants precede all dimensions and data in the Lean goal. The infima in the three displayed bounds are expressed as inequalities for every $\beta\in B_0(k)$ , avoiding the default value of an empty or unbounded real infimum. The standing conditions are $1\le k\le p$ , unit-norm columns, $\sigma>0$ and $0<\delta_0\le1$ . The first slow-rate branch retains the paper's equality for $\lambda$ . The fast branch additionally requires $\gamma_{2k}>0$ or $\lambda=0$ : this makes the $\lambda^2/\gamma_{2k}^2$ term meaningful under Lean's total division, which returns zero at a zero denominator. The displayed events use the paper's original $\mathcal G_s$ constant; this mission makes only a deterministic claim on that event.

The sparse domain for $\gamma_{2k}$ is nonempty under these conditions. All square-root radicands and logarithm arguments in the target are in their intended ranges. The formalization must rule out a universal constant that depends on $n$ , $p$ , $k$ , $X$ or $\lambda$ , and must apply to every minimizer. Contributions to the shared norm inequalities, rearrangement identity and matrix calculations are useful beyond this theorem.

Selected references

Rahul Mazumder, Peter Radchenko and Antoine Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research 71 (2023), arXiv preprint version 4 (2022), arXiv:1708.03288v4. This mission cites the preprint's page and theorem numbering.

9 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement? III: When Payment Postponement Helps or Hurts the Retailer, the Supplier and the ConsumersResearch Paper

Why payment timing matters

A retailer can pay a supplier when it places an order or after the supplier delivers it. When production yield is uncertain, the choice changes who bears the cost of missing units. It can also change the supplier's production decision and, through the amount available for sale, the surplus received by consumers. Geng, Guo, Xiao and Yang study these effects in a decentralized supply chain and show that payment postponement can help all three parties, hurt all three, or benefit some while hurting others, depending on production cost and the retailer's pricing rule. Their Proposition 4 gives the precise cost intervals for these outcomes in the SSRN author version, pp. 19–20.

The result matters to contract design in supply chains where realized output can be below planned production. Paying for units ordered and paying for units delivered allocate that shortage differently. A comparison based only on the retailer's expected profit would miss the effects on the upstream supplier and final consumers. Proposition 4 keeps all three outcomes visible while holding the retailer's pricing policy fixed.

The supply-chain game

There is one supplier and one retailer. The supplier chooses a wholesale price $w$ and plans production $Q$ at cost $cQ$ . The retailer orders $q$ and sells to a market with linear demand $d(p)=a-bp$ , where $a,b>0$ and $p$ is the retail price. The yield factor $Y$ equals $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$ , with $0<\alpha,\theta<1$ . Thus $\mu=\mathbb E Y=\alpha(1-\theta)+\theta$ . The retailer receives $\widehat q=\min\{YQ,q\}$ units; the production cost applies to planned $Q$ , including units lost to yield risk §3.1–3.2.

Under pay-by-order, the retailer transfers $wq$ to the supplier and the supplier produces $Q=q$ . Under pay-by-delivery, the transfer is $w\widehat q$ and the supplier can choose a larger production quantity. Under ex ante pricing, the retailer fixes $p$ before yield is known. Under responsive pricing, the retailer sets $p$ after observing delivery. Combining payment and pricing gives OA (order, ex ante), OR (order, responsive), DA (delivery, ex ante), and DR (delivery, responsive). The supplier first sets $w$ , the retailer next orders and possibly fixes a price, the supplier chooses production, yield is realized, and responsive pricing occurs last Table 1, p. 9.

Both firms maximize expected profit at every stage. A subgame-perfect equilibrium is a complete plan of choices after every history in which each choice is optimal at that history. For scenario $k$ , write $\pi_R^k$ and $\pi_S^k$ for equilibrium retailer and supplier profit. The consumer surplus $CS^k$ is expected surplus from sales: for delivered stock $X$ and market price $p$ , the model integrates inverse demand less $p$ from zero to $\min\{d(p),X\}$ . This is the paper's priority allocation convention for consumers with the highest willingness to pay p. 10.

Formalization targets

The main target is Proposition 4, which compares OA with DA and OR with DR. Let $\Delta(\pi_R,\pi_S,CS)$ mean the delivery-payment outcome minus its order-payment counterpart. A plus sign below means a strict increase, a minus sign a strict decrease, and zero equality. The admissible cost range is $0<c<a\mu/b$ .

For ex ante pricing, with no restriction $\alpha\ge9/16$ , the paper gives a threshold $0<\overline C<c^{DA}$ and the following pattern:

\begin{array}{c|c} \text{cost interval}&\operatorname{sign}\Delta(\pi_R,\pi_S,CS)\\ (\max\{0,c^{OA}_2\},\max\{\overline C,c^{OA}_2\}) &(+,+,+)\\ (\max\{\overline C,c^{OA}_2\},c^{DA}) &(+,+,-)\\ (0,\max\{0,c^{OA}_1\})\text{ or }(c^{DA},a\mu/b)&(0,0,0). \end{array}

For responsive pricing, assuming $\alpha\ge9/16$ , the pattern is $(+,+,+)$ on $(0,\widetilde C)$ , $(-,-,-)$ on $(\widetilde C,c^{DR}_1)$ , $(+,-,+)$ on $(c^{DR}_1,c^{DR}_2)$ , and $(0,0,0)$ on $(c^{DR}_2,a\mu/b)$ . The thresholds are those specified in the paper: $\widetilde C$ is equation (6), $\overline C$ is equation (8), and the scenario cost thresholds come from Appendix B. The first ex ante interval can be empty for some parameters; its printed endpoints are retained. The milestones establish the supplier's production and responsive pricing rules, the four scenario outcomes, and the threshold ordering used in the comparison Appendices B–C.

What the result provides

The theorem separates the effect of changing the payment contract from the effect of changing the pricing rule. For advance pricing it identifies an interval where payment postponement helps both firms and consumers, then an interval where consumers lose despite both firms gaining. For responsive pricing the direction of every effect can reverse as cost passes successive thresholds. At high cost the change in payment timing leaves all three equilibrium outcomes unchanged Proposition 4, pp. 19–20.

The paper derives the equilibrium formulas in Appendix B and proves the comparisons in Appendix C. The result is therefore a known mathematical claim, while this mission asks for a machine-checked development from the sequential game through the cost-dependent equilibrium outcomes and final comparisons. The definitions of a two-point yield game and its complete contingent strategies can support other formal studies of payment or pricing postponement. There is no claim that Proposition 4 already has a machine-checked proof.

Where the formal work is difficult

The supplier's production payoff has kinks at $Q=q$ and $Q=q/\alpha$ . The retailer's best order changes when those production choices change, and responsive pricing adds another kink when delivered stock crosses $a/2$ . As wholesale price varies, the supplier must compare outcomes on both sides of these changes. Consequently a single first-order condition for a smooth objective does not characterize the equilibrium. The cost thresholds also depend on square roots and comparisons among several formula pieces, including the larger root chosen for $c^{OA}_2$ Appendix B, pp. 33–37.

Formalization scope

Lean represents expectation by the two weighted yield outcomes. Production cost $c$ is a separate argument, so thresholds depend only on $(a,b,\alpha,\theta)$ . Parameters satisfy $a,b>0$ , $0<\alpha,\theta<1$ , and $0<c<a\mu/b$ . Wholesale and retail prices obey the strict admissibility bounds of equation (3). Orders are nonnegative; pay-by-delivery production is nonnegative; pay-by-order production equals the order. Consumer surplus is a real interval integral. Every comparison quantifies over actual subgame-perfect equilibria, and the goal separately asserts that the compared equilibria exist at every admissible cost. Equilibrium profits are computed from strategies and transfers, rather than defined to equal the Appendix B formulas.

The paper's statements require care at ties. The model selects $Q=q$ when that is a profit-maximizing pay-by-delivery production choice, including the indifferent DR regime. The printed middle DR consumer-surplus expression combines outcomes from different production choices; the equilibrium-consistent expression is used here, and Proposition 4(R)'s comparison remains valid under either expression. Equation (2) swaps the scenario labels of committed and responsive prices, so consumer surplus uses the actual ex ante price in OA and DA and the price after delivery in OR and DR. The printed $[x]^+$ in Appendix B.1 is read as $\max\{0,x\}$ , as in Lemma 1. Outcome claims use open cost intervals because uniqueness at exact thresholds fails; equilibrium existence remains part of the targets there. The threshold $c^{OA}_2$ is the larger root of the relevant quadratic factor, and $\overline C$ and $\widetilde C$ use the paper's explicit formulas. These conventions are recorded in the local moderation notes.

The development calls for real inequality reasoning, optimization of piecewise objectives, and careful handling of interval integrals. Contributions that prove the production and price best responses, establish the four equilibrium lemmas, or verify the threshold order each advance the final comparison.

Selected references

X. Geng, X. Guo, G. Xiao and N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. SSRN author version 3546872; DOI: 10.1287/msom.2022.0198.

12 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement? II: Under Reliable Yield the Postponements Are Complements Only at Intermediate CostResearch Paper

Motivation

A retailer that buys from a supplier with unreliable production has two contractual levers against supply risk, and both postpone a decision until after the yield is known. Payment postponement means paying only for the units actually delivered (pay-by-delivery) instead of the units ordered (pay-by-order). This moves the yield risk upstream. Pricing postponement means setting the retail price after the delivery is observed (responsive pricing) instead of committing to it in advance (ex ante pricing). This moves the risk downstream to consumers. Both practices are common in procurement, and the natural intuition is that two ways of shedding the same risk should be substitutes: once one lever is in use, the other should be worth less.

Geng, Guo, Xiao and Yang (MSOM 25(3), 2023; author version SSRN 3546872) compute the subgame-perfect equilibria of all four combinations of the two levers in a stylized supplier–retailer game. Their Proposition 3 shows that the intuition fails at intermediate production cost. When full yield is likely and yield loss is mild, the two postponements are complements there: postponing payment is worth more when pricing is also postponed. This mission formalizes that result together with the four equilibrium characterizations it rests on.

Setting

A supplier sells one product to a retailer, who sells it in a market with linear demand $d(p)=a-bp$ , $a,b>0$ . The supplier plans production $Q$ at unit cost $c$ and realizes the fraction $Y$ of it, where

Y=1 \text{ with probability } \theta,\qquad Y=\alpha \text{ with probability } 1-\theta,\qquad 0<\alpha,\theta<1,

and $\mu=\alpha(1-\theta)+\theta$ is the mean yield. The retailer orders $q$ and receives $\hat q=\min\{YQ,q\}$ .

The four scenarios are OA, OR, DA and DR. The first letter is the payment rule: by order (O, the transfer is $wq$ ) or by delivery (D, the transfer is $w\hat q$ ). The second letter is the pricing rule: ex ante (A, the price is fixed before the yield) or responsive (R, the price is set after $\hat q$ is observed). Each scenario is a sequential game. The supplier posts a wholesale price $w$ . The retailer orders $q$ , and also commits to a price $p$ in the ex ante scenarios. The supplier then chooses $Q$ ; under pay-by-order it produces exactly $q$ . The yield realizes, and under responsive pricing the retailer then sets $p$ . The retailer earns $p\min\{d(p),\hat q\}$ minus the transfer, and the supplier earns the transfer minus $cQ$ . Both are risk neutral. Admissible actions follow the paper's standing ranges: $0<c<a\mu/b$ , $0<p<a/b$ , and $w$ between $c$ (or $c/\mu$ under pay-by-delivery) and $a/b$ .

Write $\pi^k_R$ for the retailer's expected profit in a subgame-perfect equilibrium of scenario $k$ . The paper's Definition 1 measures the interaction of the two postponements by

V=\big(\pi^{DR}_R-\pi^{OR}_R\big)-\big(\pi^{DA}_R-\pi^{OA}_R\big):

the value of payment postponement under responsive pricing, minus its value under ex ante pricing. The postponements are substitutes if $V<0$ and complements if $V>0$ .

The parameter region of the result is $\alpha\ge 9/16$ together with $\mathcal H_3=\{\theta_2(\alpha)<\theta<1\}$ , where $\theta_2(\alpha)$ is the largest real root of the cubic $-\alpha^3+\alpha^2(5+\alpha)x+(16-19\alpha-6\alpha^2)x^2-25(1-\alpha)x^3$ . The cost thresholds $c^{DR}_1<c^{DR}_2$ (scenario DR) and $c^{DA}$ (scenario DA) are explicit algebraic functions of $(a,b,\alpha,\theta)$ given in the paper's Appendix B.

Formalization targets

Goal: Proposition 3

For $\alpha\ge9/16$ and $(\alpha,\theta)\in\mathcal H_3$ , every scenario has an equilibrium at every cost $0<c<a\mu/b$ , and there is a cost $0<\hat C<a\mu/b$ such that, at every choice of the four equilibria,

V<0 \text{ on } (0,c^{DR}_1)\cup(\hat C,c^{DA}),\qquad V>0 \text{ on } (c^{DR}_1,\hat C),\qquad V=0 \text{ on } (c^{DA},a\mu/b).

$\hat C$ is existential, as in the paper, and depends only on the parameters.

Milestones

the supplier's production response (4) under pay-by-delivery and the ex post price (5);
Lemmas 1–4: existence of the equilibrium of each scenario, and its outcome $(\pi_R,\pi_S,CS)$ in closed form on each cost interval;
Lemma 1(i): on $\mathcal H_3$ the threshold $c^{OA}_2$ is nonpositive, so scenario OA has one regime;
the threshold claims of Appendix C: $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$ for $\alpha\ge9/16$ .

Significance

The result separates the first-order question (which lever the retailer prefers, the subject of the paper's Proposition 2) from the second-order one (whether one lever raises the value of the other). It shows that two risk-shifting instruments can reinforce each other. On $(c^{DR}_1,\hat C)$ , adopting one postponement raises the value of the other. So whenever the retailer gains from adopting either lever alone, it gains even more from adopting both. Below $c^{DR}_1$ and above $\hat C$ the reverse holds. Above $c^{DA}$ , payment postponement is irrelevant, because the supplier never inflates production there.

The paper proves Lemmas 1–4 by backward induction in Appendix B and the proposition by comparing closed forms in Appendix C. None of it is machine-checked. A formal proof requires the four backward inductions with every kink and tie handled, and the polynomial inequalities between the thresholds over the parameter region. The formalization also corrects the record: the paper's explicit formula (7) for $\hat C$ does not locate the sign change of $V$ (at $(\alpha,\theta)=(0.6,0.75)$ it exceeds $c^{DA}$ ), while the existential statement of Proposition 3 holds at every sampled point.

Difficulty

Once Lemmas 1–4 are available, $V$ is a difference of explicit piecewise functions of $c$ . The difficulty lies in those lemmas and in the thresholds. Each lemma is a three-stage optimization. The supplier's profit is piecewise linear in $Q$ , with kinks at $q$ and $q/\alpha$ . The retailer's profit is piecewise in $(q,p)$ , with kinks where it becomes worth inflating the order. The supplier's value function in $w$ is piecewise quadratic, and its maximum can sit at a kink. In scenario DR it sits exactly at the price where the supplier is indifferent to inflating production. A naive reading of the paper's tie rule removes the equilibrium there altogether. On the middle DR interval the sign of $V$ changes inside the interval, at a root of a polynomial with nested square roots. On the other pieces, the signs of $V$ and the ordering $c^{DR}_1<c^{DR}_2<c^{DA}$ are polynomial inequalities in $(\alpha,\theta)$ , with $\theta_2(\alpha)$ defined implicitly as a cubic root.

Formalization scope

Parameters and cost. The parameters $(a,b,\alpha,\theta)$ form a structure. The cost $c$ is a separate argument, and every threshold depends on the parameters only.
Expectation. The expectation over the yield is the explicit two-point sum $\theta f(1)+(1-\theta)f(\alpha)$ .
Equilibrium. Strategies are functions of all earlier moves, and optimality is required at every node over the full admissible action sets.
Production ties. Under pay-by-delivery the supplier's production is a best response. When producing exactly $q$ is optimal, it produces $q$ . The paper's display (4) assigns that tie to inflation, but under that rule scenario DR has no equilibrium for intermediate cost. The convention reproduces the paper's DR profits.
Consumer surplus. It is the integral $\int_0^{\min\{d(p),\hat q\}}(p(t)-p)\,dt$ . It uses the ex post price in the responsive scenarios and the committed price in the ex ante ones; the labels of the paper's display (2) are swapped.
Closed forms. Two printed consumer-surplus values are corrected to the equilibrium values: the middle piece of OA ( $8b\alpha^2$ for $8b\alpha^3$ ) and the middle piece of DR (one factor $\alpha^2(1-\theta)+\theta$ fewer).
Cost intervals. Every statement is on open cost intervals, because at a threshold the outcome is not unique.
Thresholds. $c^{OA}_2$ , "the second root" of a quartic, is the larger root of the quadratic factor that defines it. $\theta_2$ is the supremum of the cubic's real roots, a finite nonempty set.

The equilibrium profits are outcomes of the equilibrium predicate. They are never defined by their closed forms, and the goal carries the existence of an equilibrium in each scenario. Without that, the comparison would be vacuous whenever the predicate is unsatisfiable.

Every object is elementary: real arithmetic, square roots, min/max, one interval integral and one sSup. The equilibrium predicate and the four lemmas are shared with the three companion missions of this paper (Propositions 2, 4 and 5). Proofs of the lemmas, of the threshold inequalities and of the goal are all welcome.

Selected references

X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. https://doi.org/10.1287/msom.2022.0198 ; author version SSRN 3546872, https://ssrn.com/abstract=3546872

13 thms3 active usersReviewed

Completed

Economics Information Theory Operations Research·Captain: mikedeng1

Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations II: Machine Input Never Lowers the Decision-Maker's Accuracy or Expected ValueResearch Paper

Motivation

Machine-learning systems are increasingly placed beside human experts — physicians reading scans, loan officers screening applications, judges assessing risk — rather than replacing them. The machine processes the structured data it can see; the human also has access to information the algorithm cannot observe, but her attention is limited. Whether such a partnership improves the decision is a question about how the human reallocates scarce cognitive effort once part of the information is handed to her for free.

Boyacı, Canyakmaz and de Véricourt (ESMT Working Paper 20-02, 2020; published in Management Science, 2024) model the human as a rationally inattentive decision-maker in the sense of Sims (2003): she chooses how much information to process, and pays a cost proportional to the mutual information between the state and her decision. In the binary-choice setting, Matějka and McKay (2015) showed that such problems reduce to choosing conditional choice probabilities, with logit-form solutions. The paper uses this reduction to compare a decision-maker who decides alone with one who first sees a machine's assessment. This mission formalizes its first comparison, Proposition 1: the machine never lowers the decision-maker's accuracy or her expected value.

Setting

A decision-maker (DM) must announce whether the state of the world $\omega\in\{g,b\}$ is good ( $a=y$ ) or bad ( $a=n$ ). A correct choice pays $1$ , an incorrect one $0$ . Her prior that the state is good is $\mu\in[0,1]$ , and $\lambda\ge0$ is the information cost.

A strategy is a pair $(p_g,p_b)\in[0,1]^2$ of conditional probabilities of choosing $y$ in state $g$ and in state $b$ . It induces the choice probability $p=\mu p_g+(1-\mu)p_b$ , the accuracy $A=\mu p_g+(1-\mu)(1-p_b)$ , the cognitive cost

C=\lambda\big[H(p)-(1-\mu)H(p_b)-\mu H(p_g)\big],\qquad H(x)=-x\log x-(1-x)\log(1-x),

(the mutual information between state and action, in nats) and the expected value $V=A-C$ . The DM maximizes $V$ . The optimal accuracy $A^\star(\mu)$ and optimal value $V^\star(\mu)$ are the accuracy and value at a maximizer. Two thresholds organize the solution:

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

The machine. Information is aggregated into two binary variables: $X_1$ , which the machine and the DM can both evaluate, and $X_2$ , which only the DM can assess. Realizations are $x_1,x_2\in\{-,+\}$ and the state is good iff $x_1=x_2=+$ . The DM's prior on $(X_1,X_2)$ is $\pi$ , with $\pi(x_1,x_2)>0$ for all four realizations, so $\mu=\pi(+,+)$ . The machine reveals $x_1$ at no cost; the DM updates by Bayes' rule to $\mu^x=P(\omega=g\mid X_1=x)$ and then solves her problem with prior $\mu^x$ . The machine-assisted accuracy and value are the ex-ante expectations

A^\star_m=\sum_{x}P(X_1=x)\,A^\star(\mu^x),\qquad V^\star_m=\sum_{x}P(X_1=x)\,V^\star(\mu^x).

Formalization targets

Goal: Proposition 1

For every $\lambda\ge0$ and every prior $\pi$ with positive entries,

A^\star_m\ge A^\star(\mu)\qquad\text{and}\qquad V^\star_m\ge V^\star(\mu).

Milestones

Equation (3). $\mu^-=0$ and $\mu^+=\mu/(\mu+\pi(+,-))>\mu$ .
Corollary 2, (13). For $\lambda>0$ : $A^\star(\mu)=1-\mu$ on $[0,\underline\mu]$ , $e^{1/\lambda}/(e^{1/\lambda}+1)$ on $(\underline\mu,\bar\mu)$ , and $\mu$ on $[\bar\mu,1]$ .
Corollary 2, (15). For $\lambda>0$ : $V^\star(\mu)=1-\mu$ on $[0,\underline\mu]$ , $\lambda[\log(e^{1/\lambda}+1)-H(\mu)]$ on $(\underline\mu,\bar\mu)$ , and $\mu$ on $[\bar\mu,1]$ .
Lemma 2 (accuracy and value). $A^\star_m=1-\mu/\mu^++(\mu/\mu^+)A^\star(\mu^+)$ , and the same identity for $V^\star_m$ .
Convexity of $A^\star$ on $[0,1]$ (proof of Proposition 1).
Slopes at the thresholds. The middle branch of (15) has derivative $-1$ at $\underline\mu$ and $1$ at $\bar\mu$ .
Convexity of $V^\star$ on $[0,1]$ .

Significance

The result. Proposition 1 is the baseline against which the paper's other findings are measured: although accuracy and value always improve, the machine can lower the probability of choosing the good state, raise false positives, and increase the DM's cognitive effort (Theorems 2–4 of the paper). Without Proposition 1 those effects would not be separable from a simple loss of decision quality. The closed forms (13) and (15) also show that, where the DM processes information, her accuracy depends on $\lambda$ alone and not on her prior.

Formalizing it. The proposition and its milestones are proved in the paper, in Appendix A, and the closed forms rely on the logit characterization of the optimum. None of this is machine-checked. A complete development produces a verified closed-form solution of the binary rational-inattention problem with entropy cost, with accuracy and value as explicit functions of the prior, and a verified value-of-information inequality for that problem. Both are reusable by the other four missions of this series and by any binary rational-inattention model.

Difficulty

The obvious argument — more information cannot hurt — is not available off the shelf: the DM is not a Bayesian with free information but optimizes an entropy-penalized program, and the comparison is between optimal values of two such programs at different priors. $A^\star$ and $V^\star$ are values at an optimum of a non-linear program over $[0,1]^2$ . Their closed forms require identifying exactly when the corner solutions $p_g=p_b=0$ and $p_g=p_b=1$ are optimal and handling the degenerate priors $\mu=0,1$ , where the maximizer is not unique. Both functions are piecewise in $\mu$ , so their shape on $[0,1]$ does not follow from the shape of each piece: the behaviour at the kinks $\underline\mu$ and $\bar\mu$ decides it. Accuracy is a component of the objective, not the objective itself, so statements about $A^\star$ do not follow from optimality alone.

Formalization scope

Decision problem. The paper's general information-processing problem (2) is not formalized. The DM chooses $(p_g,p_b)\in[0,1]^2$ directly — the paper's own §4 reduction (Matějka & McKay 2015), not a restriction. $H$ is Mathlib's Real.binEntropy (natural logarithm); $\lambda$ is lam.
Starred metrics. $A^\star$ and $V^\star$ are accuracy and value at a chosen maximizer (Classical.epsilon); every maximizer yields the same values. They are defined for every real $\mu$ and used on $[0,1]$ .
Machine. $\{-,+\}$ is Bool with true $=+$ ; the prior is π : Bool → Bool → ℝ with positive entries summing to $1$ . Posteriors are defined by Bayes' rule; $A^\star_m$ , $V^\star_m$ are expectations over $x_1$ .
Parameters. The goal keeps the printed $\lambda\ge0$ (at $\lambda=0$ the cost vanishes); all milestones assume the model's standing $\lambda>0$ , needed for $1/\lambda$ . The paper's parameter set $\mathcal S=\{(\mu,\mu^+)\in[0,1]^2:\mu<\mu^+\}$ is replaced by priors with positive entries, which realize exactly $0<\mu<\mu^+<1$ .
Ruled out. Defining $A^\star$ , $V^\star$ by the closed forms (13), (15); defining $A^\star_m$ , $V^\star_m$ by the right-hand sides of Lemma 2; or assuming convexity as a hypothesis — each makes the corresponding statement true by definition, and none of them is used here.
Infrastructure. Calculus of Real.binEntropy (derivative, concavity) is in Mathlib. Needed: existence of a maximizer on the square, the first-order characterization of the interior optimum, and convexity of piecewise functions glued with matching slopes. Contributions of general lemmas on these points are welcome.

Selected references

T. Boyacı, Y. Canyakmaz, F. de Véricourt, Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations, ESMT Working Paper 20-02, 2020; Management Science 70(2), 2024. https://doi.org/10.1287/mnsc.2023.4744
F. Matějka, A. McKay, Rational Inattention to Discrete Choices: A New Foundation for the Multinomial Logit Model, American Economic Review 105(1), 2015. https://doi.org/10.1257/aer.20130047
C. A. Sims, Implications of Rational Inattention, Journal of Monetary Economics 50(3), 2003. https://doi.org/10.1016/S0304-3932(03)00029-1
T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006. https://doi.org/10.1002/047174882X

11 thms3 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement? I: As Cost Rises the Retailer Prefers Payment, Then Pricing, Then Both, Then Pricing PostponementResearch Paper

Motivation

When a supplier's production is subject to random yield, only part of a planned production run turns into usable output. A retailer sourcing from such a supplier bears the resulting shortage risk unless the contract or the selling strategy moves it elsewhere. Random yield is a classical topic in production planning (Yano and Lee, 1995), and postponing a decision until uncertainty resolves is a classical risk-mitigation tool (Van Mieghem and Dada, 1999).

Geng, Guo, Xiao and Yang study two postponements available to a retailer facing an unreliable supplier. Payment postponement replaces payment for the ordered quantity by payment for the delivered quantity, which shifts the yield risk to the supplier. Pricing postponement (responsive pricing) sets the retail price after the delivery is known, which shifts the risk to consumers. Their Proposition 2 answers which of the four combinations the retailer prefers, as a function of the production cost, when the yield loss is not too severe. This mission formalizes that proposition and the equilibrium results it rests on.

Setting

A supplier sells to a retailer, who sells to a market with linear demand $d(p)=a-bp$ , $a,b>0$ . The supplier's yield factor $Y$ takes the value $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$ , with $\alpha,\theta\in(0,1)$ , and has mean $\mu=\alpha(1-\theta)+\theta$ . The supplier plans production $Q$ , pays $c$ per planned unit, and delivers $\hat q=\min\{YQ,q\}$ against an order $q$ . Throughout, $0<c<a\mu/b$ .

There are four scenarios, written $k\in\{OA,OR,DA,DR\}$ :

O (pay-by-order): the retailer pays $wq$ , and the supplier produces exactly $Q=q$ ;
D (pay-by-delivery): the retailer pays $w\hat q$ , and the supplier chooses $Q$ and may inflate production above $q$ ;
A (ex ante pricing): the retailer commits to the retail price $p$ when it orders;
R (responsive pricing): the retailer sets $p$ after seeing $\hat q$ , maximizing $p\min\{d(p),\hat q\}$ .

Each scenario is a Stackelberg game. The supplier sets the wholesale price $w$ , the retailer orders (and, ex ante, prices), the supplier produces, the yield realizes, and under responsive pricing the retailer prices. Both firms are risk neutral. The solution concept is subgame-perfect equilibrium, and $\pi^k_R$ denotes the retailer's expected equilibrium profit in scenario $k$ . Admissible prices are those of the paper's standing assumption (3): $0<p<a/b$ , and $c<w<a/b$ under pay-by-order or $c/\mu<w<a/b$ under pay-by-delivery.

The cost thresholds of the comparison are

\tilde C=\frac{a\alpha\big(1-\sqrt{\alpha^2(1-\theta)+\theta}\big)}{b(1+\alpha)},\qquad c^{DR}_2=\frac{a\alpha\mu(1-\theta)}{b(\mu+\theta)},

c^{DR}_1=\frac{a\alpha(1-\theta)\big(\mu^2+\theta-2\theta\sqrt{\alpha\mu(1-\alpha)(1-\theta)}\big)}{b\big(\alpha^2(1-\theta)^3+4\alpha\theta(1-\theta)+\theta(1+\theta)^2\big)}.

Formalization targets

Goal: Proposition 2 (p. 16)

For $9/16\le\alpha<1$ and every $0<c<a\mu/b$ , equilibria of OR, DA and DR exist, and every choice of equilibria satisfies

\begin{aligned} &\pi^{OR}_R<\pi^{DR}_R=\pi^{DA}_R && 0<c<\tilde C,\\ &\pi^{DA}_R=\pi^{DR}_R<\pi^{OR}_R && \tilde C<c<c^{DR}_1,\\ &\pi^{DA}_R<\pi^{OR}_R<\pi^{DR}_R && c^{DR}_1<c<c^{DR}_2,\\ &\pi^{DA}_R<\pi^{DR}_R=\pi^{OR}_R && c^{DR}_2<c<a\mu/b. \end{aligned}

Milestones

(4): the supplier's production under pay-by-delivery is $q$ below the wholesale price $c/(\alpha(1-\theta))$ and $q/\alpha$ above it.
(5): the responsive price is $(a-\hat q)/b$ for $\hat q<a/2$ and $a/(2b)$ otherwise.
Lemmas 2, 3, 4: existence of equilibria of OR, DA and DR, and their outcomes $(\pi_R,\pi_S,CS)$ in closed form on each open cost interval (Lemma 4 for $\alpha\ge 9/16$ ).
Threshold order (proof of Propositions 1–2): for $\alpha\ge 9/16$ , $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$ .
Position of $\tilde C$ (proof of Proposition 4): for $\alpha\ge 9/16$ , $0<\tilde C<c^{DR}_1$ .

Significance

The proposition describes a preference cycle. Payment postponement (DA) is best when production is cheap, because the supplier then absorbs yield risk by inflating production. Pricing postponement (OR) is best at intermediate cost. Using both (DR) is strictly best on $(c^{DR}_1,c^{DR}_2)$ , where the two postponements are worth more together than either alone. Above $c^{DR}_2$ the supplier stops inflating, DR and OR coincide, and pricing postponement suffices. These are the paper's managerial conclusions on contract and pricing choice under supply risk, and the other three missions of the series (strategic complementarity, and the effect of each postponement on the whole chain) rest on the same equilibria.

The paper derives the four equilibria in its Appendix B and proves the propositions in Appendix C as direct comparisons of closed forms. None of this has been machine-checked. The mission produces a formal model of the four games and a verified link from the game to the closed forms. Lemmas 2–4 are reusable by every statement about this model.

Difficulty

Once the closed forms are known, the comparison is polynomial algebra in $(\alpha,\theta,c)$ with square roots. The work lies upstream. Each equilibrium requires a backward induction over piecewise-linear objectives in $Q$ and $q$ and piecewise-quadratic objectives in $p$ and $w$ . Optima occur at kinks such as the inflation threshold $w_0=c/(\alpha(1-\theta))$ , and the supplier's value function is discontinuous there, so the maximum can sit at a boundary rather than at the center of a piece. In scenario DR the equilibrium wholesale price on $(c^{DR}_1,c^{DR}_2)$ sits exactly at $w_0$ , where the supplier is indifferent among all productions in $[q,q/\alpha]$ , so existence depends on how that tie is resolved. Uniqueness of outcomes, which the comparison needs, holds only on open cost intervals, because at each threshold two wholesale prices tie with different outcomes. The threshold inequalities for $\alpha\ge 9/16$ are not visible from the formulas and need careful estimates of the radicals.

Formalization scope

Parameters are a structure $(a,b,\alpha,\theta)$ with validity predicate $a,b>0$ , $\alpha,\theta\in(0,1)$ ; the cost $c$ is a separate real argument. The expectation over $Y$ is the two-term sum $\theta f(1)+(1-\theta)f(\alpha)$ , with no measure theory. A strategy profile consists of a wholesale price and rules for production $Q(w,q)$ , the order $q(w)$ , the ex ante price $p(w)$ and the ex post price $p^{\mathrm r}(w,q,\hat q)$ . Equilibrium requires optimality at every admissible history over the admissible sets of (3). Consumer surplus is the integral $\int_0^{\min\{d(p),X\}}(p(t)-p)\,dt$ , evaluated at the ex post price under responsive pricing and at the committed price under ex ante pricing.

Conventions and disclosed departures from the page:

Tie rule. Under pay-by-delivery, when producing exactly $q$ is optimal, the supplier produces $q$ . Display (4) assigns the tie at $w_0$ to inflation, under which DR has no equilibrium on $(c^{DR}_1,c^{DR}_2)$ . Lemma 4's printed profits there are those of the convention.
$CS^{DR}$ on the middle piece is stated with denominator $8b\alpha^2(1-\theta)^2(\alpha^2(1-\theta)+\theta)$ ; the page prints the last factor squared, which is the surplus of no single equilibrium. Proposition 2 does not involve $CS$ .
Open intervals. Lemmas are stated on open cost intervals; at the thresholds outcomes are not unique.
$\tilde C$ is instantiated by (6), as Appendix C does; the page introduces it through Proposition 1's existential.
Display (2) prints the scenario labels of $CS$ swapped; the Appendix B reading is used.

$\pi^k_R$ is the retailer's profit along an equilibrium of the game, never its closed form; a formalization that defines the profits by the Appendix B formulas, or an equilibrium predicate that no profile satisfies, would make the goal trivial. The goal therefore also asserts existence of equilibria of the three scenarios.

Contributions welcome: proofs of the milestones; general lemmas on maximizing piecewise-linear and piecewise-quadratic functions with kinks; the threshold inequalities. Proposition 1 (OA versus the others) is not part of this mission.

Selected references

X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, SSRN 3546872 (author version), 2022; published in Manufacturing & Service Operations Management 25(3), 2023. https://ssrn.com/abstract=3546872, https://doi.org/10.1287/msom.2022.0198
C. A. Yano, H. L. Lee, Lot Sizing with Random Yields: A Review, Operations Research 43(2), 1995. https://doi.org/10.1287/opre.43.2.311
J. A. Van Mieghem, M. Dada, Price Versus Production Postponement: Capacity and Competition, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1631

15 thms3 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics C: Complete Single-Life Annuity Valuation, Payment Timing and RelationshipsTextbook

Complete Single-Life Annuity Valuation, Payment Timing and Relationships

Motivation

A life annuity pays instalments conditional on an annuitant surviving to specified instants. As discussed in Dickson, Hardy and Waters (2020), actuarial value depends on the exact timing of the payments. For a pension payable in arrears, the payment event is at the end of the period. A contractual guarantee can preserve payments for the estate after death, but only once the entitlement has commenced. Those conditions must be explicitly modelled before calculating actuarial factors.

Setting

Take a finite distribution over last survived anniversaries $K=0,\ldots,h$ with nonnegative probabilities $p_k$ summing to one. The final state is right-censored: it does not assert death at the terminal age. Define $S(t)=\sum_{k=t}^{h}p_k$ . A schedule has its first index $a$ , up to $n$ instalments, an amount $b_j$ for each instalment, and an annual discount factor $v$ with $0<v\le1$ . Advance instalments fall at $j$ and arrears instalments at $j+1$ .

The first $g$ scheduled instalments are guaranteed only when survival to commencement $a$ activates the annuity. They continue to the estate after death during that period. Later instalments depend on survival at their actual payment instant. No spouse benefit is assumed.

Formalization targets

Payment events and survival

Define the realised random variable $Z(K)$ by summing actual payment indicators across the finite schedule. Derive its expectation independently from the lifetime-state mass function. Define a second valuation using survival to each payment instant, and prove the equivalence by interchanging finite sums.

\mathbb{E}[Z]=\sum_{k=0}^{h}p_kZ(k)= \sum_{j=a}^{a+n-1} b_j v^{j+\delta} \begin{cases} S(a),&j<a+g,\\ S(j+\delta),&j\ge a+g. \end{cases}

The instalment sum is truncated at the finite horizon. The timing offset $\delta$ equals zero for advance and one for arrears.

Duration, guarantee and varying benefits

Partition a non-guaranteed whole-horizon annuity into temporary and deferred periods. For a guaranteed annuity, split payments into the activated period-certain amount and the strictly later survival-contingent amount. If $g\ge n$ , its entire value is survival to commencement multiplied by the corresponding annuity-certain present value. The benefit kernel supports level, arithmetic increasing or decreasing, geometric and piecewise step-up instalments.

Arrears, fractional survival and moments

The exact finite level-annuities relationship includes the terminal payment:

\ddot a_{\overline{h}|}-a_{\overline{h}|}=1-v^hS(h).

Expected squares of realised present values yield second moments and variance. The uniform distribution of deaths (UDD) provides a separate linear interpolation of observed annual survival probabilities at fractional instants.

Continuous survival laws and a controlled limit

At a fixed payment frequency, split each annual death-state mass equally across its subperiods under UDD. The same resulting micro-lifetime distribution can be used for fractional instalments and continuous benefit-rate integrals, so their actual cashflow representations share exact event boundaries. The construction agrees with annual survival at integer anniversaries. Placing the unsplit annual masses directly at integer death times would give a different, stepwise survival model within a year.

The zero-interest level annuity has an exact finite correction to the integral of linearly interpolated UDD survival. If $C$ is that integral, $S$ annual absolute survival and $m>0$ , the due value equals $C+(S(0)-S(h))/(2m)$ , and the arrears value equals $C-(S(0)-S(h))/(2m)$ . Both have an explicit $O(1/m)$ error and converge to $C$ . Under the fixed micro-atom lifetime law, continuously paid GBP 1 per year instead equals the same-frequency arrears value at zero interest, because the real-time survival indicator is constant between atom times. The limit of these finite-atom laws recovers the UDD linear-survival valuation.

A separate real-time lifetime-state model represents a continuous benefit rate in money per year rather than discrete money per instalment. Its actual realised annuity present value is integrated across the entitlement interval, with a guarantee activated by survival at commencement and payments then continuing to the estate before expiry. A finite probability expectation of the realised integral is reconciled with independently integrated survival weights. The continuous certain value is a comparison under the same deterministic discount force.

The discrete and real-time laws are connected at annual and fractional instalment boundaries through exact survivor-event identities. A bounded continuous payment-rate function admits an appropriate Riemann-sum limit under the specific regularity assumptions in the formal declaration. A twice differentiable integrand with uniformly bounded second derivative admits the two-term Woolhouse-type endpoint correction with a finite-horizon quadrature error bound. These limiting and approximation statements remain open formal theorem obligations, with no universal error claim for arbitrary discontinuous mortality laws.

Capstone

The unified capstone reconciles actual annual advance and arrears payments and UDD subperiod payments with independent survival-weighted sums. It also reconciles the same finite lifetime-state law with real-time survival at anniversaries and continuous integrated benefit valuations, including an activated guarantee. Separate milestones handle second moments, terminal-censored assurance-annuity identity, Riemann convergence and the explicit quadrature error bound. The earlier finite due-minus-arrears relationship remains a supporting target. These obligations follow from the separately defined probability masses and cashflow events, rather than assuming any valuation equality.

Significance

The classical distinction between annuity-certain and life-annuity present values is explained by Promislow (2015) through an explicit interest-and-survivorship discount mechanism. The present model makes this accounting precise at the level of individual payment events. It is consequently possible to compare a certain payment stream with a contingent one using exactly the same instalment schedule. It is also possible to alter the instalment amount without silently altering the survival law or guarantee entitlement.

The resulting mathematical foundation is suitable for retirement income and defined benefit pension cashflows where timing and benefit continuation clauses materially affect value. It separates annual unit amount from each instalment, and survival at commencement from survival at later payment events.

Difficulty

A death before commencement cannot activate a deferred guarantee. A death during the guarantee permits payments to the estate. An arrears instalment requires survival at the subsequent instant and the final one cannot silently disappear. Proving these relationships from true payment indicators is harder than defining annuity factors so the desired equations hold automatically. Finite lifetime censoring and the last surviving anniversary must remain visible in all derivations.

Formalization scope

The proposed Lean representation is an indexed real-valued finite probability mass function, a survival indicator and Finset-based cashflow sums. The canonical scope is a single namespace and targeted imports of Mathlib's real-number and finite-big-operator files. The environment revision is pinned in the manifest, but remains subject to live remote verification. Periods are integer anniversaries, amounts are per actual instalment, and the valuation origin is zero. Only finite sums are asserted without convergence hypotheses. The existing classical annuity formulae appear in the cited books. Their underlying mathematics is known, while the original finite cashflow encoding and its Lean theorem obligations are open and unproved.

These primitives are intended to supply later work on DB pension guarantee periods, future life-insurance premium annuities and pension escalation. A future separate mission could reuse the actual realised-cashflow event semantics to value survival-contingent spouse benefits with a two-life entitlement law, while keeping spouse entitlement fixed at the policyholder's death under the scheme rules. The current work limits itself to the single-life estate-continuation benefit and therefore does not risk silently importing joint-life assumptions.

The extended finite discrete formalisation constructs an actual UDD subperiod death-state law. Its fractional annuity valuations follow from realised subperiod payment events, with each instalment equal to the nominal annual pension divided by frequency. Separate theorems reconcile second moments with pairwise survival-event intersections, derive the incremental value of guarantees and reconcile finite annual assurance with the life-annuity due while retaining the terminal censored-state residual. The separate continuous law and a quantitative two-term Woolhouse-type error inequality are now included as remotely elaborated open theorem declarations, still requiring genuine proofs. General commutation-column identities, noninteger-year deferrals under arbitrary interpolation, unbounded whole-life convergence and classical higher-order Woolhouse estimates need further formal models. An unconfirmed Foundation A owner Draft is not an importable dependency. Every theorem declaration is an open proof obligation and no accepted proofs are asserted.

Selected references

David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapters 4–5, Cambridge University Press. https://doi.org/10.1017/9781108784184
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 4, Wiley, https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521
David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2013), Actuarial Mathematics for Life Contingent Risks, second edition, Chapter 5, sections 5.3–5.13. https://assets.cambridge.org/97811070/44074/frontmatter/9781107044074_frontmatter.pdf

129 thms3 active usersReviewed

Completed

Machine Learning Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low III: ℓ2-Regularized Best Subset Selection Satisfies Slow-Rate and Fast-Rate Oracle InequalitiesResearch Paper

Motivation

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

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

Setting

The data follow the model

y=f^*+\epsilon,

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

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

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

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

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

\mathcal E_s=\big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\big\},

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

\mathcal G_s=\big\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\big\}.

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

Formalization targets

Goal: Theorem 2 (p. 14)

Let $1\le k\le p$ .

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

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

and on $\mathcal F$

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Committed conventions:

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

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

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

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

Selected references

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

8 thms3 active usersReviewed

Completed

Operations Research Optimization 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 thms3 active usersReviewed

Completed

Economics Information Theory Operations Research+1·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.

7 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory·Captain: marwahaha

Block Sensitivity vs. Sensitivity: OpenAI BaselineResearch Paper

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

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

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

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

40 thms3 active usersReviewed

Completed

Algorithmic Game Theory Analysis Operations Research+1·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 thms3 active usersReviewed

Completed

Algorithmic Game Theory Analysis Operations Research+2·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 thms3 active usersReviewed

All missions

Information Design for Congested Social Services: Optimal Need-Based Persuasion 4: Signaling Achieves the First-Best Admission Policy for All Welfare Weights Above a ThresholdResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 (Achieving first-best)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 2: Under FIFO Issuance the Heuristic Base-Stock Policy's Optimality Gap Decays Exponentially in Demand Population SizeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 12)

Milestones (proof order)

Significance

Difficulty

Formalization scope

Selected references

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 3: Under FIFO Issuance the Heuristic Base-Stock Policy Is Asymptotically Optimal as the Unit Penalty Cost GrowsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 13)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Information Design for Congested Social Services: Optimal Need-Based Persuasion 3: Information Design Pareto-Dominates Full Information Exactly When Low-Need Arrivals Exceed a ThresholdResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3(1)–(2)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Information Design for Congested Social Services: Optimal Need-Based Persuasion 1: Every Pareto-Efficient Signaling Mechanism Has a Threshold Structure at or Below the Full-Information ThresholdResearch Paper

Why information design for congested public services

Setting

Formalization targets

Goal: Theorem 1 (p. 14)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A First-Order Primal-Dual Method for Nonconvex Constrained Optimization Based on the Augmented Lagrangian 1: NAPP-AL Drives the Best Stationarity Residual to Zero at Rate o(1/√k)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.1 (p. 18)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand I: The Approximation APT Bounds the Expected Cost-to-Go from Below and Above and Is Exact in the Last PeriodResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 13)

Milestones (Appendix D, pp. 34–35, and Lemma 1, p. 12)

Significance

Difficulty

Formalization scope

Selected references

Right to Repair: Pricing, Welfare, and Environmental Implications: The Manufacturer's Optimal New-Product and Repair Prices and the Resulting No-, Partial- or Full-Repair Equilibrium (Table 1)Research Paper

Motivation

Setting

Formalization targets

Consumer behavior and reduced pricing problems

Proposition 1 and Table 1

Significance

Difficulty

Formalization scope

Goal: one threshold in $\lambda r$ (Propositions 1 and 2)

Exact slow rate on $\mathcal H$

Slow rate on $\mathcal F$

Fast rate on $\mathcal G_{2k}$