Operations Research

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

1. (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)$.
2. 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.
3. (20), p. 22: such a policy outdates cumulatively at least as much as $\pi_{\underline S}$, pathwise.
4. Proposition 3, p. 22: if $\bar D<\infty$, $\mathrm{OPT}\ge h\mathbb E[(\underline S-D)^+]+\theta\mathbb E[O_\infty(\underline S)]$.
5. (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)$.
6. (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$.
7. (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

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:

1. 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$.
2. Lemma 2's hypothesis ($\lambda<1$, or $u_L,u_H\to-\infty$) wherever existence of maximizers is used.
3. $u_L(m_{fi}-1)\ne0$ in Proposition 3. Without it the claimed $\bar\Lambda_L>0$ is false.
4. $\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.

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

1. 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$).
2. Lemma 4.1 (p. 11): the dual step $\|p^k-p^{k+1}\|$ is controlled by the primal steps.
3. Lemma 4.2 (pp. 11–12): one-step change estimates for $\mathcal L_\gamma$.
4. 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$.
5. 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

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)

1. 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]$.
2. 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})$.
3. 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)]$.
4. 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).

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.

Why a firm would hand customer data to a rival

Large platforms that also sell their own products (Amazon, JD.com, app stores) hold detailed data on consumers and sometimes share part of it with the independent sellers they compete with. The usual view in the personalized-pricing literature is that information is a competitive weapon: a firm that knows more about consumers can price discriminate and capture more surplus, so giving that knowledge to a rival should only hurt. Thisse and Vives (American Economic Review, 1988) showed that when both firms on a Hotelling line can price every consumer individually, competition intensifies and the profits of the informed firm fall.

Choe, Cong and Wang (Monash Discussion Paper 2021-10, revised October 20, 2022; published in Management Science, 2024, doi:10.1287/mnsc.2023.4689) show that this is not the whole picture: an informed firm can strictly gain by sharing data on a well-chosen segment of consumers with an uninformed rival, and the rival gains too. This mission formalizes that result, Proposition 1 of the paper, together with the steps its proof is built from.

Setting

Consumers are located on the interval $[0,1]$. A consumer's location has cumulative distribution function $F$ with density $f>0$, continuous on $[0,1]$, and the hazard rate

$$h(x)=\frac{f(x)}{1-F(x)}$$

is strictly increasing on $[0,1)$ (the monotone hazard rate condition). Firm 1 sits at $0$ and knows every consumer's location; firm 2 sits at $1$ and knows none. A consumer at $x$ who buys from firm $i$ at price $p_i$ pays $p_i$ plus a transport cost equal to her distance to firm $i$; production is costless and the market is fully covered.

Benchmark. Without data sharing, firm 2 sets one uniform price $p_2$ and firm 1 undercuts it consumer by consumer, so firm 2 serves $[z,1]$ with $p_2=2z-1$ and earns $(2z-1)(1-F(z))$. The first-order condition gives the benchmark marginal consumer $z^N$ and price $p^N_2$:

$$z^N=\frac12+\frac1{h(z^N)},\qquad p^N_2=\frac2{h(z^N)}=2z^N-1.$$

The benchmark profits are $\pi^N_1=\int_0^{z^N}(p^N_2+1-2x)\,dF(x)$ and $\pi^N_2=p^N_2(1-F(z^N))$.

Data sharing on $[a,b]$. Firm 1 gives firm 2 the locations of the consumers in $[a,b]$. Firm 2 then chooses a uniform price for the consumers it does not know and personalized prices on $[a,b]$. Its uniform price either serves only $[b,1]$, at price $2b-1$ and profit $\pi_{21}(b)=(2b-1)(1-F(b))$, or serves $[z',a]\cup[b,1]$ for some $z'\le a$, with best profit

$$\pi_{22}(a,b)=\max_{z'\in[0,a]}(2z'-1)\bigl(1-F(b)+F(a)-F(z')\bigr).$$

When firm 2 chooses the first option, the profits are

$$\pi_1(a,b)=\int_0^a\bigl((2b-1)+(1-2x)\bigr)\,dF(x),\qquad \pi_2(a,b)=\int_a^b(2x-1)\,dF(x)+\pi_{21}(b).$$

Firm 2's incentive constraint (IC) is $\pi_{21}(b)\ge\pi_{22}(a,b)$.

Formalization targets

Goal: Proposition 1

For every distribution $(F,f)$ satisfying the conditions above:

$$\pi_1(z^N,b)>\pi^N_1\quad\text{and}\quad\pi_2(z^N,b)>\pi^N_2\qquad\text{for all } b\in(z^N,1],$$

and there exists $b'\in(z^N,1)$ with

$$\pi_{21}(b')>\pi_{22}(z^N,b'),$$

so sharing data on $[z^N,b']$ satisfies firm 2's incentive constraint and makes both firms strictly better off than without sharing.

Milestones

1. Eq. (1): $z^N$ exists and is unique in $(1/2,1)$.
2. $z^N$ is the unique maximizer of $\pi_{21}$ on $[0,1]$.
3. Lemma 2: if firm 2's uniform price serves $[z',a]\cup[b,1]$ with $z'$ solving the first-order condition (5), then $z'<z^N$, firm 2's price falls below $p^N_2$, and firm 1 earns less than $\pi^N_1$.
4. $\pi_1(z^N,b)-\pi^N_1=2(b-z^N)F(z^N)$.
5. $\pi_2(z^N,b)-\pi^N_2>\int_b^1(2b-2z^N)\,dF(x)>0$ for $z^N<b<1$.
6. With $\hat\pi_{22}(b)=\pi_{22}(z^N,b)$: $\pi_{21}(z^N)=\hat\pi_{22}(z^N)$ and $\pi_{21}(1)<\hat\pi_{22}(1)$.
7. $\hat\pi_{22}(b)<\hat\pi_{22}(z^N)$ for every $b\in(z^N,1]$.

Significance

The result reverses the standard intuition that a firm's informational advantage should be guarded. Firm 1 shares data only on firm 2's own customer base $[z^N,b']$, which it could not win anyway, and keeps the data on the most loyal consumers $[b',1]$ private. Firm 2 then prefers to extract surplus from those loyal consumers with a high uniform price $2b'-1>p^N_2$, and firm 1 raises its personalized prices accordingly. Competition is softened without firm 1 conceding market share. The statement holds for every monotone-hazard-rate distribution, not for a parametric family, which is what makes it a structural claim rather than a numerical example. It underlies the paper's analysis of optimal data sharing (Section 3.3) and its welfare conclusion that consumer surplus falls (Proposition 3), and it is the benchmark against which the paper's extensions (sales fees, data sale, entry) are compared.

The paper's proof is complete for the first part. For the existence of $b'$, the written argument infers a negative derivative of $\hat\pi_{22}$ at $z^N$ from a strict inequality, which does not follow as written and presupposes differentiability of a maximum value function; the statement itself is true. A machine-checked proof closes that step. To the best of current knowledge none of these results has been formalized.

Difficulty

The two profit comparisons in the first part are integral identities and estimates that only need the fundamental theorem of calculus and $f>0$. The existence of $b'$ is the hard part. Both $\pi_{21}(b)$ and $\hat\pi_{22}(b)$ start from the same value at $b=z^N$, and $\pi_{21}$ has zero derivative there, so the comparison is decided at first order by how fast $\hat\pi_{22}$ decreases. But $\hat\pi_{22}$ is a maximum over $z'\in[0,z^N]$ whose maximizer moves with $b$ and need not be unique, so $\hat\pi_{22}$ is not known to be differentiable, and the strict decrease of milestone 7 alone does not give a linear rate. A proof has to bound $\hat\pi_{22}(b)$ from above by $\pi_{21}(z^N)$ minus a term proportional to $b-z^N$, uniformly over the possible maximizers, and compare it with the second-order behaviour of $\pi_{21}$ near its maximum. Existence of $z^N$ similarly needs the hazard rate to blow up at $1$, which uses $F(1)=1$ and $f(1)>0$.

Formalization scope

All objects are real-valued functions on $\mathbb R$ with hypotheses only on $[0,1]$. The distribution is the structure MHRDist F f: $F(0)=0$, $F(1)=1$, $F$ has derivative $f$ within $[0,1]$ at every point of $[0,1]$, $f$ is continuous and strictly positive on $[0,1]$, and $h=f/(1-F)$ is strictly increasing on $[0,1)$. The paper's "smooth" is read as continuously differentiable, a weaker assumption, so the formal theorems are at least as strong as the paper's. Every $dF$ integral is an interval integral of the integrand times $f$, always with increasing bounds. $z^N$ enters as a number zN with the hypothesis IsZN F f zN ($z^N\in(1/2,1)$ and $z^N=1/2+1/h(z^N)$); milestone 1 shows exactly one such number exists, so no statement is vacuous. $\pi_{22}$ is defined as the supremum of the profit over $z'\in[0,a]$ (a maximum, since the set is compact and the function continuous), never through the first-order condition (5); the incentive inequality in the goal is strict, as in the paper's proof.

A trivializing formalization is ruled out: $\pi_{22}$ is the actual maximum, not a free parameter or the value at a stationary point, and $z^N$ is pinned by Eq. (1), whose solution is shown to exist.

A complete development needs the fundamental theorem of calculus for interval integrals, compactness and the intermediate value theorem on $[0,1]$, and a uniform first-order estimate on a parametric maximum. The lemmas on hazard rates and on the maximizer of $(2z-1)(1-F(z))$ are reusable for other Hotelling and pricing models with monotone-hazard-rate demand. Contributions are welcome on any milestone, and alternative proofs of the existence of $b'$ are of particular interest.

Selected references

• Chongwoo Choe, Jiajia Cong, Chengsi Wang, Softening Competition through Unilateral Sharing of Customer Data, Monash University Department of Economics Discussion Paper 2021-10, revised October 20, 2022 (the version formalized here; all page and equation numbers refer to it); published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4689
• Jacques-François Thisse, Xavier Vives, On the Strategic Choice of Spatial Price Policy, American Economic Review 78(1), 1988, 127–137.
• Greg Shaffer, Z. John Zhang, Competitive One-to-One Promotions, Management Science 48(9), 2002, 1143–1160.