Operations Research

Motivation

After a sudden-onset disaster, humanitarian organizations (HOs) raise most of their response budget from private donors within days. Donors increasingly earmark their gifts, restricting them to a region, a program or a type of expense. Earmarking makes an appeal more attractive to a donor but lowers the share of each dollar that the HO can deploy immediately. Aflaki and Pedraza-Martinez (SSRN 3705595, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202) model how HOs set earmarking and fundraising effort under three institutional arrangements: competition, full collaboration (a coalition that fundraises and decides as one), and partial collaboration, in which HOs pool the cost of reaching donors on a common platform while each donor still chooses which HO to give to. Joint appeals such as the UK's Disasters Emergency Committee are of the last kind.

This mission formalizes the paper's equilibrium result for partial collaboration (Proposition 4): equilibria exist, equilibrium earmarking is determined by first-order conditions that do not involve the efforts, and only the HOs with the largest required funding relative to their unit performance pay for the platform, while the others free-ride.

Setting

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses a base utility $s_i \in [a_i, b_i]$, the attractiveness to donors that its earmarking level induces, and an effort $x_i \in [0, 1]$, the fraction of donors it pays to contact, at cost $C_i(x_i)$. Its unit performance $\delta_i(s_i) \in (0, 1]$ is the fraction of each donated dollar usable now, and $B_i > 0$ is its required funding. The mean donation is normalized to $1$.

Pooled effort reaches $\bar x = \min\left(\sum_{i \in I} x_i, 1\right)$ donors. A contacted donor gives to HO $i$ with the multinomial-logit probability

$$\theta^p_i(s) = \frac{e^{s_i}}{1 + \sum_{j \in I} e^{s_j}},$$

the $1$ being the option of not donating, so HO $i$ expects donations $\bar x\,\theta^p_i(s)$ and achieves total performance $\delta_i(s_i)\,\bar x\,\theta^p_i(s)$, of which only $\min(\cdot, B_i)$ is useful. HO $i$ is lexicographic (problem (10)): given the other HOs' strategies, it first minimizes its funding gap $\left(B_i - \delta_i(s_i)\bar x\theta^p_i(s)\right)^+$ over $[a_i, b_i] \times [0,1]$; among the gap minimizers it maximizes its utility $\min\left(\delta_i(s_i)\bar x\theta^p_i(s), B_i\right) - C_i(x_i)$; and an HO that is still indifferent picks a strategy maximizing its unconstrained total performance $\delta_i(s_i)\bar x\theta^p_i(s)$. A Nash equilibrium is a profile $(s, x)$ in the product of the boxes at which every HO's strategy is such a best response. Finally,

$$\alpha^p_i(s) = \min\left(\frac{B_i}{\delta_i(s_i)\,\theta^p_i(s)}, 1\right)$$

is the reach HO $i$ needs to close its own gap.

Formalization targets

Goal: Proposition 4

A pure Nash equilibrium exists. For every profile $(s, x)$ in the box, labelled so that $\alpha^p_1(s) \ge \dots \ge \alpha^p_n(s)$, with $\bar k = \#\{i : \alpha^p_i(s) = \alpha^p_1(s)\}$: $(s, x)$ is an equilibrium if and only if (i) for every $i$ there are $\lambda^p_{i1}, \lambda^p_{i2} \ge 0$ with

$$\frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\partial \theta^p_i(s)/\partial s_i}{\theta^p_i(s)} + \lambda^p_{i1} - \lambda^p_{i2} = 0, \quad \lambda^p_{i1}(a_i - s_i) = 0, \quad \lambda^p_{i2}(s_i - b_i) = 0, \tag{11}$$

and (ii) $\sum_{i=1}^{\bar k} x_i = \alpha^p_1(s)$ and $x_{\bar k+1} = \dots = x_n = 0$.

Milestones

1. (S11): $(s, x)$ is an equilibrium iff each $s_i$ maximizes $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ on $[a_i, b_i]$ and $x_i = \left(\alpha^p_i(s) - \sum_{j \ne i} x_j\right)^+$.
2. Log-concavity: $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ is log-concave on $[a_i, b_i]$.
3. Total effort: every solution of $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ with $\alpha$ sorted decreasingly has $\sum_i x_i \ge \alpha_1$.
4. Effort system: for $1 \ge \alpha_1 \ge \dots \ge \alpha_n \ge 0$ and $x \in [0,1]^n$, that system holds iff $\sum_{i \le \bar k} x_i = \alpha_1$ and $x_i = 0$ for $i > \bar k$.

Significance

The proposition separates the two decisions. Equilibrium earmarking solves each HO's own first-order condition (11) and does not depend on anyone's effort, because the pooled reach multiplies every HO's donations by the same factor. Equilibrium effort is a pure coordination outcome: the platform is funded exactly up to the largest required reach $\alpha^p_1$, and only the HOs attaining it contribute. The paper uses these facts to compare earmarking and performance across the three arrangements (its Propositions 5 and 7), and the free-riding structure is what drives the comparison of partial collaboration with competition.

The result is proved in the paper's Online Supplement (pp. S13–S14). No machine-checked version exists. The mission asks for a Lean proof of the proposition as stated, with the equilibrium defined from the HOs' lexicographic problem rather than from its characterization; the effort-system milestones are self-contained statements about a piecewise-linear fixed-point system and are reusable for other pooled-contribution games.

Difficulty

The obvious argument, "each HO maximizes $\delta_i\theta^p_i$, and the rest is bookkeeping", skips the case analysis behind (S11). Whether HO $i$'s gap can be closed depends on the others' efforts. When the others' pooled effort already covers HO $i$'s requirement, HO $i$'s gap and utility no longer depend on its base utility. Only the third, tie-breaking level of the best response then pins $s_i$ down, and without it (11) is false. The existence part needs a fixed point of the base-utility best-response map on $\prod_i [a_i, b_i]$; when HO $i$'s best response is not unique, that map is not even a function. In part (ii), the effort system $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ is not a contraction, and the paper's proof by successive elimination of indices is informal.

Formalization scope

HOs are Fin n with 0-based indices, so $\alpha^p_1$ is the value at index 0, and [NeZero n] is assumed. Strategies are in base-utility coordinates: $\delta_i : \mathbb R \to \mathbb R$ is a primitive function of $s_i$, as in the paper's problem (10). The earmarking coordinates are not modelled. All definitions live in one Setting structure with a Standing predicate, which every theorem assumes:

• $a_i \le b_i$ and $B_i > 0$;
• $C_i$ is nonnegative and strictly increasing on $[0,1]$;
• on an open interval containing $[a_i, b_i]$, $\delta_i$ is positive, differentiable and concave;
• $\delta_i \le 1$ on $[a_i, b_i]$.

$B_i > 0$ is implicit in the paper; with all $B_i = 0$ every base utility is an equilibrium strategy. Concavity of $\delta_i$ is used by the paper's proof. The HO problem (10) is printed with decision $(s_i, \bar x)$ and cost $C^p(\bar x)$. It is encoded with HO $i$'s own effort $x_i$ and own cost $C_i(x_i)$, the reading used by the paper's proof and by part (ii). The paper's "without loss of generality" ordering is the hypothesis that $\alpha^p(s)$ is antitone in the index, and $\bar k$ is the number of entries tied with the first; this gives $\bar k = n$ when all tie. Partial derivatives are Mathlib deriv of $t \mapsto \theta^p_i(s \text{ with } s_i := t)$. Every function differentiated is differentiable at the point by Standing. The pure-algebra milestones 3–4 use no game objects.

The equilibrium must not be defined by (S11) or (11); that would make the goal a tautology. The Setting defines it as the three-level lexicographic best response over the full strategy box, and (S11) is a milestone to be proved. A sorry-free check that the standing hypotheses hold for the paper's numerical primitives ($\delta_i(s) = 1 - s/4$, $C_i(x) = x/10$, $[a_i, b_i] = [0,1]$, $B = (0.2, 0.3)$) accompanies the draft.

A full development needs: KKT conditions for a differentiable concave function on a compact interval (including the degenerate interval $a_i = b_i$); log-concavity of the logistic share; a continuous-maximum (Berge-type) argument and Brouwer's fixed-point theorem on a product of intervals; and the algebra of the effort system. Contributions of the interval-KKT lemma and of the effort-system lemmas are welcome as separate theorems.

The source is the authors' SSRN version (abstract 3705595, dated December 2022); all proofs are in its Online Supplement, Section S3.

Selected references

• A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
• A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202

Fundraising competition after a disaster

In the days after a sudden-onset disaster, several humanitarian organizations (HOs) appeal to the same pool of donors. Donors increasingly want to earmark their gifts (restrict them to a programme, region or item), and HOs can offer more or less of that control. Earmarked money is less useful in the response: renegotiating restrictions costs time and overhead, so each dollar delivers less immediate relief. HOs therefore face a trade-off between attracting donors and using donations well, and they face it while competing with each other for the same donors.

A. Aflaki and A. J. Pedraza-Martinez model this trade-off as a game among HOs whose donors choose by a multinomial logit (MNL) rule, and compare three regimes: competition, full collaboration and partial collaboration (SSRN 3705595, December 2022; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202). This mission formalizes the equilibrium result for the competition regime, Proposition 1 of the paper. The source is the SSRN version dated December 2022; its proofs are in the bound-in Online Supplement (§S3).

The competition game

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses two numbers:

• a base utility $s_i \in [a_i, b_i]$ that it offers donors (in the paper, a monotone reparametrization of its earmarking level, used from problem (6) on);
• a fundraising effort $x_i \in [0,1]$, the fraction of donors it contacts, at cost $C_i(x_i)$ with $C_i : [0,1] \to \mathbb R_+$ strictly increasing.

Each dollar HO $i$ receives produces $\delta_i(s_i)$ dollars of immediate relief, the unit performance. HO $i$ needs $B_i > 0$ dollars of effective funding. Donors have mean budget $z > 0$.

A donor contacted by the set $J$ of HOs gives HO $i \in J$ the MNL share

$$\theta^J_i(s) = \frac{e^{s_i}}{1 + \sum_{j\in J} e^{s_j}}, \tag{4}$$

the $1$ standing for not donating. Contacts are independent, so with $w^a_i = \prod_{j \ne i} x_j^{a_j}(1-x_j)^{1-a_j}$ for $a \in A_i = \{a \in \{0,1\}^n : a_i = 1\}$ and $J_a = \{j : a_j = 1\}$, HO $i$'s expected donations are

$$\mathbb E[D_i(s;x)] = z\, x_i \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s). \tag{5}$$

The unit performance per donor contacted is $PPD_i(s;x) = \delta_i(s_i)\, z \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s)$; it does not depend on $x_i$.

Each HO is lexicographic (problem (6)): given the others' strategies, it first minimizes its funding gap $(B_i - \delta_i(s_i)\mathbb E[D_i(s;x)])^+$ over $[a_i,b_i]\times[0,1]$, and among the minimizers it maximizes

$$U_i(s_i,x_i) = \min\big(\delta_i(s_i)\mathbb E[D_i(s;x)],\, B_i\big) - C_i(x_i).$$

A Nash equilibrium is a profile $(s;x) \in \prod_i [a_i,b_i]\times[0,1]^n$ in which every HO's strategy solves its problem (6).

Assumption 1 (p. 16) asks that $\log\delta_i$ be sufficiently concave: $\partial^2 \log\delta_i(s_i)/\partial s_i^2 \le -\tfrac14 + e^{s_i}/(1+e^{s_i})^2$ on $[a_i,b_i]$.

Formalization targets

Goal: Proposition 1 (p. 16)

Under the standing hypotheses and Assumption 1, a Nash equilibrium exists, and a profile in the strategy box is an equilibrium if and only if for every $i$

$$x_i = \min\Big(\frac{B_i}{PPD_i(s;x)},1\Big),\qquad \frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\sum_{a\in A_i} w^a_i\,\partial\theta^{J_a}_i(s)/\partial s_i}{\sum_{a\in A_i} w^a_i\,\theta^{J_a}_i(s)} + \lambda_{i1}-\lambda_{i2} = 0,$$

with $\lambda_{i1},\lambda_{i2}\ge 0$, $\lambda_{i1}(a_i-s_i) = 0$ and $\lambda_{i2}(s_i-b_i) = 0$ (system (7)).

Milestones

1. Lemma 2 (p. 15): $\mathbb E[D_i]$ is nondecreasing in $x_i$ and $s_i$ and nonincreasing in $x_j$, $s_j$ for $j\ne i$.
2. Claim (S5) (p. S10): HO $i$'s strategy solves (6) iff $s_i$ maximizes $PPD_i$ over $[a_i,b_i]$ and $x_i = \min(B_i/PPD_i,1)$.
3. (S8) (p. S12): $\partial^2 \log\big[\sum_{a} w^a_i\theta^{J_a}_i(s)\big]/\partial s_i^2 \le \tfrac14 - e^{s_i}/(1+e^{s_i})^2$ for efforts in $[0,1]$.
4. Log-concavity (p. S12): under Assumption 1, $s_i \mapsto PPD_i$ is log-concave on $[a_i,b_i]$.

Significance

Proposition 1 is the foundation of the paper's comparison of fundraising regimes: Propositions 2, 5, 6 and 7 compare equilibria characterized by (7) with the full- and partial-collaboration outcomes, and the numerical study of the Haiti response (§8) computes equilibria by solving (7). The proposition reduces a two-level game with a non-smooth objective to a per-HO KKT system plus a closed-form effort, and it shows that equilibrium earmarking balances the relative loss in unit performance against the relative gain in donor share.

The result is proved on paper, in the Online Supplement; no machine-checked version exists. Formalizing it would check the reduction from the lexicographic problem to (S5), which hinges on $B_i>0$ and strictly increasing costs, and supply a sound proof of the bound (S8), whose printed derivation is loose (see below). The log-mixture-of-logit bound (S8) and the lexicographic best-response reduction are reusable for other MNL competition models.

Difficulty

The central difficulty is (S8). Each single share $\theta^J_i$ is log-concave in $s_i$, but a mixture of log-concave functions is not log-concave in general, so concavity of $\log\sum_a w^a\theta^{J_a}$ fails and only the weaker, $s_i$-dependent bound (S8) holds. The printed argument passes through a quasi-concavity step and a termwise inequality that do not combine as written; a correct argument must control the variance-like term of the mixture uniformly in the weights. Numerical tests on random instances support (S8).

Existence is a fixed-point argument, but Assumption 1 with "$\le$" yields only concavity, so best responses in $s_i$ can be intervals rather than points, and a single-valued map need not exist. The correspondence is convex-valued, which is where the obvious Brouwer argument needs adjustment.

The reduction (S5) requires handling both regimes of the lexicographic problem: the gap can be closed (effort $B_i/PPD_i$, minimal cost) or cannot (full effort).

Formalization scope

HOs are Fin n. The paper's sum over $a\in A_i$ is a sum over finite sets $J$ with $i\in J$; $w^a_i$ is the product of $x_j$ over $J\setminus\{i\}$ and of $1-x_j$ over $j\notin J$. All statements live in base-utility coordinates: $\delta_i:\mathbb R\to\mathbb R$ is a primitive function of $s_i$ (earmarking $e_i$ and the map $s_i(e_i,\delta_i(e_i))$ are not modelled), and expected donations are the formula (5) (Lemma 1's Gumbel derivation is not formalized).

The standing hypotheses, collected in one predicate, are: $n\ge1$; $a_i\le b_i$; $B_i>0$; $z>0$; $C_i\ge0$ and strictly increasing on $[0,1]$; $\delta_i$ twice continuously differentiable on $\mathbb R$ with $0<\delta_i\le1$ on $[a_i,b_i]$. The additions relative to the page are $B_i>0$ (without it every $s_i$ is a best response and the "only if" fails), $z>0$, $\delta_i>0$ (needed for $\log\delta_i$ and $B_i/PPD_i$), and smoothness on all of $\mathbb R$ rather than on $[a_i,b_i]$. Assumption 1 is a separate predicate, assumed only by the goal and the log-concavity milestone. Derivatives are Mathlib's deriv; $\partial\theta^{J}_i/\partial s_i$ is the derivative of $t\mapsto\theta^J_i(s_{-i},t)$.

The equilibrium is defined as the lexicographic best response of problem (6) over the full strategy box, never by (7), (S5) or an argmax of $PPD_i$; with any of those as the definition the goal would be trivial. Multipliers are existential. Uniqueness of the equilibrium is not claimed.

Welcome contributions: proofs of the milestones, a reusable lemma that the KKT conditions characterize maximizers of a concave differentiable function on a closed interval, and Kakutani-type existence for convex-valued best responses.

Selected references

• A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
• A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, 1973.

Motivation

Electric-vehicle makers such as NIO sell cars without the battery and lease the battery separately, a business model called Battery as a Service (BaaS). The leased battery can be swapped at a station in minutes, so a customer is not tied to one battery size: a driver who leases a small battery for the daily commute can rent a large one for a long holiday trip, and a driver who leases a large battery can downgrade for a while and pay less. Shi and Hu (M&SOM 2024, doi:10.1287/msom.2022.0587) ask whether such flexible battery leasing is good for all three parties at once: the manufacturer (profit), the customers (total cost) and the environment (total battery capacity that has to be produced). A business-model innovation of this kind is adopted only if it improves profit; it is defensible publicly only if it does not raise customer cost or the number of batteries in circulation. The paper's answer is a "win-win-win" region of parameters, and that result is the goal of this mission.

Setting

A manufacturer serves a unit mass of customers with two batteries. The low-capacity battery has range $r_l=0$, lease rate $p_l=0$ and acquisition cost $c_l=0$ (normalizations). The high-capacity battery has range $r_h$, lease rate $p_h$ and incremental acquisition cost $c_h$. Driving a distance beyond the battery's range costs the customer the shortfall: a need $x$ served by range $r$ costs $(x-r)^+$ plus the lease rate.

Each customer has a regular need $d\sim\mathcal U[0,1]$, known when choosing a primary battery, and a peak need $D\sim\mathcal U[0,a]$ with $a>1$, independent of $d$ and learned later. A fraction $\rho$ of the time is regular usage, $1-\rho$ peak usage. The standing assumptions are $a>1$, $a/(2+a)<\rho<1$, $0<r_h\le a$ and $0\le c_h\le(1-\rho)a$.

Simple leasing. The manufacturer sets $p_h$; each customer leases low capacity iff $\rho d+(1-\rho)\mathbb E[D]\le p_h+\rho(d-r_h)^++(1-\rho)\mathbb E[(D-r_h)^+]$. With $\tau^b$ the low-capacity volume, the profit is $\Pi^b=(1-\tau^b)(p_h-c_h)$, the total customer cost $CT^b$ is the integral over $d$ of the cost each customer bears, and the total battery capacity is $BT^b=(1-\tau^b)r_h$.

Flexible leasing. A two-period game. The manufacturer sets $p_h$; customers choose primary batteries anticipating the peak period; the manufacturer then sets an upgrade rate $\bar p_h$ and a downgrade rate $\bar p_l$; customers learn $D$ and choose whether to swap according to Table 1 of the paper (a low lessee pays $(D-r_h)^++\bar p_h$ after upgrading, a high lessee pays $D+\bar p_l$ after downgrading). Upgrades $U$ in excess of downgrades $V$ must be met by buying $Q_h=[U-V]^+$ extra high-capacity batteries. The peak-period objective is (1): $(1-\tau)p_h+V(\bar p_l-p_h)+U\bar p_h-c_hQ_h/(1-\rho)$, and the total profit is (2): $\Pi^f=\rho(1-\tau)p_h+(1-\rho)\cdot(1)-(1-\tau)c_h$. A flexible equilibrium is a lease rate $p_h$ with optimal peak rates, a lease volume $\tau$ that customers rationally expect, and a profit no other lease rate and continuation can beat. $CT^f$ is the total expected cost of the customers' choices, and $BT^f=(1-\tau+Q_h)r_h$.

Formalization targets

Write $c_0=a(1-\rho)/2$; by Proposition 2 this is the cost at which the manufacturer stops buying extra batteries.

Goal: Proposition 6 (win-win-win)

For $a>1$, $a/(2+a)<\rho<1$:

1. if $\rho<7a/(8+7a)$, there is $\delta>0$ such that for each $c_h\in(c_0-\delta,c_0)$ there is $R<a$ such that for all $r_h\in(R,a]$, a benchmark optimum and a flexible equilibrium exist, and every pair of them satisfies

$$Q^f_h>0,\qquad \Pi^b<\Pi^f,\qquad CT^f<CT^b,\qquad BT^f<BT^b;$$

2. there is $\delta>0$ such that for each $c_h\in(c_0,c_0+\delta)$ there is $R<a$ such that for all $r_h\in(R,a]$, the same holds with $Q^f_h=0$.

Milestones

Lemma 1 and Proposition 1 (the benchmark), Lemma 2 (peak volumes), Lemma 3 (optimal peak rates), Lemma 4 (flexible lease volume), Proposition 2 in its first case (the flexible equilibrium for $c_h<c_0$), Proposition 4 near the corner $(r_h,c_h)=(a,c_0)$ (customer cost), and Proposition 5 in its first bullet (capacity is smaller iff $\rho<7a/(8+7a)$ and $c_h\le T(r_h)$ for an explicit $T$).

Significance

The result identifies conditions under which a pricing innovation helps the firm, its customers and the environment at the same time: a battery cost near $a(1-\rho)/2$ and a high-capacity range close to the largest peak need. Flexible leasing reallocates high-capacity batteries from customers who do not need them in the peak period to customers who do, so fewer batteries have to be produced. But the manufacturer prices the up/downgrade options to extract the efficiency gain and may buy extra batteries, so lower customer cost and lower capacity are not automatic. Proposition 6 states where all three improvements coexist.

The paper proves its results by calculus on closed forms. Nothing here is machine-checked yet. A formalization adds three things. First, it derives the closed forms from the model itself (customer choices from Table 1, volumes as measures of customer sets, equilibria as maximizers), where the paper states them. Second, it settles which reading of "sufficiently close" and "sufficiently large" is true. Third, it records the regimes in which the intermediate lemmas hold, which the printed statements leave implicit.

Difficulty

The closed forms of Lemmas 1–4 are routine integrals of piecewise-linear functions. The difficulty is global optimality and the corner analysis.

• Equilibrium is global. A flexible equilibrium must beat every lease rate together with every rationally expected continuation, including continuations in the regime where the manufacturer buys no extra batteries and at lease rates where customers all lease one type. A first-order condition on one regime does not establish this.
• The $Q^f_h=0$ side is not the printed one. For $c_h$ just above $c_0$ the equilibrium is a kink regime that the paper does not describe. The paper's second-case formulas in Proposition 2 are not the equilibrium there, so the goal's second branch cannot be obtained from them.
• Order of limits. At the corner $(r_h,c_h)=(a,c_0)$ the two capacities coincide. Profit and customer cost are strictly better under flexible leasing there, but capacity is only weakly better. The capacity comparison holds only when $r_h$ approaches $a$ after $c_h$ is fixed.

Formalization scope

The model is the paper's base model of §3–§4: flexible leasing introduced into an existing BaaS program with independent regular and peak needs. The extensions of §5 (correlated needs, range choice, launching with flexible leasing) and the numerical calibration (§4.1, Figures 2–5) are out of scope.

Representation. All parameters are real numbers. Expectations over $D\sim\mathcal U[0,a]$ are interval integrals divided by $a$; volumes of customers are Lebesgue measures of subsets of $[0,1]$. Every volume, expected cost and equilibrium is defined from the model; the paper's closed forms are theorems, never definitions. Customers lease low when indifferent, upgrade on $\le$ and downgrade on $>$, following the proofs. The lease rate ranges over all of $\mathbb R$; the paper's remark "we require $p_h<\min(1,r_h)$" is not imposed, because the benchmark optimum can exceed 1. The peak rates range over the set $\bar p_h\le a$, $p_h-a\le\bar p_l\le p_h$ that the paper requires (p. 13). An equilibrium is optimal against every continuation at every lease rate.

Readings and added hypotheses.

• Proposition 6 is posed as "$c_h$ sufficiently close to $c_0$, then $r_h$ sufficiently large". A single neighbourhood of $(a,c_0)$ in both variables is false on both sides. On the $Q^f_h>0$ side, Proposition 5's threshold $T(r_h)$ equals $c_0$ at $r_h=a$ and is below it for $r_h<a$. The point $c_h=c_0$ is excluded.
• Each branch of the goal asserts existence of a benchmark optimum and a flexible equilibrium, so it is not vacuous. A goal of the form "every equilibrium is win-win-win" without existence would be trivially true where no equilibrium exists, and is ruled out.
• Lemma 2's interior cases hold with $r_h$ in place of $a$ (and $\bar p_h\ge0$). The statement also gives the missing outer cases for rates below zero or beyond $r_h$, covering every real rate.
• Lemma 3 is posed in the regime $\tau>c_h/(a(1-\rho))$, the only one in which its acquisition quantity is nonnegative. Its rates are assumed to lie below $r_h$.
• Lemmas 1, 4 and Propositions 1, 2, 5 carry the proofs' interior conditions as explicit parameter inequalities: the indifferent customer lies below $r_h$, and Proposition 1's range for $c_h$ holds.
• Proposition 5(i) is the $\le$ form, as in its proof. Proposition 4 is posed in its corner-neighbourhood clauses only.
• Proposition 2's second case, Proposition 3 and the remaining clauses of Propositions 4–5 are not posed: the second case of Proposition 2 is false on part of its range, and Proposition 3's threshold is garbled in the manuscript.

What a complete development needs. Lebesgue measure of intervals, interval integrals of piecewise-linear functions, and maximization of concave quadratics with a kink. It also needs the kink-regime equilibrium on the $Q^f_h=0$ side and continuity arguments at the corner. Lemmas 1–4 are reusable for any variant of the model, and proofs of the milestones in any order are welcome.

Selected references

• L. Shi and B. Hu, Battery as a Service: Flexible Electric Vehicle Battery Leasing, Manufacturing & Service Operations Management, Frontiers in Operations, 2024. Read as the authors' manuscript of 13 January 2024. https://doi.org/10.1287/msom.2022.0587

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.