Stochastic Systems

Why give data away

Firms that own data increasingly sell it as a product: market research panels, consulting reports, datasets for training demand models. A common commercial practice is to hand out a free sample of the data before quoting a price for the rest. Under standard Bayesian reasoning this practice looks self-defeating. Every free data point reduces the buyer's uncertainty, which reduces what the remaining data are worth to her. This is a holdup problem: once information is revealed, it cannot be sold.

Drakopoulos and Makhdoumi (Providing Data Samples for Free, SSRN 3611003; Management Science, 2022, doi:10.1287/mnsc.2022.4534) identify when free samples nevertheless raise the seller's revenue. The mechanism is disagreement about the prior. When the seller believes the buyer's initial estimate is biased, she expects the free data to move the buyer's belief toward states in which the buyer values the remaining data more. The paper calls this the persuasion benefit, and it can outweigh the holdup cost. This mission formalizes the paper's main theorem, Theorem 1(a), together with the lemmas its proof rests on.

The model

An unknown real parameter $\theta$ determines a buyer's payoff $u(a,\theta)$ from an action $a\in\mathbb R$. The Buyer holds the prior $\mathcal N(\theta_0,\sigma_0^2)$ with $\sigma_0^2>0$. The Seller believes $\theta_0$ is a biased estimate, with bias distributed as $\mathcal N(\mu_b,\sigma_b^2)$ and $\sigma_b^2\ge0$. Her prior is $\mathcal N(\theta_0+\mu_b,\sigma_s^2)$ with $\sigma_s^2=\sigma_0^2+\sigma_b^2$, and it is taken to be the correct one.

Data arrive continuously. The first $t\ge0$ samples are equivalent to the signal

$$Y_t=\theta t+\sigma B_t,$$

where $B$ is a standard Brownian motion independent of $\theta$ and $\sigma^2>0$ is the noise variance. Both parties agree on this law of the data given $\theta$ (they are concordant) and disagree only on the prior. The information after $t$ samples is $\mathcal F_t=\sigma(Y_s:s\le t)$.

The Buyer's posterior after $t$ samples is $\mathcal N(\theta_t,\sigma_t^2)$, with $\sigma_t^2=\sigma_0^2\sigma^2/(\sigma_0^2t+\sigma^2)$ and $\theta_t=(\sigma_t^2/\sigma_0^2)\theta_0+(\sigma_t^2/\sigma^2)Y_t$. The Seller's posterior $\mathcal N(\tilde\theta_t,\tilde\sigma_t^2)$ is given by the same formulas from her own prior. The Seller's estimate of the Buyer's error is $g_t=\tilde\theta_t-\theta_t$, and $g_0=\mu_b$.

With belief $\mathcal N(\theta,v)$, the Buyer's best expected utility is $U(\theta,v)=\max_a\mathbb E_{\mathcal N(\theta,v)}[u(a,\cdot)]$. Her Bayes risk

$$BR(\theta,v)=\mathbb E_{\mathcal N(\theta,v)}\big[\max_a u(a,\cdot)\big]-U(\theta,v)$$

is the value to her of learning $\theta$ exactly. Its second argument is a variance, and $BR_\theta$, $BR_{\theta\theta}$ and $BR_{\sigma^2}$ denote its partial derivatives.

A free-sample policy gives data for free up to a stopping amount $T$, a stopping time of $(\mathcal F_t)$, and then sells the remainder. Once the free samples stop, the best price for the remainder is $BR(\theta_T,\sigma_T^2)$ (Lemma 3). The Seller's expected revenue is therefore $\mathbb E^S_0[BR(\theta_T,\sigma_T^2)]$, computed under her prior. Selling in one round is $T=0$, with revenue $BR(\theta_0,\sigma_0^2)$.

Formalization targets

Goal: Theorem 1(a)

If the Seller-side drift of the Bayes risk is positive at the start,

$$\tfrac12 BR_{\theta\theta}(\theta_0,\sigma_0^2)-BR_{\sigma^2}(\theta_0,\sigma_0^2)+\frac{\mu_b}{\sigma_0^2}BR_\theta(\theta_0,\sigma_0^2)>0, \tag{4}$$

then some free-sample policy $T$ satisfies

$$\mathbb E^S_0\big[BR(\theta_T,\sigma_T^2)\big]>BR(\theta_0,\sigma_0^2).$$

The goal has no constants. It asserts only that the optimal free-sample policy strictly beats every one-round policy.

Milestones

• Proposition 1 (p. 13): the posteriors given the whole data path are the Gaussians above.
• Lemma 1(i)–(iii) (p. 14): the posterior variance decreases at rate $\sigma_t^4/\sigma^2$. The Buyer's estimate has drift $0$ for the Buyer and $g_t\sigma_t^2/\sigma^2$ for the Seller. Its squared increment is $\sigma_t^4/\sigma^2\,dt+O(dt^{3/2})$.
• Lemma 3 (p. 16): the Buyer pays at most $BR$ for any partial release, and exactly $BR$ for full release.
• Lemma 4(b) (p. 17): from the Seller's perspective, $\mathbb E^S[BR(\theta_h,\sigma_h^2)]$ has initial slope $\big(\tfrac12BR_{\theta\theta}-BR_{\sigma^2}+\tfrac{\mu_b}{\sigma_0^2}BR_\theta\big)\sigma_0^4/\sigma^2$.
• Lemma 4(a) (p. 17): from the Buyer's perspective, the same with $\mu_b$ replaced by $0$.
• Theorem 1(b) (p. 18): if the Seller-side drift is non-positive for every posterior mean, misspecification, and positive variance, then no free-sample policy beats selling in one round.

Significance

Theorem 1 splits the drift of the Bayes risk from the Seller's viewpoint into a holdup cost, $\tfrac12BR_{\theta\theta}-BR_{\sigma^2}$, which is the drift the Buyer herself expects, and a persuasion benefit, $(g_t/\sigma_t^2)BR_\theta$. Part (a) turns the sign of this drift at the start into a revenue comparison. In the paper's pricing example (unknown demand elasticity, $BR(\theta,v)=\tfrac14e^{-\theta}(e^{v/2}-e^{-v/2})$), condition (4) reduces to $\mu_b<\sigma_0^2/(1-e^{\sigma_0^2})$: a sufficiently biased Buyer should be given free data. In the estimation example ($BR=\sigma_t^2$) part (b) applies and one-round selling is optimal. The theorem is the basis of the paper's later results on myopic stopping rules and on the comparison with dynamic pricing.

The theorem is proved in the paper, in $dt$-notation and through Itô's lemma and the optional stopping theorem. It has not been machine-checked. A formal proof requires Gaussian conjugacy with respect to a Brownian filtration, moment computations for the posterior mean, an Itô-type expansion for a $C^2$ function of the belief, and control of the integrability of the stopped Bayes risk. Each of these is reusable for other continuous-time Bayesian learning models.

Difficulty

The informal argument reads off Lemma 4 that $BR(\theta_t,\sigma_t^2)$ is a Seller-submartingale near the start, and then stops it. The $dt$-identities of Lemmas 1 and 4 are statements about conditional expectations at every time. Made rigorous, they require integrability of the Bayes risk and its derivatives along the belief path, and an exchange of differentiation and expectation. Neither is given by the paper's hypotheses on $u$. The Gaussian conjugacy itself must also be established for conditioning on the whole path $(Y_s)_{s\le t}$, not only on $Y_t$.

Formalization scope

All objects are defined in one file, FreeSamples.Revenue.Setting, on top of Mathlib's gaussianReal, IsBrownianReal, Filtration.natural and IsStoppingTime. Committed conventions:

• Variances are real numbers, and $\mathcal N(m,v)$ is gaussianReal m v.toNNReal. $BR$ and $U$ take the variance, not the standard deviation, as their second argument.
• A model with prior $\mathcal N(m,v)$ is a probability space carrying measurable $\theta\sim\mathcal N(m,v)$ and a Brownian motion $B$ independent of $\theta$. The Seller's and the Buyer's measures are the two instances, which makes concordance hold by construction. Every revenue is an expectation under the Seller's measure.
• The filtration is the natural filtration of $Y$ without augmentation. Free-sample policies are bounded stopping times. The paper requires only measurability of $T$, but its own construction is bounded by a large constant $M$.
• Standing hypotheses on $u$, all disclosed pins: the maxima in $U$ and $BR$ exist and are attained, with all expectations integrable (HasMax); Assumption 1 is read as $U,BR\in C^2(\mathbb R\times(0,\infty))$; and $BR$ and its partial derivatives grow at most like $Ce^{c|\theta|}$ for variances in $(0,\sigma_0^2]$.
• The $dt$-statements of Lemmas 1 and 4 are posed as one-sided derivatives at time $0$ of plain expectations, for arbitrary parameters. The time-$t$ versions follow by restarting from the posterior state and are not posed.
• Lemma 4's printed factor $\sigma_t^4/\sigma_0^2$ is formalized as $\sigma_t^4/\sigma^2$, as Lemma 1 gives. Condition (5) of Theorem 1(b) keeps the page's universal quantifiers over the posterior mean, misspecification and positive variance. Quantification over all $g_t$ forces $BR_\theta\equiv0$; the paper's application on p. 33 checks only the realized $g_t$, so it does not establish the printed condition for that example.

Trivializing formalizations are ruled out. Every revenue in a conclusion is asserted integrable, so a junk-zero integral cannot satisfy it. The maxima in $U$ and $BR$ are assumed attained, so no real supremum takes its junk value. The goal is stated for the Gaussian–Brownian model and its posterior map, not for an arbitrary process with a postulated drift. Its conclusion exhibits a policy instead of comparing a supremum over policies.

Not posed: the stochastic differential equation of Lemma 1, Lemma 2, Proposition 2 (its free boundary is part of the hypothesis), Corollaries 1–3, and Appendix B. Contributions are welcome on the conjugacy computation (Proposition 1), on the Gaussian moment estimates (Lemma 1), and on a reusable Itô-type expansion of $h\mapsto\mathbb E[F(m_h,v_h)]$ for $C^2$ functions of exponential growth.

Selected references

• K. Drakopoulos and A. Makhdoumi, Providing Data Samples for Free, SSRN 3611003; Management Science, 2022. https://ssrn.com/abstract=3611003, https://doi.org/10.1287/mnsc.2022.4534
• S. Morris, Trade with Heterogeneous Prior Beliefs and Asymmetric Information, Econometrica 62(6), 1994. https://doi.org/10.2307/2951755
• R. J. Aumann, Agreeing to Disagree, Annals of Statistics 4(6), 1976. https://doi.org/10.1214/aos/1176343654
• J. M. Steele, Stochastic Calculus and Financial Applications, Springer, 2001. https://doi.org/10.1007/978-1-4684-9305-4

Motivation

Machines in production lines deteriorate in ways that are only partly visible. A machine may run in a degraded state that raises costs without announcing itself, and eventually fail in a way that cannot be missed. The decision maker must choose between continuing production, paying for an inspection that reveals the hidden state, and replacing the machine preventively. Models of this kind are partially observable Markov decision processes (POMDPs), and for POMDPs closed-form optimal policies are rare: the value function lives on the space of beliefs and is usually only computed numerically.

H. Zhang and W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures (Management Science, 2022; read here as SSRN 2945049, version of 2022-08-21), solve the classical two-state version of this problem completely. Working in the dual "efficient frontier" framework of Zhang (2010), they show that the optimal solution has exactly six possible structures and give each in closed form, with explicit or implicitly characterized thresholds on the replacement and inspection costs.

Setting

A machine is in a hidden state $x\in\{0,1\}$ (good or bad) or in the observable failure state $F$. Each period, if the machine has failed it is replaced correctively at cost $c^F$; otherwise one of three actions is chosen:

• production $P$ costs $0$ in state 0 and $c^P$ in state 1;
• inspection $I$ costs $c^I$ and reveals the current state;
• preventive replacement $R$ costs $c^R$ and resets the machine to state 0.

Production always takes place. From state 0 the machine moves to state 1 with probability $\gamma_0$; from state 1 it fails with probability $\gamma_1$. Write $\bar\gamma_x=1-\gamma_x$, $\mathbf p_0=(\bar\gamma_0,\gamma_0)'$, $\mathbf p_1=(0,\bar\gamma_1)'$, $\mathbf g^P(u_F)=(0,c^P+\beta\gamma_1u_F)'$, $\mathbf g^I(u_F)=(c^I,c^I+\beta\gamma_1u_F)'$ and $\mathbf P^P\mathbf u=(\mathbf p_0'\mathbf u,\mathbf p_1'\mathbf u)'$. Costs are discounted by $\beta$ over an infinite horizon.

A continuation-cost vector $\mathbf u=(u_0,u_1)'$ records the cost of a continuation policy from each hidden state, and $u_F$ the cost after a failure. The expected optimal cost at an (unnormalized) belief $\boldsymbol\pi=(\pi_0,\pi_1)'\ge0$ is $V(\boldsymbol\pi)=\min_{\mathbf u\in U^*}\boldsymbol\pi'\mathbf u$, where $U^*$ is the set of extreme points of the efficient frontier. The pair $(U^*,u^*_F)$ is the fixed point of the dual value iteration (12)–(16). In support-function form, a pair $(W,w_F)$ is mapped to

$$W'(\boldsymbol\pi)=\min\Big\{\boldsymbol\pi'\mathbf g^P(w_F)+\beta W\big((\mathbf P^P)'\boldsymbol\pi\big),\ (\pi_0+\pi_1)\big(c^R+\beta W(\mathbf p_0)\big),\ \boldsymbol\pi'\mathbf g^I(w_F)+\beta\big(\pi_0W(\mathbf p_0)+\pi_1W(\mathbf p_1)\big)\Big\},$$ $$w_F'=c^F+\beta W(\mathbf p_0),$$

the three terms being $P$, $R$ and $I$. A finite set $U$ with a number $u_F$ is the optimal solution for an action set if value iteration from zero terminal costs converges to $\min_{\mathbf u\in U}\boldsymbol\pi'\mathbf u$ for every $\boldsymbol\pi\ge0$ and to $u_F$ after a failure.

The structures are built from two point sequences. The production sequence is $\mathbf u_{i+1}=\mathbf g^P(u_F)+\beta\mathbf P^P\mathbf u_i$. Started on the diagonal at $(u^R,u^R)'$ with $u_F=u^R+c^F-c^R$, the self-consistency equation $u^R=c^R+\beta\mathbf p_0'\mathbf u_m$ has a unique solution $u^R=f(m)$ (31). Started instead at the inspection point (35), it gives $g(m)$ (40).

Formalization targets

Goal: Theorem 2 (pp. 27–28, Table 1)

Let $\theta=\dfrac{c^P+\beta\gamma_1c^F}{1-\beta+\beta(\gamma_0+\gamma_1)}$ and $\hat c=(1+\beta\gamma_0)c^P-\beta\bar\gamma_1(1-\beta+\beta\gamma_0+\beta\gamma_1)c^R+\beta^2\gamma_1\bar\gamma_1c^F$. Under $\{P,I,R\}$:

$$c^R\ge\theta\ \Rightarrow\ [P];\qquad \tfrac{\gamma_0}{\gamma_1}\theta\le c^R<\theta\ \Rightarrow\ R[P],\ IR[P]\ \text{or}\ [PIR]\ \text{by explicit thresholds on }c^I;$$ $$c^R<\min\{\tfrac{\gamma_0}{\gamma_1}\theta,\theta\}\ \Rightarrow\ \exists\,0<\hat c_1\le\hat c_2<c^R:\ [PR],\ I[PR]\ \text{or}\ [PIR]\ \text{as}\ c^I\ge\hat c_2,\ \hat c_1\le c^I<\hat c_2,\ c^I<\hat c_1,$$

with every structure an explicit pair $(U^*,u^*_F)$ from Table 1, and the thresholds characterized implicitly ($\mathbf u^{I\dagger}$ on the frontier of $U^\dagger$ at $c^I=\hat c_2$; $\min f=\min g$ at $c^I=\hat c_1$).

Milestones

Proposition 2 (the fixed-point equations), Proposition 3 (the cost of producing forever), Lemma 1 and Lemma 6 (the two sequences in closed form), Lemma 3 and Lemma 7 (the anchors $f$ and $g$), Proposition 4 (unimodality of $f$), Theorem 1 (the two-action solution: $[P]$, $R[P]$, $[PR]$, with extreme-point exactness) and Lemma 5 (when inspection enters).

Significance

The result. The theorem turns a POMDP into a finite list of explicit policies. Each structure is a periodic plan that needs no belief updating: produce for $m^\dagger$ periods and replace; or inspect every $m^*$ periods and replace only if the machine is found bad. The thresholds tell when inspection is worth its cost, and the comparative statics of $m^\dagger$ and $m^*$ follow from the closed forms. The authors use the solution to justify common maintenance practices.

Formalizing it. The result is proved in the paper (main text §4, proofs in its e-companion, App. A); no part is machine-checked. The proofs of Theorems 1 and 2 argue geometrically from figures of convex curves in the plane ("the curve bends back", "all the points are still extreme points"). A formal development has to turn these into inequalities between piecewise-linear concave functions, and has to prove convergence of value iteration to the stated sets. The implicit thresholds of part (3) were not checked numerically when this mission was planned. Parts (1) and (2) and Theorem 1 were.

Difficulty

Verifying that a candidate set $U$ is a fixed point is not enough: the goal asserts that value iteration from zero converges to it, so uniqueness of the bounded fixed point must be proved (a contraction argument in the supremum norm over the simplex). More importantly, finding the frontier requires knowing which points of the infinite production sequence are extreme, which depends on the location of the anchor relative to the curve $\{\mathbf u_i:i\ge0\}$ (Fig. 5 of the paper, five subcases). The natural induction on $m$ fails because $f$ is not monotone: its least minimizer $m^\dagger$ must be located through the unimodality of the real extension (Proposition 4). In part (3) the thresholds $\hat c_1,\hat c_2$ are defined implicitly, and showing that the three regimes are ordered in $c^I$ requires monotonicity of the whole frontier in $c^I$.

Formalization scope

Everything is defined in the namespace MaintPOMDP.Frontier. Vectors and beliefs are Fin 2 → ℝ (index 0 = good state); beliefs are unnormalized, $\boldsymbol\pi\ge0$. The optimal solution is the limit of the support-function value iteration started from $W\equiv0$, $w_F=0$; "the structure is X" means that this limit equals $\min$ over the points of row X of Table 1, with the failure cost of that row.

Standing assumptions: $0<\beta<1$, $0<c^P<c^I<c^R<c^F$ (p. 14), and $0<\gamma_0<1$, $0<\gamma_1<1$, which the paper never states and which are added (the thresholds divide by $\gamma_1$). The hypothesis $\gamma_0\ne\gamma_1$ is added only to Lemmas 1, 3, 6, 7 and Proposition 4, whose printed formulas divide by $\gamma_1-\gamma_0$; $f$ and $g$ themselves are defined as solutions of the affine anchor equations, so Theorems 1 and 2 cover $\gamma_0=\gamma_1$. Proposition 4 also carries the range of $c^R$ that its proof uses. "$m^\dagger=\arg\min f$" is the least minimizer, and its existence is part of the conclusion. In Theorem 2, the indices $n_R,n_I$ of Table 1 are existential and extreme-point exactness is not asserted for the $I[PR]$ and $[PIR]$ rows (Table 1's $I[PR]$ row conflicts with the paper's Proposition 8). It is asserted in Theorem 1. In part (3) the thresholds are chosen before $c^I$ and the claims hold for every $c^I\in(c^P,c^R)$.

Trivializing readings are ruled out: the value function is the limit of the iterates, not an arbitrary fixed point or a junk limit; identities hold for every belief $\boldsymbol\pi\ge0$, not only at vertices; every frontier set is given by formulas, so no extra points can be slipped in; minimizers are asserted, not assumed; and thresholds involving $\gamma_0/\gamma_1$ are evaluated with $\gamma_1>0$.

A complete development needs convergence of value iteration for a monotone contraction on bounded functions over the cone $\boldsymbol\pi\ge0$, explicit solutions of two-dimensional linear recurrences, and lemmas on lower envelopes of finitely many linear functions in two variables. These are reusable beyond this mission, for other two-state POMDPs. Contributions of any milestone, of the γ0 = γ1 closed forms (App. B), or of a proof of Theorem 1 alone are welcome.

Selected references

• H. Zhang, W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4547 (read as SSRN 2945049, https://ssrn.com/abstract=2945049)
• H. Zhang, Partially Observable Markov Decision Processes: A Geometric Technique and Analysis, Operations Research 58(1), 2010. https://doi.org/10.1287/opre.1090.0697
• R. D. Smallwood, E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071
• S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), 1971. https://doi.org/10.1287/mnsc.17.9.587

Motivation

Linear opinion models describe how individuals in a social network revise their views by averaging what their neighbours think, what external media tell them, and what they themselves believed a moment ago. The last ingredient, an autoregressive or memory term, appears in the Friedkin–Johnsen family of models and in its stochastic variants. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969, Mathematics of Operations Research, 2025) study such a model on large directed random graphs with vertex attributes and random media signals. They show that the opinion of a typical vertex has a stationary law that is described, in the large-graph limit, by a recursion on a marked Galton–Watson tree.

A natural question is what the memory term does to that stationary law. Simulations in the paper (Section 5.4, Figures 6–7) suggest that memory smooths individual trajectories and makes the stationary opinion less dispersed. Proposition 6 turns this into a theorem: on a Galton–Watson limit, the stationary opinion with memory has variance at most that of a no-memory recursion that keeps the same relative weights of neighbours and media.

Setting

Nodes of the limiting tree are labelled by finite words $\mathbf i=(i_1,\dots,i_k)$, the root being $\varnothing$; $(\mathbf i,j)$ is the $j$-th child of $\mathbf i$. Each node carries a mark $\mathcal X_{\mathbf i}$, from which the model reads an in-degree $\mathcal N_{\mathbf i}$, weights $\mathcal C_{(\mathbf i,1)},\mathcal C_{(\mathbf i,2)},\dots\in[0,1]$ summing to $c$ when $\mathcal N_{\mathbf i}\ge1$, and an internal opinion $\mathcal Q_{\mathbf i}\in[-1,1]$. Parameters satisfy $c\in[0,1)$, $d\in(0,1]$, $c+d\le1$. The tree is a delayed marked Galton–Watson tree: marks are independent, and all non-root marks have the same law.

Each node receives media signals $\mathcal Z_{\mathbf i}^{(k)}\in[-1,1]$, $k\ge0$, conditionally i.i.d. given its mark and conditionally independent across nodes, and the external signal

$$\mathcal W_{\mathbf i}^{(k)}=d\,\mathcal Z_{\mathbf i}^{(k)}+\mathcal Q_{\mathbf i}\Big(c-\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\Big).$$

The general recursion (8) and the no-memory recursion (9) are

$$\mathcal M_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\mathcal M_{(\mathbf i,j)}^{(k)}+\mathcal W_{\mathbf i}^{(k)}+(1-c-d)\mathcal M_{\mathbf i}^{(k)},\qquad \mathcal R_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\frac{\mathcal C_{(\mathbf i,j)}}{c+d}\mathcal R_{(\mathbf i,j)}^{(k)}+\frac{\mathcal W_{\mathbf i}^{(k)}}{c+d}.$$

Writing $\Delta$ for the linear map on the right-hand side without the signal, the limiting root opinion is the series $\sum_{s\ge0}(\Delta^s\mathcal W^{(s)})(\varnothing)$; it is $\mathcal M^*$ for (8) and $\mathcal R^*$ for (9). The moments

$$\rho_1^*=E\Big[\sum_{i=1}^{\mathcal N_\varnothing}\mathcal C_i\Big],\quad \rho_1=E\Big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}\Big],\quad \rho_2^*=E\Big[\sum_{i=1}^{\mathcal N_\varnothing}\mathcal C_i^2\Big],\quad \rho_2=E\Big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}^2\Big]$$

and the series $p_m=\sum_{s\ge0}\binom{s+m}{s}^2(1-c-d)^{2s}(c+d)^{2(m+1)}$ enter every formula below.

Formalization targets

Goal: Proposition 6

If $c,d>0$, $c+d<1$ and $P(\mathcal N_\varnothing>0)=P(\mathcal N_1>0)=1$, then

$$\mathrm{Var}(\mathcal M^*)\le\mathrm{Var}(\mathcal R^*).$$

The goal asserts the comparison only, not the closed forms, so it is the weakest statement the paper's computation supports.

Milestones

1. Theorem 8 (pp. 32–33): closed forms for $E$ and $\mathrm{Var}$ of the limiting opinions of the root and of a neighbour, in terms of $\rho_1^*,\rho_1,\rho_2^*,\rho_2$, $\mathcal Y_{\mathbf i}=E[\mathcal W_{\mathbf i}\mid\mathcal X_{\mathbf i}]$, $\mathcal V_{\mathbf i}=\mathrm{Var}(\mathcal W_{\mathbf i}\mid\mathcal X_{\mathbf i})$ and a Geometric expectation of $p_T$.
2. Remark 10.2 (pp. 33–34): the specialisation to the Section 5.1 signals with $\mathcal N_\varnothing,\mathcal N_1>0$ a.s.; it expresses $\mathrm{Var}(\mathcal M^*)$ through $\mathrm{Var}(\mathcal Z)$ and $E[\mathrm{Var}(\mathcal Z\mid\mathcal X)]$.
3. (15) (p. 31): $\mathrm{Var}(\mathcal R^*)=\frac{d^2}{(c+d)^2}\mathrm{Var}(\mathcal Z_\varnothing)+\frac{\rho_2^*d^2}{(c+d)^2((c+d)^2-\rho_2)}\mathrm{Var}(\mathcal Z_1)$.
4. Coefficient bound (pp. 31–32): $p_m\in(0,1)$ and $\frac{1}{1-\rho_2}E[(c+d)^{-2(T+2)}p_{T+1}]\le\frac{1}{(c+d)^2((c+d)^2-\rho_2)}$, $T$ Geometric with success probability $1-\rho_2$.

Additional item (not a milestone): Lemma 9 (p. 34), the mean and variance of $\mathcal R^{(k+1)}$ for the general recursion with general signals, started from $0$, at the root and at non-root nodes; it is the finite-time step behind Theorem 8.

Significance

The proposition isolates the effect of memory on dispersion: with the same proportional influence of neighbours and media, adding inertia never increases the variance of the stationary opinion of a typical individual. In the paper's interpretation, slower updating produces less polarised stationary opinions, which matters when the model is used to compare network interventions or media exposure. Theorem 8 and Lemma 9 go further and give exact first and second moments of the stationary opinion on Galton–Watson limits with possibly stubborn (in-degree zero) vertices and arbitrary mark-dependent signals; such closed forms are rare for models of this kind.

The results are proved in the paper. None of them has a machine-checked proof. Formalizing them produces a Lean development of moment computations for linear recursions on marked Galton–Watson trees (conditioning on independent subtrees, laws of total variance along generations, and negative-binomial series), which is reusable for other smoothing-transform and branching-recursion problems. Two printed slips are corrected along the way (see Formalization scope).

Difficulty

The difficulty is not the comparison itself but the exact variance of $\mathcal M^*$. With memory, a signal emitted at time $s$ by a node at depth $l$ reaches the root with coefficient $\binom{s}{l}(1-c-d)^{s-l}$ times the product of weights along the path, so its contributions spread over all later times. The variance then involves the squared coefficients $\sum_s\binom{s}{l}^2(1-c-d)^{2(s-l)}$, which do not factor as the coefficients do in the no-memory case. The obvious route, comparing the two recursions pathwise or coupling them, fails: the two root opinions are not ordered, and only their variances are. The comparison emerges only after the conditional variances of the media signals are separated from the variance of their conditional means, and after the Geometric average of $p_{T+1}$ is bounded.

Formalization scope

• Model. The tree is encoded with Ulam–Harris labels List ℕ (0-based children; the paper's node $1$ is [0]), and marks are read through measurable maps $\mathcal N$, $\mathcal C$, $\mathcal Q$ on a measurable space $M$. The media signals are $\zeta(\mathcal X_{\mathbf i},U_{\mathbf i}^{(k)})$ with i.i.d. uniforms independent of the marks. This quantile representation is equivalent in law to the paper's conditional i.i.d. assumption and is the paper's own device (p. 25). The general signals of Theorem 8 and Lemma 9 are $\xi(\mathcal X_{\mathbf i},U_{\mathbf i}^{(k)})$ with $|\xi|\le d+c-\sum_j\mathcal C_{(\mathbf i,j)}$.
• Limit tree, not graph sequence. The paper's statements assume "the assumptions of Theorem 2" with the Galton–Watson tree as local limit. Those assumptions only identify the tree's root opinion with the large-graph typical opinion; every claim here is about the tree. All statements are made on the tree under the Section 5 standing assumptions, which is a generalization.
• Conventions. Limiting opinions are the absolutely summable series $\sum_s(\Delta^s\mathcal W^{(s)})(\mathbf i)$; $E$ is the Bochner integral, Var/Cov are Mathlib's variance/covariance, conditional moments are condExp/condVar given $\sigma(\mathcal X_{\mathbf i})$; the Geometric expectation is the explicit series $\sum_k\rho^k(1-\rho)g(k)$.
• Corrections. Remark 10.2's printed mean lacks a factor $d$; the corrected mean is stated. Lemma 9's root variance is stated for $k\ge1$ (it fails at $k=0$) and its root mean under $\rho_1>0$. Equation (15) is Proposition 4 applied to recursion (9) after rescaling.
• No trivialization. Every random variable involved is bounded, so no variance, integral or series takes a junk value; the denominators $c+d-\rho_1$, $(c+d)^2-\rho_2$, $1-\rho_2$ are positive under the standing assumptions, and the goal's hypotheses are satisfied by, e.g., the path tree ($\mathcal N\equiv1$, $\mathcal C\equiv c$), where both variances are positive.
• Infrastructure. Useful contributions include: summability and boundedness of the opinion series; independence of subtrees in Ulam–Harris encodings; the law of total variance (integral_condVar_add_variance_condExp in Mathlib); the identities $\sum_s\binom{s}{l}x^{s-l}=(1-x)^{-(l+1)}$ and the negative-binomial bound $p_m<1$.

Selected references

• N. Fraiman, T.-C. Lin, M. Olvera-Cravioto, Opinion dynamics on directed complex networks, arXiv:2209.00969v2, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2209.00969
• N. E. Friedkin, E. C. Johnsen, Social influence and opinions, Journal of Mathematical Sociology 15(3–4), 1990. https://doi.org/10.1080/0022250X.1990.9990069
• M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69(345), 1974. https://doi.org/10.1080/01621459.1974.10480137

Motivation

Linear opinion models describe each individual's opinion as a weighted average of the opinions of the people they listen to, of an outside signal, and of their own previous opinion. The model goes back to DeGroot (DeGroot 1974) and Friedkin–Johnsen, and its basic questions are when a population reaches consensus and when it polarizes. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969v2, Mathematics of Operations Research, 2025) study it on large directed random graphs with vertex attributes, where each vertex also receives a stream of media signals. Their Theorem 2 shows that the opinion of a typical vertex converges, as the graph grows, to a random variable $\mathcal R^*$ defined on the graph's local limit. When that local limit is a marked Galton–Watson tree, $\mathcal R^*$ becomes explicit enough that its mean and variance can be written in closed form, and the variance formula is what the paper uses to say when consensus happens.

This mission formalizes those closed-form moments in the no-memory case, where an individual's new opinion does not depend on their own previous opinion.

Setting

The tree. Nodes carry Ulam–Harris labels: the root is $\emptyset$, and the children of a node $\mathbf i$ are $(\mathbf i,1),(\mathbf i,2),\dots$ (in the tree, the children of $\mathbf i$ are its inbound neighbours). Each node $\mathbf i$ has a mark $\boldsymbol{\mathcal X}_{\mathbf i}$, which determines its in-degree $\mathcal N_{\mathbf i}$, the weights $\mathcal C_{(\mathbf i,1)},\dots,\mathcal C_{(\mathbf i,\mathcal N_{\mathbf i})}\in[0,1]$ it puts on its inbound neighbours, and an internal opinion $\mathcal Q_{\mathbf i}\in[-1,1]$. Two parameters $c\in[0,1)$, $d\in(0,1]$ with $c+d\le1$ fix the proportions: if $\mathcal N_{\mathbf i}\ge1$, then $\sum_j\mathcal C_{(\mathbf i,j)}=c$. The tree is a delayed marked Galton–Watson tree: the marks are independent, and all marks except the root's are identically distributed.

Signals. Each node receives media signals $\mathcal Z_{\mathbf i}^{(k)}\in[-1,1]$, $k\ge0$, conditionally i.i.d. given its mark and conditionally independent across nodes. The external signal is

$$\mathcal W_{\mathbf i}^{(k)}=d\,\mathcal Z_{\mathbf i}^{(k)}+\mathcal Q_{\mathbf i}\Big(c-\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\Big),$$

so a vertex with inbound neighbours gives weight $d$ to the media and $c$ to its neighbours, and a vertex without them falls back on its internal opinion.

Dynamics. Opinions evolve by

$$\mathcal R_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\mathcal R_{(\mathbf i,j)}^{(k)}+\mathcal W_{\mathbf i}^{(k)}+(1-c-d)\mathcal R_{\mathbf i}^{(k)}.$$

With the operator $\Delta f(\mathbf i)=\sum_j\mathcal C_{(\mathbf i,j)}f((\mathbf i,j))+(1-c-d)f(\mathbf i)$, the stationary root opinion is

$$\mathcal R^*=\sum_{s\ge0}\big(\Delta^s\mathcal W^{(s)}\big)(\emptyset).$$

The no-memory case is $c+d=1$. In that case $\mathcal R^*=\sum_{j}\mathcal C_j\mathcal R_j+\mathcal W_\emptyset^{(0)}$, where the subtree opinions $\mathcal R_j$ are i.i.d. copies of the endogenous solution $\mathcal R$ of the smoothing transform $\mathcal R\overset{\mathcal D}{=}\sum_j\mathcal C_{(1,j)}\mathcal R_j+\mathcal W_1^{(1)}$. The moments are expressed through $\rho_2=E\big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}^2\big]$ (a non-root node) and $\rho_2^*=E\big[\sum_{i=1}^{\mathcal N_\emptyset}\mathcal C_i^2\big]$ (the root).

Formalization targets

Goal: Proposition 4 (p. 11)

If $c+d=1$ and $P(\mathcal N_\emptyset>0)=P(\mathcal N_1>0)=1$, then

$$E[\mathcal R^*]=d\,E[\mathcal Z_\emptyset]+c\,E[\mathcal Z_1],\qquad \operatorname{Var}(\mathcal R^*)=d^2\operatorname{Var}(\mathcal Z_\emptyset)+\frac{\rho_2^*d^2}{1-\rho_2}\operatorname{Var}(\mathcal Z_1).$$

Milestones, in attack order

1. The expansion $\Delta^sf(\mathbf i)=\sum_{l\le s}\sum_{|\mathbf j|=l}\frac{\Pi_{(\mathbf i,\mathbf j)}}{\Pi_{\mathbf i}}a_{l,s}f((\mathbf i,\mathbf j))$ with $a_{l,s}=\binom sl(1-c-d)^{s-l}$ (proof of Proposition 3, p. 29).
2. Proposition 3 (pp. 9–10): $\mathcal R^*=\sum_s\sum_{l\le s}\sum_{|\mathbf j|=l}\Pi_{\mathbf j}a_{l,s}\mathcal W_{\mathbf j}^{(s)}$.
3. Remark 6 (p. 10): the decomposition (6)–(7) of $\mathcal R^*$ without memory, the i.i.d. structure of the $\mathcal R_j$, and the fixed-point equation.
4. Display (14) (p. 30): $E[\mathcal R]=E[\mathcal Z_1]$ and $\operatorname{Var}(\mathcal R)=\frac{d^2}{1-\rho_2}\operatorname{Var}(\mathcal Z_1)$.
5. Displays (12)–(13) (p. 30): the conditional mean and variance of $\mathcal R^*$ given $\boldsymbol{\mathcal X}_\emptyset$ in terms of $\mathcal R$.
6. Proposition 5 (p. 14): $E[\mathcal R^*\mid\boldsymbol{\mathcal X}_\emptyset]=dE[\mathcal Z_\emptyset\mid\boldsymbol{\mathcal X}_\emptyset]+cE[\mathcal Z_1]$ and $\operatorname{Var}(\mathcal R^*\mid\boldsymbol{\mathcal X}_\emptyset)=d^2\operatorname{Var}(\mathcal Z_\emptyset\mid\boldsymbol{\mathcal X}_\emptyset)+\frac{d^2}{1-\rho_2}\sum_{i}\mathcal C_i^2\operatorname{Var}(\mathcal Z_1)$.

Significance

The result. The variance formula identifies consensus with small media variance: the weights enter only through the second moments $\rho_2,\rho_2^*$, so consensus is possible for any network structure as long as $d\mathcal Z$ has small variance. The conditional formulas of Proposition 5 separate the part of the opinion explained by the vertex's own attributes from the part contributed by the network, which is how the paper describes polarization: individuals with similar attributes end with similar opinions when $\operatorname{Var}(\mathcal R^*\mid\boldsymbol{\mathcal X}_\emptyset)$ is small. The no-memory formulas are also the comparison point for the general case $c+d<1$ (Proposition 6 of the paper, a separate mission of this series).

The formalization. The results are proved in the paper; none is machine-checked. A formal development produces a reusable encoding of marked Galton–Watson trees with i.i.d. marks and signals, the expansion of powers of the averaging operator over the generations of a tree, and the moment computation for the endogenous solution of the linear smoothing transform, a fixed-point equation that recurs in the study of branching processes and of ranking algorithms such as PageRank on random graphs.

Difficulty

The moment identities are short once Remark 6 is available. The work is in making Remark 6 precise: the subtree opinions $\mathcal R_j$ are infinite series over random subtrees, and the proof needs them to be measurable, mutually independent, identically distributed, and independent of the root's mark and signal. That independence comes from the disjointness of the label sets they read, together with the independence of all marks and all uniform variables, and it must be carried through a random in-degree and random weights. The conditional variance step then requires conditional independence given $\boldsymbol{\mathcal X}_\emptyset$ of a random number of summands. Simply invoking the law of total variance is not enough: computing $\operatorname{Var}(\mathcal R)$ from the fixed-point equation needs $\operatorname{Var}(\mathcal R)<\infty$, which here follows from boundedness, $|\mathcal R|\le 1/d$.

Formalization scope

Labels are List ℕ with 0-based children: the paper's node $1$ is [0] and its $j$-th child of $\mathbf i$ is i ++ [j-1]. Marks live in an arbitrary measurable space and are read through measurable maps giving $\mathcal N$, $\mathcal C$, $\mathcal Q$. The signals are written $\mathcal Z_{\mathbf i}^{(k)}=\zeta(\boldsymbol{\mathcal X}_{\mathbf i},U_{\mathbf i}^{(k)})$ with i.i.d. uniform $U$ independent of the marks; this produces exactly the paper's conditional i.i.d. structure (take $\zeta(x,\cdot)$ the quantile function), and every statement concerns laws. Signals are indexed by time $k\ge0$; $E[\mathcal Z_1]$ and $\operatorname{Var}(\mathcal Z_1)$ are taken at $k=0$, as their laws do not depend on $k$. The relative path weights $\Pi_{(\mathbf i,\mathbf j)}/\Pi_{\mathbf i}$ are products along the path, never quotients, which removes the paper's convention for $\mathcal C_j=0$.

The paper states Propositions 3–5 under "the assumptions of Theorem 2" with a tree as local limit. Those assumptions only serve to identify $\mathcal R^*$ with the typical opinion of a large graph; the statements and proofs concern $\mathcal R^*$ on the limit tree. The Lean statements are therefore made on the tree, under the Section 5 standing assumptions above, without a graph sequence. $\mathcal R^*$ is the series $\sum_s(\Delta^s\mathcal W^{(s)})(\emptyset)$.

Conditional expectations and variances given $\boldsymbol{\mathcal X}_\emptyset$ are Mathlib's condExp and condVar with respect to the σ-algebra generated by the root's mark, and the conditional statements are equalities almost everywhere, not pointwise. No trivializing reading is available: every series is absolutely summable for every outcome under the standing assumptions, every variable is bounded by $1/d$, so Lean's junk values for a non-summable tsum, a non-integrable integral or a non-$L^2$ variance never apply, and $1-\rho_2\ge1-c^2>0$, so the division is genuine. The standing assumptions are satisfiable together with $c+d=1$ and $\mathcal N\ge1$ (a path tree with uniform signals). The hypotheses $P(\mathcal N_\emptyset>0)=P(\mathcal N_1>0)=1$ are used: without them the term $c\mathcal Q$ enters at vertices with no inbound neighbours and the formulas change.

Needed infrastructure: independence of functions of disjoint blocks of an independent family, measurability of series over random finite generations, conditional variance of conditionally independent sums. Contributions on each milestone, on general lemmas for marked Galton–Watson trees, and alternative proofs are welcome.

Selected references

• N. Fraiman, T.-C. Lin, M. Olvera-Cravioto, Opinion dynamics on directed complex networks, Mathematics of Operations Research, 2025; arXiv:2209.00969v2. https://arxiv.org/abs/2209.00969
• M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69 (1974) 118–121. https://doi.org/10.1080/01621459.1974.10480137
• D. J. Aldous, A. Bandyopadhyay, A survey of max-type recursive distributional equations, Annals of Applied Probability 15 (2005) 1047–1110. https://doi.org/10.1214/105051605000000142
• G. Alsmeyer, J. D. Biggins, M. Meiners, The functional equation of the smoothing transform, Annals of Probability 40 (2012) 2069–2105. https://doi.org/10.1214/11-AOP670

Motivation

Tele-driving separates a ride-hailing driver from the vehicle: a remote driver operates a car over a wireless link, and on finishing a trip can immediately take control of another car anywhere in the service region. Several companies have run pilots of this model; Benjaafar, Wang and Yang cite Vay's car-sharing service operated by tele-drivers and Halo's remotely operated robo-taxi pilot with T-Mobile. A platform with remote drivers can therefore hold more vehicles than drivers. The practical question is how many drivers such a platform needs.

Benjaafar, Wang and Yang (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687) model the system as a loss system with a state-dependent service rate and compare a fleet with $n$ remote drivers to one with a driver in every vehicle ($n = m$). This mission formalizes their answer for large markets that have many vehicles relative to demand (the supply-rich regime): asymptotically, a fraction $1/\alpha$ of the fleet size suffices, where $\alpha > 2$ measures how much the fleet exceeds the offered load. All page numbers refer to the SSRN working paper, version of 1 June 2023, which is the source of this mission.

Setting

Customers arrive as a Poisson process of rate $\lambda > 0$. The platform has $m$ vehicles and $n \le m$ remote drivers. When $q$ customers are being served, trips are completed at total rate $q\,\mu(m,q)$, where the service rate $\mu(m,q)$ accounts for the pick-up time (which shrinks as more idle vehicles are available) and the trip time. A customer arriving while all $n$ drivers are busy is lost. With

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)} \qquad (1)$$

the number of customers in service is a birth–death process on $\{0, \dots, n\}$ with stationary distribution

$$\pi_{m,n}(0) = \Big[1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)\Big]^{-1}, \qquad \pi_{m,n}(q) = \pi_{m,n}(0)\prod_{k=1}^{q}\rho(k), \quad 1 \le q \le n. \qquad (2)\text{–}(3)$$

The service level, the long-run fraction of demand served, is $SL(m,n) = 1 - \pi_{m,n}(n)$.

For the asymptotic analysis the paper uses the service rate of Besbes et al.,

$$\mu(m,q) = \Big[\frac{s}{\sqrt{m-q+1}} + s\Big]^{-1}, \qquad (4)$$

where $s > 0$ is the mean trip time and $s/\sqrt{m-q+1}$ the mean pick-up time with $m - q$ idle vehicles. The fleet grows with demand as $m_\lambda = \lfloor \alpha\lambda s\rfloor$ for a constant $\alpha > 0$; the offered load is $\lambda s$, so $\alpha$ is the ratio of fleet size to offered load. The supply-rich regime is $\alpha > 2$.

For the rate (4) and $m > 2\lambda s$, the equation $\rho(q) = 1$ has a unique root $q_3$ in $[\lambda s, m]$; to its left $\rho > 1$ (the chain drifts upward), to its right $\rho < 1$. For a tolerance $\epsilon > 0$ the paper defines

$$n^*_\lambda = \min\{\, n : SL(m_\lambda, m_\lambda) - SL(m_\lambda, n) < \epsilon \,\},$$

the smallest number of remote drivers whose service level is within $\epsilon$ of that of a fleet with one driver per vehicle.

Formalization targets

Goal: Theorem 2.C (p. 22)

For $\alpha > 2$ and every $\epsilon > 0$,

$$\limsup_{\lambda\to\infty} \frac{n^*_\lambda}{m_\lambda} \le \frac{1}{\alpha}.$$

The bound does not depend on $\epsilon$, and since $\alpha > 2$ it says that a large supply-rich system can be run with at most about half as many drivers as vehicles.

Milestones

1. App. D, case (iii) (p. 42): for the rate (4) and $m > 2\lambda s$, $\rho(q) = 1$ has a unique root $q^* \in [\lambda s, m]$, and on $(0, m]$, $\rho(q) < 1$ exactly when $q > q^*$.
2. App. D.3 (p. 48): $\lim_{\lambda\to\infty} \lambda s / q_3 = 1$.
3. Lemma 5 (pp. 47–48): with $n_\epsilon = \lfloor (1+\epsilon) q_3\rfloor$ drivers,

$$\lim_{\lambda\to\infty}\Big[\sum_{i=\lfloor (1+\epsilon/2)q_3\rfloor}^{n_\epsilon}\pi_{m_\lambda,n_\epsilon}(i) + \sum_{i=0}^{\lfloor(1-\epsilon/2)q_3\rfloor}\pi_{m_\lambda,n_\epsilon}(i)\Big] = 0.$$

4. Footnote 14 (pp. 22–23): $\lim_{\lambda\to\infty}\big[SL(m_\lambda,m_\lambda) - SL(m_\lambda, \lfloor(1+\delta)q_3\rfloor)\big] = 0$.

Significance

The result. Theorem 2.C quantifies the labour saving of tele-driving in markets where vehicles are plentiful. A conventional platform needs one driver per vehicle; a remote-driver platform with $m_\lambda \approx \alpha\lambda s$ vehicles needs only about $\lambda s$ drivers, essentially the offered load, while losing at most $\epsilon$ of service level. Together with Theorems 2.A and 2.B of the same paper (the supply-limited and intermediate regimes), it gives a complete asymptotic picture of when pooling drivers across vehicles pays off: in the supply-rich regime, the gain appears as fewer drivers rather than as a higher service level. Footnote 14 strengthens this: the service level with $(1+\delta)q_3$ drivers matches the full-staffing service level in the limit.

Formalizing it. The result is proved on paper in Appendix D.3; it has no machine-checked proof. The formalization adds a precise reading of the limit statements (the range of the minimum defining $n^*_\lambda$, the meaning of "small $\epsilon$") and a verified account of the concentration of a birth–death distribution with a state-dependent rate, in the form of Lemma 5. The same model underlies four sibling missions on this paper.

Difficulty

The obvious first idea, comparing $SL(m,n)$ with the Erlang loss formula for a constant service rate, does not apply: under (4) the service rate depends on the state through the pick-up time, so the stationary weights $\prod_{k\le q}\rho(k)$ are not Poisson probabilities and their tails have no closed form. The quantities that govern the answer are defined only implicitly: the critical point $q_3$ solves $\rho(q) = 1$, and its explicit expression (17) involves the arccosine of a cubic's coefficients, which is unusable for estimates. The statements also take a limit $\lambda\to\infty$ in which the number of states, the root $q_3$ and the floors $\lfloor(1\pm\epsilon/2)q_3\rfloor$ all move together, so any bound on the stationary distribution must hold uniformly along this family rather than for a fixed chain. Finally, $n^*_\lambda$ is a minimum over integers of a difference of service levels, and the goal concerns its growth rate relative to $m_\lambda$, not a single system.

Formalization scope

The Lean development lives in the namespace TeleDriving.AsymRich.

• Model. rho mu lam m q is (1) with $q$ real; piMN mu lam m n q and SL mu lam m n are (2)–(3) and the service level, with $q, n$ natural; muBesbes s is the rate (4); mLam alpha s lam is $\lfloor\alpha\lambda s\rfloor$ as a natural-number floor. The shared Model file also contains the paper's Assumptions 1–2, its size restriction, the regime predicates and the maximal service-level ratio, which this mission does not use.
• Domains. $\pi_{m,n}(q)$ is the paper's only for $q \le n$, $SL(m,n)$ only for $1 \le n \le m$, the rate (4) only for $q \le m+1$; Lean's junk values outside these ranges are never invoked by the statements.
• $n^*_\lambda$ (nStar) is the minimum over $n \in \{1,\dots,m_\lambda\}$, a set that contains $n = m_\lambda$ when $m_\lambda \ge 1$ and $\epsilon > 0$; the paper leaves this range implicit.
• Limits are written in $\varepsilon$-form: $\limsup f \le c$ as "for every $\delta > 0$, eventually $f(\lambda) \le c + \delta$"; plain limits use Filter.Tendsto along atTop on $\mathbb R$.
• The root $q_3$ is a function of $\lambda$ with the hypothesis that, for all sufficiently large $\lambda$, $\lambda s \le q_3(\lambda) \le m_\lambda$ and $\rho(q_3(\lambda)) = 1$. By milestone 1 this determines $q_3(\lambda)$ uniquely once $m_\lambda > 2\lambda s$, which holds eventually for $\alpha > 2$. The closed form (17) is not used.
• "Small $\epsilon$" and "any $\delta > 0$" in Lemma 5 and footnote 14 are read as $0 < \epsilon, \delta < \alpha - 1$: exactly in this range $\lfloor(1+\epsilon)q_3\rfloor \le m_\lambda$ for large $\lambda$, so the number of drivers does not exceed the number of vehicles. The goal's tolerance $\epsilon > 0$ is unrestricted, as printed.
• The paper uses $\epsilon$ for both the service-level tolerance of Theorem 2.C and the window of Lemma 5; the Lean statements use distinct names.

The goal carries no hypothesis on $\pi$, $SL$, $n^*_\lambda$ or $q_3$: its only assumptions are $s > 0$, $\alpha > 2$ and $\epsilon > 0$, so it cannot be discharged by an assumption that makes the minimum small by fiat. A complete development needs elementary real analysis of the rate (4) (concavity of $q/(\lambda s) - 1/\sqrt{m-q+1}$), estimates for products of $\rho$ along integer ranges, and asymptotics with floors; the concentration estimate for birth–death chains with state-dependent rates is reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757 ; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2112

Motivation

Autonomous vehicles that cannot yet drive every trip on their own can be supervised or driven by remote (tele-)drivers who sit in a control center and take over a vehicle only while it serves a customer. Because a remote driver is not tied to one vehicle, a platform may operate more vehicles than drivers. Benjaafar, Wang and Yang ask when this decoupling pays off: given a fleet of $m$ vehicles, how many remote drivers $n \le m$ should a ride-hailing operator staff, and how much better is the best choice than the conventional one driver per vehicle ($n = m$)?

The question is sharpened by a feature of ride-hailing that classical loss systems lack. A trip consists of a pick-up leg and a delivery leg, and the pick-up leg is long when few vehicles are idle. Following Besbes, Castro and Lobel (2022), the paper models this through a state-dependent service rate: with $q$ customers in service, each trip ends at rate $\mu(m,q)$, which falls as $q$ approaches $m$. Withholding drivers keeps idle vehicles available, shortens pick-ups and can raise throughput. This mission formalizes the asymptotic size of that gain in the supply-limited regime, where vehicles are scarce relative to demand.

The source is the authors' SSRN working paper (abstract 4130757, version of 1 June 2023); all numbering in this mission is that version's. The paper was published in Management Science in 2024.

Setting

Customers arrive as a Poisson process of rate $\lambda > 0$. A customer who arrives when all $n$ remote drivers are busy is lost. The number $q$ of customers in service is a birth–death process with birth rate $\lambda$ and death rate $q\,\mu(m,q)$. Its load is

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)} \qquad (1),$$

and its stationary distribution is

$$\pi_{m,n}(q) = \frac{\prod_{k=1}^{q}\rho(k)}{1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)}, \qquad 0 \le q \le n \qquad (2)\text{–}(3).$$

The service level is the long-run fraction of demand served, $SL(m,n) = 1 - \pi_{m,n}(n)$.

The mission uses the service rate

$$\mu(m,q) = \Big[\frac{s}{\sqrt{m-q+1}} + s\Big]^{-1} \qquad (4),$$

where $s > 0$ is the expected trip time and $s/\sqrt{m-q+1}$ is the expected pick-up time when $m - q$ vehicles are idle. Demand and fleet scale together: for a fixed $\alpha > 0$ the fleet has

$$m_\lambda = \lfloor \alpha\lambda s \rfloor$$

vehicles. The load at full occupancy is $\rho(m_\lambda) = 2\lambda s/m_\lambda \to 2/\alpha$. The case $\alpha \in (0,1)$ is the supply-limited regime: there $\rho(k) > 1/\alpha > 1$ at every occupancy $1 \le k \le m_\lambda$.

In Lean the namespace is TeleDriving.AsymLimited; the functions are rho, piMN, SL, muBesbes (the rate (4)), mLam ($m_\lambda$) and maxSLRatio (the maximum below).

Formalization targets

Goal: Theorem 2.A (p. 22)

For $\alpha \in (0,1)$,

$$\liminf_{\lambda\to\infty}\ \Big[\max_{n\in\{1,\dots,m_\lambda\}}\frac{SL(m_\lambda,n)}{SL(m_\lambda,m_\lambda)}\Big] \ \ge\ 2-\alpha.$$

The theorem asserts a lower bound on the limiting gain only; it does not assert that $2-\alpha$ is attained or that the limit exists.

Milestones (Appendix D.1, pp. 44–46)

With $a = 1/\alpha$:

1. $\rho(k) > 1/\alpha$ for $1 \le k \le m_\lambda$ (p. 44).
2. The comparison probability $\tilde\pi = 1/\big[1+\sum_{i=0}^{m_\lambda-1} 1/(\rho(m_\lambda)a^i)\big]$ of (19) satisfies $\tilde\pi < \pi_{m_\lambda,m_\lambda}(m_\lambda)$ and $\tilde\pi \to (2a-2)/(2a-1)$ (p. 44).
3. For $m > 4$, $H(n) = 1/\rho(n)$ strictly increases and then strictly decreases on $[0,m]$, so it has a unique maximizer $n^*$ (p. 45).
4. For $0 < \epsilon < 1$, $\sum_{i=0}^{\lfloor(1-\epsilon)n^*\rfloor}\pi_{m_\lambda,\lfloor n^*\rfloor}(i) \to 0$ (display (21), pp. 45–46).
5. The comparison probability $\hat\pi$ of (22) satisfies $\hat\pi \to 1-(1-\epsilon)/a$ and $\hat\pi > \pi_{m_\lambda,\lfloor n^*\rfloor}(\lfloor n^*\rfloor)$ (p. 46).

Significance

Theorem 2.A quantifies the value of decoupling drivers from vehicles when vehicles are scarce. A platform that staffs only enough remote drivers to keep some vehicles idle serves, asymptotically, at least $2-\alpha$ times the fraction of demand it would serve with one driver per vehicle. The bound decreases in $\alpha$ and reaches $1$ at $\alpha = 1$, where the companion Theorem 2.B (intermediate regime, $\alpha \in (1,2)$) shows the gain vanishes. Theorems 2.A–2.C together describe how the benefit of remote driving changes from supply-limited to supply-rich markets.

The result is proved in the paper, by explicit comparison distributions. As far as is known it has not been machine-checked; no ride-hailing or state-dependent loss-system result of this kind is formalized in Mathlib or on the platform. A formal proof would establish the asymptotics of a birth–death loss system whose rates depend on the system size in a non-classical way, using only elementary real analysis: geometric series, floors and limits of explicit expressions. The intermediate statements, such as the vanishing of the low-occupancy mass, are reusable for the sibling missions on Theorems 2.B and 2.C.

Difficulty

The obvious argument compares the two blocking probabilities with an Erlang loss system, but the load $\rho(q)$ is not constant: it depends on $q$, on $m_\lambda$ and on $\lambda$ simultaneously, and all three grow together. Neither the stationary distribution with $m_\lambda$ drivers nor the one with the optimal number of drivers converges to a fixed geometric law. The goal concerns a ratio of two quantities that both tend to explicit nonzero limits only after the distribution has been localized near a moving maximizer $n^*$ of $1/\rho$. That maximizer has a closed form only through cube roots, and the localization has to hold uniformly as $\lambda \to \infty$. The two bounds also use different comparison distributions, and the floors $\lfloor n^*\rfloor$, $\lfloor(1-\epsilon)n^*\rfloor$ and $\lfloor\alpha\lambda s\rfloor$ must be controlled at the same time.

Formalization scope

• Model. $\mu$ is a function ℕ → ℝ → ℝ; the rate (4) is muBesbes s. $\rho$ takes a real occupancy, while $\pi_{m,n}(q)$ and $SL(m,n)$ take natural arguments. $\pi_{m,n}$ is written as one quotient of products; it equals (2)–(3). The objects carry the page's meaning only on the page's domains ($1 \le q \le m$ for $\rho$, $0 \le q \le n \le m$ for $\pi$), because Lean's division by $0$ returns $0$ and Real.sqrt of a negative number returns $0$. Every statement stays inside these domains.
• Standing hypotheses. $s > 0$ and $\alpha \in (0,1)$. Assumptions 1–2 and the size restriction of p. 13 are part of the shared model file but are not hypotheses here: the rate (4) satisfies them, and the size restriction holds for all large $\lambda$.
• Maximum. $\max_{n\in\{1,\dots,m\}}$ is a supremum over Fin m with index $n \mapsto n+1$. It ranges over $n \in \{1,\dots,m_\lambda\}$ only, and $m_\lambda \ge 1$ for large $\lambda$.
• Limits. $\liminf \ge c$ is stated in $\varepsilon$-form (for every $\varepsilon > 0$, eventually $\ge c-\varepsilon$), and $\lim$ as Filter.Tendsto along atTop on $\mathbb R$. The $\varepsilon$ of the liminf is not the $\epsilon$ of D.1's cut-off $(1-\epsilon)n^*$, which is named eps.
• The maximizer $n^*$. It is a function of $\lambda$, characterized by a hypothesis that holds for all large $\lambda$: $n^*(\lambda) \in [0,m_\lambda]$ maximizes $H$ there. It is not computed from the closed form (20), whose cube roots of negative numbers Lean's Real.rpow does not represent. The unimodality milestone is stated for every $m > 4$ and $\lambda > 0$; the page states it for $m = m_\lambda$.
• Eventual inequalities. The strict inequalities $\tilde\pi < \pi$ and $\hat\pi > \pi$ are stated for large $\lambda$, because they fail in degenerate small cases ($m_\lambda = 1$; $\lfloor n^*\rfloor = \lfloor(1-\epsilon)n^*\rfloor$).
• Ruled out. No hypothesis states a limit of $\pi_{m_\lambda,m_\lambda}(m_\lambda)$ or of any ratio, so the goal cannot be trivialized. The maximum is not taken over all $n$, so values of $\pi_{m,n}$ outside the page's domain cannot enter.

No external library is needed beyond Mathlib. Proofs of any milestone are welcome, and so are alternative proofs of the goal that bypass them.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757 ; published in Management Science, 2024, https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2112