Operations Research

Motivation

In reward based crowdfunding, customers must decide whether to back a product before its quality is known to them. The entrepreneur knows that quality and chooses a funding price. A high quality entrepreneur may therefore use price to convey information, but the same price is available to a low quality entrepreneur. The choice also changes the chance that the campaign meets its financing target. Bolandifar, Chen, Kouvelis, and Zhou study how these effects interact when the entrepreneur chooses a second, regular selling price after the campaign succeeds. The one price mechanism in this mission concerns the case in which only the funding price is posted in advance.

The question matters to the design and interpretation of crowdfunding campaigns. A lower funding price can be a credible quality signal even though it forgoes immediate revenue. Whether that signal is sustainable depends on the later selling opportunity, the financing target, and the different incentives of the two quality types. The paper gives a precise threshold for the financing target below which one separating outcome survives a refinement of the equilibrium concept.

Setting

The entrepreneur's product has privately known quality $q_i$, either low $q_L$ or high $q_H$, with $0<q_L<q_H$. The financing target is $T>0$. The entrepreneur posts a funding price $p_1\ge T$. Funding period customers all share a taste $\theta_c$ uniformly distributed on $[0,1]$ and evaluate the product using believed quality $q_j$. They back it when $\theta_cq_j\ge p_1$. The funding market has size one, so a successful campaign raises at least $T$ and occurs with probability $1-p_1/q_j$ for $T\le p_1\le q_j$. The formal definition extends this probability by zero for larger prices.

After success, true quality is revealed and the entrepreneur sets a regular selling price $p_2\in(0,q_i]$. A fraction $\alpha\in(0,1)$ of regular period customers have the same taste as the funding customers. Their taste distribution is therefore updated after success. The other regular customers have a fresh, independent uniform taste. The regular market also has size one. Production cost, salvage value, and discounting contribute no additional terms. Conditional regular period profit is $\pi^{ij}_2(p_2\mid p_1)$, the two branch function in equation (2) of the manuscript. Its optimal value $\pi^{ij*}_2(p_1)$ is the supremum over feasible $p_2$. The total expected profit $\pi^{ij}(p_1)$ is the success probability times $p_1+\pi^{ij*}_2(p_1)$.

A separating equilibrium assigns different feasible funding prices $p_H$ and $p_L$ to the two entrepreneur types. Customers believe quality is high at $p_H$ and low at every other price, including off path prices. Under those beliefs, neither type benefits from a feasible deviation. The intuitive criterion removes an equilibrium if an off path price would strictly improve the high type's profit while strictly reducing the low type's profit, were customers to interpret that deviation as a high quality signal. This is the paper's stated test, with the strict low type comparison used in its appendix.

Formalization targets

The separating equilibrium

Define the price threshold

$$\bar p_1=\frac{4q_H-(1-\alpha)q_L-\sqrt{(q_H-q_L)\bigl(16q_H-(1-\alpha)^2q_L\bigr)}}{8}.$$

The goal is Proposition 1 of the manuscript. If $T\le\bar p_1$, there is a separating equilibrium surviving the intuitive criterion, and every surviving separating equilibrium has exactly the prices

$$p_H=\bar p_1,\qquad p_L=\frac{3+\alpha}{8}q_L.$$

The formal goal also says that no separating equilibrium exists when $\bar p_1<T<q_L$. Its scope on this side of the threshold follows the manuscript's proof and the nondegenerate funding market; the printed “otherwise” sentence does not hold literally when $T\ge q_L$.

Supporting targets

Lemma 1 identifies the optimal regular price and its attained profit in each of three funding price ranges, split at $q_j/2$ and $\min\{q_j/[2(1-\alpha)],q_j\}$. Lemma 2 identifies the funding profit's single peak and the maximizing price $\max\{[4q_j-(1-\alpha)q_i]/8,T\}$. The three parts of Lemma 3 characterize the low type's mimicking indifference prices, the high type's upper indifference price, and the ordering of these thresholds. These are the milestones leading to Proposition 1.

Significance

The proposition gives both types' prices and shows why the high type's credible signal is a lower funding price than the low type's. It also identifies a financing target above which this separation disappears within the paper's nondegenerate range. The result relates a platform design parameter, the target, to equilibrium information revealed by price.

The result is proved in the cited manuscript, with proofs in Appendix A. The remaining work in this mission is a machine checked proof of the model's price optimization and equilibrium claims. The definition of the two period payoff, the treatment of the later optimal price, and the explicit deviation predicates may be reusable for other crowdfunding signaling mechanisms. The draft statements are open proof targets; the present mission does not claim those proofs are already formalized.

Difficulty

The later optimal price changes form as the funding price crosses two thresholds. That makes total expected profit a piecewise function, even before the two types' incentives are compared. Maximizing either type's full information payoff alone does not determine a separating equilibrium: the low type might imitate the high type, while the high type might deviate to a price customers would interpret as low quality. The intuitive criterion imposes a further comparison at prices outside the equilibrium path. The claim requires all of these comparisons with the same underlying payoff definition.

Formalization scope

Lean uses one tuple of real parameters $q_L,q_H,\alpha,T$ and the standing restrictions $0<q_L<q_H$, $0<\alpha<1$, and $T>0$. The prior probability of high quality does not occur in the separating price statements. The regular profit is the printed equation (2), with a positive regular price at most true quality. Campaign success probability is clipped at zero for funding prices above believed quality. Funding prices range over all reals at least $T$; the maximum profits are defined as suprema over those feasible prices. Milestones assert attainment, so those suprema cannot be replaced by convenient formula values.

The model uses the paper's market size, cost, salvage, and discount normalizations. Lemma 1 excludes $p_1=q_j$: at that endpoint the printed third case can specify an infeasible regular price. Lemma 2 assumes $T<q_j$ and quantifies only over the four true and believed quality combinations. Lemma 3 is stated for $T\le\bar p_1$ to avoid its circular printed preamble, and one threshold comparison is expressed as a strict profit inequality because the lower crossing can lie below $T$. Proposition 1 does not assert pooling existence, which would require the omitted prior; its no separation clause is restricted to $T<q_L$.

Contributions toward the piecewise optimization lemmas, the threshold characterization, and the equilibrium theorem are welcome. The separating equilibrium is defined by incentive comparisons over all feasible deviations, and its refinement is defined by the off path deviation test. The optimal profits are supremum values of the model payoffs. These choices keep the goal from collapsing into a restatement of a closed form or of the paper's derived necessary and sufficient conditions.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis, and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, revision of 2022-05-30, §§3–4 and Appendix A. SSRN. Published as Manufacturing & Service Operations Management, DOI 10.1287/msom.2022.1177; the cited artifact here is the SSRN manuscript.

Motivation

Same-day and on-demand delivery services (groceries, meals, parcels) must decide how to assign incoming orders to drivers. One option is flexible dispatching: any driver may serve any order in the service region. Another is districting: the region is cut into $m$ districts, one per driver, and each driver serves only the orders from their own district. Districting is easier to run, since drivers learn their territory, routes are short and responsibility is clear, but it gives up the flexibility of pooling. A basic question is when a districting policy loses nothing against the best flexible policy.

Carlsson, Liu, Salari and Yu (Operations Research 72(1), 2024; accepted manuscript SSRN 3915544) answer this in heavy traffic, the regime where the drivers are almost always busy. Their comparison point is the policy $\pi^*$ of Bertsimas and van Ryzin (1993), whose expected delivery time has an explicit leading-order formula in heavy traffic. Their Theorem 6 gives two integral conditions on a partition under which districting matches $\pi^*$ to first order.

Timeline.

• 1959. Beardwood, Halton and Hammersley: the shortest tour through $n$ random points with density $f$ has length $\sim\beta\sqrt n\iint\sqrt{f}$.
• 1991–1993. Bertsimas and van Ryzin: the dynamic traveling repairman and its capacitated, multi-vehicle versions, with heavy-traffic lower bounds and a policy $\pi^*$ that attains the leading-order formula (Theorem 3 of the paper, p. 8).
• 2024. Carlsson, Liu, Salari and Yu: a partition that is equitable for two measures gives a districting policy that is asymptotically optimal in heavy traffic (Theorem 6), together with algorithms to compute such partitions.

Setting

A service region $\mathscr R\subseteq\mathbb R^2$ is compact and convex and contains a depot $x_0$. Orders arrive at rate $\lambda$ at random locations drawn from a demand density $f\ge0$ on $\mathscr R$, Lipschitz, with $\iint_{\mathscr R}f(x)\,dx=1$. There are $m\ge1$ identical vehicles with speed $v>0$ and capacity $q\in\mathbb N_+$, and each order needs an on-site service of mean $\bar s\ge0$. The constant $\beta>0$ comes from the Beardwood–Halton–Hammersley theorem.

The workload factor of the fleet is

$$\rho+\frac{2\lambda\iint_{\mathscr R}\|x-x_0\|f(x)\,dx}{mvq},\qquad \rho=\frac{\lambda\bar s}{m},$$

the long-run fraction of time a vehicle spends in on-site service and in travel to and from the depot. The system is stable when it is below $1$, and heavy traffic is the limit in which it tends to $1$ from below, with only $\lambda$ varying.

Theorem 3 of the paper (Bertsimas and van Ryzin) states that $\pi^*$ achieves

$$T(\pi^*)\sim\frac{\beta^2\lambda(1-\frac1q)^2\left[\iint_{\mathscr R}\sqrt{f(x)}\,dx\right]^2}{2m^2v^2\left(1-\rho-\frac{2\lambda\iint_{\mathscr R}\|x-x_0\|f(x)\,dx}{mvq}\right)^2}$$

in heavy traffic. A policy $\pi$ is asymptotically optimal if $T(\pi)/T(\pi^*)\to1$ in heavy traffic.

A region partitioning policy fixes a partition $\{\mathscr R_1,\dots,\mathscr R_m\}$ of $\mathscr R$ and dedicates one vehicle to each $\mathscr R_i$. District $i$ then receives orders at rate $\lambda_i=\lambda\iint_{\mathscr R_i}f$ with conditional density $f_i=f/\iint_{\mathscr R_i}f$. Its vehicle runs the single-vehicle version of $\pi^*$, so Theorem 3 with $m=1$ gives its delivery time $T_i$. The policy's overall expected delivery time is $T=\sum_i\mathbb P(x\in\mathscr R_i)\,T_i$.

Formalization targets

Goal: Theorem 6 (p. 11)

If for every $i$

$$\iint_{\mathscr R_i}\sqrt{f(x)}\,dx=\frac1m\iint_{\mathscr R}\sqrt{f(x)}\,dx,\qquad \iint_{\mathscr R_i}(\bar svq+2\|x-x_0\|)f(x)\,dx=\frac1m\iint_{\mathscr R}(\bar svq+2\|x-x_0\|)f(x)\,dx,$$

and $T(\pi^*)$ and every $T_i$ obey Theorem 3, then

$$\frac{\sum_{i=1}^m\mathbb P(x\in\mathscr R_i)\,T_i}{T(\pi^*)}\longrightarrow1\quad\text{in heavy traffic.}$$

Milestones

These are the displayed steps of the printed proofs of Theorems 5 and 6 (pp. ec5–ec6):

1. Normalization identities. $\iint_{\mathscr R_i}\sqrt{f_i}=\iint_{\mathscr R_i}\sqrt f/\sqrt{\iint_{\mathscr R_i}f}$ and $\iint_{\mathscr R_i}\|x-x_0\|f_i=\iint_{\mathscr R_i}\|x-x_0\|f/\iint_{\mathscr R_i}f$.
2. Per-district workload identity. Under the second condition, district $i$'s workload factor $\rho_i+2\lambda_i\iint_{\mathscr R_i}\|x-x_0\|f_i/vq$ equals the fleet's for every $\lambda$. The two heavy-traffic limits therefore coincide.
3. Leading-term chain. Under both conditions, the Theorem 3 term of district $i$ (one vehicle, data $\lambda_i,f_i$) equals the fleet's term.
4. Per-district ratio. $T_i/T(\pi^*)\to1$ for every $i$.
5. Total expectation. If $T_i/T(\pi^*)\to1$ for every $i$, then $\sum_i\mathbb P(x\in\mathscr R_i)T_i/T(\pi^*)\to1$.

Significance

The result. Theorem 6 turns a question about stochastic, dynamic routing into a static geometric condition: find a partition that gives every district a $1/m$ share of two measures, $\mu_1=\iint\sqrt f$ (local tour length) and $\mu_2=\iint(\bar svq+2\|x-x_0\|)f$ (service plus round-trip load). The rest of the paper builds on this. It computes such partitions with convex pieces, bounds the loss when the shares are only approximately equal (Proposition 3, the subject of the companion mission), and tests the policy in simulation. The theorem also shows that the arrival rates need not be equal across districts. What has to be equal is the combined load.

Formalizing it. The result has a short pen-and-paper proof, and no machine-checked version exists. The mission records exactly which part of the argument is real analysis (integral identities over a partition, and how heavy-traffic limits pass to ratios) and which part is borrowed from Bertsimas and van Ryzin. It also gives the platform a first districting and continuous-approximation development. Its definitions (workload factor, Theorem 3's leading term, heavy-traffic filter, conditional subregion data) can be reused for other results in the continuous-approximation literature.

Difficulty

The algebra in the proof is simple once Theorem 3 is applied to each district with its own rate $\lambda_i$, density $f_i$ and one vehicle. The obstacle is in the limits. Theorem 3 for district $i$ holds along that district's heavy-traffic limit, where its own workload factor tends to $1$, while asymptotic optimality is measured along the fleet's limit. These are different limits unless the second equitable condition makes the two workload factors equal as functions of $\lambda$. A tempting shortcut is to state the district hypothesis directly with the fleet's quantities, such as $(1/m)\iint_{\mathscr R}\sqrt f$ and the fleet's workload factor. That assumes milestones 2 and 3 and empties the theorem. Division also needs care: $f_i$ and the ratios $T_i/T(\pi^*)$ have denominators that must be shown nonzero from the hypotheses, not assumed.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2) with the Euclidean norm, and integrals are Bochner set integrals for Lebesgue measure. The definition file CarlssonPartition.Equitable.Setting contains:

• the instance $(\mathscr R,x_0,f,m,v,q,\bar s,\beta)$;
• the standing assumptions listed in Setting;
• the workload factor and Theorem 3's leading term, both generic in (vehicle count, rate, region, density);
• $\mathbb P(x\in S)$, $\lambda_i$ and $f_i$;
• partitions;
• the heavy-traffic filter.

Conventions:

• The model is not formalized. The stochastic dynamic routing model (renewal arrivals, TSP batching, queues of tours) has no Mathlib substrate. The paper itself uses it only through Theorem 3 of Bertsimas and van Ryzin. So $T(\pi^*)$ and the $T_i$ are arbitrary real functions of $\lambda$, and Theorem 3 is a hypothesis on them: for the fleet, and for each district with $m=1$ along the district's own limit.
• Heavy traffic is Filter.comap (fun λ => workload) (𝓝[<] 1): the arrival rates along which the workload factor tends to $1$ from below. Every "$\sim$" is a ratio tending to $1$.
• Partitions are read up to null sets: null-measurable pieces, pairwise almost-everywhere disjoint, with union $\mathscr R$.
• Added hypothesis $q\ge2$. At $q=1$ the factor $(1-1/q)^2$ makes Theorem 3's leading term zero, so its ratio hypotheses could not hold and the theorem would be vacuous.
• No positivity of $\iint_{\mathscr R_i}f$ is assumed in the goal, because it follows from the first equitable condition. The milestones that manipulate $f_i$ state it explicitly.
• The Lipschitz condition is kept as a standing assumption of the paper, although only continuity is needed.

Two formalizations would make the goal trivial and are ruled out: defining $T(\pi^*)$ or $T_i$ as the leading-order formula, and writing the district hypothesis with fleet quantities or the fleet's filter. The verification development checks that the heavy-traffic filter is not the bottom filter whenever $\bar s>0$.

Welcome contributions: proofs of the milestones; a general lemma on averaging ratio limits under a probability vector; and finite additivity of set integrals over a.e.-disjoint partitions in the form used here.

Selected references

• J. G. Carlsson, S. Liu, N. Salari, H. Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, Operations Research 72(1):91–109, 2024. https://doi.org/10.1287/opre.2021.0588 (accepted manuscript: https://ssrn.com/abstract=3915544)
• D. J. Bertsimas, G. van Ryzin, Stochastic and Dynamic Vehicle Routing in the Euclidean Plane with Multiple Capacitated Vehicles, Operations Research 41(1):60–76, 1993. https://doi.org/10.1287/opre.41.1.60
• D. J. Bertsimas, G. van Ryzin, A Stochastic and Dynamic Vehicle Routing Problem in the Euclidean Plane, Operations Research 39(4):601–615, 1991. https://doi.org/10.1287/opre.39.4.601
• J. Beardwood, J. H. Halton, J. M. Hammersley, The Shortest Path Through Many Points, Mathematical Proceedings of the Cambridge Philosophical Society 55(4):299–327, 1959. https://doi.org/10.1017/S0305004100034095

Why distribution and pricing interact

A manufacturer that already sells directly to consumers may also supply an independent retailer. Adding the retailer can reach consumers who prefer its service, but the two channels then compete for some of the same buyers. A wholesale price affects both the retailer's ability to serve consumers and its retail pricing. The manufacturer's choice of distribution channel therefore depends on the pricing tools available to each firm. Jullien, Reisinger, and Rey study this choice when either or both firms can charge prices tailored to individual consumers in Personalized Pricing and Distribution Strategies. The source used here is their authors' manuscript of March 2022, whose proof of Proposition 3 appears in Online Appendix A.

This mission addresses a particular case of that analysis: the manufacturer charges a single retail price, while the retailer may charge either a single price or a price tailored to each buyer. The consumers' valuations for both channels move in the same direction with their type. Under those conditions, the paper claims that opening the retailer channel raises total industry profit under either retailer pricing policy. This is a question about the distribution decision, with the downstream retail game determining the profit achieved by each decision.

The market and its two retail games

A consumer type is a real number $x$ in $[0,X]$, with unit density. Firm A is the manufacturer and direct seller; firm B is an independent retailer that obtains each unit from A. Their values to a consumer are

$$u_A(x)=\max\{1-x,0\},\qquad u_B(x)=\max\{v-sx,0\}.$$

There are no fixed costs of opening a channel and no variable production or distribution costs. The market parameters satisfy $0<s<v<1$ and $X\ge v/s$. These conditions express the positively correlated case in §5 and keep the market large enough that its upper boundary does not limit B's demand. The two values cross at $\hat x=(1-v)/(1-s)$, with common value $\hat u=(v-s)/(1-s)>0$. Types below $\hat x$ value A's offer more; types above it value B's offer more, until valuations fall to zero.

A two-part tariff has a fixed fee $F$ and a wholesale price $w$ per unit B buys from A. The fee divides profit between the firms. Total industry profit is what consumers pay, so $F$ cancels from that total. The wholesale price is nonnegative. At the wholesale stage, the firms compare the total industry profit attainable with both channels against the profit from A selling alone. As on p. 9 of the manuscript, a tie is resolved in favor of mono distribution; a strictly greater profit is required for dual distribution.

When A sells alone and charges a uniform price $p$, its profit is $p$ times the measure of types for whom $u_A(x)\ge p$. If both firms charge uniform prices, denoted UU, they set $p_A$ and $p_B$ simultaneously. A consumer buys the product with highest nonnegative net utility. A earns $p_A$ on each of its retail sales and $w$ on each B sale. B earns $p_B-w$ on each of its sales. A downstream Nash equilibrium requires each price to maximize its firm's variable profit against the other price, including deviations into market regions where demand is zero or the identity of the preferred firm changes.

If A charges a uniform price and B tailors its price, denoted UP, A announces $p_A$ first. B then responds separately to each consumer. Under the continuation selected in the manuscript, B serves a type $x$ when $u_B(x)-w$ exceeds both zero and A's nonnegative consumer surplus. Its price is $u_B(x)-\max\{u_A(x)-p_A,0\}$. Otherwise, A sells if its price does not exceed the consumer's value. A chooses its uniform price to maximize its retail receipts plus wholesale receipts. Industry profit is the integral over $[0,X]$ of the price actually paid by each consumer.

Formalization targets

The mono-distribution benchmark is

$$\Pi_U^m=\max_p\Pi_U^m(p)=\Pi_U^m(1/2)=\frac14.$$

The paper derives a wholesale price $w^*_{UU}$ and retail prices $p_A(w^*_{UU}),p_B(w^*_{UU})$ for the UU game, together with a profit $\Pi^*_{UU}$ satisfying

$$\Pi^*_{UU}-\Pi_U^m=\frac{(1+s)(v-s)^2}{s(4+5s)(1-s)}>0.$$

For UP it derives $w^*_{UP}$, A's leader price $p_A(w^*_{UP})$, and a profit $\Pi^*_{UP}$. Equation (15) gives $\Pi^*_{UP}>\Pi^*_{UU}$. The milestone list follows these source results, including the consumer demands and the two profit identities. Its last comparison completes the UP side after the UU gain is established.

The goal is Proposition 3: for each of UU and UP, some nonnegative wholesale price admits a downstream equilibrium and every equilibrium at that price yields industry profit strictly greater than A could earn with any uniform price in mono distribution. The goal leaves the wholesale price existential, as the proposition does. It does not assume the paper's calculated candidates are the only possible wholesale prices that work.

What the result establishes

Proposition 3 identifies a robust distribution choice within the positively correlated case: while A uses uniform pricing, permitting the retailer channel raises joint profit whether B uses uniform or personalized retail prices. The conclusion separates the effect of B's pricing technology from the effect of A's own pricing technology; the latter changes the distribution comparison in Proposition 4 of the same manuscript. The result also supplies a precise instance in which additional downstream competition and additional market coverage must be assessed together.

The paper proves Proposition 3 in its Online Appendix A. The remaining work for this mission is a machine-checked derivation of the downstream equilibrium conditions, the demand and payment integrals, and the strict profit comparisons. The Lean statements here are open proof obligations. A complete development would make the consumer-choice and profit model reusable for related distribution games, while the rational formulas and equilibrium calculations are specific to this paper's linear valuations.

Where the formalization is difficult

The paper writes simple linear demand expressions in the region where both firms have positive sales. Actual demands are measures of consumer choice sets and change formula at market boundaries, when a price excludes a product, or when all consumers refuse to buy. A first-order condition within one region does not by itself establish a global best response in the full retail game. The UU equilibrium milestone consequently states global Nash optimality and uniqueness at the selected wholesale price. In UP, A's leader price must likewise maximize its variable profit over every real uniform price after B's per-consumer response. The integral of actual payments must then be shown to equal the paper's closed form.

Formalization scope

Lean represents consumer types by real numbers in $[0,X]$ and their mass by Lebesgue volume. The Model fields are $v,s,X$; Model.Standing records exactly $0<s<v<1$ and $X\ge v/s$. The valuations and crossing point are defined from these fields. Retail demand is clipped to the consumer interval, and profit is calculated from demand or actual payments. The expressions printed as (12) and (14) are theorem conclusions, not definitions of industry profit. A real supremum is unnecessary for mono distribution: the theorem bounds profit at every price and proves attainment at $1/2$.

The UP response uses the manuscript's selected personalized-pricing continuation. At indifference, the choice rules assign UU ties between the firms to A and give B a sale in UP only with a strict margin. Ties occur only at isolated types at the candidate equilibrium prices; zero-price deviations can create ties across the flat zero-valuation tail, and the rules specify their outcome. Global best responses quantify over all real retail prices, including zero and negative deviations. The goal restricts wholesale prices to $w\ge0$, the range used in the manuscript's analysis. The fixed fee is omitted from the model because it transfers profit between firms without changing industry profit. The goal includes existence of a continuation equilibrium, so a vacuous universal statement over an empty equilibrium set cannot establish dual distribution.

The development needs elementary properties of Lebesgue measure on real intervals, measurable piecewise choice sets, interval integration, and algebraic inequalities for the rational candidate prices. Proofs of the equilibrium and integral milestones, or reusable lemmas about volumes of intervals cut by affine utility comparisons, are welcome contributions. The shared primitives are duplicated in the companion mission on personalized pricing by A because unpublished draft definitions cannot be imported across proposals.

Selected references

• B. Jullien, M. Reisinger, and P. Rey, Personalized Pricing and Distribution Strategies, authors' manuscript of March 2022; published in Management Science (2023). DOI: 10.1287/mnsc.2022.4437. Source artifact in this repository: source.pdf, SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, printed pp. 5–14 and Online Appendix A, pp. 1–4.

Why spatial pricing needs a dynamic control

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

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

The pricing network and benchmark

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

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

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

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

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

Formalization targets

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

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

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

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

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

What the result establishes

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

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

Main difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 6.2 (p. 26)

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A firm can learn a customer's preference before choosing a customized product, or it can let the customer choose a requested design. The two approaches assign the design decision to different parties. That matters when design changes both the value of a sale and a cost the seller must incur before the price is negotiated. Guo's study of customer voice in customization compares these approaches in a model where a buyer has private information about how much it values quality. The payoff comparison asks who gains from holding the design right and whether the answer survives a modest fixed cost of using that approach.

This mission concerns Proposition 8 of the SSRN author copy, printed page 23. The result is a comparative statement about two already specified separating equilibrium outcomes. Earlier results in the same paper characterize when the outcomes arise: Proposition 1 treats communication before seller design, and Proposition 3 treats a buyer's design request. Proposition 8 compares the parties' payoffs at the qualities associated with those outcomes. Its four clauses distinguish gross payoff rankings from net rankings after an incremental fixed cost. The paper states Proposition 8 without a separate proof; its surrounding discussion explains its interpretation. All page and result numbers here follow the SSRN version of 2023-11-29.

Setting

There is one seller and a unit mass of buyers. Each buyer has one-unit demand and a privately known quality preference $\theta_i$, with type $i\in\{H,L\}$ and $\theta_H>\theta_L>0$. The high type has population share $\alpha\in(0,1)$, while the low type has share $1-\alpha$. A product's quality is a nonnegative real number $q$. Producing a unit of quality $q$ costs $kq^2$, and offering that product incurs a selling cost $sq^2$, where $k,s>0$. The selling cost is incurred before the price is settled. The seller makes a take-it-or-leave-it offer with probability $\gamma\in(0,1)$; the buyer does so with probability $1-\gamma$. These primitives and the timing are specified in Section 2.

In A-Learning, the buyer sends a costless message about its preference and the seller chooses the design. In O-Learning, the buyer requests a quality and the seller decides whether to accept it. The paper compares separating outcomes, so each type is associated with its true preference when the equilibrium payoff is evaluated. The pricing stage is represented by the paper's payoff formulas. If the seller regards a buyer's preference as $\hat\theta$, its payoff from quality $q$ is

$$v(q,\hat\theta)=\gamma(\hat\theta q-kq^2)-sq^2.$$

The buyer's payoffs $u^A(\theta,\hat\theta,q)$ and $\mu(q,\theta,\hat\theta)$ retain the nonnegative parts in equations (5) and (9): each is $\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}$, with its arguments ordered as in the relevant equation. For type $i$, the paper's A-Learning and O-Learning equilibrium qualities are

$$q^A_i=\frac{\gamma\theta_i}{2s+2\gamma k},\qquad q^O_i=\min\left\{\frac{\gamma\theta_i}{s+\gamma k},\frac{\theta_i}{2k}\right\}.$$

Write $\alpha_H=\alpha$ and $\alpha_L=1-\alpha$. The seller's expected gross payoffs are $V^A=\sum_i\alpha_i v(q^A_i,\theta_i)$ and $V^O=\sum_i\alpha_i v(q^O_i,\theta_i)$. The buyer payoffs $U^A_i$ and $U^O_i$ evaluate $u^A$ and $\mu$ at type $i$'s quality and truthful preference. These are the payoffs defined around equations (8) and (13) of the paper.

Formalization targets

The first comparison says that the seller earns more from its own design, while each buyer type earns more from its requested design:

$$V^A>V^O,\qquad U^A_i<U^O_i\quad(i\in\{H,L\}).$$

The two fixed-cost clauses hold the preference levels, population share, bargaining weight, and production-cost coefficient fixed while the positive selling-cost coefficient $s$ varies. For every seller-side incremental fixed cost $F>0$, there is a positive threshold $\tilde s_F$ such that

$$0<s<\tilde s_F\quad\Longrightarrow\quad V^A(s)-F<V^O(s).$$

For every buyer-side incremental fixed cost $G>0$ and each type $i$, there is a positive threshold $\tilde s_{iG}$ such that

$$0<s<\tilde s_{iG}\quad\Longrightarrow\quad U^A_i(s)>U^O_i(s)-G.$$

The goal is the conjunction of these four clauses, exactly the payoff content of Proposition 8. The milestone list also includes the paper's strict quality comparison $q^A_i<q^O_i$ and its observation that the quality difference tends to zero as $s$ tends to zero. The printed statement and discussion are on pages 22–23.

Significance

The gross comparisons separate the seller's and buyers' preferences over who chooses quality. The fixed-cost clauses show why the party favored by the gross comparison need not favor that approach once its own extra effort or implementation expense is counted. The thresholds make this claim uniform over all sufficiently small positive selling costs, rather than treating the single case $s=0$. This distinction is relevant when comparing preference solicitation, which requires seller effort, with buyer-led design, which requires customer effort.

Formalizing the result gives a reusable two-type model of quadratic production and selling costs, the two reduced-form buyer payoffs, and a finite-population expected-payoff calculation. It also creates separate targets for each clause, so the gross-payoff and small-cost claims can be checked independently. The result is proved in the mathematical paper only to the extent of its stated Proposition 8 and accompanying discussion; the local Lean statements in this proposal compile with proof placeholders and do not yet constitute machine-checked proofs.

Difficulty

The two approaches select different quality formulas, and O-Learning uses a minimum of two expressions. As $s$ changes, that minimum can switch branches. The buyer payoff formulas also contain maxima with zero, so replacing them unconditionally with simplified quadratic expressions would change the model. A valid payoff comparison must account for the relevant branch and preserve the strict inequalities for both buyer types. For the fixed-cost clauses, pointwise closeness at $s=0$ does not itself state a uniform claim for every sufficiently small positive $s$; the threshold must be positive and chosen before $s$.

Formalization scope

The Lean model uses a two-constructor buyer type, real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$, and a Standing predicate carrying every displayed positivity and interval assumption. Qualities are real-valued, with the paper's intended domain $q\geq0$; the closed-form equilibrium qualities in this mission are nonnegative under those assumptions. Expected seller payoffs use a finite sum over exactly the high and low types, weighted by $\alpha$ and $1-\alpha$. Buyer payoffs use the original maxima with zero. The pricing stage is in reduced form through equations (4), (5), and (9). The model and payoff notation are local to CustomerVoice.Payoffs, because the other missions' definitions are unpublished drafts.

The statements compare the printed closed-form qualities without adding the separate inequalities that guarantee both separating equilibria exist. Thus their domain is all parameter choices satisfying Section 2's standing assumptions; this is the stronger reading identified in the paper's planning notes for Proposition 8. In the small-$s$ statements, withS changes only the selling-cost coefficient, and the quantified values of $s$ satisfy $0<s<\tilde s$. The proof targets cannot be reduced by deleting the nonnegative parts of the buyer payoffs, allowing a zero threshold, or checking only the limit at $s=0$. Contributions to the elementary quality comparisons, branch-sensitive payoff inequalities, and positive-side limits all support the goal. The finite weighted-payoff and limit infrastructure can be reused in other small-cost comparisons.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, version of 2023-11-29, §§2–3.4 and Proposition 8. SSRN record.
• Liang Guo, The Voice of Customers in Customization, Management Science, 2021. DOI:10.1287/mnsc.2021.04025. The mission's statement indices follow the SSRN copy above.

Motivation

When customers request a customized product, their requests can reveal information about what they value. A seller can use that information when setting a price, while a customer can choose a request with the resulting price in mind. The question is whether customers with different preferences can make different requests in equilibrium. Liang Guo's The Voice of Customers in Customization, §3.3, studies this question in a two-type model of buyer-led product design, called O-Learning. It compares O-Learning with a separate game in which the seller chooses quality after a customer's cheap-talk message. This mission concerns only the O-Learning game.

Proposition 3 of the SSRN author copy identifies when a particular cheap-signaling equilibrium exists: each type asks for the quality it would prefer if its type were known. Section 3.3 then asks whether a different pair of requests could separate the types when that equilibrium fails. The Appendix, under “No Other Separating Equilibrium under the O-Learning Customization,” establishes nonexistence below the same threshold. It is this latter claim, for every request pair and every admissible off-path belief, that is the mission's target.

Setting

A buyer has one-unit demand and a privately known quality preference $\theta\in\{\theta_H,\theta_L\}$, where $\theta_H>\theta_L>0$. A fraction $\alpha\in(0,1)$ of buyers have the high preference. Quality is a real number $q\ge0$. Producing or delivering a product of quality $q$ costs $kq^2$, while preparing to sell it costs $sq^2$, with $k,s>0$. The latter is sunk before the price is determined. These are the assumptions of §2 of the paper, pp. 5–9.

Under O-Learning, the buyer requests a quality. The seller observes the request, forms a perceived type $\hat\theta$, and accepts or rejects. If rejected, both parties receive zero. If accepted, the price-setting stage follows the paper's reduced-form bargaining rule: the seller has the opportunity to make the price offer with probability $\gamma\in(0,1)$ and the buyer has it with probability $1-\gamma$. The buyer's expected payoff, conditional on acceptance, is equation (9):

$$\mu(q,\theta,\hat\theta) =\gamma\max\{\theta q-\hat\theta q,0\} +(1-\gamma)\max\{\theta q-kq^2,0\}.$$

The seller accepts precisely when $\gamma(\hat\theta q-kq^2)-sq^2\ge0$, including equality. A separating pure-strategy equilibrium consists of two distinct, nonnegative requests $q_H$ and $q_L$, plus a belief about the buyer's type after each possible request. The seller identifies the correct type at $q_H$ and $q_L$; away from those two requests its belief can vary. Given that belief and the seller's acceptance rule, neither buyer type can improve its payoff by making any other nonnegative request. The pricing stage is represented by the payoff formula rather than by a separate bargaining game, as in §3.3 of the source.

For a buyer whose type is known, equation (10) gives the complete-information request

$$q^*(\theta)=\min\left\{\frac{\gamma\theta}{s+\gamma k},\frac{\theta}{2k}\right\}.$$

Proposition 3 defines three ratios and their combined threshold:

$$\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s},\qquad \Lambda_{H2}=\frac{1+\gamma}{1-\gamma},\qquad \Lambda_L=\frac{s}{\gamma k},\qquad \Lambda=\max\{\min(\Lambda_{H1},\Lambda_{H2}),\Lambda_L\}.$$

The prior $\alpha$ is part of the model, although the separation threshold does not depend on it.

Formalization targets

No separation below the threshold

The goal says that, whenever the standing assumptions hold,

$$\frac{\theta_H}{\theta_L}<\Lambda \quad\Longrightarrow\quad \text{there is no separating pure-strategy equilibrium of the O-Learning game}.$$

Equivalently, the existence of any such equilibrium requires $\theta_H/\theta_L\ge\Lambda$. The goal quantifies over all pairs of nonnegative requests and all belief functions consistent at those requests. It does not prescribe the requests $q^*(\theta_H),q^*(\theta_L)$ or Proposition 3's supporting off-path beliefs.

The milestone list follows the two failure regimes stated in the Appendix, pp. 28–29. When $\theta_H/\theta_L<\min\{\Lambda_{H1},\Lambda_{H2}\}$, it first identifies the low type's equilibrium request and then rules out separation. When $\theta_H/\theta_L<\Lambda_L$, it records the form of $q^*$ and the bounds on acceptable equilibrium requests before ruling out separation in either order of $q_H$ and $q_L$. These are the author's stated intermediate claims, with their source text attached to each milestone.

Significance

Proposition 3 shows when the two complete-information requests can be sustained as a separating equilibrium. The Appendix result strengthens the interpretation of its threshold: below $\Lambda$, changing the requests or the off-path beliefs cannot restore separation. This matters for the paper's comparison of who controls quality design and when customization can reveal preferences. Without the nonexistence result, the failure of the cheap-signaling request profile would leave open another separating profile with distorted qualities.

The result is proved in the SSRN author copy, and this mission asks for a machine-checked version of that proof. The proposed definitions and statements compile as Lean declarations, but their proofs are open. A completed development would also supply reusable calculations about the seller's acceptance range and buyer payoffs with quadratic costs and endogenous beliefs. The milestones identify these specific pieces of work; they do not claim that a general signaling-game library is already formalized.

Difficulty

Ruling out just the request profile $q^*$ would be insufficient. An equilibrium candidate can use another pair of qualities and can assign either type to requests outside its path. Acceptance changes the payoff discontinuously: a request that would be attractive if accepted instead pays zero when rejected. The buyer's conditional payoff also contains two $\max\{\cdot,0\}$ terms, so a polynomial formula obtained on an accepted range need not hold at every quality. The main challenge is to control all deviations and beliefs under the actual acceptance rule, while maintaining the strict threshold inequalities in both failure regimes.

Formalization scope

Lean uses a two-constructor buyer type, a model with real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$, and a predicate for the paper's standing assumptions: $\theta_H>\theta_L>0$, $0<\alpha<1$, $0<\gamma<1$, $k>0$, and $s>0$. Requests and deviations are restricted to $q\ge0$. Beliefs are total functions from real requests to the two named types, constrained only at the equilibrium requests. Seller acceptance is the printed inequality and accepts at equality; a rejected request pays zero. The conditional payoff retains both maxima from equation (9), and $\Lambda$ is the printed expression, not a value defined through equilibrium existence. No fixed cost for learning or customization is included, as in the paper's main analysis.

The equilibrium predicate does not fix off-path beliefs, require the requests to equal $q^*$, or replace seller acceptance with a derived threshold. The proof therefore cannot become a restatement of Proposition 3. The local O-Learning definitions duplicate the draft model of the companion mission because unpublished drafts cannot be imported. The paper's last sentence on p. 19 calls the cheap-signaling equilibrium “the only separating equilibrium.” The Appendix proves nonexistence when the ratio is below $\Lambda$; it does not establish global uniqueness when the ratio is above it, and global uniqueness is false. This mission states the Appendix's precise claim.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, author copy dated 2023-11-29, §§2 and 3.3, Proposition 3 and Appendix pp. 28–29. SSRN; Management Science DOI.

Why dispatch and pricing interact

A delivery vendor controls both how a courier serves orders and what customers pay. Serving one order per trip avoids waiting for a second order, but serving two together can save travel time when demand is high. If the vendor can change its price, it also changes the rate at which customers join the system. The preferred dispatch rule therefore depends on an economic decision as well as a queueing calculation. Chen and Hu study this interaction for a single courier in a disk-shaped market and compare the vendor's revenue under dedicated and two-order batch delivery in their paper. The present mission concerns their crowded-market results, Propositions 3 and 4, in the authors' SSRN version of 2022-09-21.

The paper first analyzes fixed demand rates, then lets the vendor choose a demand rate by setting a price. The latter decision changes the comparison: customers with a high cost of waiting favor a less crowded, dedicated service, while sufficiently patient customers can make batching more profitable. The service radius has an analogous effect. The paper's threshold is expressed through the product of wait cost and radius, so these two comparative statics describe the same switch Chen and Hu, §5 and Online Appendix A.

Delivery model and limiting revenue

A vendor is located at the center of a disk of radius $r>0$. Customers arrive at locations uniformly distributed over that disk. The vendor has one courier and chooses between dedicated delivery, one order per round trip, and batch delivery, two orders per trip. The effective demand rate is $\lambda$. A customer incurs wait cost at rate $c>0$ and has a valuation in $[0,1]$. The vendor's price induces its chosen demand rate. Chen and Hu give the dedicated service rate $\mu_D=3/(4r)$ and batch service rate $\mu_B=45\pi/[4r(32+15\pi)]$ in equations (4) and (9).

The paper uses the following expected waiting times, with variation coefficients $C_D=9/8$ and $C_B\approx0.583$:

$$W_D(\lambda,\mu,C)=\frac{\lambda C}{2\mu(\mu-\lambda)},\qquad W_B(r,\lambda,\mu,C)=\frac{1}{2\lambda}+\frac{\lambda C}{2\mu(2\mu-\lambda)}+\frac r3.$$

Dedicated delivery is evaluated for $0\le\lambda<\mu_D$; batch delivery for $0<\lambda<2\mu_B$. The first batch term is the wait to form a pair. The final term represents travel while the other order is delivered. The batch in-line wait is the paper's Kingman-based approximation for an $E_2/G/1$ queue, whereas the dedicated in-line wait uses its $M/G/1$ expression equations (5), (11), and (12).

In a finite market, the valuation distribution affects the price needed to induce demand. As the potential arrival rate grows, the paper's crowded-market revenue becomes

$$V_\infty(\lambda,w)=\lambda(1-cw).$$

For each dispatch rule, insert its wait into this function and optimize over its stable demand range. The resulting optimal revenues are denoted $\operatorname{Opt}_D(c,r)$ and $\operatorname{Opt}_B(C_B,c,r)$. The mission uses suprema to express these values. The paper motivates this limiting objective in (14)–(15) and Lemma 1 (16)–(17).

Formalization targets

One threshold for both parameters

The goal is a single $\alpha^*>0$ such that, for every $c,r>0$,

$$\operatorname{Opt}_B(C_B,c,r)>\operatorname{Opt}_D(c,r)\quad\Longleftrightarrow\quad cr<\alpha^*, \qquad \operatorname{Opt}_D(c,r)>\operatorname{Opt}_B(C_B,c,r)\quad\Longleftrightarrow\quad cr>\alpha^*.$$

Thus the wait-cost threshold at a fixed radius is $c_\infty=\alpha^*/r$, and the radius threshold at a fixed wait cost is $r_\infty=\alpha^*/c$. At the threshold the two optimized revenues agree. For the paper's numerical $C_B=0.583$, it reports $\alpha^*\approx0.1355$ Online Appendix (A.7)–(A.8).

Demand and price at the switch

As either $c$ or $r$ increases through its threshold, the optimal demand rate has a downward jump and the corresponding optimal price has an upward jump. The formal statements require both one-sided limits to exist and the inequalities between them to be strict. They cover every selection of optimal demands, including any ambiguity at the tie. These are parts (ii) of Propositions 3 and 4.

The milestones cover strict concavity of the revenue objectives, their explicit optimizers and values where attained, the single crossing of the revenue gap, the demand comparison at the tie, and the two propositions individually. The goal combines those propositions through the common product $cr$.

What the result and formalization establish

The threshold tells the vendor which dispatch rule maximizes limiting revenue after the price has been adjusted optimally. It also locates a discontinuous operational change: a small movement in customer impatience or service area across the threshold changes the chosen mode, demand rate, and price. Comparing the waiting-time formulas at one fixed demand would not provide this revenue decision, because each mode can choose a different demand rate Chen and Hu, §5.

Chen and Hu prove the paper result analytically, while the threshold and its supporting claims here are proposed Lean statements awaiting proofs. A completed formalization would connect exact claims about the rational waiting-time expressions, optimization over open stability ranges, the unique revenue crossing, and one-sided limits. It would also record which conclusions use the paper's approximated batch wait and numerically estimated coefficient. These are reusable patterns for queue-based pricing models, even though this mission formalizes this paper's particular geometry and service rules.

Where the argument is delicate

The two dispatch modes have different singular boundaries and different optimizers. The batch wait diverges as demand tends to zero, yet batch revenue can have a finite boundary supremum that is not attained for some parameter values. The dedicated objective has a different service-rate pole. Consequently, replacing either optimization with an unrestricted real supremum, or asserting that every batch supremum has a maximizer, changes the claim. The revenue comparison also needs one crossing for the full positive range of $cr$, including values beyond the range where the appendix's interior batch optimizer applies. Finally, a strict jump in demand does not by itself supply the existence of both one-sided limits; the formal statements ask for those limits explicitly Online Appendix A.

Formalization scope

Lean uses real-valued $r,c,\lambda$ and the paper's closed-form waits, service rates, and limiting revenue. The name lam denotes $\lambda$. The batch coefficient is a real parameter satisfying $0.58\le C_B\le0.59$, an explicit interval around the paper's numerical $0.583$ rather than a claimed exact evaluation of its integral. Every threshold statement assumes $c,r>0$; the auxiliary optimum statements use the page's $cr<T_B$ range when they assert an interior maximizer. The domains are $[0,\mu_D)$ and $(0,2\mu_B)$, with zero excluded for batch because its $1/(2\lambda)$ wait is singular. The optimal revenues are defined as suprema of the actual objective images. The threshold is existential and is never defined from the desired answer.

The formal development does not construct the Poisson arrival process, random trip lengths, $M/G/1$ queue, or $E_2/G/1$ approximation behind the waits. It takes the paper's equations (5) and (12) as definitions. The finite-density function $V_n$ is recorded for context, but Lemma 1's convergence from finite to limiting optimized revenue is outside this mission's milestone list; the goal is explicitly the crowded-market limit. The printed (A.6)–(A.8) contain a coefficient error in the batch value, so the formal batch value uses the corrected expression and defines the revenue gap directly from the suprema. The printed batch optimization interval includes zero, which the stated waiting-time formula does not support. Definitions for objectives, stable domains, optimal demand, and one-sided jumps are reusable within related pricing formalizations. Contributions that establish the stated optimizer, crossing, or limit claims without changing their domains are within scope Chen and Hu, equations (12), (15), (A.3)–(A.8).

Selected references

• Mingliu Chen and Ming Hu, Courier Dispatch in On-Demand Delivery, SSRN preprint 3675063, version of 2022-09-21. SSRN record and paper.
• Mingliu Chen and Ming Hu, Courier Dispatch in On-Demand Delivery, Management Science, 2023, DOI 10.1287/mnsc.2023.4858. The formal statements use the SSRN version above.

Why content bundling matters

News publishers depend on direct visits for advertising revenue, while social platforms can show publishers' content inside their own feeds. That arrangement can move reading time from the publisher's site to the platform without changing how much news a consumer reads. It can therefore change the publisher's return from improving content quality. De Cornière and Sarvary study this question in a sequential model of a monopoly newspaper, a social platform, and consumers who divide a fixed amount of attention between the two sites. Their Proposition 1 says that unilateral content bundling lowers the publisher's profit, yet can either raise or lower its equilibrium quality depending on the cost of quality. De Cornière and Sarvary, working paper, pp. 7–12.

This mission concerns the paper's unilateral content bundling regime: the platform can incorporate news into its feed without a payment or a negotiated agreement with the newspaper. The source for theorem numbering is the Toulouse School of Economics Working Paper n° 1152, August 2021. The article later appeared in Management Science in 2023. The working paper's Proposition 1, Lemmas 1–4, and equation (2) are the targets here. The paper separately studies subscription pricing, voluntary participation, and negotiated bundling; those are separate settings. De Cornière and Sarvary, working paper, §§4–6.

The game

A newspaper first chooses news quality $q\in[0,1]$. A platform next chooses a news share $\lambda\in[0,\Lambda]$ in its feed. Consumers finally allocate one unit of time between the newspaper's site and the platform. Write $T_1\in[0,1]$ for newspaper time and $T_0=1-T_1$ for platform time. The newspaper shows only news. A fraction $\lambda$ of platform time exposes the consumer to news; the remaining fraction exposes the consumer to user-generated content (UGC). News and UGC consumption are

$$x_N=T_1+\lambda T_0,\qquad x_U=(1-\lambda)T_0.$$

The representative consumer obtains utility $U(x_U,x_N)=x_U+(1+q)x_N-x_N^2/2$. When unconstrained by the available mix, the consumer wants news consumption $x_N=q$. The platform earns $R_0=(1-\lambda+\lambda\phi_0)T_0$, where one unit of UGC time yields one unit of revenue and one unit of news time yields $\phi_0$. The newspaper earns $R_1=\beta T_1+\phi_1\lambda T_0$: direct time pays $\beta$ per unit and indirect news time pays $\phi_1$. Producing quality costs $cq^2/2$, giving newspaper profit $\pi_1=R_1-cq^2/2$. De Cornière and Sarvary, working paper, pp. 8–9, equation (1).

A subgame-perfect equilibrium (SPE) specifies consumer attention after every feasible pair $(q,\lambda)$, a platform news share after every feasible $q$, and an initial quality. At each stage the chosen action maximizes that stage's payoff given the continuation strategies. The no-bundling benchmark is the same game with $\Lambda=0$, which forces $\lambda=0$. Consumer surplus is utility at the equilibrium attention allocation. De Cornière and Sarvary, working paper, pp. 9–10, §4.1.

Formalization targets

The goal is Proposition 1, comparing every bundling SPE with every benchmark SPE. Both sorts of equilibrium must exist. Publisher profit is strictly lower under bundling. Away from the crossover cost, quality and consumer surplus increase exactly in the low-cost regime:

$$\pi_1^*<\hat\pi_1,\qquad q^*>\hat q\ \Longleftrightarrow\ c<c^\dagger,\qquad CS^*>\widehat{CS}\ \Longleftrightarrow\ c<c^\dagger, \quad(c\ne c^\dagger),$$

where $c^\dagger=\bigl(\beta+\phi_1(1-2\Lambda)\bigr)/\bigl(2\Lambda(1-\Lambda)\bigr)$. A further clause records that at $c=c^\dagger$ there is an equilibrium with quality below the benchmark. De Cornière and Sarvary, working paper, p. 12, Proposition 1; p. 31, proof.

The milestones follow the paper's named results and displays: Lemma 1 gives benchmark quality $\hat q=\beta/c$ and profit $\hat\pi_1=\beta^2/(2c)$; Lemma 2 gives consumer attention $T_1(q,\lambda)=\max\{(q-\lambda)/(1-\lambda),0\}$; Lemma 3 identifies the platform share $\min\{q,\Lambda\}$; equation (2) gives the publisher's two-branch profit; the displayed definitions on p. 12 identify the branch maximizers and $c^\dagger$; and Lemma 4 characterizes equilibrium quality. The proof of Proposition 1 also states the ordering $q_L<\hat q<q_H$ and relates surplus to the optimal content mix. De Cornière and Sarvary, working paper, pp. 10–12, 31.

What the result gives

The profit and quality effects answer different questions. Even if total news consumption stays at the consumer's preferred level, moving some of that consumption onto the platform reduces the publisher's direct traffic and hence its profit. Quality responds to a comparison of the publisher's gains from direct and indirect readers. The cost threshold distinguishes when the equilibrium moves toward a higher-quality strategy that attracts direct visits and when it moves toward a lower-quality strategy consumed through the platform. Because surplus in this model rises with equilibrium quality, the same threshold governs consumer surplus. De Cornière and Sarvary, working paper, pp. 12–13, 31.

The paper proves these claims mathematically; the Lean theorems in this proposal are open statements awaiting machine-checked proofs. Formalizing the complete sequential game would produce reusable specifications for attention allocation, contingent strategies, and equilibrium comparisons in platform markets. The first-stage profit identity and the best-response theorems are also usable independently of the final comparative-static result. This mission does not assert that the article's other models have already been formalized.

Where the proof is difficult

Checking only the realized quality and platform share does not establish subgame perfection. A different quality chosen by the newspaper changes the platform's subsequent action and then the consumer's allocation; those continuation choices must be valid after every feasible deviation. The publisher's resulting objective also changes form at $q=\Lambda$. At the cost $c=c^\dagger$ the two candidate qualities both maximize profit, so an assertion about “the” equilibrium quality requires care. The article prints a low-quality choice at equality, while the game itself admits both. De Cornière and Sarvary, working paper, pp. 11–12, equation (2), Lemma 4; p. 31, proof.

Formalization scope

The Lean model uses real parameters $\beta,\phi_0,\phi_1,c,\Lambda$. The standing assumptions are exactly Table 1: $0<\phi_0,\phi_1<1$, $\phi_1<\beta$, $2\beta<c$, and $0<\Lambda<1/2$. Quality, attention, and platform share range over $[0,1]$, $[0,1]$, and $[0,\Lambda]$ respectively. The paper's earlier $\Lambda\in[0,1/2]$ convention is superseded here by its Table 1 interior range; $\Lambda=0$ appears only as the benchmark instance. Real division in the candidate formulas is used under assumptions that make every denominator nonzero. De Cornière and Sarvary, working paper, pp. 8, 10, Table 1; p. 31, proof of Lemma 4.

The pin $c\ne c^\dagger$ applies only to Proposition 1's two “if and only if” comparisons. At equality, Lemma 4 is stated with both possible equilibrium qualities, and the goal retains the strict publisher-profit comparison. The platform's share theorem excludes $q=1$, where platform time is zero and its choice is indifferent. The consumer-attention theorem assumes $\lambda<1$ before dividing by $1-\lambda$. The benchmark is an SPE with cap zero, and surplus is evaluated from utility; neither is inserted as a closed formula. Equilibrium strategies are defined by best responses after all feasible histories, and explicit existence clauses prevent claims about all SPEs from holding vacuously. These choices rule out defining equilibrium quality, benchmark quality, or surplus by the expressions that the milestones are meant to establish.

The development needs real arithmetic and interval sets from Mathlib, a model-specific strategy profile, utility and revenue definitions, and the three stagewise best-response conditions. Contributions establishing the consumer, platform, or publisher stages, the crossover case, and the final profit and surplus comparison are within scope. Subscription pricing and negotiated bundling require different games and are outside this mission.

Selected references

• Alexandre de Cornière and Miklos Sarvary, Social Media and News: Content Bundling and News Quality, Toulouse School of Economics Working Paper n° 1152, August 2021; published in Management Science, 2023. DOI: 10.1287/mnsc.2022.4341.