Optimization

Motivation

Many problems in optimization reduce to a subgradient inclusion $0\in\partial\varphi(x)$: for a smooth $\varphi$ this is the gradient equation $\nabla\varphi(x)=0$, and for an extended-real-valued $\varphi=f+g$ (a smooth loss plus an indicator or a nonsmooth regularizer) it is the first-order optimality condition of a composite problem. Newton's method is the classical way to solve such equations with a superlinear rate, but its textbook form needs $\varphi\in C^2$ and a nonsingular Hessian. Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023) design a Newton-type method in which the Hessian is replaced by Mordukhovich's second-order subdifferential $\partial^2\varphi$, and prove local superlinear convergence under two assumptions that are weaker than the usual ones: metric regularity (instead of strong metric regularity or tilt stability) and the semismooth* property of Gfrerer and Outrata.

Timeline of the ingredients:

• 1996: Poliquin and Rockafellar introduce prox-regular functions and show that, for small parameters, their Moreau envelopes are $C^{1,1}$ near the reference point and their proximal mappings are single-valued and Lipschitz there (Trans. AMS 348).
• 2002: Klatte and Kummer develop Newton methods for Lipschitzian equations through generalized derivatives (Nonsmooth Equations in Optimization, Kluwer).
• 2021: Gfrerer and Outrata define semismooth* set-valued maps and a semismooth* Newton method (SIAM J. Optim. 31).
• 2021: Mordukhovich and Sarabi give a generalized Newton method for tilt-stable minimizers of prox-regular functions (SIAM J. Optim. 31).
• 2020/2022: Khanh, Mordukhovich and Phat replace tilt stability and strong metric regularity by metric regularity of $\partial\varphi$.

Setting

Let $\varphi:\mathbb R^n\to(-\infty,\infty]$ be proper. Its limiting subdifferential $\partial\varphi(x)$ collects the limits of Fréchet subgradients at points $x_k\to x$ with $\varphi(x_k)\to\varphi(x)$. For a set $\Omega$, the regular normal cone $\widehat N_\Omega(z)$ contains the vectors $a$ with $\langle a,w-z\rangle\le o(\|w-z\|)$ for $w\in\Omega$; the limiting normal cone $N_\Omega(z)$ contains the limits of regular normals at nearby points. For a set-valued $G$, the coderivative is $D^*G(x,y)(w)=\{u:(u,-w)\in N_{\operatorname{gph}G}(x,y)\}$, and the second-order subdifferential is $\partial^2\varphi(x,v)=D^*\partial\varphi(x,v)$.

The function $\varphi$ is prox-regular at $\bar x$ for $\bar v\in\partial\varphi(\bar x)$ with modulus $r>0$ if it is l.s.c. around $\bar x$ and, for some $\varepsilon>0$, $\varphi(x)\ge\varphi(u)+\langle v,x-u\rangle-\tfrac r2\|x-u\|^2$ whenever $x,u$ lie within $\varepsilon$ of $\bar x$, $|\varphi(u)-\varphi(\bar x)|<\varepsilon$ and $v\in\partial\varphi(u)$ lies within $\varepsilon$ of $\bar v$. It is continuously prox-regular if, in addition, $\varphi(x_k)\to\varphi(\bar x)$ along every $(x_k,v_k)\to(\bar x,\bar v)$ with $v_k\in\partial\varphi(x_k)$. It is prox-bounded if it is bounded below by a quadratic function.

For $\lambda>0$, the Moreau envelope and proximal mapping are

$$e_\lambda\varphi(x)=\inf_y\Big\{\varphi(y)+\tfrac1{2\lambda}\|y-x\|^2\Big\},\qquad \operatorname{Prox}_\lambda\varphi(x)=\operatorname*{argmin}_y\Big\{\varphi(y)+\tfrac1{2\lambda}\|y-x\|^2\Big\}.$$

Algorithm 6.2 starts at $x^0\in U_\lambda=\operatorname{rge}(I+\lambda\partial\varphi)$. While $0\notin\partial\varphi(x^k)$ it sets $v^k=\lambda^{-1}(x^k-\operatorname{Prox}_\lambda\varphi(x^k))$, picks any $d^k$ with $-v^k\in\partial^2\varphi(x^k-\lambda v^k,v^k)(\lambda v^k+d^k)$, and moves to $x^{k+1}=x^k+d^k$.

The standing assumptions at a solution $\bar x$ are:

• (H1) the inclusion $-v\in\partial^2\varphi(x,v)(d)$ is solvable for every $(x,v)\in\operatorname{gph}\partial\varphi$ near $(\bar x,0)$;
• (H2) $\partial\varphi$ is metrically regular around $(\bar x,0)$;
• (H3) $\partial\varphi$ is semismooth* at $(\bar x,0)$.

Formalization targets

Goal: Theorem 6.6 (corrected parameter range)

If $\varphi$ is proper, prox-bounded, continuously prox-regular at $\bar x$ for $0\in\partial\varphi(\bar x)$ with constants $r,\varepsilon$, and (H1)–(H3) hold, then

$$\exists\,\lambda_0\in(0,r^{-1}]\ \ \forall\lambda\in(0,\lambda_0)\ \ \exists\,U\in\mathcal N(\bar x),\ U\subseteq U_\lambda:\ \text{Algorithm 6.2 is well-defined from }U\text{ and every run from }U\text{ converges Q-superlinearly to }\bar x.$$

Milestones

• Lemma 5.4: for continuous $F$, metric regularity around $\bar x$ holds iff $\|v\|\ge c\|u\|$ for all $v\in D^*F(x)(u)$, $x$ near $\bar x$.
• Lemma 5.6: $D^*F(\bar x)(u_1+u_2)\subseteq D^*F(\bar x)(u_1)+D^*F(\bar x)(u_2)$ for locally Lipschitz $F$.
• Lemma 5.5: for $C^{1,1}$ $\varphi$, $\nabla\varphi$ is semismooth* at $\bar x$ iff $\nabla\varphi(x)-\nabla\varphi(\bar x)-\partial^2\varphi(x)(x-\bar x)\subseteq o(\|x-\bar x\|)$.
• Theorem 5.7: the $C^{1,1}$ Newton method (Algorithm 5.3) converges locally Q-superlinearly under (H1)–(H3) for $\nabla\varphi$.
• Lemma 6.3 (i)–(iii), corrected: near $\bar x+\lambda\bar v$, and for $\lambda$ small, $e_\lambda\varphi$ is $C^{1,1}$, $\operatorname{Prox}_\lambda\varphi$ is single-valued, monotone and Lipschitz, and $\nabla e_\lambda\varphi(x)=\lambda^{-1}(x-\operatorname{Prox}_\lambda\varphi(x))$.
• Lemma 6.4, corrected: $x^*\in D^*\nabla e_\lambda\varphi(x,v)(v^*)\iff x^*\in\partial^2\varphi(x-\lambda v,v)(v^*-\lambda x^*)$.
• Remark 6.5, corrected: the steps of Algorithm 6.2 are the steps of Algorithm 5.3 for $e_\lambda\varphi$.

Significance

The result gives a Newton method for nonsmooth, nonconvex subgradient inclusions whose convergence does not require strong metric regularity. Example 5.2 of the paper exhibits a $C^{1,1}$ function whose gradient is metrically regular and semismooth* but not strongly metrically regular, so the theorem covers solutions that earlier generalized Newton theories exclude. Through the Moreau envelope, the method reduces to a $C^{1,1}$ gradient equation; the same reduction, with the forward–backward envelope, drives the paper's composite algorithm (the companion mission) and its applications to Lasso-type problems.

The paper's results are proved on paper; none of them, nor the underlying theory of coderivatives, second-order subdifferentials or semismooth* maps, is formalized in Mathlib. This mission produces a machine-checked development of that layer and of the convergence theorem. It also fixes a defect: as printed, Lemma 6.3 and Theorem 6.6 claim their conclusions for every $\lambda\in(0,r^{-1})$, which is false (see Formalization scope); the formal statements are the corrected ones.

Difficulty

The obvious argument says "Algorithm 6.2 is Algorithm 5.3 for $e_\lambda\varphi$, so apply Theorem 5.7". Each step of that sentence carries the difficulty. Transferring (H1)–(H3) from $\partial\varphi$ to $\nabla e_\lambda\varphi$ requires the coderivative of the inverse $(\lambda I+\partial\varphi^{-1})^{-1}$, which needs a local graphical calculus for limiting normals that Mathlib does not have. The $C^{1,1}$ property of the envelope and single-valuedness of the proximal map hold only for small $\lambda$ and near $\bar x+\lambda\bar v$: prox-regularity is local while $\operatorname{Prox}_\lambda\varphi$ minimizes globally, so a far-away deep well can capture the proximal point. Theorem 5.7 itself rests on a uniform coderivative bound from metric regularity (Lemma 5.4, a pointwise-to-uniform form of the Mordukhovich coderivative criterion) and on the semismooth* estimate (Lemma 5.5), which combines directional normal cones with the symmetry of generalized Hessians.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); definitions are stated on real inner product spaces, and $E\times F$ carries the sup norm (the cones are norm-independent).
• $\partial$ is the published analytic limiting subdifferential NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric (2.9) for functions l.s.c. around the point, which covers every function $\partial$ is applied to here.
• $\varphi$ takes values in EReal and is assumed proper; the envelope is EReal-valued, and finiteness is asserted wherever it is differentiated.
• $\operatorname{Prox}_\lambda\varphi(x)$ is the argmin set. A run of an algorithm selects any proximal point and any direction solving the Newton inclusion. The stop of Step 1 is a constant tail. Well-definedness means every partial run from $U$ can be continued.
• Metric regularity uses $\operatorname{dist}(\cdot;\emptyset)=+\infty$. Q-superlinear convergence is stated in $\varepsilon$-form, avoiding $0/0$. $C^{1,1}$ is local to a neighbourhood.
• Correction. Lemma 6.3, Lemma 6.4, Remark 6.5 and Theorem 6.6 are posed as "there is $\lambda_0\in(0,r^{-1}]$ such that for every $\lambda\in(0,\lambda_0)$", on neighbourhoods instead of $U_\lambda$. As printed they fail for $\varphi(y)=\tfrac12y^2$ on $[-5,5]$, $-1000-|y-10|$ on $[9,11]$, $+\infty$ elsewhere, with $\bar x=0$, $r=1$, $\lambda=\tfrac12$: there $\operatorname{Prox}_\lambda\varphi(x)=\{9\}$ near $0$, and Algorithm 6.2 jumps to the stationary point $9$. Lemmas 5.4–5.6 and Theorem 5.7 are posed as printed.
• Trivializing formalizations are ruled out: $\lambda_0>0$ is part of the conclusion, so the $\forall\lambda$ is never vacuous; conclusions hold for every run rather than for a run chosen by Classical.choose; and $\varphi$ is not specialized (no convexity, which would make $U_\lambda=\mathbb R^n$; no $C^2$; no strong metric regularity; no assumption that $\bar x$ is a minimizer).
• Reusable infrastructure: normal cones to graphs, limiting and directional coderivatives, metric regularity, semismooth*, prox-regularity, Moreau envelopes. Formalizations of Mordukhovich's coderivative criterion, of the scalarization formula $D^*F(\bar x)(u)=\partial\langle u,F\rangle(\bar x)$ for Lipschitz $F$, and of Poliquin–Rockafellar's Theorem 4.4 are especially welcome.

Selected references

• P. D. Khanh, B. S. Mordukhovich, V. T. Phat, A Generalized Newton Method for Subgradient Systems, arXiv:2009.10551v2, 2022; Math. Oper. Res., 2023. https://arxiv.org/abs/2009.10551
• R. A. Poliquin, R. T. Rockafellar, Prox-regular functions in variational analysis, Trans. Amer. Math. Soc. 348, 1996. https://doi.org/10.1090/S0002-9947-96-01544-9
• H. Gfrerer, J. V. Outrata, On a semismooth Newton method for solving generalized equations*, SIAM J. Optim. 31, 2021. https://doi.org/10.1137/19M1257408
• B. S. Mordukhovich, M. E. Sarabi, Generalized Newton algorithms for tilt-stable minimizers in nonsmooth optimization, SIAM J. Optim. 31, 2021. https://doi.org/10.1137/20M1329937
• B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Two classical online selection problems sit at opposite ends of an information spectrum. In the secretary problem items arrive in uniformly random order, only their relative ranks are observed, and the best possible probability of stopping on the best item tends to $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant $\approx 0.745$ of Hill and Kertz (1982), shown tight by Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017).

Correa, Cristi, Epstein and Soto (arXiv:2011.06516) interpolate between the two with the $p$-sample-driven optimal stopping problem. Each of $N$ items is sampled independently with probability $p$; the decision maker observes the relative rankings of the sampled items, then faces the remaining items online, observing relative rankings, and makes irrevocable stop/continue decisions. Stopping on the item of overall rank $i$ earns a reward $Y_i$, with $Y_1\ge Y_2\ge\cdots$. At $p=0$ and $Y=(1,0,0,\dots)$ this is the secretary problem; for adversarial $Y$ the optimal guarantee tends to $0.745$ as $p\to1$, the i.i.d. prophet constant.

For known $Y$, the paper writes a linear program over the stopping probabilities of rank-based algorithms (after Buchbinder, Jain and Singh, 2014) and takes its limit as $N\to\infty$. The analysis rests on one structural result, Theorem 2: this limiting program can be restricted, without loss, to solutions of an explicit threshold form, so that the optimal algorithm stops on an item of current rank $i$ after a time $t_i$. This mission is that theorem.

Setting

Fix $p\in[0,1)$. Time runs over $[p,1]$ (time $t$ is the fraction of the $N$ items seen so far; the sample accounts for the first fraction $p$ in the limit), and ranks $\ell=1,2,\dots$ refer to the relative rank of the current item among all items seen so far. A candidate solution is a function $q(t,\ell)$, the density of stopping at time $t$ on an item of relative rank $\ell$.

The cumulative mass of $q$ is $M_q(t)=\int_p^t\sum_{s\ge1}q(\tau,s)\,d\tau$. A solution is feasible for the continuous linear program CLP$_p$ when $q(t,\ell)\ge0$, each $q(\cdot,\ell)$ is integrable on $[p,1]$, and

$$t\,q(t,\ell)+M_q(t)\le1\qquad\forall t\in[p,1],\ \forall\ell\ge1 .$$

For $k\ge1$ the negative-binomial term is $\mathrm{nb}_{k,\ell}(t)=\sum_{j=\ell}^{k}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^{\ell}$, the probability that a NegativeBinomial$(\ell,t)$ variable is at most $k$, and

$$F_k(q)=\sum_{\ell=1}^{k}\int_p^1 q(t,\ell)\,\mathrm{nb}_{k,\ell}(t)\,dt .$$

$F_k(q)$ is the limit of the probability that the algorithm stops on an item of overall rank at most $k$. The objective of CLP$_p$ is $Y_1-\sum_{k\ge1}(Y_k-Y_{k+1})(1-F_k(q))$ for a non-increasing sequence $Y$, so any solution that increases every $F_k$ is at least as good.

A threshold sequence is a non-decreasing $(t_i)_{i\ge0}\subseteq[p,1]$ with $t_0=p$; put $T_i=\prod_{j=1}^{i}t_j$.

Formalization targets

Goal: Theorem 2 (p. 8)

For every feasible $q$ there are a feasible $q^*$ and a threshold sequence $(t_i)$ with $F_k(q^*)\ge F_k(q)$ for all $k\ge1$, such that for every $\ell\ge1$ and $t\in[p,1)$

$$t\,q^*(t,\ell)+\int_p^t\sum_{s\ge1}q^*(\tau,s)\,d\tau=1\ \ (t\ge t_\ell),\qquad q^*(t,\ell)=0\ \ (t<t_\ell),\tag{5–6}$$ $$q^*(t,\ell)=\begin{cases}T_i/t^{i+1}&t\in[t_i,t_{i+1}),\ \ell\le i,\\0&\text{else.}\end{cases}\tag{7}$$

Milestones

1. Lemma 17 (p. 28): $\mathrm{nb}_{k,\ell}$ is non-decreasing on $[0,1]$ for $1\le\ell\le k$.
2. Lemma 18 (p. 29): $\mathrm{nb}_{k,\ell}(t)$ is non-increasing in $\ell\ge1$ for $t\in[0,1]$.
3. (8) (p. 9): one mass-moving step $q_{n-1}\mapsto q_n$, which pushes each component to the right up to the envelope $\frac1t(1-M_{q_{n-1}}(t))$, keeps each component's mass, satisfies $M_{q_n}\le M_{q_{n-1}}$ in the form (8), and preserves feasibility.
4. $F_k(q_{n-1})\le F_k(q_n)$ (p. 9) for the same step.
5. Uniqueness (p. 10): for fixed thresholds, (5)–(6) have at most one feasible solution on $[p,1)$.
6. Existence (p. 10): the function (7) satisfies (5)–(6).

Significance

Theorem 2 turns an infinite-dimensional linear program over functions of two variables into the reduced problem RP$_p$, an optimization over a single non-decreasing sequence of thresholds. Every quantitative result of the paper is read off RP$_p$: the optimal ratio for each $p$, its limit as $p\to1$ (Theorem 8, mission II of this series) and the explicit lower bound $\alpha^*p$ (Theorem 9, mission III). It also identifies the optimal rank-based algorithms as threshold rules: accept the current item if it is among the $i$ best seen so far, where $i$ grows at the times $t_i$.

The result is proved in the paper. It has not been formalized, and neither has any part of the continuous-LP approach to secretary and prophet problems. The formal development produces a reusable layer: continuous stopping LPs with extended-real cumulative constraints, monotonicity of negative-binomial distribution functions in both parameters, and a rearrangement argument for integrals against monotone weights.

Difficulty

The obvious argument is to improve $q$ greedily: push each component's mass as far right as the constraint allows. One step is easy, but the step changes the constraint itself, since the envelope $\frac1t(1-M_q(t))$ depends on all components. The proof iterates, needs the thresholds $t_\ell(n)$ to be monotone in $n$, and must pass to a limit $q_\infty$ in $L^1$ with a dominating function that exists only because the smallest threshold is bounded away from $0$. The limit thresholds need not be monotone in $\ell$, and the components must then be reordered using Lemma 18. Finally, (5)–(6) are an integral equation in which each component depends on the sum of all others; identifying their unique solution with (7) needs both a uniqueness argument for a linear ODE and a telescoping computation.

Formalization scope

• A solution is a function q : ℝ → ℕ → ℝ, a representative of an element of $L^1([p,1]\times\mathbb N)$. Ranks, $k$, $i$, $j$ are 1-based; $q(\cdot,0)$ is never used. Constraints are imposed pointwise for all $t$, as printed.
• The cumulative mass $M_q(t)$ is the lower Lebesgue integral of $\sum_{s\ge1}q(\tau,s)$ in $[0,\infty]$, never a Bochner integral of a real series, which Lean would set to $0$ on divergent data.
• Integrability of each $q(\cdot,\ell)$ is part of feasibility, so $F_k$ is never a junk value.
• Equations (5)–(7) are imposed on $[p,1)$, not on $[p,1]$. At the single point $t=1$ the printed (5) and (7) contradict each other whenever finitely many thresholds are below $1$ (already for $q=0$). Feasibility of $q^*$ is required on all of $[p,1]$.
• The threshold intervals $[t_i,t_{i+1})$ are half-open, as in (7); they are pairwise disjoint because $(t_i)$ is non-decreasing.
• "Increasing" in Lemma 17 and "decreasing" in Lemma 18 are read as non-decreasing and non-increasing.
• The mass-moving step (milestones 3–4) takes the thresholds $t_\ell(n)$ as hypotheses satisfying their defining equation, and requires them to be positive (this only matters at $p=0$, where the paper's equation already forces it).
• Milestone 6 assumes $t_1>0$, and claims (5) at $t$ when $t<t_i$ for some $i$ or when $T_m/t_m^m\to0$; on the page these conditions are implicit, and without them the claim fails.
• A statement of Theorem 2 that keeps only "there is a feasible $q^*$ with $F_k(q^*)\ge F_k(q)$" is trivial ($q^*=q$); equations (5)–(7) are part of the goal and must not be dropped.
• Mathlib supplies interval and lower Lebesgue integrals, series in $[0,\infty]$ and binomial coefficients. Contributions welcome: the negative-binomial lemmas, the rearrangement inequality for monotone weights, and a Grönwall-type uniqueness argument for the integral equation.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021. https://arxiv.org/abs/2011.06516
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2), 1982. https://doi.org/10.1214/aop/1176993861
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms for a random stream of customers, ACM EC 2017. https://doi.org/10.1145/3033274.3085137
• N. Buchbinder, K. Jain, M. Singh, Secretary problems via linear programming, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0604

Why static prices in vehicle sharing

In one-way car sharing, bike sharing and ride hailing, a vehicle that serves a trip from location $i$ to location $j$ ends up at $j$. Prices therefore do two jobs: they collect revenue and they steer the fleet. The best dynamic (state-dependent) pricing policy reacts to where every vehicle is, but computing it is a Markov decision problem over a state space that grows combinatorially with the fleet. A static policy, one fixed price per origin–destination pair, is easy to compute and to post, and the question is how much it gives up.

Waserhole and Jost (2016) bounded the loss when travel times are negligible. Banerjee, Freund and Lykouris (arXiv:1803.07841, Operations Research 2022) gave guarantees for large fleets. Benjaafar and Shen (SSRN 3998297; Operations Research Technical Note, 2023, doi:10.1287/opre.2023.2446) prove a bound valid for every fleet size $K$ that accounts for travel times, and then a sequence of progressively tighter bounds. This mission formalizes that chain.

Setting

There is a finite set $\mathcal N$ of $N$ locations and $K\ge 1$ vehicles. Trip requests from $i$ to $j$ arrive at rate $\Lambda_{ij}\ge 0$; the pairs with positive demand form $\mathcal A=\{(i,j):\Lambda_{ij}>0\}$, and the network $(\mathcal N,\mathcal A)$ is strongly connected. A trip from $i$ to $j$ lasts on average $1/\mu_{ij}$. A quantile policy $q=(q_{ij})$, $q_{ij}\in[0,1]$, is the fraction of requests that accept the posted price; the effective rates are $\lambda_{ij}=q_{ij}\Lambda_{ij}$ and $\lambda_i=\sum_j\lambda_{ij}$. Each served trip earns $I_{ij}(q_{ij})$, and $q\mapsto qI_{ij}(q)$ is concave.

The fluid problem (2) is

$$\max_q\ R_s(q)=\sum_{(i,j)\in\mathcal A}\Lambda_{ij}q_{ij}I_{ij}(q_{ij})\quad\text{s.t.}\quad\sum_j\Lambda_{ij}q_{ij}=\sum_j\Lambda_{ji}q_{ji}\ \forall i,\quad \sum_{(i,j)\in\mathcal A}\frac{\Lambda_{ij}q_{ij}}{\mu_{ij}}\le\Delta,\quad q_{ij}\in[0,1],$$

with $\Delta\ge K$. Its optimal solution $q^s$ is the static policy; it is assumed to induce a strongly connected network. The value $R_s(q^s)$ is the fluid optimum.

Under a static policy the fleet moves through a closed queueing network: a single-server pick-up queue at each location, served at rate $\lambda_i$, and an infinite-server transit queue for each pair, with mean time $1/\mu_{ij}$. The paper invokes the BCMP theorem for this network; the mission writes its stationary law as the product form. With $r$ a positive solution of the traffic equations (9), $r_i=\sum_j r_j\lambda_{ji}/\lambda_j$, a state $x$ (vehicle counts at locations and in transit, total $K$) has weight

$$w(x)=\prod_i\Bigl(\frac{r_i}{\lambda_i}\Bigr)^{x_i}\prod_{(i,j)}\frac{1}{x_{ij}!}\Bigl(\frac{r_i\lambda_{ij}}{\lambda_i\mu_{ij}}\Bigr)^{x_{ij}}.$$

The availability $\alpha_i(K)$ is the weight share of the states with $x_i\ge 1$: the probability that a customer at $i$ finds a vehicle. The reward rate of the static policy is (3):

$$R(q^s)=\sum_{(i,j)\in\mathcal A}\alpha_i\,\Lambda_{ij}q^s_{ij}I_{ij}(q^s_{ij}).$$

Finally $\Lambda=\sum_{\mathcal A}\Lambda_{ij}$, $1/\mu=\sum_{\mathcal A}\Lambda_{ij}/(\Lambda\mu_{ij})$, and $\lambda/\mu=\sum_{\mathcal A}\Lambda_{ij}q^s_{ij}/\mu_{ij}$.

Formalization targets

Goal: Theorem 2, static half (p. 9)

With $B^j_0(q^s)=B^j_0=0$ and, for $1\le i\le K$,

$$B^K_i(q^s)=\frac{K}{N+K-1+\frac{\lambda}{\mu}\bigl(1-B^{K-1}_{i-1}(q^s)\bigr)},\qquad B^K_i=\frac{K}{N+K-1+\frac{\Lambda}{\mu}\bigl(1-B^{K-1}_{i-1}\bigr)},$$

the goal is: for every $i=1,\dots,K$,

$$\frac{R(q^s)}{R_s(q^s)}\ \ge\ B^K_i(q^s)\ \ge\ B^K_i\ \ge\ \frac{K}{N+K-1+\Lambda/\mu},$$

and $B^K_{i+1}>B^K_i$ for $i=1,\dots,K-1$.

The paper's Theorem 2 begins with one more inequality, $R(q^s)/R(q^*)\ge R(q^s)/R_s(q^s)$, where $q^*$ is the best state-dependent policy. That inequality is Proposition 1 (p. 6). Its proof needs the stationary behaviour of the network under an arbitrary state-dependent policy with matrix-exponential trip times, together with Jensen's inequality and Little's law; that model is not formalized here. Proposition 1 is not part of this mission. The goal is the remaining chain, and it implies the paper's theorem once Proposition 1 is available.

Milestones

1. Equal availability under balanced flows (p. 7, Appendix p. 23): $\alpha_i(K)=\alpha_j(K)$.
2. The ratio equals the availability (pp. 7–8): $R(q^s)/R_s(q^s)=\alpha$.
3. Equation (5) (p. 8): $\alpha(K)=K/\bigl(K+N-1+\frac{\lambda}{\mu}(1-\alpha(K-1))\bigr)$.
4. Theorem 1, static half (p. 7): $R(q^s)/R_s(q^s)\ge K/(K+N-1+\Lambda/\mu)$.
5. Equation (6) and $0\le\alpha(K-i)\le(K-i)/(N+K-i-1)$ (p. 9).
6. $B^K_K(q^s)=\alpha(K)$ (p. 10).
7. $B^K_{i+1}(q^s)>B^K_i(q^s)$ (p. 10).

Significance

The bound $K/(N+K-1+\Lambda/\mu)$ holds for every fleet size, tends to $1$ at rate $O(1/K)$, and reduces to the Waserhole–Jost bound when travel times vanish. The sequence $B^K_i(q^s)$ gives a computable certificate between that bound and the exact ratio $B^K_K(q^s)=\alpha(K)$, which an operator can evaluate from $N$, $K$ and the fluid solution alone. Equation (5), a one-step recursion in the fleet size for a network mixing single-server and infinite-server stations, is the reusable core: the two sibling missions (the demand-free bound of Theorem 3 and the split-network bound of Theorem 4) rest on the same recursion.

The results are proved in the paper; none is formalized elsewhere as far as a search of the platform shows. The platform has the multiclass BCMP framework and single-server closed Jackson networks, but not availability in networks with infinite-server stations, nor equation (5). This mission adds a product-form availability layer, the equal-availability lemma, the recursion (5), and the bound chain.

Difficulty

The paper derives (5) from the random observer (arrival) theorem and Little's law, and neither is available as a formal tool, so the recursion has to be obtained from the product form itself, as an identity between sums over the state spaces with $K$ and $K-1$ vehicles. Equal availability needs uniqueness, up to scale, of the positive solution of the traffic equations on a strongly connected network (a Perron–Frobenius-type fact for an irreducible stochastic matrix). In the bound chain, $B^K_i(q^s)\ge B^K_i$ needs the recursion map to be monotone in both the workload and the previous value, which holds only once $0\le B\le 1$ is established; strict monotonicity in $i$ is a double induction.

The obvious shortcut, defining $\alpha$ by the recursion (5), makes Theorem 1 a one-line consequence of $\alpha(K-1)\ge 0$ and deletes the content of the first three milestones; the mission rules it out by defining $\alpha$ as the product form.

Formalization scope

Locations form a Fintype with Nonempty; $N$ is its cardinality. Demand, travel rates, rewards and policies are functions on all ordered pairs, self-pairs included; sums over $\mathcal A$ are sums over all pairs, which agree because each summand carries $\Lambda_{ij}$. Strong connectivity, of $(\mathcal N,\mathcal A)$ and of the network induced by $q^s$, uses nonempty paths (Relation.TransGen), so every location has positive accepted demand and $\mathcal A\ne\emptyset$. Every ordered pair has a transit queue; a pair with $\lambda_{ij}=0$ has load $0$ and stays empty ($0^0=1$). All arithmetic on $K$, $N$ and $i$ is in $\mathbb R$; $B(K,0)=0$ for every $K\ge 0$, including the $B^0_0$ that the paper's definition omits. $R_s(q^s)>0$ is a hypothesis of the ratio statements, since otherwise the ratio is $0/0$. The statements keep the paper's hypothesis that $q^s$ is optimal for (2) with $\Delta\ge K$; the proofs use only feasibility and balanced flows, and the queueing milestones are stated for every balanced quantile policy inducing a strongly connected network.

The product form is a definition: the mission does not prove that it is the stationary law of the network's Markov chain (the BCMP theorem). The general closed product-form network (single-server and infinite-server stations on an arbitrary finite station set) is a separate definition and is reusable beyond this mission. Contributions welcome: proofs of (5) via normalizing constants, the traffic-equation uniqueness lemma, and the elementary bound-sequence inequalities.

Selected references

• S. Benjaafar, X. Shen, Pricing in On-Demand (and One-Way) Vehicle Sharing Networks, SSRN abstract 3998297, version of 2023-01-10. https://ssrn.com/abstract=3998297 ; Technical Note, Operations Research, 2023. https://doi.org/10.1287/opre.2023.2446
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2), 1975. https://doi.org/10.1145/321879.321887
• S. Banerjee, D. Freund, T. Lykouris, Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework, Operations Research 70(3), 2022. https://arxiv.org/abs/1803.07841
• A. Waserhole, V. Jost, Pricing in Vehicle Sharing Systems: Optimization in Queuing Networks with Product Forms, EURO J. Transportation and Logistics 5, 2016. https://doi.org/10.1007/s13676-014-0054-4
• D. K. George, C. H. Xia, Fleet-Sizing and Service Availability for a Vehicle Rental System via Closed Queueing Networks, European J. Operational Research 211(1), 2011. https://doi.org/10.1016/j.ejor.2010.12.015
• M. Reiser, S. S. Lavenberg, Mean-Value Analysis of Closed Multichain Queuing Networks, J. ACM 27(2), 1980. https://doi.org/10.1145/322186.322195

Motivation

One-way vehicle-sharing systems (car sharing, bike sharing, ride-hailing fleets) set a price for every origin–destination trip. Prices decide which trips are taken, and so they decide where vehicles end up. Pricing that depends on the current position of every vehicle is in principle optimal, but its state space grows combinatorially with the fleet. Practitioners therefore use static prices, which depend only on the origin and destination. The question is how much revenue, throughput or welfare such prices give up.

Benjaafar and Shen (SSRN 3998297; Technical Note, Operations Research, 2023, doi:10.1287/opre.2023.2446) answer this with explicit lower bounds on the performance ratio of the static policy obtained from a fluid relaxation. Banerjee, Freund and Lykouris (arXiv:1611.07624) proved the earlier guarantee, which requires the fleet size $K$ to be at least $100$ and the workload to be at most $K-2\sqrt{K\ln K}$. Benjaafar and Shen give two bounds that hold for every $K$. The first is $K/(N+K-1+\Lambda/\mu)$ (their Theorems 1–2), and it degrades when total demand $\Lambda$ grows with $K$. The second, Theorem 3, does not depend on demand or travel times at all. This mission is about Theorem 3.

Setting

There is a finite set $\mathcal N$ of $N$ locations and $K$ vehicles. Trip requests from $i$ to $j$ arrive as a Poisson process of rate $\Lambda_{ij}\ge0$, and $\mathcal A=\{(i,j):\Lambda_{ij}>0\}$ is the set of pairs with demand. The graph $(\mathcal N,\mathcal A)$ is strongly connected. A trip from $i$ to $j$ lasts a random time with mean $1/\mu_{ij}$. A static policy is a matrix $q=(q_{ij})$ of quantiles: $q_{ij}\in[0,1]$ is the fraction of $(i,j)$ customers who accept the posted price. Each accepted trip earns a reward $I_{ij}(q_{ij})$, and $q\mapsto q\,I_{ij}(q)$ is concave. A customer who finds no vehicle at the origin is lost.

Problem (2) is the fluid relaxation, in which vehicles are always available:

$$\max_q\ R_s(q)=\sum_{(i,j)\in\mathcal A}\Lambda_{ij}q_{ij}I_{ij}(q_{ij}) \quad\text{s.t.}\quad \sum_j\Lambda_{ij}q_{ij}=\sum_j\Lambda_{ji}q_{ji},\quad \sum_{(i,j)\in\mathcal A}\frac{\Lambda_{ij}q_{ij}}{\mu_{ij}}\le\Delta,\quad q_{ij}\in[0,1].$$

The first constraint balances the flows, and the second caps the workload $\lambda/\mu=\sum\Lambda_{ij}q_{ij}/\mu_{ij}$ (the mean number of vehicles in transit) by a budget $\Delta$. Let $q^s$ be an optimal solution that induces a strongly connected network.

Under a static policy the vehicles move in a closed queueing network. Each location has a single-server pick-up queue with service rate $\lambda_i=\sum_j\Lambda_{ij}q_{ij}$. Each pair has an infinite-server transit queue with mean service time $1/\mu_{ij}$. This network is of BCMP type, so its stationary law has product form. With $r$ a positive solution of the traffic equations (9), a state with $x_i$ vehicles at location $i$ and $x_{ij}$ in transit from $i$ to $j$ has weight $\prod_i(r_i/\lambda_i)^{x_i}\prod_{(i,j)}(r_i\lambda_{ij}/(\lambda_i\mu_{ij}))^{x_{ij}}/x_{ij}!$. The availability $\alpha_i(K)$ is the stationary probability that location $i$ holds at least one vehicle. The reward rate of the policy is Equation (3):

$$R(q)=\sum_{(i,j)\in\mathcal A}\alpha_i\,\Lambda_{ij}q_{ij}I_{ij}(q_{ij}).$$

Formalization targets

Goal: Theorem 3, static half

For $K\ge1$, $\Delta=K$, $q^s$ optimal for (2), inducing a strongly connected network, with $R_s(q^s)>0$:

$$\frac{R(q^s)}{R_s(q^s)}\ \ge\ 1-\left(\sqrt{\Bigl(\tfrac{N-1}{2K}+\tfrac{1}{2(N+K)}+1\Bigr)^2-1}-\Bigl(\tfrac{N-1}{2K}+\tfrac{1}{2(N+K)}\Bigr)\right).$$

The paper states the bound for $R(q^s)/R(q^*)$, where $q^*$ is the optimal dynamic policy. It passes from one ratio to the other with Proposition 1, $R(q^*)\le R_s(q^s)$ (p. 6), whose proof needs the stationary analysis of arbitrary state-dependent policies. Proposition 1 is not part of this mission. The goal implies the paper's Theorem 3 once Proposition 1 is available.

Milestones

1. Equal availability (pp. 7, 23): under balanced flows, $\alpha_i(K)=\alpha_j(K)$ for all $i,j$.
2. $R(q^s)/R_s(q^s)=\alpha$ (pp. 7–8).
3. Equation (5) (p. 8): $\alpha(K)=K/\bigl(K+N-1+(\lambda/\mu)(1-\alpha(K-1))\bigr)$.
4. $\beta(K)=K/(N+K-1+\Delta(1-\beta(K-1)))$, $\beta(0)=0$, is non-decreasing and concave (p. 10).
5. $\alpha(K)\ge\beta(K)$ for $K\ge1$ when $\lambda/\mu\le\Delta$ (p. 11).
6. $\beta(K)-\beta(K-1)\le\beta(1)=1/(N+\Delta)$ (p. 11).
7. $\beta(K)\ge\bigl(b_K-\sqrt{b_K^2-4K\Delta}\bigr)/(2\Delta)$ with $b_K=N+K-1+\Delta+\Delta/(N+\Delta)$ (p. 11).

Significance

The bound tends to $1$ at rate $1-O(1/\sqrt K)$, uniformly in demand rates, travel times and the reward functions. It is the regime-free counterpart of the $K/(N+K-1+\Lambda/\mu)$ bound: that bound is better for light demand, this one for heavy demand (Remark 7). Remark 6 reports that it is also numerically tighter than the guarantee of Banerjee et al., and unlike that guarantee it applies to every fleet size.

Formalizing it adds several things to the platform. The first is availability in closed networks of single-server and infinite-server stations, defined from the product form. Two classical facts about this model follow: availability is equal across locations under balanced flows, and it satisfies the mean-value recursion (5). Milestone 4 is a concavity statement about the throughput of a closed network in its population, and for $N=1$ it contains the concavity of the Erlang-B carried load in the number of servers. The paper does not prove it; it cites George and Xia (2011) and Shanthikumar and Yao (1988). None of these results is formalized anywhere that this mission is aware of, so the mission formalizes a proved result, not an open problem.

Difficulty

The algebra at the end (milestones 6–7 and the substitution $\Delta=K$) is elementary. Two steps are not.

Equation (5) is stated as a relation between availabilities, but its content is an identity between normalizing constants $G(K-1)/G(K)$ of the product form. The paper derives it from the arrival theorem and Little's law, and neither is available. A direct proof has to compute $G(K)$ under balanced flows, which takes a counting argument over the state space. Equal availability likewise needs the positive solution of (9) to be unique up to scale on a strongly connected network.

Concavity of $\beta$ is the hard milestone. A natural first attempt is induction on the recursion: if $\beta(K)-\beta(K-1)$ is non-increasing up to $K$, show that the next increment is no larger. The map $\beta(K-1)\mapsto\beta(K)$ is increasing and convex in its argument, and convexity points the wrong way, so increments do not propagate directly. The published proofs go through the closed-network interpretation, not through the recursion.

Formalization scope

The Lean development lives in VehicleSharePricing.DemandFree. Locations are a Fintype with Nonempty, and $N$ is its cardinality. Λ, μ, q are real matrices on all pairs, and entries outside $\mathcal A$ enter only multiplied by $\Lambda_{ij}=0$. Strong connectivity is the transitive closure of the positive-flow relation (Relation.TransGen). This guarantees $\lambda_i>0$ at every location, even for $N=1$. Availability is the product-form busy probability of the general definition ProductFormNetwork, applied to the induced network. That law is a definition that records the paper's appeal to BCMP (p. 6), not a theorem of this mission. Theorems quantify over every positive solution $r$ of (9). $R(q)$ is Equation (3) with per-location availabilities. The sequence $\beta$ is defined by its recursion, which is correct because it is a proof device, not the availability of $q^s$. All arithmetic is in $\mathbb R$, and $K-1$ appears only under $K\ge1$.

Two trivializations are ruled out. Defining $\alpha$ by the recursion (5) would make milestones 1–3 empty, and defining $R(q)$ as $\alpha R_s(q)$ would make milestone 1 empty. The hypothesis $R_s(q^s)>0$ is added because the ratio is otherwise $0/0$.

The proof of the goal uses only feasibility of $q^s$ and the strong connectivity of the induced network; optimality is kept because it is the paper's hypothesis. Contributions are welcome on any milestone. A library for normalizing constants of closed product-form networks, and the concavity of throughput in the population, would be reusable well beyond this paper.

Selected references

• S. Benjaafar, X. Shen, Pricing in On-Demand (and One-Way) Vehicle Sharing Networks, SSRN abstract 3998297, version of 2023-01-10; Technical Note, Operations Research, 2023. https://ssrn.com/abstract=3998297, https://doi.org/10.1287/opre.2023.2446
• S. Banerjee, D. Freund, T. Lykouris, Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework, Operations Research, 2022 (cited by the paper as forthcoming); arXiv:1611.07624. https://arxiv.org/abs/1611.07624
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, Journal of the ACM 22(2), 1975. https://doi.org/10.1145/321879.321887
• D. K. George, C. H. Xia, Fleet-Sizing and Service Availability for a Vehicle Rental System via Closed Queueing Networks, European Journal of Operational Research 211(1), 2011. https://doi.org/10.1016/j.ejor.2010.12.015
• J. G. Shanthikumar, D. D. Yao, Second-Order Properties of the Throughput of a Closed Queueing Network, Mathematics of Operations Research 13(3), 1988. https://doi.org/10.1287/moor.13.3.524

Motivation

One-way vehicle-sharing systems (car sharing, bike sharing, on-demand fleets) move a fixed fleet of $K$ vehicles among $N$ locations. Customers take a vehicle at one location and leave it at another, so prices shape both revenue and where the fleet ends up. The optimal dynamic pricing policy, which reacts to the current position of every vehicle, solves a dynamic program whose state space grows combinatorially in $N$ and $K$. Static policies, with one fixed price per origin–destination pair, are simple to compute and to operate, and the question is how much they lose.

Benjaafar and Shen (SSRN 3998297; Operations Research, 2023, doi:10.1287/opre.2023.2446) take the static policy $q^s$ that solves a fluid relaxation, Problem (2), and bound its performance ratio. When $q^s$ induces a strongly connected network, Theorem 1 gives the ratio $K/(N+K-1+\Lambda/\mu)$. Waserhole and Jost (2016) observed that the best static policy may deliberately disconnect the network: prices that make some trips unattractive can leave two or more separate networks. The fleet then has to be split among the pieces, and Theorem 1 no longer applies. This mission formalizes Theorem 4 of the paper (§6, p. 18), which shows that the same guarantee holds in that case, provided the vehicles are allocated optimally among the networks.

Setting

There are $N$ locations and $K$ vehicles. Trip requests from location $i$ to $j$ arrive at rate $\Lambda_{ij}\ge0$, and $\mathcal A=\{(i,j):\Lambda_{ij}>0\}$ is strongly connected. A trip on $(i,j)$ lasts on average $1/\mu_{ij}$. A static policy is a vector of quantiles $q_{ij}\in[0,1]$ (the fraction of customers who accept the price), and earns $I_{ij}(q_{ij})$ per trip, with $q\mapsto qI_{ij}(q)$ concave.

Problem (2) maximises the fluid reward $R_s(q)=\sum_{\mathcal A}\Lambda_{ij}q_{ij}I_{ij}(q_{ij})$ over balanced flows ($\sum_j\Lambda_{ij}q_{ij}=\sum_j\Lambda_{ji}q_{ji}$ at every location) with workload $\sum_{\mathcal A}\Lambda_{ij}q_{ij}/\mu_{ij}\le\Delta$, where $\Delta\ge K$. Let $q^s$ be an optimal solution.

The policy $q^s$ splits the locations into networks $c$ with location sets $\mathcal N_c$ ($N_c=|\mathcal N_c|$) and pair sets $\mathcal A_c$: accepted demand $\Lambda_{ij}q^s_{ij}>0$ only joins locations of the same network, and within each network it is strongly connected. With $K_c$ vehicles, network $c$ is a closed queueing network: a single-server pick-up queue at each location (rate $\lambda_i=\sum_j\Lambda_{ij}q^s_{ij}$) and an infinite-server transit queue on each pair. Its stationary law is the BCMP product form, with loads computed from a positive solution $r$ of the traffic equations (9). The availability $\alpha(q^s,K_c,N_c)$ is the stationary probability that a location of network $c$ has a vehicle.

An allocation $\mathbf K=(K_c)$ with $\sum_cK_c=K$ earns $R(q^s,\mathbf K)=\sum_{\mathcal A}\alpha_i\Lambda_{ij}q^s_{ij}I_{ij}(q^s_{ij})$ (Equation (3)), and Problem (8) chooses $\mathbf K^*$ to maximise it. Write $M_c=\sum_{\mathcal A_c}\Lambda_{ij}q^s_{ij}/\mu_{ij}$, $p_c$ for network $c$'s share of $R_s(q^s)$, $\Lambda=\sum_{\mathcal A}\Lambda_{ij}$ and $1/\mu=\sum_{\mathcal A}\Lambda_{ij}/(\Lambda\mu_{ij})$.

Formalization targets

Goal: Theorem 4, static half (p. 18)

$$\frac{R(q^s,\mathbf K^*)}{R_s(q^s)}\ \ge\ \frac{K}{N+K-1+\Lambda/\mu}.$$

The paper's Theorem 4 opens with $R(q^s,\mathbf K^*)/R(q^*)\ge R(q^s,\mathbf K^*)/R_s(q^s)$, where $R(q^*)$ is the reward of the optimal dynamic policy. That inequality is Proposition 1 ($R(q^*)\le R_s(q^s)$, p. 6). It needs the stationary distribution of the network under an arbitrary state-dependent policy, a controlled-Markov-chain development that is not part of this mission. The goal is the rest of the chain, and it implies the paper's theorem once Proposition 1 is available.

Milestones (p. 18–19)

1. The recursion (5) on each network: $\alpha(q^s,K_c,N_c)=K_c/(N_c+K_c-1+(1-\alpha(q^s,K_c-1,N_c))M_c)$.
2. The mixture identity $R(q^s,\mathbf K)/R_s(q^s)=\sum_c\alpha(q^s,K_c,N_c)p_c$, with $\sum_cp_c=1$.
3. The per-network bound $p_cK_c/(N_c+K_c-1+M_c(1-\alpha(q^s,K_c-1,N_c)))\ge p_cK_c/(N_c+K_c-1+M_c)$.
4. The reduction $R(q^s,\mathbf K^*)/R_s(q^s)\ge\max_{\sum K_c=K}\sum_cp_cK_c/(N_c+K_c-1+M_c)$.
5. The Chu–Vandermonde identity $\sum_{K_1=0}^K\binom{K+T-K_1-T_1-1}{K-K_1}\binom{T_1+K_1-1}{K_1}=\binom{K+T-1}{K}$ for real $T_1,T_2>0$.
6. The reduced inequality for $C=2$: $\max_{K_1+K_2=K}\sum_{i=1}^2p_iK_i/(N_i+K_i-1+M_i)\ge K/(N+K-1+M)$.
7. The same for any number of networks, the case $C>2$.

Significance

The result. Theorem 4 removes the connectivity assumption from Theorem 1. A static policy chosen by the fluid relaxation may disconnect the network, and it then still earns at least $K/(N+K-1+\Lambda/\mu)$ of the fluid optimum, uniformly in the demand and reward data. The bound tends to $1$ as $K\to\infty$ for fixed $N$ and $\Lambda/\mu$. Milestones 6–7 hold for arbitrary weights, location counts and workloads, so they apply to any separable allocation problem whose pieces satisfy recursion (5).

Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked so far. The mission adds closed-network availability on a disconnected network, the mixture decomposition of the performance ratio, a real-argument Vandermonde identity in the paper's own notation, and a discrete allocation inequality proved by an averaging argument. The companion missions of this series formalize Theorems 1–3 of the same paper.

Difficulty

The obvious argument applies Theorem 1 to each network: $\alpha(q^s,K_c,N_c)\ge K_c/(N_c+K_c-1+M_c)$. This leaves a maximisation over allocations, and no single allocation obviously beats $K/(N+K-1+M)$. Proportional splitting fails because $N_c+K_c-1$ does not scale with $K_c$, and the best allocation depends on all of $p_c$, $N_c$ and $M_c$. The paper does not exhibit a good allocation. It averages the objective against probability weights from the Chu–Vandermonde identity, which needs binomial coefficients with real upper arguments. It then passes from two networks to many by an induction that merges networks. The recursion (5) itself rests on a computation with the normalising constants of a product form that has both single-server and infinite-server stations.

Formalization scope

Locations form a finite type. $\mathcal A$ is the set of pairs with $\Lambda_{ij}>0$, and its strong connectivity is a transitive closure. The split is a surjective map from locations onto a finite index type of networks. Every pair with positive accepted demand stays inside one class, and each class is strongly connected under accepted demand, again as a transitive closure. So every location has positive accepted demand. The paper's $C>1$ is relaxed to $C\ge1$.

Availability is the BCMP product form of each network on its own, with loads $r_i/\lambda_i$ (pick-up) and $r_i\Lambda_{ij}q_{ij}/(\lambda_i\mu_{ij})$ (transit), and $r$ a positive solution of (9). This is a disclosed definition, since the paper invokes the BCMP class without writing it. Availability is defined per location; its equality across a network follows from milestone 1. $R(q^s,\mathbf K)$ is Equation (3) with per-location availabilities. Problem (8) is an explicit maximisation over the finite set of allocations. All ratios are real numbers, $R_s(q^s)>0$ is assumed so that the ratio is defined, and $N+K-1$ is computed in $\mathbb R$.

Defining availability by the recursion (5), or $R$ as $\alpha\cdot R_s$, would make milestones 1–2 trivial and is ruled out.

A complete development needs:

• the product-form computation behind (5);
• equal availability within a network;
• the Vandermonde identity for generalized binomials (Mathlib's Ring.add_choose_eq);
• the averaging argument and the induction.

The closed-network definitions and milestones 5–7 are reusable beyond this mission. Proofs of any milestone are welcome, and so is a proof of Proposition 1.

Selected references

• S. Benjaafar, X. Shen, Pricing in On-Demand (and One-Way) Vehicle Sharing Networks, SSRN abstract 3998297, version of 2023-01-10. https://ssrn.com/abstract=3998297 ; published as a Technical Note in Operations Research, 2023. https://doi.org/10.1287/opre.2023.2446
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2), 1975, 248–260. https://doi.org/10.1145/321879.321887
• A. Waserhole, V. Jost, Pricing in Vehicle Sharing Systems: Optimization in Queuing Networks with Product Forms, EURO J. Transportation and Logistics 5(3), 2016, 293–320. https://doi.org/10.1007/s13676-014-0054-4
• D. K. George, C. H. Xia, Fleet-Sizing and Service Availability for a Vehicle Rental System via Closed Queueing Networks, European J. Operational Research 211(1), 2011, 198–207. https://doi.org/10.1016/j.ejor.2010.12.015