Probability

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

Online platforms such as ride-hailing, delivery and marketplace companies routinely test a new policy (a pricing rule, a dispatching algorithm) by switching it on and off over time on a single unit, a city or a market, rather than by randomizing over users. These switchback experiments avoid the interference that user-level randomization creates in two-sided markets, but they face a different problem: a treatment administered at one time keeps affecting outcomes for several periods afterwards (carryover effects). Bojinov, Simchi-Levi and Zhao, Design and Analysis of Switchback Experiments (arXiv:2009.00148, Management Science 69(7), 2023), derive the minimax-optimal design when the carryover lasts at most $m$ periods, and then ask how to do inference with it. This mission formalizes the inference half: under the optimal design, the Horvitz–Thompson estimator of the lag-$m$ effect is asymptotically normal as the number of epochs grows, which is what justifies the paper's normal-approximation test and confidence intervals.

The result is a finite-population central limit theorem: the potential outcomes are fixed, non-random numbers, and all randomness comes from the experimenter's coin flips. It belongs to the line of design-based limit theorems of Li and Ding (2017), Aronow et al. (2017) and Bojinov et al. (2021). Its probabilistic engine is the central limit theorem of Romano and Wolf (2000) for triangular arrays of $\phi$-dependent random variables, which goes back to the $m$-dependent central limit theorem of Hoeffding and Robbins (1948).

Setting

There are $T$ time periods $t\in[T]=\{1,\dots,T\}$. An assignment path $w_{1:T}\in\{0,1\}^T$ records treatment ($w_t=1$) or control ($w_t=0$) in each period. The potential outcomes are real numbers $Y_t(w_{1:T})$. They are assumed non-anticipating (Assumption 1: $Y_t$ depends only on $w_{1:t}$) and to have $m$-carryover effects (Assumption 2: for $t>m$, $Y_t$ does not depend on $w_{1:t-m-1}$). Assumption 3 bounds them: $|Y_t(w_{1:T})|\le B$. Write $Y_t(\mathbf 1_{m+1})$ and $Y_t(\mathbf 0_{m+1})$ for the outcome after $m+1$ consecutive treatments, respectively controls. The lag-$m$ causal effect is

$$\tau_m=\frac1{T-m}\sum_{t=m+1}^{T}\big[Y_t(\mathbf 1_{m+1})-Y_t(\mathbf 0_{m+1})\big].$$

A regular switchback design flips an independent coin with success probability $q_k\in(0,1)$ at each randomization point $t_0=1<t_1<\dots<t_K$, and every period copies the most recent coin. The Horvitz–Thompson estimator $\hat\tau_m$ weights the observed outcome at time $t$ by the inverse probability that the last $m+1$ assignments were all treatments (respectively all controls).

In the $n$-replica experiment $T=nm$, and the optimal design of the paper's Theorem 2 uses fair coins at

$$\mathbb T^*=\{1,\;2m+1,\;3m+1,\;\dots,\;(n-2)m+1\}.$$

The periods split into $n-1$ blocks $\{(k+1)m+1,\dots,(k+2)m\}$, $k=0,\dots,n-2$, with block sums $\bar Y_k(\mathbf 1_{m+1})$, $\bar Y_k(\mathbf 0_{m+1})$ and block errors $\bar{\mathbb 1}_k$, so that $\hat\tau_m-\tau_m=(T-m)^{-1}\sum_k\bar{\mathbb 1}_k$. Assumption 4 (non-negligible variance) requires $\mathrm{Var}(\hat\tau_m)\ge c/n$ for some $c>0$ and all large $n$.

Formalization targets

Goal: Theorem 3 (asymptotic normality)

For fixed $m$, under Assumptions 1–2, Assumption 3 with one bound $B$ for all $n$, and Assumption 4,

$$\frac{\hat\tau_m-\tau_m}{\sqrt{\mathrm{Var}(\hat\tau_m)}}\xrightarrow{D}\mathcal N(0,1)\qquad(n\to\infty).$$

The statement fixes no rate and does not require $\mathrm{Var}(\hat\tau_m)$ to converge.

Milestones

1. Block decomposition (EC.4.1–EC.4.2): $\hat\tau_m-\tau_m=(T-m)^{-1}\sum_{k=0}^{n-2}\bar{\mathbb 1}_k$ with $\mathbb E\bar{\mathbb 1}_k=0$.
2. 1-dependence (proof of Theorem 3): the block errors $\bar{\mathbb 1}_0,\dots,\bar{\mathbb 1}_{n-2}$ form a 1-dependent sequence.
3. Lemma 2: the closed form (10) of $\mathrm{Var}(\hat\tau_m)$ in terms of the block sums.
4. Block-variance bound (proof of Theorem 3): $B^2_{n,k,a}\le16kB^2/(n-1)^2$ for the scaled partial sums.
5. Lemma EC.1 (Romano–Wolf): the central limit theorem for $\phi$-dependent triangular arrays.

Companions

Corollary 1, the conservative bound $\mathrm{Var}(\hat\tau_m)\le\mathrm{Var}^U(\hat\tau_m)$ with the unbiased estimator $\hat\sigma^2_U$, and Corollary 2(i), that (10) still holds when the design is built for an overestimated order $p>m$.

Significance

Theorem 3 is what turns the optimal design into a usable inferential procedure: together with Corollary 1 it gives the test statistic $|\hat\tau_m|/\sqrt{\hat\sigma^2_U}$ and its normal $p$-value, a conservative large-sample test of the null of no lag-$m$ effect that needs no model for the outcomes. Corollary 2 extends the guarantee to a misspecified carryover order $p>m$. Lemma EC.1 is a general tool, applicable to any statistic that decomposes into a sum of weakly dependent pieces, such as block designs, time-series bootstraps and spatial experiments.

The paper proves these results. None of them is formalized: Mathlib has the central limit theorem for i.i.d. sequences only, and no central limit theorem for dependent arrays exists on the platform. The work here is to formalize the known proof: the exact second-moment computations of the design, the 1-dependence of the blocks, and a proof of the Romano–Wolf theorem itself, which the paper takes from the literature.

Difficulty

The randomness is a finite set of coin flips and the outcomes change with $n$, so no i.i.d. structure is available: the block errors are neither independent nor identically distributed, and the classical Lindeberg–Lévy theorem does not apply. The obvious reduction, treating neighbouring blocks as independent, fails, because adjacent blocks share a coin. This is why the cross terms appear in (10), and why a dependent-array central limit theorem is needed. The variance normalisation is random-design specific and may oscillate in $n$, so the limit theorem has to be proved with a self-normalisation that does not converge. Lemma EC.1 is the main obstacle: a $\phi$-dependent central limit theorem for triangular arrays with Lyapunov-type moment conditions, which is not in Mathlib.

Formalization scope

A path is a function ℕ → Bool of which only $1,\dots,T$ is read; potential outcomes are ℕ → Path → ℝ. The design law is encoded as independent coins at the randomization points, mapped to paths; in the $n$-replica experiment the probability space is the uniform measure on the coin vectors of $\mathbb T^*$. Row $n$ of the sequence has $T=nm$ and potential outcomes Y n. Rows $n<4$ exist in Lean but are degenerate and irrelevant to the limit. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is gaussianReal 0 1. $\Omega(n^{-1})$ and $O(1)$ are explicit constants with an eventual threshold. The estimand, estimator and variance in the goal are the model's definitions, not a hand-written formula in the coins.

Three hypotheses are added to the printed statements, each necessary and disclosed in the item's Formalization Note:

• Theorem 3 assumes Assumption 3 with one $B$ for all $n$. The page omits it, the proof uses it, and without it the statement is false.
• Lemma EC.1 assumes $d_n\to\infty$. This is Romano and Wolf's sixth condition for fixed $\phi$, and without it the lemma fails with $d_n=1$.
• Lemma EC.1 assumes $L_n>0$, which the ratios in its conditions 4–5 presuppose.

The goal does not assume 1-dependence, the variance formula or any condition of Lemma EC.1; those are milestones, so the goal cannot be discharged by a hypothesis.

A complete development needs:

• finite-coin product measures and the independence of functions of disjoint coordinates;
• exact second-moment computations for the design;
• a $\phi$-dependent central limit theorem for triangular arrays.

The last two, Lemma EC.1 and Definition EC.1, are reusable well beyond this mission. Contributions to any milestone, including alternative proofs of Lemma EC.1, are welcome.

Selected references

• I. Bojinov, D. Simchi-Levi, J. Zhao, Design and Analysis of Switchback Experiments, Management Science 69(7), 2023. https://arxiv.org/abs/2009.00148 (v4)
• J. P. Romano, M. Wolf, A more general central limit theorem for m-dependent random variables with unbounded m, Statistics & Probability Letters 47, 115–124, 2000.
• W. Hoeffding, H. Robbins, The central limit theorem for dependent random variables, Duke Mathematical Journal 15(3), 773–780, 1948.
• X. Li, P. Ding, General forms of finite population central limit theorems with applications to causal inference, Journal of the American Statistical Association 112, 1759–1769, 2017.
• I. Bojinov, N. Shephard, Time series experiments and causal estimands: exact randomization tests and trading, Journal of the American Statistical Association 114, 1665–1682, 2019.

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

Motivation

Centralized matching markets (kidney exchange, ride hailing, freight and labor platforms) repeatedly decide which waiting participants to match now and which to hold for a better opportunity later. Matching early collects value sooner; waiting lets the platform see more arrivals and avoid matches that later turn out to be wasteful. A natural yardstick is the best set of matches that could have been made with hindsight from all arrivals up to a given time, and the question is how far an online policy, which cannot see the future, must fall behind that yardstick.

Kerimov, Ashlagi and Gurvich (SSRN 3824407, September 2022; Management Science 2023, doi:10.1287/mnsc.2021.01215) answer this for multi-way matching networks with patient agents. They identify a single parameter of the fluid relaxation, the general position gap $\epsilon$, and show that the regret against the hindsight benchmark can be kept at order $\epsilon^{-1}$ at all times, and that no policy does better in order on non-trivial networks. This mission formalizes the upper bound. The paper places itself next to constant-regret results for online packing (Bumpensanti and Wang 2020; Vera and Banerjee 2021), where resolving a linear program at each arrival achieves bounded regret.

Setting

There are $n$ agent types and $d$ matches. Match $m$ is a set $\mathcal A(m)$ of at least two types, every type belongs to some match, and the matching matrix $M\in\{0,1\}^{n\times d}$ has $M_{im}=1$ iff $i\in\mathcal A(m)$. Performing match $m$ uses one agent of each type in $\mathcal A(m)$ and earns $r_m>0$. Time is discrete; at each time $t=1,2,\dots$ one agent arrives, of type $i$ with probability $\lambda_i>0$, $\sum_i\lambda_i=1$, independently over time. $A^t_i$ counts the type-$i$ arrivals by time $t$.

A matching policy records $D^t_m$, the number of times match $m$ has been performed by time $t$. It is admissible when it is non-anticipative and only matches agents present: $MD^t\le A^t$. The pre-match queue is $Q^t=A^t-MD^{t-1}$, the value collected is $\mathcal R^{D,t}=\mathbb E[r\cdot D^t]$, and the hindsight benchmark is

$$\mathcal R^{*,t}=\mathbb E\big[\max\{r\cdot y: My\le A^t,\ y\in\mathbb Z^d_{\ge0}\}\big].$$

The static-planning problem is the linear program

$$\text{(SPP)}\qquad \max\ r\cdot z\quad\text{s.t.}\quad Mz+s=\lambda,\ z\ge0,\ s\ge0.$$

For an optimal $(z^*,s^*)$ let $\mathcal M_+=\{m:z^*_m>0\}$ (active matches), $\mathcal M_0$ the rest (redundant matches), $\mathcal Q_+=\{j:s^*_j>0\}$ (under-demanded types) and $\mathcal Q_0$ the rest (over-demanded types). The network satisfies general position (GP) if (SPP) has a unique optimal solution and it is non-degenerate, $|\mathcal M_+|+|\mathcal Q_+|=n$. The general position gap is the smallest positive basic value,

$$\epsilon=\min_{m\in\mathcal M_+}z^*_m\ \wedge\ \min_{j\in\mathcal Q_+}s^*_j .$$

The exhaustive resolving policy with inter-action delay $\tau$ acts only at the epochs $t_k=k\tau$. There it performs an optimal solution of the integer program $\max\{r\cdot z: Mz\le Q^{t_k},\ z\in\mathbb Z^d_{\ge0}\}$ with the redundant matches removed, and then discards the leftover agents of the under-demanded types.

Formalization targets

Goal: Theorem 3.1 (Upper bound), p. 14

There are constants $\kappa,\Gamma>0$ depending only on $n,d,M,r$ such that, under GP, the exhaustive resolving policy with $\tau=\lceil\kappa\epsilon^{-1}\rceil$ (any tie-breaking) is admissible and

$$\mathcal R^{*,t}-\mathcal R^{D,t}\le\Gamma\,\epsilon^{-1}\qquad\text{for all }t\ge1 .$$

The constants are not fixed, so the goal survives any improvement of them.

Milestones

1. §2, p. 8: $\mathcal R^{*,t}=\max_{D}\mathcal R^{D,t}$, attained by the ultimate batching policy.
2. §4.2, (4), p. 20: under GP the optimal basis $\mathcal B$ is invertible, $(z^*_{\mathcal M_+},s^*_{\mathcal Q_+})=\mathcal B^{-1}\lambda$, and the entries of $\mathcal B^{-1}$ are bounded by a constant of the topology.
3. §4.2, p. 20: $\theta=\sum_{m\in\mathcal M_+}r_my^m$ is the optimal dual of (SPP), $\theta\ge0$, and $\theta_i>0$ on $\mathcal Q_0$.
4. Lemma 4.1, p. 19 (optimality test): a policy without redundant matches whose over-demanded queues have mean $O(\epsilon^{-1})$ has regret $O(\epsilon^{-1})$.
5. Lemma 4.2, p. 21: a Foster–Lyapunov drift condition bounds stationary means (Glynn and Zeevi 2008).
6. (11), p. 23: $\mathbb E_\pi[h^*(Q^0)]=O(\epsilon^{-1})$ for the stationary law of the epoch chain.
7. App. D, p. 49: $\mathbb E_{\mathbf 0}[h^*(Q^{t_k})]=O(\epsilon^{-1})$ for all $k\ge1$.

Here $h^*(u)$ is the $\theta$-weighted leftover in $\mathcal Q_0$ after an optimal integer matching of $u$ (display (7)).

Significance

The upper bound says that, under GP, hindsight-optimal performance up to an additive constant is achievable at every time simultaneously, not just at a known horizon. Long-run average optimality and near-optimality under discounting follow (Remark 2.1). The bound also quantifies the cost of acting often: the delay $\tau$ and the regret both scale with $\epsilon^{-1}$, so networks close to degeneracy force batching. Combined with the paper's lower bound, $\epsilon^{-1}$ is the right order on non-trivial networks.

The result has a printed proof (§4, Appendices B and D) but no machine-checked one. Several intermediate statements of the printed proof do not hold as stated and are not posed here. The goal and the stated displays (11) and App. D are posed as the paper states them, so a formal proof requires a correct argument for the uniform-in-$\lambda$ bound on the over-demanded queues. Lemma 4.1, the basis and duality facts and Lemma 4.2 are self-contained and checkable on their own.

Difficulty

The obvious approach compares the policy's realized matches with the fluid optimum $t\,z^*$ and controls the deviation with concentration bounds. That gives errors of order $\sqrt t$, not a constant. The constant comes from showing that the over-demanded queues stay of order $\epsilon^{-1}$ uniformly in time and in $\lambda$. Between epochs these queues behave like a multidimensional reflected random walk whose drift toward zero is only of order $\epsilon\tau$, while its fluctuations over an epoch are of order $\sqrt\tau$. The delay $\tau\asymp\epsilon^{-1}$ balances the two, but the queue state enters through the integer program (3), whose solution changes discontinuously with the queues, and the quantities that measure the drift are signed combinations of arrival counts, to which the usual one-sided concentration bounds for nonnegative sums do not apply. On top of this every constant must be independent of $\lambda$.

Formalization scope

• Types are Fin n and matches Fin d (0-based); the topology with its two standing assumptions ($|\mathcal A(m)|\ge2$, every type in a match) is a structure, and $\lambda>0$ with $\sum\lambda_i=1$ and $r>0$ are hypotheses.
• Time is $\mathbb N$; "for all $t>0$" is $t\ge1$. The arrival at time $s+1$ is the $s$-th entry of a path $\omega:\mathbb N\to$ Fin n. Expectations at horizon $t$ are finite sums over the first $t$ arrivals weighted by $\prod\lambda_{\omega_s}$, so no expectation is a default value.
• Admissible policies are non-anticipative cumulative counts with $MD^t\le A^t$ and no rejections. The resolving policy's removal of under-demanded leftovers acts on its own virtual queue, which agrees with the actual queue on $\mathcal Q_0$; its matches are feasible without removals, so it is admissible.
• (3) is solved with the redundant matches set to zero, and statements quantify over every tie-breaking selection. A selection exists (a sanity file exhibits one), so these statements are not vacuous.
• GP is a hypothesis on an explicit pair $(z^*,s^*)$; $\epsilon$ is the minimum of the positive basic values. The basis inverse is never a matrix-inverse function: statements assert the existence of a two-sided inverse.
• $h^*$ is defined in the form $\min\{\sum_{\mathcal Q_0}\theta_is_i: Mz+s=u,\ z_{\mathcal M_0}=0\}$, equivalent to (7) under the paper's reduction $\mathcal M_0=\emptyset$; $\theta$ is any solution of the complementary-slackness system, which is unique under GP.
• Every $O(\cdot)$ is an explicit constant, quantified after the topology and $r$ and before $\lambda$. Placing it after $\lambda$ would turn the theorem into a per-instance boundedness statement and is ruled out.
• A trivializing formalization (some unspecified policy, a $\tau$ independent of $\epsilon$, or GP replaced by an unsatisfiable condition) is ruled out: the policy is constructed, $\tau=\lceil\kappa/\epsilon\rceil$, and a sanity file proves GP for the Figure 1 network with $\epsilon=1/5$.
• Not posed: the lower bound of Theorem 3.1, Proposition 4.1 (8)–(9), Lemmas B.1–B.2, Proposition B.1 and displays (21)–(22), which do not hold as printed; Theorem 5.2 and §6.

Contributions welcome: proofs of the LP facts (milestones 2–3) and Lemma 4.1, a Mathlib-ready proof of Lemma 4.2, and any correct argument for the epoch bounds.

Selected references

• S. Kerimov, I. Ashlagi, I. Gurvich, Dynamic Matching: Characterizing and Achieving Constant Regret, SSRN 3824407 (version of Sep 14, 2022); Management Science, 2023. https://ssrn.com/abstract=3824407, https://doi.org/10.1287/mnsc.2021.01215
• P. W. Glynn, A. Zeevi, Bounding stationary expectations of Markov processes, in Markov Processes and Related Topics, IMS Collections 4, 2008. https://doi.org/10.1214/074921708000000381
• P. Bumpensanti, H. Wang, A re-solving heuristic with uniformly bounded loss for network revenue management, Management Science 66, 2020. https://doi.org/10.1287/mnsc.2019.3365
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997.

Learning treatment policies from logged data

Many decisions are made by assigning one of several actions to an individual on the basis of observed features: which of $d$ drugs to prescribe, which of several promotions to show, which job-training programme to offer. Experimentation is often costly or unethical, while historical records of past assignments and their outcomes are plentiful. Offline policy learning asks for a rule that maps features to actions, chosen from such observational records, whose expected outcome is close to that of the best rule in a prescribed class. The binary-action case was settled by Kitagawa and Tetenov (2018) with known propensities and by Athey and Wager (2021) with estimated ones; Zhou, Athey and Wager extend the doubly robust approach to $d \ge 2$ actions. This mission formalizes the statistical half of that paper: the regret guarantee of its cross-fitted learner.

Timeline. Robins, Rotnitzky and Zhao (1994) introduced augmented inverse-propensity weighting (AIPW). Dudík, Langford and Li (2011) used doubly robust scores for multi-action policy evaluation and optimization. Chernozhukov et al. (2018) showed that cross-fitting removes the bias of flexible nuisance estimates in semiparametric estimation. Athey and Wager proved $\sqrt n$-rate regret for binary actions with VC classes. Zhou, Athey and Wager (arXiv 2018; Operations Research, 2023) treat $d$ actions with a Hamming entropy integral as the complexity measure.

Setting

There are $d$ actions, written $1,\dots,d$ and identified with the standard basis vectors of $\mathbb R^d$, so that for $\gamma\in\mathbb R^d$ the inner product $\langle\pi(x),\gamma\rangle$ is the coordinate $\gamma_{\pi(x)}$. A draw consists of features $X\in\mathcal X$, potential outcomes $(Y(1),\dots,Y(d))$ and a logged action $A$; only the triple $(X,A,Y)$ with $Y=Y(A)$ is observed. The data are $n$ iid draws.

The model consists of a law $P_X$ of the features and two conditional laws given $X=x$: one for the outcome vector, one for the action. Given $X$ the two are independent (unconfoundedness). The propensity is $e_a(x)=P(A=a\mid X=x)$ and the mean reward is $\mu_a(x)=\mathbb E[Y(a)\mid X=x]$. A policy is a map $\pi:\mathcal X\to\{1,\dots,d\}$ from a class $\Pi$. Its value is $Q(\pi)=\mathbb E[Y(\pi(X))]$ and its regret is $R(\pi)=\sup_{\pi'\in\Pi}Q(\pi')-Q(\pi)$.

The learner, CAIPWL (Algorithm 1), divides the sample into $K\ge2$ evenly sized folds. For each fold $k$ it fits estimators $\hat\mu^{-k}_a$, $\hat e^{-k}_a$ on the observed data outside fold $k$, forms the cross-fitted AIPW score

$$\hat\Gamma_{i,j}=\hat\mu^{-k(i)}_j(X_i)+\mathbf 1\{A_i=j\}\frac{Y_i-\hat\mu^{-k(i)}_{A_i}(X_i)}{\hat e^{-k(i)}_{A_i}(X_i)},$$

and returns a maximizer $\hat\pi_{CAIPWL}$ over $\Pi$ of $\hat Q_{CAIPWL}(\pi)=\frac1n\sum_i\hat\Gamma_{i,\pi(X_i)}$. The oracle score $\Gamma_i$ is the same expression with the true $\mu$ and $e$; it gives $\tilde Q(\pi)=\frac1n\sum_i\Gamma_{i,\pi(X_i)}$. Write $\Delta$, $\tilde\Delta$, $\hat\Delta$ for the differences $Q(\pi_1)-Q(\pi_2)$, $\tilde Q(\pi_1)-\tilde Q(\pi_2)$, $\hat Q(\pi_1)-\hat Q(\pi_2)$, and

$$V_*=\sup_{\pi_a,\pi_b\in\Pi}\mathbb E\big[(\Gamma_{\pi_a(X)}-\Gamma_{\pi_b(X)})^2\big].$$

The complexity of $\Pi$ is measured through the Hamming distance $H(\pi_1,\pi_2)=\frac1m\#\{j:\pi_1(x_j)\ne\pi_2(x_j)\}$ on points $x_1,\dots,x_m$. The covering number $N_H(\varepsilon,\Pi)$ is the supremum over all finite point sequences of the least number of policies of $\Pi$ that $\varepsilon$-cover $\Pi$ in $H$. The entropy integral is $\kappa(\Pi)=\int_0^1\sqrt{\log N_H(\varepsilon^2,\Pi)}\,d\varepsilon$.

The assumptions are: overlap, $e_a(x)\ge\eta>0$; bounded rewards, $|Y(a)|\le B$; Assumption 2, $\mathbb E[(\hat\mu^{-k}_a-\mu_a)^2]\cdot\mathbb E[(\hat e^{-k}_a-e_a)^2]=o(1)/n$; and Assumption 3, $N_H(\varepsilon,\Pi)\le C\exp(D\varepsilon^{-\omega})$ with $0<\omega<1/2$.

Formalization targets

Goal: Theorem 3 in the form of Remark 8, (18), p. 22

$$R(\hat\pi_{CAIPWL})=O_p\Big(\kappa(\Pi)\sqrt{\tfrac{V_*}{n}}\Big),$$

read per $n$: for every $\varepsilon>0$ there are $M>0$ and $N$ with $\mathbb P\big(R(\hat\pi_{CAIPWL})>M\kappa(\Pi)\sqrt{V_*/n}\big)\le\varepsilon$ for all $n\ge N$. This is the paper's own "simpler way of stating the regret bound in Theorem 3". It fixes the rate and the dependence on $\kappa(\Pi)$ and $V_*$, but no constants.

Milestones

1. Lemma 1 (1): the inner product distance $I_\Gamma$ satisfies the triangle inequality.
2. (48): $\mathbb E[\tilde Q(\pi)]=Q(\pi)$.
3. (17): $\hat\Delta-\tilde\Delta=\sum_j(S^j_1+S^j_2+S^j_3)$, the algebraic split into error terms.
4. Lemma 3 (pinned): $\sup_{\pi_1,\pi_2\in\Pi}|\hat\Delta-\tilde\Delta|=o_p(n^{-1/2})$.
5. Oracle concentration (Lemma 2 as used in (18), pinned): $\sup_{\pi_1,\pi_2\in\Pi}|\tilde\Delta-\Delta|=O_p(n^{-1/2})$.
6. (18): $R(\hat\pi)\le\sup_{\pi_1,\pi_2\in\Pi}|\hat\Delta-\Delta|$ for every empirical maximizer.

Printed statements not posed

• Theorem 3's explicit display, $R\le(54.4\sqrt2\kappa(\Pi)+435.2+\sqrt{2\log(1/\delta)})\sqrt{V_*/n}$, together with Theorem 1, Lemma 2 (11) and Theorem 2, is not posed. Lemma 1(2), which the proof of Theorem 1 uses, is false. With three points, $d=2$, $\pi_0\equiv1$, $\pi_k$ switching to action 2 at the point $k$ only, and $\gamma_i=(1,0)$, one gets $N_{I_\Gamma}(0.7)=4>3\ge N_H(0.49)$.
• The $\sqrt{V_*}$ scaling of Theorem 1 fails for interval-switching classes, where $\kappa(\Pi)$ stays bounded, $V_*=2p$, and the Rademacher complexity is of order $\sqrt{p\log(1/p)}$.
• $54.4\sqrt2(\kappa+8)$ equals $54.4\sqrt2\kappa+435.2\sqrt2$, not $54.4\sqrt2\kappa+435.2$.
• The $o(1/\sqrt n)$ and $o_p(1/\sqrt n)$ remainders cannot be absorbed into one explicit constant at a fixed probability.
• Lemma 1(2) is not posed, being false.

Significance

The theorem shows that a learner can use flexible machine-learning estimates of the propensities and outcome regressions, each converging more slowly than $n^{-1/2}$, and still attain the regret rate of an oracle that knows them, provided the product of their errors is $o(n^{-1/2})$. This doubly robust rate condition is what makes cross-fitted AIPW scores usable for policy learning with random forests, boosting or neural-network nuisances. The dependence on $\Pi$ only through $\kappa(\Pi)$ covers the multi-action classes the paper uses later, such as depth-$L$ decision trees.

On formalization: the result is proved on paper, with explicit constants that are not established as printed. No machine-checked proof of any part of it is known. A complete development would give a checked doubly robust policy-learning guarantee with the hypotheses a correct proof needs, stated explicitly. It would also deliver, as by-products, a checked uniform-entropy bound for empirical processes indexed by policy differences and a cross-fitting lemma with fold-wise conditional independence.

Difficulty

Two parts are hard. The oracle concentration needs a chaining (Dudley-type) bound for the empirical process $\{\tilde\Delta(\pi_1,\pi_2)-\Delta(\pi_1,\pi_2)\}$, indexed by pairs of policies, in which the covering numbers are uniform over point sets and the entropy integrand uses $\varepsilon^2$. Bounding one fixed pair by a central limit theorem is not enough, because the supremum over $\Pi\times\Pi$ is the whole point. Lemma 3 needs the conditional independence that cross-fitting creates: given the data outside fold $k$, the terms of fold $k$ are iid with conditional mean zero in the first two error terms of (17). The uniform $o_p(n^{-1/2})$ bound then comes from a localized chaining argument whose radius shrinks with the nuisance errors. A naive argument conditioning on all the data at once loses the mean-zero structure.

Formalization scope

Actions are Fin d; policies are deterministic maps X → Fin d (endnote 3, p. 45), and a class is Pol : Set (X → Fin d). The model is a probability measure PX with two Markov kernels κY, κA, and the joint law is PX ⊗ₘ (κY ×ₖ κA). This builds unconfoundedness into the law. The sample of size $n$ is the product measure on Fin n → Draw X d. Estimators of fold $k$ are functions of the observed triples indexed by {i // fold n i ≠ k}, so they cannot see fold $k$ or unobserved potential outcomes. The regret uses $\sup_{\pi'\in\Pi}Q(\pi')$ in place of $Q(\pi^*)$. $\kappa(\Pi)$ is an ℝ≥0∞ lower integral, finite under Assumption 3. $O_p$ and $o_p$ are read for each $n$ separately: Definition 8's "$\forall n\ge N$ with probability $1-\varepsilon$" presupposes one probability space for all $n$. Bounded support is stated for each $x$ under κY x.

Hypotheses added to the printed ones:

• (i) both mean-squared errors tend to $0$ separately, in addition to (3). The proof of Lemma 3 uses separate rates, and with $\hat\mu\equiv0$, $\hat e=e$, condition (3) holds while the first term of (17) has exact order $n^{-1/2}$.
• (ii) $|\hat\mu|\le\hat B$, $\hat e\ge\hat\eta>0$, and both estimators are measurable.
• (iii) the policies are measurable, and the class is permissible: for each $m$ and action pattern, the set of point sequences on which some policy realizes the pattern is measurable.

Without (ii) and (iii), Lean's integrals of non-measurable functions are $0$ and Assumption 2 would be vacuous. The hypotheses are satisfiable: the oracle estimators $\hat\mu=\mu$, $\hat e=e$ meet every estimator condition, and a finite class of constant policies meets Assumption 3 and permissibility. The degenerate cases $\kappa(\Pi)=0$ or $V_*=0$ force zero regret, so the goal is not trivialized there.

Needed infrastructure: product measures and kernels (Mathlib), and Hamming covering numbers (local, Definition 4). Still to build: uniform-entropy chaining for bounded classes, and Talagrand/Bousquet-type concentration. Contributions are welcome on the chaining bound, the cross-fitting conditional-independence lemma, and the elementary items (48), (17) and Lemma 1(1). These are reusable in any doubly robust estimation mission.

Selected references

• Z. Zhou, S. Athey, S. Wager, Offline Multi-Action Policy Learning: Generalization and Optimization, arXiv:1810.04778v2, 2018; Operations Research 71(1), 2023. https://arxiv.org/abs/1810.04778
• S. Athey, S. Wager, Policy Learning with Observational Data, Econometrica 89(1), 2021. https://arxiv.org/abs/1702.02896
• T. Kitagawa, A. Tetenov, Who Should Be Treated? Empirical Welfare Maximization Methods for Treatment Choice, Econometrica 86(2), 2018. https://doi.org/10.3982/ECTA13288
• V. Chernozhukov et al., Double/Debiased Machine Learning for Treatment and Structural Parameters, The Econometrics Journal 21(1), 2018. https://arxiv.org/abs/1608.00060
• M. Dudík, J. Langford, L. Li, Doubly Robust Policy Evaluation and Learning, ICML 2011. https://arxiv.org/abs/1103.4601
• J. Robins, A. Rotnitzky, L. P. Zhao, Estimation of Regression Coefficients When Some Regressors Are Not Always Observed, JASA 89(427), 1994. https://doi.org/10.1080/01621459.1994.10476818