Operations Research

Motivation

Ranking and selection asks which of $M$ simulated alternatives has the largest mean, when each simulation run returns one noisy sample and the simulation budget is limited. A large literature allocates the budget using the large-deviations analysis of Glynn and Juneja (2004): for a static allocation in which alternative $x$ receives a fixed fraction $\alpha_x$ of the samples, the probability of incorrect selection decays exponentially, and the allocation that maximizes the decay rate is characterized by a system of nonlinear optimality conditions. Those conditions depend on the unknown means, so practical procedures plug in estimates and solve the system repeatedly, which is costly and comes with few guarantees.

Chen and Ryzhov (Proc. 2019 Winter Simulation Conference) propose Balancing Optimal Large Deviations (BOLD), a sequential rule that never solves the optimality conditions: at each step it evaluates the two sides of one condition at plug-in estimates and samples whichever alternative appears to be falling behind. It has no tuning parameters and applies to any sampling distribution whose rate function can be evaluated. The paper states that BOLD learns the optimality conditions with probability 1; the full proofs are in the companion article (Chen and Ryzhov, Management Science, 2023).

Setting

There are $M > 2$ alternatives with distinct means $\mu_1,\dots,\mu_M$; the best is $x^* = \arg\max_x \mu_x$. Alternative $x$ produces independent samples from a law $F_x$ with mean $\mu_x$, a member of a distributional family $\{F_x(\theta)\}$ indexed by its mean $\theta$. The families may differ between alternatives.

The rate function of the member with mean $\theta$ is the Fenchel–Legendre transform of its log-moment generating function,

$$I_x(u;\theta) = \sup_{\gamma}\big(\gamma u - \log \mathbb E\,e^{\gamma W}\big),\qquad W \sim F_x(\theta),$$

with values in $[0,\infty]$, and $D_x(u;\theta) = \partial I_x(u;\theta)/\partial u$. For a normal law with variance $\lambda_x^2$, $I_x(u;\theta) = (u-\theta)^2/(2\lambda_x^2)$.

An allocation chooses alternative $x^n$ at stage $n = 0,1,\dots$. Write $N^n_x$ for the number of samples of $x$ among stages $0,\dots,n-1$ and $\theta^n_x$ for their mean (an arbitrary $\theta^0_x$ while $N^n_x = 0$). The plug-in rate is $I^n_x(\cdot) = I_x(\cdot;\theta^n_x)$, likewise $D^n_x$. For $x \ne y$, $u^n_{x,y}$ is the solution of

$$N^n_x D^n_x(u) + N^n_y D^n_y(u) = 0 \qquad (10)$$

and $\Gamma^n_{x,y} = N^n_x I^n_x(u^n_{x,y}) + N^n_y I^n_y(u^n_{x,y})$ (11).

BOLD (Figure 1 of the paper): let $x^{*,n}$ be the leader, an alternative with the largest $\theta^n_x$. If the leader is not unique, sample the tied leader with the fewest samples. Otherwise sample the leader if

$$\sum_{x\ne x^{*,n}} \frac{I^n_{x^{*,n}}(u^n_{x^{*,n},x})}{I^n_x(u^n_{x^{*,n},x})} > 1, \qquad (12)$$

and if not, sample the $x \ne x^{*,n}$ minimizing $\Gamma^n_{x^{*,n},x}$ (13). Remaining ties are broken arbitrarily.

Formalization targets

Goal: BOLD learns the optimality conditions

Under Assumptions 1–4 of the paper, with probability 1,

$$\lim_{n\to\infty}\sum_{x\ne x^*}\frac{I^n_{x^*}(u^n_{x^*,x})}{I^n_x(u^n_{x^*,x})} = 1 \quad\text{and}\quad \lim_{n\to\infty}\frac{\Gamma^n_{x^*,y}}{\Gamma^n_{x^*,z}} = 1 \ \text{ for all } y,z\ne x^*.$$

These are the plug-in forms of the total balance condition (5) and the individual balance conditions (6), which together characterize the optimal static allocation. The paper states them as Theorems 3 and 4; the goal is their conjunction.

Milestones

1. Theorem 1 (consistency). Under Assumptions 1–3, $N^n_x \to \infty$ for every $x$, almost surely.
2. Theorem 2. Under Assumptions 1–3, $\limsup_n N^n_x/N^n_y < \infty$ for all $x, y$, almost surely.
3. Theorem 3. The total balance limit above.
4. Theorem 4. The individual balance limit above.

Significance

The result. Convergence of BOLD to the optimality conditions shows that the static optimum of Glynn and Juneja can be learned by a cheap sequential rule without knowing the proportion of the budget the best alternative should receive. Top-two methods require that proportion as an input. The paper claims the guarantee for any sampling distributions satisfying four regularity assumptions, not only normal ones. As the paper notes, convergence to the static optimum does not by itself transfer the static exponential rate to the adaptive procedure; the result concerns learning the conditions.

The formalization. The WSC paper gives proof outlines only, and the complete argument lives in a long journal article. No part of it has been machine-checked. A formal proof would check a strong-law argument for an adaptive procedure with two interleaved decision criteria and would yield a reusable formal model of sequential sampling for ranking and selection with general rate functions.

Difficulty

The obvious argument is "sample means converge, hence the plug-in conditions converge". It fails because the sample means converge only if every alternative is sampled infinitely often, and BOLD gives no forced exploration: an alternative is sampled only when (12) or (13) selects it. Consistency must therefore come from the structure of the rule itself. Even with consistency, the limits in Theorems 3–4 are not continuity statements: the plug-in quantities depend on the sample sizes as well as the sample means, and they oscillate around the level 1 as (12) alternately holds and fails, so convergence requires quantitative control of how long the rule can neglect any one alternative. Discrete sampling laws add ties among sample means and a sample mean that can coincide with another alternative's true mean (Assumption 3).

Formalization scope

• Model. Alternatives are Fin M with 2 < M (indexed from 0). The family is Fam : Fin M → ℝ → Measure ℝ of probability measures, with true law Fam x (μ x). Samples form an observation array W x k (the $(k+1)$-th sample of $x$), mutually independent, with W x k ∼ Fam x (μ x); this gives the same law of the sample path as the paper's sequential sampling.
• Rate function. $I_x(u;\theta)$ is the extended-real Legendre transform of the extended-real log-MGF, from the published BellWilliams2001.ThresholdPolicy.LargeDeviation, so $+\infty$ is a genuine value. $D_x$ is the derivative of its real part. Conditions on $D_x$ are imposed on the effective domain $\mathcal D_x$, where $I_x$ is finite nearby.
• Parameter space. For each $x$ there is an open interval $\Theta_x \supseteq H_x$ that contains the samples almost surely, on which $F_x(\theta)$ has mean $\theta$ and $I_x(\cdot;\theta)$ is finite between any two parameters. The initial means lie in $\Theta_x$. These conditions are not printed, but without them the plug-in rule can starve an alternative forever: a law with $I_x(\cdot;\theta) = +\infty$ off one point gives $\Gamma = +\infty$. Bernoulli laws, whose sample means reach $0$ or $1$, fall outside this convention, although the paper says they are covered.
• Assumptions. The interval $H$ of Assumptions 1–2 is one fixed interval $H_x = [a_x,b_x]$ per alternative with $\mu_x$ in its interior. Assumption 3 is written without division. Assumption 4 is joint $C^1$ on $\mathcal D_x$.
• Algorithm. BOLD is a predicate IsBOLD on allocation sequences, so every tie-breaking rule is covered. The initial means $\theta^0$ are arbitrary. The solution of (10) is a chosen solution between the two sample means; its uniqueness is the paper's claim, not a hypothesis.
• Conventions. Ratios and $\Gamma$ are in $[0,\infty]$, with $a/0 = \infty$ for $a > 0$, so a never-sampled leader triggers (12) as in the paper. Theorem 2's limsup is taken in $[0,\infty]$. Every theorem is an almost-sure statement, with "probability 1" taken from §4.
• Ruled out. The theorems are not vacuous: a BOLD run exists on every realization (a local check proves this). The rate function is the Legendre transform of the actual family, not an unconstrained function. The family is not fixed to the normal or any single parametric case.

The development needs strong laws of large numbers along adaptively chosen sample counts, properties of Legendre transforms of log-moment generating functions (convexity, a unique zero at the mean), and law-of-the-iterated-logarithm-type rates for sample means. Lemmas on Legendre transforms of log-MGFs and the observation-array model are reusable for other large-deviations allocation rules. Contributions toward any milestone are welcome. Statements specialized to normal families are not substitutes for the general milestones.

Selected references

• Y. Chen and I. O. Ryzhov, Balancing Optimal Large Deviations in Ranking and Selection, Proc. 2019 Winter Simulation Conference, pp. 3368–3379, IEEE.
• Y. Chen and I. O. Ryzhov, Balancing Optimal Large Deviations in Sequential Selection, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4527
• P. Glynn and S. Juneja, A Large Deviations Perspective on Ordinal Optimization, Proc. 2004 Winter Simulation Conference, pp. 577–585, IEEE.
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 2009. https://doi.org/10.1007/978-3-642-03311-7

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

Ride-hailing platforms such as Uber and Lyft match riders with self-scheduling drivers who decide for themselves whether to work. Two features make capacity planning on such a platform different from classical fleet management. Demand is spatially imbalanced: more trips start in some locations than end there, so cars accumulate where they are not needed unless they drive back empty. And capacity is endogenous: the number of participating drivers depends on what drivers expect to earn, which in turn depends on how the platform uses them.

Afèche, Liu and Maglaras (MSOM 2023) study how much a platform gains from two operational controls under these conditions: admission control (rejecting some ride requests, depending on destination) and centralized repositioning (directing idle drivers to move empty between locations). The benchmark of their comparison is the regime in which the platform has both controls, called centralized control (regime $C$). This mission formalizes the paper's characterization of that benchmark: how a fixed number of drivers should be allocated, what each driver then earns, and why the resulting driver equilibrium is the platform's optimum.

Setting

There are two locations and four routes $lk$, $l,k\in\{1,2\}$. Route $lk$ has potential demand rate $\Lambda_{lk}$ and travel time $t_{lk}>0$. The price is $p$ per unit of travel time; the platform keeps a share $\gamma\in(0,1)$ and drivers keep $\bar\gamma p$, with $\bar\gamma=1-\gamma$, while paying a driving cost rate $c$, with $\bar\gamma p-c>0$. Demand is imbalanced: $0<\Lambda_{12}<\Lambda_{21}$ (Assumption 1). Repositioning is profitable: $c\,t_{12}<t_{21}(\bar\gamma p-c)$ and $c\,t_{21}<t_{12}(\bar\gamma p-c)$ (Assumption 2).

A pool of $N$ potential drivers has opportunity cost rates drawn from a continuous distribution with CDF $F$, strictly increasing on $[0,\bar c_o]$ with $\bar c_o\ge p-c$, $F(0)=0$ and $F(\bar c_o)=1$ (Assumption 3). If drivers expect a profit rate $\pi$, then $n=NF(\pi)$ of them participate.

In steady state the platform splits a driver capacity $n$ into service capacity $s_{lk}\le S_{lk}:=\Lambda_{lk}t_{lk}$ on each route, repositioning capacity $r_{12},r_{21}$ (empty driving) and queueing capacity $q_1,q_2$ (idle drivers). With totals $\bar s$, $\bar r$, $\bar q$ and $\bar S=\sum_{lk}S_{lk}$, the set $\mathcal C_C(n)$ of feasible allocations is

$$\frac{s_{12}+r_{12}}{t_{12}}=\frac{s_{21}+r_{21}}{t_{21}},\qquad \bar s+\bar r+\bar q=n,\qquad 0\le s\le S,\ r\ge0,\ q\ge0 .$$

The first equation balances the flows of cars between the locations. The platform earns $\Pi(s)=\gamma p\bar s$; each driver earns

$$\pi(s,r,n)=\frac{(\bar\gamma p-c)\bar s-c\bar r}{n}.$$

The platform's problem (13) maximizes $\Pi(s)$ over $(s,r,q,n)$ with $(s,r,q)\in\mathcal C_C(n)$ and the participation equation $n=NF(\pi(s,r,n))$; its value is $\Pi^*_C$.

The paper solves (13) in two steps. Step 1 fixes $n$, computes the maximal revenue $\Pi_C(n)$ over $\mathcal C_C(n)$, and among the revenue-maximizing allocations selects one that maximizes $\pi$, giving the per-driver profit $\pi_C(n)$. Step 2 solves $n_C=NF(\pi_C(n_C))$. The constants

$$n^C_1:=\bar S-(\Lambda_{21}-\Lambda_{12})t_{21},\qquad n^C_2:=\bar S+(\Lambda_{21}-\Lambda_{12})t_{12}$$

split capacities into scarce, moderate and ample zones.

Formalization targets

Goal: Corollary 1

$$\pi_C \text{ continuous and nonincreasing on }(0,\infty),\ \text{strictly decreasing on }(n^C_1,\infty);\qquad \exists!\,n_C>0:\ n_C=NF(\pi_C(n_C));$$ $$\pi_C(n)=\max_{(s,r,q)\in\mathcal C_C(n)}\pi(s,r,n)\quad(0<n\le N);\qquad \Pi^*_C=\Pi_C(n_C),\ \text{attained by the two-step tuple at } n_C .$$

Milestones

1. Proposition 1(1)–(3): the selected optimal allocation in each zone — $\bar s=n$, $r=q=0$ for $n\le n^C_1$; $\bar s+r_{12}=n$ with $r_{12}=\frac{t_{12}}{t_{12}+t_{21}}(n-n^C_1)$, $r_{21}=0$, $q=0$ for $n^C_1<n\le n^C_2$; $\bar s=\bar S$, $r_{12}=n^C_2-\bar S$, $r_{21}=0$, $\bar q=n-n^C_2$ for $n>n^C_2$.
2. Display (18): the closed form of $\pi_C(n)$ in the three zones.
3. Lemma 1 at $X=C$: if $\pi_C$ is driver-optimal (16) and nonincreasing, the two-step solution solves (13).

Significance

The corollary is what makes centralized control a usable benchmark. It says the platform's joint problem, which couples a linear program with a fixed-point equation in $n$, decomposes: the platform can optimize a fixed capacity and then let drivers settle, with no loss. Under the other regimes of the paper this alignment of platform and driver incentives can fail, and the paper's comparisons of regimes (value of admission control, value of repositioning) are measured against the regime-$C$ optimum characterized here. Proposition 1 also makes explicit that a centralized platform keeps drivers idle only when all demand is served.

The paper's proofs are in its e-companion, which is not part of the source this mission cites; no machine-checked version of these results exists. The mission produces a checked parametric solution of a small linear program, a checked closed form of the per-driver profit, and a checked equilibrium-and-optimality argument, with every standing assumption made explicit.

Difficulty

Proposition 1 is a parametric linear program in eight variables, but stating its solution is not enough: each zone needs an upper bound on $\bar s$ valid on all of $\mathcal C_C(n)$, and a second optimization (per-driver profit) over the set of revenue maximizers, which is not a singleton. Driver-optimality (16) is a separate claim about a different objective over the full set $\mathcal C_C(n)$; it holds only because Assumption 2 makes the capacity used for excess cross-location demand still profitable for drivers. Finally, Lemma 1 compares tuples of (13) at different capacities, which requires monotonicity of $\Pi_C$ and $\pi_C$ in $n$ and the participation equation at both capacities. The natural reading of "$n^*_C=n_C$" as uniqueness of the optimal capacity is false when $n_C>n^C_2$, since wasteful repositioning can keep revenue $\gamma p\bar S$ at a smaller capacity; the targets assert attainment instead.

Formalization scope

All objects live in the namespace RideHailing.Central, in one definition file. Routes are named fields (Λ11 … Λ22, t11 … t22), not indexed. $F$ is ProbabilityTheory.cdf μ of a measure μ on $\mathbb R$. The standing hypothesis Model.Standing bundles $0<\gamma<1$, $\bar\gamma p-c>0$, Assumptions 1–3 as printed, and the paper's implicit conventions, made explicit: $t_{lk}>0$, $\Lambda_{11},\Lambda_{22}\ge0$, $p>0$, $N>0$, $c>0$, $\mu$ a probability measure with continuous CDF.

$\Pi_C(n)$ and $\pi_C(n)$ are defined as suprema over the allocation problem; every target states attainment with IsGreatest or with membership in the selected set, so no conclusion rests on a supremum convention. Capacities in (13) and (16) are strictly positive, because (12d) divides by $n$.

Trivializing formalizations are ruled out: $\pi_C$ is defined through the two-step selection, never by its closed form (18); "max" is never an unattained supremum; feasibility for (13) includes the participation equation and $n>0$; and $n_C$ is characterized by $\exists!$ and then quantified over, never chosen.

Regimes $M$ and $A$ of the paper, which need objects defined only in the e-companion, are out of scope, as are the reformulation of §2.4 and Remark 2. Proofs of any milestone, and lemmas on monotonicity of $\Pi_C$ or attainment of linear programs over $\mathcal C_C(n)$, are welcome.

Selected references

• P. Afèche, Z. Liu, C. Maglaras, Ride-Hailing Networks with Strategic Drivers: The Impact of Platform Control Capabilities on Performance, Manufacturing & Service Operations Management, Articles in Advance, 2023. https://doi.org/10.1287/msom.2023.1221

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

The European Union's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers privacy rights over the personal data that firms collect: data may be collected only with explicit consent (opt-in), consent is separated from the purchase itself, and a consumer may later have her data deleted (erasure, the "right to be forgotten"). The same regulations carry a data security mandate, because data held by a firm is exposed to breaches. Regulators, firms and economists want to know how these rights change what data is collected, what prices are charged, and who gains.

Ke and Sudhir (SSRN 3643979; published in Management Science, 2022, doi:10.1287/mnsc.2022.4614) build a two-period model in which a firm sells a basic good, may collect a consumer's data with her consent, and uses the data to sell a personalized good in the second period. Consumers trade off the personalization benefit against the expected cost of a data breach. This mission formalizes the paper's first main result, Proposition 1: the equilibrium of the monopoly market with privacy rights. The companion mission (number 2 of this series) formalizes the benchmark without privacy rights.

Setting

A monopolist faces a unit mass of consumers whose valuation $v$ of the basic good is uniform on $[0,1]$. A consumer values the personalized good at $(1+\kappa)v$, where $\kappa\in\{\kappa_L,\kappa_H\}$ with probability $1/2$ each and $\kappa_H>\kappa_L>0$. Write

$$\mu=\frac{\kappa_H+\kappa_L}{2},\qquad \sigma=\frac{\kappa_H-\kappa_L}{2}.$$

A consumer learns her $\kappa$ only after the first period, and the firm never learns it. Both sides discount the second period by $\delta\in(0,1]$. Each period in which the firm holds a consumer's data costs her an expected breach cost $c\ge0$.

Period 1. The firm posts a price $p_1$. Each consumer chooses among not buying, buying without opting in, and buying and opting in. Opting in reveals $v$ to the firm and costs $c$.

Period 2. The firm posts a basic price $p_2$ and offers each opted-in consumer a personalized price $r(v)$. A consumer who did not opt in buys the basic good iff $v\ge p_2$; she never opts in in the last period. An opted-in consumer either keeps her data and buys the personalized good, with utility $(1+\kappa)v-r(v)-c$, or erases her data and takes $\max\{v-p_2,0\}$.

An equilibrium is a profile $(p_1,\ p_2(\cdot),\ r(\cdot,\cdot),\ \text{choice}(\cdot,\cdot))$ in which every personalized price $r(v,q)$ maximizes the expected revenue from consumer $v$ at basic price $q$; after every first-period price $p_1$, the basic price $p_2(p_1)$ maximizes the firm's second-period profit; after every $p_1$, every consumer's first-period action is optimal; and $p_1$ maximizes the firm's total profit over all real prices. The paper also imposes Assumption 1:

$$\mu\ \ge\ \max\Big\{(3+\delta)\sigma,\ \tfrac12+(2+\delta)\sigma\Big\}.$$

Formalization targets

Goal: Proposition 1

Under Assumption 1, an equilibrium exists with the following outcome in each regime. The constants $v_1^*$ and $P_1^*$ are those of the paper's appendix.

• A. $0\le c\le\delta\sigma/2$: $p^*_{1M}=P_1^*$ and $p^*_{2M}=1$. Consumers with $v\ge v_1^*$ opt in and then buy the personalized good at $(1+\mu-\sigma)v-c$. Consumers with $v<v_1^*$ never buy.
• B. $\delta\sigma/2<c\le\delta\sigma/\sqrt2$: $p^*_{1M}=1/2$ and $p^*_{2M}=1$. Consumers with $v\ge c/(\delta\sigma)$ opt in and pay $(1+\mu-\sigma)v-c$. Those with $1/2\le v<c/(\delta\sigma)$ buy only in period 1. The rest never buy.
• C. $\delta\sigma/\sqrt2<c<\delta\sigma$: $p^*_{1M}=p^*_{2M}=1/2$. Consumers with $v\ge c/(\delta\sigma)$ opt in and pay $(\mu-\sigma)v+1/2-c$. Those with $1/2\le v<c/(\delta\sigma)$ buy the basic good in both periods. The rest never buy.
• D. $c\ge\delta\sigma$: no one opts in, $p^*_{1M}=p^*_{2M}=1/2$, and a consumer buys in each period iff $v\ge1/2$.

Milestones

The equilibrium personalized price, eqs. (1)–(2):

$$r^*_M(v,p_2)=(\mu-\sigma)v+\min\{v,p_2\}-c,$$

which is optimal whenever $2(\kappa_Lv-c)\ge\kappa_Hv-c\ge0$, a condition Assumption 1 guarantees above the opt-in threshold.

The opt-in threshold, eq. (4):

$$v^*_M(p_1)=\max\Big\{\frac{c}{\delta\sigma},\frac{p_1+c}{1+\delta\sigma}\Big\}.$$

The second-period basic price, eq. (3): $p^*_{2M}(p_1)=1/2$ if $v^*_M(p_1)\ge1/\sqrt2$, and $1$ otherwise.

The remaining milestones are the identification of the firm's profit with the reduced first-period profit of p. 15, and the three cases of the appendix proof that locate its maximizer.

Significance

Proposition 1 is the basis of the paper's comparative statics and policy conclusions. The comparison with the benchmark (Proposition 2) shows when privacy rights raise or lower opt-in, profits and consumer surplus. Corollary 3 shows that under privacy rights, opt-in and profit fall strictly with the breach cost. In the paper's interpretation, the result explains how data-security investment and the rights themselves interact: privacy rights let consumers avoid the hold-up problem of sharing data before knowing its value to them.

The result is proved on paper in the appendix, by reducing the game to a piecewise-quadratic maximization. It has not been machine-checked. A formal proof adds a fully specified equilibrium concept with optimality at every history and an explicit treatment of tie-breaking and knife-edge regimes. It also corrects one misprint in the SSRN text (the price in case B(i)). This is the platform's first two-period data-market game with opt-in and erasure; existing privacy items are one-shot models.

Difficulty

The difficulty is that the goal is a statement about a game, not about the closed forms. A solver must exhibit strategies at every history, including first-period prices far from equilibrium and arbitrary basic prices. They must then show that the consumers' choices form a threshold set whose measure and integrals are the ones the reduced profit assumes.

The tempting shortcut is to read eq. (2) as the firm's personalized price everywhere. Eq. (1) shows it is optimal only in case (i); for small $v$ the firm prefers to price only to the high type or to let both types erase. The equilibrium survives because no such consumer opts in, which must be shown from the consumers' side. The global maximization of the first-period profit over all real $p_1$ involves a function with kinks at $p_1=c/(\delta\sigma)$, at the price where $v^*_M(p_1)=1/\sqrt2$, and where $v^*_M(p_1)$ reaches $1$. Both halves of Assumption 1 are used in comparing its pieces.

Formalization scope

Parameters are a structure Params with fields kL, kH, d ($\delta$) and c; $\mu$, $\sigma$, the standing assumptions ($0<\kappa_L<\kappa_H$, $0<\delta\le1$, $0\le c$) and Assumption 1 are definitions, and every theorem carries both predicates as hypotheses. Consumers are $v\in[0,1]$ with Lebesgue measure. Expectations over $\kappa$ are averages of the two types. All quantities are real numbers, and prices range over all of $\mathbb R$.

Committed conventions:

• An indifferent consumer buys.
• An opted-in consumer keeps her data on a tie.
• "No basic good is offered" is the basic price $1$.
• The goal asserts existence of an equilibrium with the stated outcome, not uniqueness, which the paper does not claim.
• The knife-edge $c=\delta\sigma/\sqrt2$ belongs to B, as in the proposition.
• In B(i) the formal statement uses the price $(1+\mu-\sigma)v-c$ that eq. (2) gives when no basic good is sold; the SSRN text prints C's price there.

Profits are integrals over the sets of consumers defined by the profile's own choices. A formalization that defined profits by the paper's closed forms would be trivial and is excluded. So are optimality checked only on the equilibrium path, a dropped Assumption 1, a missing bullet of the proposition, and a uniqueness claim. A sorry-free check confirms that the hypotheses are satisfiable at the paper's figure point $\kappa_L=4$, $\kappa_H=6$, $\delta=0.8$.

The development needs interval integrals and Lebesgue measure of intervals on $\mathbb R$, and elementary real inequalities with square roots. The reduced-profit identity (consumers' optimal choices form threshold sets up to null sets) is the reusable core and would serve the benchmark mission too. Proofs of individual milestones are welcome independently.

Selected references

• T. Tony Ke and K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, SSRN working paper 3643979 (pdfTeX build 2022-09-14). https://ssrn.com/abstract=3643979
• T. Tony Ke and K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4614
• Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

Motivation

Cutting plane methods minimize a convex function, or find a point in a convex set, using only a separation oracle: a routine that, given a query point, either certifies it is good or returns a halfspace containing the target. Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) gave a cutting plane method for a convex set in $\mathbb R^n$ inside a box of radius $R$ that uses an expected $O(n\log(nR/\epsilon))$ oracle calls and $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time, improving on the $O(n^{\omega+1}\log(nR/\epsilon))$ additional time of Vaidya's method from over 25 years earlier, and derived from it faster algorithms for submodular function minimization, matroid intersection and submodular flow.

The speed-up depends on not recomputing the leverage scores of the current constraint matrix from scratch at every step. The algorithm maintains approximations and refreshes a few of them per step. Section 7.2 of the paper isolates the bookkeeping question this raises as a two-player game, the stochastic chasing $\vec 0$ game, and shows that a simple greedy strategy keeps the accumulated error small. The game is self-contained and has nothing to do with convexity: it is a statement about a random walk in $\mathbb R^m$ that is partially reset at every step.

Setting

Fix a dimension $m\ge1$ and constants $c>0$, $R>0$. For $\vec v\in\mathbb R^m$, $\|\vec v\|_\infty=\max_i|v_i|$ and $\|\vec v\|_2=(\sum_iv_i^2)^{1/2}$.

A point starts at $\vec x^{(1)}=\vec 0$. Each round $k=1,2,\dots$ runs as follows (Algorithm 4).

1. A stochastic adversary chooses a probability distribution $\mathcal D^{(k)}$ on $\mathbb R^m$ with mean $\vec 0$ and $\|\vec\Delta\|_2\le c$ for every $\vec\Delta$ in its support.
2. The adversary chooses an observation $\vec y^{(k)}$ with $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$.
3. The player chooses a coordinate $i^{(k)}$, knowing only $\vec y^{(k)}$: neither $\vec x^{(k)}$, nor $\mathcal D^{(k)}$, nor the step.
4. A step $\vec\Delta^{(k)}$ is drawn from $\mathcal D^{(k)}$ and the point moves to

$$x^{(k+1)}_{i^{(k)}}=0,\qquad x^{(k+1)}_j=x^{(k)}_j+\Delta^{(k)}_j\quad(j\ne i^{(k)}).$$

The adversary may use everything that has happened so far to make its choices. The player wants to keep $\vec x^{(k)}$ near $\vec 0$ in $\|\cdot\|_\infty$; the adversary wants to push it away. The largest-coordinate strategy is $i^{(k)}=\operatorname{argmax}_i|y^{(k)}_i|$: reset the coordinate that looks largest.

Formalization targets

Goal: Theorem 34

If the player uses the largest-coordinate strategy, then for every $p\in(0,1]$, with probability at least $1-p$,

$$\|\vec x^{(k)}\|_\infty\le2(c+R)\log\big(4mk^2/p\big)\qquad\text{for all }k\ge1.$$

The bound holds simultaneously for all rounds, against every adaptive adversary, and grows only logarithmically in $k$, in $m$ and in $1/p$.

Milestones

The milestones are the steps that the paper's proof of Theorem 34 (pp. 43–44) displays:

1. the exponential inequality $e^x\le1+x+\tfrac{x^2}{2}e^{|x|}$ and its consequence $e^{\alpha x+\alpha\delta}\le e^{\alpha x}+\alpha\delta e^{\alpha x}+\tfrac12\alpha^2\delta^2e^{\alpha x+|\alpha|c}$ for $|\delta|\le c$;
2. the one-step drift bound for the potential $\Phi(\vec x)=\sum_ie^{\alpha x_i}+\sum_ie^{-\alpha x_i}$:

$$\mathbb E_{\vec\Delta\sim\mathcal D}\,\Phi(\vec x+\vec\Delta)\le\Phi(\vec x)+\alpha^2e^{\alpha c}c^2\eta,\qquad\eta=\max\big(\max_ie^{\alpha x_i},\max_ie^{-\alpha x_i}\big);$$

3. the choice $\alpha=1/(2(c+R))$, for which $e^{2\alpha(c+R)}(\alpha(c+R))^2\le1$ and $\alpha^2e^{\alpha c}c^2\le e^{-\alpha(R+c)}$;
4. the union-bound arithmetic $1-\sum_{k\ge1}2m/\lambda_k=1-\sum_{k\ge1}p/(2k^2)\ge1-p$ for $\lambda_k=4mk^2/p$.

Significance

Within the paper, Theorem 34 is what lets the cutting plane method keep its leverage-score estimates within a bounded multiplicative error while refreshing only one estimate per step; this is one of the ingredients behind the $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time. The game reappears whenever an algorithm tracks many slowly drifting quantities with noisy observations and can afford to recompute only a few of them exactly per step, which makes the statement useful beyond this paper.

None of the statements in this mission has a machine-checked proof. The theorem is published with a proof. The mission asks for a formal proof of the statement exactly as published, with the constant $4$ inside the logarithm. A formal proof of the milestones alone would already give a reusable exponential-potential toolkit for adaptive random processes in $\mathbb R^m$.

Difficulty

The point process is not a martingale: the player's resets depend on a noisy observation, the adversary is adaptive, and the reset can hit a coordinate that is up to $2R$ smaller in absolute value than the largest one. Per-coordinate tail bounds do not suffice, because the adversary may concentrate its moves on whichever coordinates the player is not resetting. A bound that holds for all $k$ at once, with only logarithmic dependence on $k$, has to control all coordinates jointly. Establishing such joint control, with the specific constant $4$ inside the logarithm, against the most adversarial interaction between the observation error $R$ and the step size $c$, is where the work lies.

Formalization scope

• Probability model. The randomness is a probability space $(\Omega,\mu)$ with a filtration $(\mathcal F_k)_{k\ge0}$. The adversary's adaptive choice of $\mathcal D^{(k)}$ is modelled by the conditional law of the step: each coordinate of the step has conditional mean $0$ given the past, the step is measurable with respect to the next $\sigma$-algebra, and $\sum_i\Delta_i^2\le c^2$ holds everywhere. The observation $\vec y^{(k)}$ is measurable with respect to the current $\sigma$-algebra, so it is fixed before the step is drawn, and $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$ holds on the actual trajectory.
• Indexing. Coordinates are Fin m (0-based), with $m\ge1$. Lean round $k\in\mathbb N$ is the paper's round $k+1$, so the goal's bound reads $\log(4m(k+1)^2/p)$; at Lean round $0$ the point is $\vec 0$.
• Norms. $\|\cdot\|_\infty$ is Lean's sup norm on Fin m → ℝ. The step bound $\|\vec\Delta\|_2\le c$ is written as $\sum_i\Delta_i^2\le c^2$, never as a sup-norm bound. The paper's prose once writes $\|\vec\Delta\|_2^2\le c$; Algorithm 4 and the proof use $\|\vec\Delta\|_2\le c$, which is what is formalized.
• Tie rule. $\operatorname{argmax}_i|y_i|$ breaks ties by the least index; the paper's theorem is claimed for any tie rule.
• Constants. $c>0$, $R>0$ (Algorithm 4), $0<p\le1$, natural logarithm. The drift milestone adds $\alpha\ge0$.
• Not trivial by construction. The hypotheses are satisfiable by genuinely random adversaries (a fair-coin step of size $c$ is one), and the conclusion is a probability lower bound on an event, not a statement that holds vacuously; a formalization in which the observation could depend on the step, or in which the step bound were a sup-norm bound, would not be the paper's theorem.
• Out of scope. Running time, the leverage-score application (Section 7.1, Theorem 31) and the rest of the cutting plane method.
• Infrastructure. Conditional expectation with respect to a filtration, Markov's inequality and countable union bounds are in Mathlib. Supermartingale lemmas for nonnegative adapted processes, and the passage from a per-step drift inequality to a bound on the expected potential, are reusable well beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

• Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, FOCS 2015; arXiv:1508.04874v2, 2015. https://arxiv.org/abs/1508.04874
• P. M. Vaidya, A new algorithm for minimizing convex functions over convex sets, FOCS 1989; Mathematical Programming 73 (1996) 291–341. https://doi.org/10.1007/BF02592216