Missions · Prove2Me

Completed

Economics Operations Research Probability·Captain: mikedeng1

Operational Risk Management: Optimal Inspection Policy II: The Optimal Hybrid Inspection Policy Strictly Beats the Random Policy and Weakly Beats the Periodic PolicyResearch Paper

Why inspection timing matters

Banks and other financial firms lose money through operational errors: mistyped trades, missed reconciliations, compliance lapses. Regulators require the firm to hold capital against these losses, and internal audit teams spend most of their effort deciding when to inspect. Two inspection schedules are common in practice: a periodic schedule (inspect every month) and a random schedule (surprise audits). A periodic schedule leaves no error undetected for long, but an employee who knows the date can relax right after an inspection and work hard only before the next one. A random schedule removes that back-loading, but leaves some errors undetected for long stretches.

Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy (SSRN 3491006; published in Management Science, DOI 10.1287/mnsc.2021.00322), model this trade-off as a principal–agent problem with moral hazard. They show that neither pure schedule dominates the other (their Proposition 4, the subject of mission I of this series), and then propose a hybrid schedule that combines them. This mission formalizes their Proposition 5: the best hybrid schedule beats the best random schedule strictly and the best periodic schedule weakly.

The source used throughout is the authors' SSRN preprint, version of July 2023. All labels (Proposition 5, Lemma 5, (EC.55), …) and page numbers are those of that version, not of the published article.

The model

A firm (the principal) employs an agent whose errors arrive as a Poisson process with rate $\lambda e^{-a_t}$ . Here $a_t\ge0$ is the agent's effort at time $t$ since the last inspection, at unit cost $c$ . Each undetected error costs the principal $L$ per unit of time until an inspection finds it. At each inspection the agent pays a penalty $P$ per error found. The principal pays a wage $w$ per unit of time and an inspection cost $K$ per inspection, earns base profit $\mu$ , and both parties discount at rate $r$ . The agent accepts the job only if his payoff is at least his reservation payoff $\bar\pi$ . Write $\bar\mu=\mu-r\bar\pi$ .

The time $\tau$ between two inspections is drawn independently in every cycle from a law chosen by the principal, with mean $1/v$ (the frequency $v$ ):

random policy $R$ : $\tau\sim\mathrm{Exp}(v)$ ;
periodic policy $D$ : $\tau=1/v$ ;
hybrid policy $H(q)$ , $q\in[0,1]$ : inspect at time $q/v$ with probability $q$ ; otherwise wait a further $\mathrm{Exp}(v)$ time. Its distribution function is (21):

F_\tau(t)=\begin{cases}1-(1-q)e^{-v(t-q/v)}, & t>q/v,\\ q, & t=q/v,\\ 0, & t<q/v.\end{cases}

$H(1)$ is the periodic policy and $H(0)$ the random one.

Given a policy and a strategy $(v,P,w)$ , the agent chooses an effort path that maximizes his discounted payoff (1). The principal's discounted payoff is (3):

\Pi(v,P,w)=\frac{\mu-w}{r}-L\,\frac{\mathbb E[\int_0^\tau N^{a^*}_t e^{-rt}dt]}{1-\mathbb E[e^{-r\tau}]}+P\,\frac{\mathbb E[N^{a^*}_\tau e^{-r\tau}]}{1-\mathbb E[e^{-r\tau}]}-\frac{K}{e^{r/v}-1},

where $a^*$ is the agent's optimal effort and $N^{a}_t$ is the number of errors made by time $t$ in a cycle. The principal maximizes $\Pi$ over $v,P,w\ge0$ subject to participation (4)–(5). Throughout, Assumption 1 holds: $c<L\lambda/r<\bar\mu$ . The optimal payoff under policy $I$ is written $\Pi_I(S^*_I)$ .

Formalization targets

Goal: Proposition 5 (p. 20)

For every inspection cost $K>0$ there is a payoff $x_H$ achievable by some hybrid policy such that

x_R<x_H\ \text{ for all achievable random payoffs } x_R,\qquad x_D\le x_H\ \text{ for all achievable periodic payoffs } x_D .

In the paper's notation, $\Pi_{H(q^*)}(S^*_{H(q^*)})>\Pi_R(S^*_R)$ and $\Pi_{H(q^*)}(S^*_{H(q^*)})\ge\Pi_D(S^*_D)$ .

Milestones

(6), p. 10. At an optimal strategy the participation constraint binds, and $\Pi_I=V_I(v,P)$ , the reduced payoff (6).
Lemma 3, p. 13. Under $R$ the optimal effort is constant, with $e^{-a^*}=\min\{\frac{c}{P\lambda}\frac{r+v}{v},1\}$ , and it is zero when $P\le c/\lambda$ .
Lemma 5(a), pp. 19–20. Under $H(q)$ the optimal effort is given by (22): dynamic before $q/v$ , constant after it.
Lemma EC.3, p. ec8. The optimal random strategy is $S^1_R$ (effort inducement) or $S^0_R$ (error correction).
Proposition 1, p. 14. $S^1_R$ is optimal above a threshold $K_R$ and $S^0_R$ below it, in closed form with an implicitly defined $\alpha$ and $v^0_R$ .
(EC.55), pp. ec34–ec35. With zero effort, $V^0_{H(q)}(v)>V^0_R(v)$ if and only if $v>v^q$ , where $e^{qr/v^q}=1+qr/v^q+(qr/v^q)^2$ , and $v^q<qr$ .

Significance

Proposition 5 says that reducing the randomness of a surprise-audit schedule, in the hybrid way, strictly improves the principal's optimal payoff whatever the inspection cost. Combined with Proposition 4 it yields the paper's Corollary 1: when inspections are expensive, the optimal mix lies strictly between the two pure policies. The comparison is between optima: each policy is evaluated at its own best frequency, penalty and wage, with the agent best-responding.

The result is proved in the paper (pp. ec34–ec35); to our knowledge it has no machine-checked proof. Formalizing it requires a measure-theoretic treatment of renewal-type payoffs against three inspection laws, the agent's optimal control problem under each law, and the closed-form solution of the random policy (Proposition 1). The model layer (laws, payoffs, best response, achievable payoffs) is shared with mission I of this series.

Where the difficulty lies

The weak part is immediate, because the periodic policy is the hybrid policy with $q=1$ . The strict part is not a comparison of two closed forms: the hybrid optimum has no closed form, and the optimal mix $q^*$ is not computed. The random optimum itself is one of two strategies of different nature (Lemma EC.3), effort-inducing or error-correcting, and the agent's response under $H(q)$ has a different shape from his response under $R$ (Lemma 5), so the regime boundaries of the two policies do not coincide. The naive claim that $H(q)$ beats $R$ at every strategy is false: with zero effort, $V^0_{H(q)}(v)<V^0_R(v)$ whenever $v<v^q$ (EC.55), so whether mixing helps depends on the frequency.

Formalization scope

Model layer. The $\mathcal M$ error classes enter only through $\lambda=\sum_m\lambda_m$ and $L=\sum_m(\lambda_m/\lambda)L_m$ , as in the paper from p. 10 on. The model starts at the reformulated payoffs (1) and (3): the cycle decomposition of EC.4.1 is not formalized, and expected counts are $\mathbb E[N^a_t]=\lambda\int_0^te^{-a_s}ds$ , independent of $\tau$ .
Standing assumptions. $r,c,\lambda,L,\mu,\bar\pi,K>0$ and Assumption 1 ( $c<L\lambda/r<\bar\mu$ ).
Effort paths are functions of the time since the last inspection, the same in every cycle. They are measurable, nonnegative and bounded; boundedness keeps every integral finite and loses no optimal effort of Lemmas 3–5.
Frequencies are $v>0$ , because (6) contains $e^{r/v}$ .
Laws. $\mathrm{Exp}(v)$ is Mathlib's ProbabilityTheory.expMeasure v; the periodic law is a Dirac mass at $1/v$ ; the hybrid law is $q\,\delta_{q/v}$ plus $(1-q)$ times the shifted exponential law.
Optima. "Policy $A$ 's optimum beats policy $B$ 's" is stated as: some achievable $A$ -payoff is larger than every achievable $B$ -payoff. No supremum is used, so no junk value of an empty or unbounded set can make a statement true. The argmax $q^*$ of (25) is not formalized, because the paper does not prove that it exists; one dominating hybrid payoff is exactly what the comparison with $\Pi_{H(q^*)}$ asserts.
Agent optimality is tested at wage $0$ ; the wage enters (1) only as $w/r$ .
Divisions. The effort formulas (11) and (22) divide by $P$ ; they are stated under $P>c/\lambda$ , with the zero-effort case stated separately.
Implicit numbers. $\alpha$ , $v^0_R$ and $v^q$ are variables carrying their defining equations and positivity.

The goal cannot be satisfied vacuously: it asserts the existence of an achievable hybrid payoff, so an empty achievable set does not make it true.

Contributions are welcome at every level: the integral identities for the three laws (Fubini for $\mathbb E[\int_0^\tau\cdot]$ ), the pointwise solution of the agent's problem, the two-variable optimization behind Proposition 1, and the final perturbation argument. The law lemmas and the agent's problem are reusable for any renewal-type inspection model.

Selected references

Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy, SSRN 3491006, version of July 2023. https://ssrn.com/abstract=3491006
Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy, Management Science (published version; not the numbering used here). https://doi.org/10.1287/mnsc.2021.00322

9 thms2 active usersReviewed

Actuarial Science Operations Research Partial Differential Equations+1·Captain: mikedeng1

Dynamic Optimal Reinsurance and Dividend Payout in Finite Time Horizon I: The HJB Variational Inequality Has a Unique Classical Solution with v_x ≥ 1, v_xx ≤ 0 and λv_x + v_xx ≥ 0Research Paper

Dividends, reinsurance and a finite horizon

An insurer that pays dividends to its shareholders faces a trade-off studied since de Finetti (1957): paying out surplus early raises the discounted payout but brings ruin closer. Reinsurance changes the trade-off, because ceding part of each claim lowers the volatility of the surplus at the price of a reinsurance premium. When the insurer may choose both the dividend stream and, at every moment, an arbitrary reinsurance contract, the problem becomes a mixed singular–classical stochastic control problem. Most of the literature treats it on an infinite horizon, where the value function solves an ordinary differential equation. On a finite horizon $T$ the value function also depends on time to maturity, the Hamilton–Jacobi–Bellman (HJB) equation becomes a parabolic variational inequality with a gradient constraint, and neither its solvability nor the regularity of its solution is classical.

Guan, Xu and Zhou (arXiv:2008.00391v3, Mathematics of Operations Research, 2023) show by PDE methods that this variational inequality has a classical solution, identify it with the value function, and read the optimal reinsurance contract and dividend barrier off its derivatives. This mission formalizes the PDE part: Theorem 3.1 and the steps of Appendix A that lead to it.

Setting

Claims are nonnegative random variables with common distribution function $F$ , $F(0-)=0$ , possibly discontinuous. The paper assumes the tail condition

z^3\,(1-F(z))\ \text{is bounded on }[0,\infty), \tag{3.3}

so the moments $\mu_1=\int_0^\infty z\,dF(z)$ and $\mu_2=\int_0^\infty z^2\,dF(z)$ are finite. The other data are the net reinsurance loading $\gamma>0$ , the discount factor $c>0$ and the horizon $T>0$ ; the mission assumes $\gamma<\mu_1$ throughout.

A reinsurance contract is described by the retained loss $H(z)$ the insurer keeps out of a claim of size $z$ , with $0\le H(z)\le z$ ; $\mathcal H$ is the set of such functions. For a function $v(x,t)$ of the surplus $x$ and the time to maturity $t$ the operator

\mathcal Lv=\sup_{H\in\mathcal H}\Big(\frac{v_{xx}}2\int_0^\infty H(z)^2\,dF(z)+v_x\int_0^\infty H(z)\,dF(z)\Big)-\gamma v_x-cv \tag{3.2}

is the generator of the controlled diffusion approximation of the surplus. The HJB equation is the variational inequality, on $\mathcal Q_T=(0,\infty)\times(0,T]$ ,

\min\{v_t-\mathcal Lv,\ v_x-1\}=0,\qquad v(0,t)=0,\qquad v(x,0)=x. \tag{3.1}

The functions

A(y)=\int_0^{1/y}z(1-F(z))\,dz,\qquad B(y)=\int_0^{1/y}(1-F(z))\,dz\qquad(y>0),

with $A=\mu_2/2$ and $B=\mu_1$ for $y\le0$ , compute the supremum in (3.2), and $f(y)=-yA(y)+B(y)-\gamma$ has a unique root $\lambda>0$ . The penalized gradient problem (A.17) on $\mathcal Q_{L,T}=(0,L)\times(0,T]$ is

u_t-\mathcal Tu+\beta_\varepsilon(u-1)=0,\quad (\lambda u+u_x)(0,t)=f_\varepsilon(t),\quad u(L,t)=1,\quad u(x,0)=1,

with $\mathcal Tu=A(-u_x/u)u_{xx}+B(-u_x/u)u_x-\gamma u_x-cu$ , a penalty function $\beta_\varepsilon$ and a boundary datum $f_\varepsilon$ that ramps from $\lambda$ down to $0$ on $[0,\varepsilon]$ .

Formalization targets

Goal: Theorem 3.1

There is a unique $v\in C^{2,1}(\overline{\mathcal Q}_T\setminus\{(0,0)\})\cap C(\overline{\mathcal Q}_T)$ that solves (3.1) and satisfies

v_x\ge1,\quad v_t\ge0,\quad v_{xx}\le0,\quad v_{xxx}\ge0\ \text{(weakly)},\quad v_{xt}\ge0,\quad \lambda v_x+v_{xx}\ge0 .

Uniqueness is among solutions in the same class with the same six properties, as equality on $\overline{\mathcal Q}_T$ .

Milestones

(A.7)–(A.9): $A$ , $B$ are non-increasing, Lipschitz, bounded by $\tfrac12\min\{y^{-2},\mu_2\}$ and $\min\{y^{-1},\mu_1\}$ , with $y^3A'=y^2B'=F(1/y)-1$ .
(A.10): $\mathcal Lv=A(-v_{xx}/v_x)v_{xx}+B(-v_{xx}/v_x)v_x-\gamma v_x-cv$ when $v_x>0$ .
(A.12)–(A.13): $f'=-A<0$ everywhere, and $f$ has a unique root, which is positive.
Lemma A.1: $A(-y/z)$ and $B(-y/z)$ are Lipschitz on $\mathbb R\times[1,\infty)$ .
Lemma A.2: a comparison principle for (A.17) between functions $\ge1$ .
Lemma A.3: (A.17) has a $C^{2,1}$ solution, and $1\le u^\varepsilon\le Ke^{\Lambda t}/(x+1/\lambda)$ for small $\varepsilon$ , with $K=L+1/\lambda+1$ , $\Lambda=\mu_2/\gamma^2+\gamma\lambda$ .
Lemmas A.4–A.6: $u^\varepsilon_t\ge0$ , $u^\varepsilon_x\le0$ , $\lambda u^\varepsilon+u^\varepsilon_x\ge0$ , $u^\varepsilon_{xx}\ge0$ .

Significance

Theorem 3.1 is the analytic core of the paper. The verification theorem (Theorem 3.2) needs a classical solution that is increasing and concave in $x$ , which Theorem 3.1 provides, and Section 4 derives the shape of the optimal policy from (3.4)–(3.9): the optimal retained loss is $\min\{z,\,-v_x/v_{xx}\}$ , and (3.9) bounds the reinsurance barrier away from zero. Without the existence of a classical solution, the HJB equation could only be interpreted in the viscosity sense, whose uniqueness theory for this mixed singular–classical problem is not available, and the strategies would not be well defined.

The result is proved in the paper; nothing in it has been machine-checked. A formal development would produce, beyond the theorem, a reusable formal treatment of a parabolic obstacle problem with a Robin boundary condition through penalization, comparison principles for quasilinear parabolic equations, and the explicit reduction of a supremum over reinsurance contracts against an arbitrary claim distribution. The appendix lemmas (A.7)–(A.13) and Lemma A.1 are elementary real analysis and are self-contained targets.

Difficulty

The supremum in $\mathcal L$ is over a function space and $F$ may have atoms, so even the closed form (A.10) and the everywhere-differentiability of $f$ require care with one-sided derivatives at the jumps of $F$ . The operator is fully nonlinear and degenerates as $-v_{xx}/v_x\to\infty$ , since $A(y)\to0$ . The inequality carries a gradient constraint $v_x\ge1$ rather than an obstacle, and the left boundary condition $(\lambda u+u_x)(0,t)=0$ is incompatible with the initial condition at the corner $(0,0)$ , which is why the solution is only claimed to be $C^{2,1}$ away from that corner. The obvious route, solving (3.1) directly by a fixed-point argument, does not control $v_{xx}$ ; the paper differentiates in $x$ and works with the gradient $u=v_x$ , which turns the gradient constraint into an obstacle but introduces the Robin condition with the wrong sign for a direct maximum principle. The passage $\varepsilon\to0$ needs $W^{2,1}_p$ and Hölder estimates uniform in $\varepsilon$ , which are not in Mathlib.

Formalization scope

Functions of $(x,t)$ are ℝ → ℝ → ℝ; $t$ is time to maturity. Partial derivatives are explicit functions $v_x, v_{xx}, v_t$ tied to $v$ by HasDerivAt on sections at interior points ( $x>0$ , $0<t<T$ ) and continuous on $\overline{\mathcal Q}_T\setminus\{(0,0)\}$ ; boundary values are these continuous extensions, and (3.1) holds at $t=T$ through them.
The claim law is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$ , and $F(z)=\mu((-\infty,z])$ ; no density is assumed. $\mathcal H$ consists of measurable $H$ with $0\le H(z)\le z$ for $z\ge0$ , and $\mathcal L$ is defined by the supremum (3.2), not by (A.10).
$0<\gamma<\mu_1$ is a standing hypothesis (the paper imposes it from Section 4; without it $f$ has no positive root and (3.9) is undefined).
(3.7) is read as monotonicity of $x\mapsto v_{xx}(x,t)$ , (3.8) as monotonicity of $t\mapsto v_x(x,t)$ , (3.9) for every positive root of $f$ .
Uniqueness is equality on $\overline{\mathcal Q}_T$ within the class of solutions with (3.4)–(3.9). Uniqueness among all classical solutions is not posed: the paper's argument on an unbounded domain uses no growth condition.
Penalty data are taken at one fixed $\varepsilon$ ; the limit $\varepsilon\to0$ of $\beta_\varepsilon$ is not part of the data. "Sufficiently small $\varepsilon$ " is an $\varepsilon_0>0$ depending on the model and $L$ .
A formalization in which $\mathcal L$ is given by its closed form, the derivatives are deriv evaluated at boundary points, or uniqueness is stated as equality of functions on all of $\mathbb R^2$ , would trivialize or falsify the goal; the statements avoid all three.

Needed infrastructure: interval integrals of monotone functions and their one-sided derivatives, maximum and comparison principles for linear and quasilinear parabolic equations in one space dimension, existence for quasilinear parabolic problems (Leray–Schauder with Schauder estimates), and compactness in Hölder and Sobolev spaces. The parabolic comparison principle and the penalization scheme are reusable well beyond this mission. Proofs of individual milestones, in particular the elementary ones (A.7)–(A.13) and Lemma A.1, are welcome independently.

Selected references

C. Guan, Z. Q. Xu, R. Zhou, Dynamic optimal reinsurance and dividend-payout in finite time horizon, Mathematics of Operations Research, 2023; preprint arXiv:2008.00391v3. https://arxiv.org/abs/2008.00391
B. de Finetti, Su un'impostazione alternativa della teoria collettiva del rischio, Transactions of the XVth International Congress of Actuaries, 1957.
G. M. Lieberman, Second Order Parabolic Differential Equations, World Scientific, 1996. https://doi.org/10.1142/3302
L. C. Evans, Partial Differential Equations, 2nd ed., American Mathematical Society, 2010. https://doi.org/10.1090/gsm/019

13 thms2 active usersReviewed

Actuarial Science Operations Research Partial Differential Equations+1·Captain: mikedeng1

Dynamic Optimal Reinsurance and Dividend Payout in Finite Time Horizon II: For Discrete Claims the Reinsurance Boundaries Are C¹, Start at 0 and Are Spaced Less Than (z_j − z_{j−1})/2c ApartResearch Paper

Motivation

An insurance company pays out dividends to its shareholders and buys reinsurance to limit its exposure to large claims. Both decisions are dynamic: the right amount to cede and the right moment to pay depend on the current surplus and on the time left until a fixed maturity $T$ . Guan, Xu and Zhou (2023) solve the combined problem for a diffusion-approximated surplus with a general claim distribution, a general reinsurance contract (any retained-loss function $0\le H(z)\le z$ ), and a finite horizon. Their main structural output is a description of the optimal strategy by free boundaries in the surplus–time plane: a dividend barrier $d(\tau)$ , and for each claim size $z$ a reinsurance barrier $K(z,\tau)$ .

A companion mission formalizes the existence and uniqueness of the classical solution of the HJB variational inequality (Theorem 3.1 of the paper). This mission takes that solution as given and formalizes the shape of the boundaries (Section 4 of the paper), culminating in the description of the reinsurance boundaries for discrete claim distributions (Theorem 4.5).

Setting

Claims are i.i.d. copies of a nonnegative random variable $Z_1$ with distribution function $F$ , satisfying the tail condition that $z^3(1-F(z))$ is bounded on $[0,\infty)$ . Write $\mu_1=\int_0^\infty z\,dF(z)$ and $\mu_2=\int_0^\infty z^2\,dF(z)$ . The reinsurance loading is $\gamma>0$ , the discount rate $c>0$ , the horizon $T>0$ , and throughout $0<\gamma<\mu_1$ (for $\gamma\ge\mu_1$ the problem is trivial).

The value function $v(x,\tau)$ , with $x\ge0$ the surplus and $\tau\in[0,T]$ the time to maturity, is the solution of the variational inequality

\min\{v_\tau-\mathcal Lv,\ v_x-1\}=0\ \text{on }(0,\infty)\times(0,T],\qquad v(0,\tau)=0,\qquad v(x,0)=x,

where

\mathcal Lv=\sup_{0\le H(z)\le z}\Bigl(\frac{v_{xx}}{2}\int_0^\infty H^2\,dF+v_x\int_0^\infty H\,dF\Bigr)-\gamma v_x-cv .

It is the unique function of class $C^{2,1}([0,\infty)\times[0,T]\setminus\{(0,0)\})\cap C([0,\infty)\times[0,T])$ that solves this inequality and satisfies $v_x\ge1$ , $v_\tau\ge0$ , $v_{xx}\le0$ , $v_{xx}$ nondecreasing in $x$ , $v_x$ nondecreasing in $\tau$ , and $\lambda v_x+v_{xx}\ge0$ . Here $\lambda$ is the unique positive root of

f(y)=-yA(y)+B(y)-\gamma,\qquad A(y)=\int_0^{1/y}z(1-F(z))\,dz,\quad B(y)=\int_0^{1/y}(1-F(z))\,dz\quad(y>0).

The no-dividend region is $\mathcal{ND}=\{(x,\tau): v_x(x,\tau)>1\}$ , and the dividend boundary is

d(\tau)=\inf\{x\ge0: v_x(x,\tau)=1\}.

For a claim of size $z$ the optimal retained loss is $-v_x/v_{xx}$ if $-v_{xx}/v_x>1/z$ and $z$ otherwise, and the ceded loss $\hat I(z,x,\tau)$ is the difference from $z$ . The reinsurance boundary is $K(z,\tau)=\sup\{x>0: -v_{xx}/v_x(x,\tau)>1/z\}$ . For a discrete law $\mathbb P(Z_1=z_j)=p_j>0$ with $0<z_1<\dots<z_N$ , the $j$ -th reinsurance boundary is

K_j(\tau)=\inf\Bigl\{x>0: -\frac{v_{xx}}{v_x}(x,\tau)\le\frac1{z_j}\Bigr\}.

Formalization targets

Goal: Theorem 4.5

For a discrete claim law, every $K_j$ is continuously differentiable on $(0,T]$ , and for every $\tau\in(0,T]$ :

K_j(\tau)=0\ \text{ if }z_j\le\tfrac1\lambda;\qquad 0<K_{i_0}(\tau)<\frac{z_{i_0}-1/\lambda}{2c};\qquad 0<K_j(\tau)-K_{j-1}(\tau)<\frac{z_j-z_{j-1}}{2c}\ \ (j>i_0);\qquad \lim_{\tau\to0+}K_j(\tau)=0,

where $z_{i_0}$ is the smallest atom above $1/\lambda$ .

Milestones

Theorem 4.2: $d$ is continuous and nondecreasing on $(0,T]$ , and $d(0+)=0<d(\tau)\le\sqrt{(\mu_1+c\gamma)(c\mu_2+\gamma^2)/(\gamma c^3)}$ .
Lemma 4.3: $v_x,v_\tau\in C^{2,1}$ in $\mathcal{ND}$ , $v_{xx}<0$ in $\mathcal{ND}$ , and $\hat I(z,x,\tau)=\max\{z+v_x/v_{xx},0\}$ there.
Lemma 4.4: $-v_x/v_{xx}=1/\lambda$ at $x=0$ , $-v_x/v_{xx}>1/\lambda$ in $\mathcal{ND}$ , and $\partial_x(-v_x/v_{xx})\ge2c$ in $\mathcal{ND}$ .
Section 4.2, p. 18: for $z>1/\lambda$ , $K(z,\tau)\le z/(2c)-1/(2c\lambda)$ .

Significance

The theorems turn an existence result for a fully nonlinear variational inequality into a usable description of the optimal policy. Claims below $1/\lambda$ are never reinsured; a claim of size $z>1/\lambda$ is partly ceded only when the surplus lies below a barrier that starts at the origin at maturity, stays below $z/(2c)-1/(2c\lambda)$ , and stays below the dividend barrier, which is itself bounded by an explicit constant independent of the horizon. For discrete claims the barriers are smooth, ordered, and separated by gaps of at most $(z_j-z_{j-1})/(2c)$ . The quantity $-v_x/v_{xx}$ , the optimal retention level, is shown to grow at rate at least $2c$ in the surplus; this single monotonicity estimate is what makes the regions of the surplus–time plane ordered and nonoverlapping.

The results are proved in the paper; none of them, nor Theorem 3.1 on which they rest, has a machine-checked proof. Formalizing them requires the parabolic regularity statements of Lemma 4.3 (the paper's proof invokes interior Schauder estimates) and the implicit function theorem in a form that gives one-variable $C^1$ dependence of a level set. Statements of the boundary properties in this mission are posed for any function with the properties of Theorem 3.1, so they can be proved independently of the companion mission.

Difficulty

Most of the elementary statements reduce to a sign or a monotonicity property of $-v_x/v_{xx}$ , and the first idea is to differentiate the equation. That requires $v_{xxx}$ and $v_{x\tau}$ to exist as classical derivatives in $\mathcal{ND}$ , which the class of Theorem 3.1 does not provide: it gives only two $x$ -derivatives and one $\tau$ -derivative, and a weak monotonicity of $v_{xx}$ . Lemma 4.3's interior regularity is therefore not a formality but the gateway to Lemma 4.4, and its proof uses Hölder estimates for linear parabolic equations, which are not available in Mathlib.

The positivity $d(\tau)>0$ and the limit $d(0+)=0$ are statements about the free boundary itself, not about $v$ at fixed points, and need the uniqueness part of Theorem 3.1 or a comparison argument. The strict inequalities in (4.13)–(4.14) need more than the bound $\partial_x(-v_x/v_{xx})\ge2c$ as stated.

Formalization scope

All objects live in the namespace DynReinsDiv.Barriers. Conventions:

The claim law is a probability measure μ on $\mathbb R$ with $\mu((-\infty,0))=0$ ; $F(z)=\mu((-\infty,z])$ ; no density is assumed. $\mu_1,\mu_2$ are Bochner integrals, finite under the tail condition. The standing hypothesis $0<\gamma<\mu_1$ is a field of the model.
$v:\mathbb R\to\mathbb R\to\mathbb R$ takes $(x,\tau)$ , and the derivatives vx vxx vt are explicit functions: they are HasDerivAt derivatives of the sections at interior points ( $x>0$ , $0<\tau<T$ ) and continuous on $[0,\infty)\times[0,T]\setminus\{(0,0)\}$ ; boundary values (at $x=0$ and $\tau=T$ ) are the continuous extensions. " $v_{xxx}\ge0$ in the weak sense" is monotonicity of $v_{xx}$ in $x$ , " $v_{x\tau}\ge0$ " is monotonicity of $v_x$ in $\tau$ .
The only hypothesis on $v$ is the conclusion of Theorem 3.1, bundled as IsTheorem31Solution. The milestone conclusions ( $v_{xx}<0$ , the bounds on $-v_x/v_{xx}$ , $d(0+)=0$ ) are never hypotheses; with them as hypotheses Theorem 4.5 would be a short mean-value argument.
$\mathcal L$ is the supremum over measurable retained-loss functions, not its closed form.
Infima and suprema of empty sets are $0$ in Lean. Theorem 4.2 concludes that $\{x\ge0: v_x=1\}$ is nonempty; $K(z,\tau)$ uses $0$ for the empty set, as the paper does.
Atoms are indexed by Fin N from $0$ . The paper's index $i_0$ is replaced by conditions on $z_j$ and $z_{j-1}$ , which also cover laws whose atoms all lie below $1/\lambda$ .
Not formalized: $d(\infty)$ (the horizon is finite; $d(\tau)\le x_2$ for every $\tau\le T$ and every $T$ carries the same content), the $C^\infty$ regularity of $d$ for bounded claims (only sketched in the paper), and the Verification Theorem 3.2.

Contributions welcome: the interior regularity of Lemma 4.3, the monotonicity estimate (4.10), and the derivation of Theorem 4.5 from the milestones.

Selected references

Chonghu Guan, Zuo Quan Xu, Rui Zhou, Dynamic optimal reinsurance and dividend-payout in a finite time horizon, Mathematics of Operations Research, 2023; read as arXiv:2008.00391v3 (2022). https://arxiv.org/abs/2008.00391

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Marketplace Leakage 1: With Uniform Switching Costs the Equilibrium Fee Is min{μ, v − c}, Leakage Is Positive but Partial, and the Marketplace's Profit Increases in μResearch Paper

Motivation

Online marketplaces such as Airbnb, Amazon, eBay, Preply or Upwork earn most of their revenue from transaction fees: a seller who sells through the marketplace pays a fee on every sale. Many of these sellers also run their own sales channel, and a buyer who discovers a seller on the marketplace can often complete the purchase directly with that seller, avoiding the fee. This is marketplace leakage (also called disintermediation or showrooming of the platform). Marketplaces respond with measures the paper lists on its first pages: bundling transaction-related services, restricting buyer–seller communication before a transaction, and penalizing sellers caught taking clients off the platform.

Hagiu and Wright (Marketplace Leakage, Management Science, 2023) build a minimal model of this tension. Their baseline analysis answers the first question any of the later strategies depends on: if the marketplace can only choose its fee, what fee does it set, how much leakage remains in equilibrium, and how do these respond when buying directly becomes more costly for buyers? This mission formalizes that baseline result, Proposition 1 of the paper, for uniformly distributed switching costs.

Setting

There is one marketplace $M$ , one seller $S$ and a unit mass of buyers, each wanting one unit of $S$ 's product. Every buyer values the product at $v$ ; $S$ 's marginal cost is $c$ , with $c<v$ ; the outside option is worth $0$ .

$S$ can sell through $M$ , paying $M$ a fee $f$ per transaction, or through its direct channel, which carries no fee. It sets a price $p_m$ on $M$ and a direct price $p_d$ . A buyer who buys directly bears a switching cost $s$ ; in this mission $s$ is uniformly distributed on $[0,\mu]$ with $\mu>0$ , so its CDF is

G(s)=\min\Bigl\{\max\Bigl\{\frac s\mu,0\Bigr\},1\Bigr\}.

The timing is: $M$ sets $f$ ; observing $f$ , $S$ sets its prices; buyers then choose. The paper's Lemma 1 lets one fix $p_m=v$ , so $S$ only chooses $p_d\le v$ . A buyer buys directly iff $s\le v-p_d$ , so a share $G(v-p_d)$ of buyers — the leakage — buys directly. $S$ 's profit at fee $f$ is

\pi_f(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),

and $M$ earns $\Pi=f\,(1-G(v-p_d))$ . A direct price is seller-optimal at $f$ if it maximizes $\pi_f$ over $p_d\le v$ . An equilibrium outcome is a pair $(f,p_d)$ with $f\le v-c$ , $p_d$ seller-optimal at $f$ , such that no other fee $f'\le v-c$ , followed by a seller-optimal response, gives $M$ more.

Formalization targets

Goal: Proposition 1

For every $\mu>0$ an equilibrium outcome exists, and every equilibrium outcome $(f^*,p_d^*)$ satisfies

f^*(\mu)=\min\{\mu,v-c\},\qquad p_d^*(\mu)=v-\min\Bigl\{\frac\mu2,\frac{v-c}2\Bigr\},\qquad \Pi^*(\mu)=\begin{cases}\mu/2 & \mu\le v-c,\\ (v-c)\bigl(1-\frac{v-c}{2\mu}\bigr) & \mu\ge v-c,\end{cases}

with leakage $G(v-p_d^*)=\frac1\mu(v-p_d^*)\in(0,1)$ . As $\mu$ increases, the fee weakly increases, the direct price and the leakage weakly decrease, and the marketplace's profit strictly increases.

Milestones

(4): for every fee $f\ge0$ the seller's optimal direct price is unique and equals $v-f/2$ if $f\le2\mu$ and $v-\mu$ if $f\ge2\mu$ .
(5): at such a response the marketplace earns $f(1-f/(2\mu))$ if $f\le 2\mu$ and $0$ if $f\ge2\mu$ .
The optimal fee (proof of Proposition 1): $(f,p_d)$ is an equilibrium outcome iff $f=\min\{\mu,v-c\}$ and $p_d$ is seller-optimal at $f$ .
Equilibrium leakage (proof of Proposition 1): $G(v-p_d^*)=f^*/(2\mu)=\min\{1/2,(v-c)/(2\mu)\}$ .

Significance

Proposition 1 is the baseline against which the paper measures every anti-leakage strategy: investment in transaction benefits, communication bans, referral fees and price-parity clauses are each compared with the fee-only outcome $\Pi^*(\mu)$ , and Proposition 3 of the paper uses the closed form (6) directly. The result also has a substantive message: a fee-setting marketplace never eliminates leakage, but never lets it become total, and it gains from higher switching costs even though its own fee response offsets part of their effect on leakage.

The proposition is proved in the paper by elementary calculus. To our knowledge it has no machine-checked proof. Formalizing it produces a checked version of the baseline game, a verified statement of the seller's best response and the marketplace's value as functions of the fee, and a template that the companion missions on this paper reuse.

Difficulty

The seller's problem is not a smooth concave program: the clamped distribution $G$ creates a kink at $v-p_d=\mu$ , below which every buyer switches and the profit is linear in $p_d$ . The first-order condition $p_d=v-f/2$ is the optimum only while $f\le2\mu$ ; above that the optimum sits at the kink. The marketplace's objective inherits a kink at $f=2\mu$ , and its feasible set $f\le v-c$ adds a corner that binds exactly when $\mu>v-c$ . Negative fees are feasible and must be ruled out. The comparative statics compare equilibrium objects across two parameter values that may lie in different regimes, so the statement cannot be read off one formula.

Formalization scope

All parameters are real numbers, with the standing assumptions $c<v$ and $\mu>0$ as explicit hypotheses. $G$ is the clamped uniform CDF above. The statements use the reduced seller problem (1) with $p_m=v$ , as the paper does after Lemma 1; Lemma 1 itself, which concerns the full game in which $S$ also chooses $p_m$ , is not posed. Seller-optimality is an optimality predicate over $p_d\le v$ , and the equilibrium is an optimality predicate over feasible fees $f\le v-c$ (negative fees included); "max" is attained, not a supremum. The displays (4) and (5) are stated for $f\ge0$ , which is what they require; the paper's preface "Assuming $f\le v-c$ " is not needed and does not exclude $f<0$ .

Trivializing formalizations are ruled out: the seller's response and the marketplace's profit are not defined by the closed forms (4)–(5), the marketplace's value is not an unattained sSup, the equilibrium fee is not selected by Classical.choose, and the comparative statics are stated about equilibrium outcomes at two values of $\mu$ , not about the formulas alone.

The development needs only Mathlib's real arithmetic, min/max and order lemmas. A proof of the seller's best response for a clamped uniform distribution is reusable in the companion missions on transaction benefits, communication bans and price parity, which restate the same model. Proofs of any milestone are welcome independently.

Selected references

A. Hagiu and J. Wright, Marketplace Leakage, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4757 (formalized from the authors' manuscript dated March 2023; Proposition 1 on pp. 9–10, proof in §8.2, p. 34).

6 thms2 active usersReviewed

Probability Quantum Information Statistics·Captain: mikedeng1

Direct Fidelity Estimation from Few Pauli Measurements 2: A Unit Vector Nearly Orthogonal to 2^{cd} Given States With Every Non-Identity Pauli Expectation ≤ √(72π³)·√(log d)/√dResearch Paper

Motivation

Quantum state tomography reconstructs an unknown $d$ -dimensional quantum state from measurements on many copies of it. For $n$ qubits, $d = 2^n$ , so the number of copies a tomography procedure needs grows exponentially in $n$ , and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli measurements: each qubit is measured in the eigenbasis of one of $\sigma_x, \sigma_y, \sigma_z$ .

Flammia and Liu, Direct fidelity estimation from few Pauli measurements (arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011), show that the fidelity of an experimental state with a target pure state can be estimated with far fewer copies than full tomography needs. To make the comparison meaningful they also prove that full tomography of a pure state with Pauli measurements requires $\Omega(d^2/\log d)$ copies. That lower bound has two steps. The first builds a large family of nearly orthogonal pure states whose Pauli expectation values are all small, so that Pauli measurements extract little information about which state is present. Its engine is Lemma 1 of the paper (p. 7), the subject of this mission. The second step, an information-theoretic argument over a noisy classical channel, is not in scope.

Setting

Fix $n \ge 1$ qubits and put $d = 2^n$ . States are unit vectors $\psi \in \mathbb C^d$ , $\|\psi\|_2 = 1$ ; the overlap $\langle\varphi|\psi\rangle = \sum_x \overline{\varphi_x}\psi_x$ is conjugate-linear in $\varphi$ .

The single-qubit Pauli matrices are $I$ , $\sigma_x$ , $\sigma_y$ , $\sigma_z$ . A Pauli label $k \in \{0,1,2,3\}^n$ determines the $n$ -qubit Pauli operator $W_k = \sigma_{k_1}\otimes\cdots\otimes\sigma_{k_n}$ (with $\sigma_0 = I$ ). There are $d^2$ labels; the all-zero label gives $W_k = I$ . Every $W_k$ is Hermitian and unitary, so the Pauli expectation $\langle\psi|W_k|\psi\rangle$ is a real number in $[-1, 1]$ .

A Haar-random state is a vector $\psi$ drawn from the uniform (rotation-invariant) probability measure on the unit sphere of $\mathbb C^d$ , a real sphere of dimension $2d - 1$ . The constants of the lemma are

\varepsilon = \sqrt{9\pi^3(\log 2)\,c},\qquad \tau = \sqrt{72\pi^3},\qquad C_1 = \frac{2}{9\pi^3},

with $\log$ the natural logarithm and $c > 0$ a parameter.

Formalization targets

Goal: Lemma 1

Let $\varphi_1, \dots, \varphi_s \in \mathbb C^d$ be states with $s \le 2^{cd}$ . Then there is a state $\psi \in \mathbb C^d$ with

|\langle\varphi_i|\psi\rangle| \le \varepsilon \quad (1 \le i \le s), \qquad |\langle\psi|W_k|\psi\rangle| \le \tau\sqrt{\log d}/\sqrt d \quad (W_k \ne I).

These are (31) and (32) of the paper. The goal is an existence statement with no measure in it.

Milestones (all p. 7)

(33): for a state $\varphi$ , $|\langle\varphi|\psi\rangle - \langle\varphi|\psi'\rangle| \le \|\psi - \psi'\|_2$ .
$\mathbb E\langle\varphi|\psi\rangle = 0$ for Haar-random $\psi$ .
(34): $\Pr[|\langle\varphi|\psi\rangle| \ge \varepsilon] \le 4\exp(-C_1 d\varepsilon^2/\eta^2)$ with $\eta = 1$ .
(35): $\Pr[(31)\text{ fails for some } i] \le 4\exp(cd\log 2 - C_1 d\varepsilon^2) = 4\cdot 2^{-cd}$ .
(36): on unit vectors, $|\langle\psi|W_k|\psi\rangle - \langle\psi'|W_k|\psi'\rangle| \le 2\|\psi - \psi'\|_2$ .
$\mathbb E\langle\psi|W_k|\psi\rangle = 0$ for $W_k \ne I$ .
(37): $\Pr[|\langle\psi|W_k|\psi\rangle| \ge \tau\sqrt{\log d}/\sqrt d] \le 4\exp(-C_1\tau^2(\log d)/\eta^2)$ with $\eta = 2$ .
(38): $\Pr[(32)\text{ fails for some } k] \le 4\exp(2\log d - C_1\tau^2(\log d)/4) = 4/d^2$ .

Every constant is the paper's; none is replaced by an unspecified absolute constant.

Significance

The result. Lemma 1 is a packing statement: applied repeatedly, it yields $2^{\Omega(d)}$ states that are pairwise almost orthogonal and whose non-identity Pauli expectations are all $O(\sqrt{\log d/d})$ . Such states are hard to tell apart with Pauli measurements, since each measurement outcome is nearly unbiased. The paper converts this into the $\Omega(d^2/\log d)$ copy lower bound for full tomography with Pauli measurements (pp. 3, 7–8). Since direct fidelity estimation of an arbitrary pure state uses $O(d)$ copies (for fixed accuracy and failure probability), the lower bound is what shows that the scheme beats tomography followed by a fidelity computation by a factor of about $d$ .

Formalizing it. The lemma and its proof are published, but none of it is machine-checked: Mathlib has no Pauli operators, no concentration of measure on spheres with explicit constants, and no Levy lemma. A formal proof needs a concentration inequality on the complex unit sphere with the explicit constant $C_1 = 2/(9\pi^3)$ (or any sharper one), the vanishing of the means by symmetry, and the union bounds. Each milestone is a reusable fact about Haar-random states.

Difficulty

The two union bounds (35) and (38) and the Lipschitz estimates (33) and (36) are elementary. The central difficulty is the tail bounds (34) and (37). The paper obtains them from Levy's lemma, which it cites (P. Lévy, 1951) and does not prove; Levy's lemma rests on the isoperimetric inequality on the sphere, which Mathlib does not have, and (37) concerns a quadratic form of $\psi$ rather than a linear one. Both tail bounds also need a working theory of the uniform measure on the complex unit sphere (rotation invariance, the distribution of a coordinate), little of which exists in Lean today.

A second difficulty is that the printed proof does not cover every parameter. The union bound produces a good $\psi$ only when $4\cdot 2^{-cd} + 4/d^2 < 1$ . For small $d$ , or small $c$ with few given states, the goal is still true, but a complete proof must handle those cases separately; they are not in the paper.

Formalization scope

Representation. Basis labels are Q n = Fin n → Fin 2, Pauli labels P n = Fin n → Fin 4, states live in EuclideanSpace ℂ (Q n), and $W_k$ is the entrywise product of single-qubit Pauli matrices (the Kronecker product). $d$ is the real number $2^n$ ; $\log$ is Real.log; ⟨φ|ψ⟩ is Mathlib's inner ℂ φ ψ.
Measure. The uniform measure on the sphere is Mathlib's Measure.toSphere of an additive Haar measure on $\mathbb C^d$ (as a real vector space), normalised to total mass one. The paper's "Haar-random vector in $S^{d-1}$ " is read as this measure on the unit sphere of $\mathbb C^d$ .
Added hypotheses, all disclosed. The goal assumes $n \ge 1$ : at $n = 0$ ( $d = 1$ ) and small $c$ the lemma is false, since every unit vector of $\mathbb C^1$ has overlap $1$ with $\varphi_1$ . It assumes $c > 0$ , under which $\varepsilon$ is defined. "States" means unit vectors, for the given $\varphi_i$ and for the produced $\psi$ . The mean-zero statement for Pauli operators assumes $W_k \ne I$ (for $W_k = I$ the mean is $1$ ); the paper's "for each $k$ " refers to the non-identity labels of (32). " $W_k \ne I$ " is formalized as "the label $k$ is not all zeros".
Non-trivialization. The produced $\psi$ must be a unit vector, so $\psi = 0$ does not satisfy the goal; the given states are unit vectors, so (31) is not trivially false; and the mean-zero milestones assert integrability together with the value of the integral, so they cannot hold merely because a non-integrable integral is $0$ .
Infrastructure needed. Facts about $n$ -qubit Pauli operators (Hermitian, unitary, traceless for $W_k \ne I$ ); rotation invariance of the normalised sphere measure; a concentration inequality for Lipschitz functions on the complex unit sphere with an explicit constant. The concentration inequality and the sphere-measure facts are reusable well beyond this mission and are welcome as separate contributions.

Selected references

S. T. Flammia and Y.-K. Liu, Direct fidelity estimation from few Pauli measurements, Phys. Rev. Lett. 106, 230501 (2011); arXiv:1104.4695v3. https://arxiv.org/abs/1104.4695
P. Lévy, Problèmes concrets d'analyse fonctionnelle, Gauthier-Villars, Paris, 1951 (reference [10] of the paper; no stable online link).
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089
P. Hayden, D. W. Leung and A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 95–117 (2006); arXiv:quant-ph/0407049. https://arxiv.org/abs/quant-ph/0407049

11 thms2 active usersReviewed

Analysis Control Theory Economics+1·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost IV: Low Switching Cost, Control-Band Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships are dynamic contracts in which the principal cannot observe the agent's effort, only its noisy consequences. Cao, Sun and Tian (Management Science, 2024) study such a relationship when the principal can suspend the agent and must pay a fixed switching cost to restart work. Suspension is a punishment that does not end the relationship, and it is used in practice for platform workers, contractors and franchisees. The paper shows that, when the switching cost and the revenue are low, the optimal contract has a control-band structure: the agent's promised utility is kept inside an interval, the agent is suspended when it falls below the lower end, and work resumes at the upper end. Two-threshold policies of this kind are standard in optimal switching problems with switching costs (Duckworth and Zervos, 2001; Vath and Pham, 2007), whose verification arguments the paper compares with its own.

This mission is the fourth of a series formalizing the analytic core of the paper. It covers the low-switching-cost region (Area III of the paper's Figure 2).

Setting

A Poisson process of arrivals brings revenue $R$ each. The base arrival rate is $\underline\mu\ge0$ ; if the agent works, at cost $b>0$ per unit of time, the rate becomes $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's cost rate while the agent works is $c\ge b$ , restarting work costs $K>0$ , and the principal and the agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ . The constants are

\beta=\frac b{\Delta\mu},\quad \bar w=\frac{\beta\mu}\rho,\quad \underline v=\frac{\underline\mu R}r,\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}r,\quad \bar V(w)=\frac{R\mu-c-(\rho-r)w}r .

The promised utility $w\ge0$ is the state. For a function $f$ on $\mathbb R_+$ with left derivative $f'$ , the paper's operators are

(\mathcal A_If)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu,

for the working state $I$ and the suspended state $\emptyset$ . A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$ .

Two families of functions enter. In the suspended state, $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24) solves $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ . In the working state, for $\tilde w<\bar w$ , $V_{\tilde w}$ is the $C^1$ solution of the delay differential equation (25), in which $V(w)$ is coupled to the look-ahead value $V((w+\beta)\wedge\tilde w)$ , with $V_{\tilde w}=\bar V(\tilde w)$ beyond $\tilde w$ ; $\mathcal V_{\tilde w}$ is its concavification (Lemma 2), linear below a threshold $\check w(\tilde w)$ . Lemma 3's $\hat{\mathrm w}$ is the unique $\tilde w$ with $\mathcal V_{\tilde w}(0)=\underline v$ under Condition 1.

The parameter regions are Condition 1 ( $\mu\ge\rho-r$ or $R<\hat R$ ), Condition 2 (its negation) and Condition 3: Condition 1 and $K<\bar K_1$ , or Condition 2 and $K<\underline K$ , with $\hat R$ (28), $\bar K_1$ (K1) and $\underline K$ (33) explicit thresholds.

The paper uses three different hats: Definition 1's payment threshold $\hat w$ , Lemma 3's upright $\hat{\mathrm w}$ , and Proposition 6's bold $\hat{\mathbf w}$ , the upper end of the control band.

Formalization targets

Goal: Proposition 7, first claim

Under Condition 3 there are parameters $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ satisfying Proposition 6 such that

V_I(w)=\begin{cases}V_{\mathsf c}(w),&w<\underline\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w),&w\ge\underline\vartheta\end{cases},\qquad V_\emptyset(w)=\begin{cases}V_{\mathsf c}(w),&w<\bar\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w)-K,&w\ge\bar\vartheta\end{cases}\qquad(46)

satisfy (20)–(22).

Proposition 6

Under Condition 3 there is $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ with $\mathsf c>0$ , $\underline\vartheta<\bar\vartheta<\hat{\mathbf w}$ and value matching and smooth pasting at both thresholds:

\mathcal V_{\hat{\mathbf w}}(\underline\vartheta)=V_{\mathsf c}(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}'(\underline\vartheta)=V_{\mathsf c}'(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}(\bar\vartheta)=V_{\mathsf c}(\bar\vartheta)+K,\quad \mathcal V_{\hat{\mathbf w}}'(\bar\vartheta)=V_{\mathsf c}'(\bar\vartheta)>1 .

Milestones

Lemma EC.4 (the first step of the EC.3.9 construction), Proposition 6, and the two hardest parts of (20) at the constructed tuple: Lemma EC.12 ( $\mathcal A_\emptyset V_\emptyset\ge0$ on $[\bar\vartheta,\hat{\mathbf w})$ ) and Lemma EC.13 ( $\mathcal A_IV_I\ge0$ below $\underline\vartheta$ ). The other steps of the construction are posed as further statements of the mission without milestone status: Lemma EC.7 (the root of $\psi=K$ under Condition 1), Lemma EC.8 and Lemma EC.11 (the Condition 2 counterparts of EC.4 and EC.7).

Significance

Proposition 7 is the analytic certificate behind the paper's Theorem 5: combined with the verification Theorem 1, it shows that the control-band contract is optimal in the low-cost region, and that the principal's value is $V_\emptyset(w)-w$ . Without it the third case of the paper's main Theorem 2 is unproved. The construction of Proposition 6 also gives a computable description of the band, which the paper uses for its numerical illustrations.

The results are proved in the paper's e-companion; none of them has a machine-checked proof. This mission states the analytic part as Lean targets. The delay-ODE layer (existence, uniqueness and shape of $V_{\tilde w}$ ) is shared with the first mission of the series, and Proposition 7's proof depends on it. The stochastic contract model, the verification theorem and the optimality Theorems 1–5 are not formalized in this series.

Difficulty

Each piece of (20)–(22) is a one-variable inequality, but the functions are not explicit. $\mathcal V_{\hat{\mathbf w}}$ is defined through a delay equation, and the band's endpoints are defined implicitly through four nested steps: matching at $\underline\theta$ , a range bound $\underline\theta^0$ , an upper threshold $\bar\theta(\underline\theta)$ and a root of a gap function $\psi$ . The natural argument, convexity or concavity of $\mathcal A_IV_I$ on the suspension region, fails: on $[0,\underline\vartheta)$ the function $\mathcal A_IV_I$ mixes $V_{\mathsf c}$ with the look-ahead value $V_I(w+\beta)$ and is not convex (p. 28), so the convexity arguments of the switching literature do not apply. The paper's proof of this single inequality occupies EC.3.12, with eight auxiliary lemmas.

Formalization scope

Functions are ℝ → ℝ and every statement quantifies over $w\ge0$ . The standing assumptions are $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ and Assumption 1; $\underline\mu\ge0$ and $b>0$ are disclosed additions. Conventions:

$f'$ in $\mathcal A_I,\mathcal A_\emptyset$ is the left derivative; derivatives of $V_{\tilde w}$ , $\mathcal V_{\tilde w}$ are taken within $\mathbb R_+$ .
(20) is posed for $w>0$ : at $0$ the left derivative does not exist and $V_{\mathsf c}'(0^+)=+\infty$ .
$V_{\tilde w}$ is a solution of (25)–(26) chosen when one exists; $\check w$ , $\hat{\mathrm w}$ , $\bar K_1$ , $\underline\theta^0$ , $\bar\theta$ are infima or suprema of sets the paper describes; $\tilde w(\underline\theta)$ , $C(\underline\theta)$ are chosen matching pairs.
"Increasing/decreasing" is strict.
$\underline K$ (33) uses the corrected bracket $((\rho-\mu)/\rho)\beta$ in place of the printed $(r/\rho)\beta$ ; the printed form contradicts the proof's (EC.69).
Proposition 6's " $\hat{\mathbf w}<\hat{\mathrm w}$ " is read as $\hat{\mathbf w}<\bar w$ in the Condition 2 case, where $\hat{\mathrm w}$ does not exist; $0<\underline\vartheta$ is stated.
The goal is existential over Proposition 6 tuples. Lemmas EC.12 and EC.13 are stated at the tuple constructed in EC.3.9, in both cases of Condition 3; EC.13 is posed on $(0,\underline\vartheta)$ .
Lemma EC.11's second limit is printed at $0$ ; it is stated at $\breve{\underline\theta}$ , as the proof computes it.

The tuple is never defined by the property that (46) satisfies (20)–(22); the construction definitions are Steps 1–4 of EC.3.9 only, and the goal requires all of Proposition 6's conclusions. The second claim of Proposition 7, (48) on the contract's utility, is out of scope.

A complete development needs existence, uniqueness and regularity for the linear delay equation (25) (reusable for other delay problems), implicit-function arguments for $\tilde w(\underline\theta)$ , and the sign analysis of EC.3.12. Proofs of single milestones, and of the delay-ODE lemmas of the series' first mission, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
K. Duckworth, M. Zervos, A model for investment decisions with switching costs, Annals of Applied Probability 11(1), 2001. https://doi.org/10.1214/aoap/998926992
V. L. Vath, H. Pham, Explicit solution to an optimal switching problem in the two-regime case, SIAM Journal on Control and Optimization 46(2), 2007. https://doi.org/10.1137/050638783

11 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Digital Privacy II: Against the Social Optimum, a Business Never Under-Collects While Over-Protecting Data, and a Purely Usage-Driven One Under-Collects and Under-ProtectsResearch Paper

Motivation

Digital businesses (search engines, social networks, marketplaces) record what their users do and decide how well to protect what they record. Both choices affect users: stored data can improve the service, and it can also be accessed by adversaries such as hackers, fraudsters or data brokers, whose activity harms users. Regulation of data collection and data protection (the GDPR, the CCPA, liability rules for breaches) presupposes an answer to a basic question: in which direction does a profit-maximizing business's data strategy deviate from the one a benevolent planner would choose?

I. P. Fainmesser, A. Galeotti and R. Momot, Digital Privacy (Management Science 69(6), 2023; author manuscript SSRN 3459274), answer it in a model where users, adversaries and the business all respond to each other. Their Theorem 2 shows that the deviation is not arbitrary: one combination of errors never occurs, and the sign of the error is pinned down completely for a business whose revenue depends only on usage. This mission formalizes those two claims.

Setting

A data strategy is a pair $(\xi, C)$ : the share $\xi \in [0,1]$ of each user's activity that the business stores, and a protection level $C \ge 0$ , which costs $\psi C$ . The parameters are real numbers: a network effect $\beta \in [0,1)$ , the users' marginal benefit from stored data $\rho \in [0,1)$ , the cost $\psi$ , the revenue model $P \in [0,1]$ , and the planner's weight $\alpha \in [0,1]$ .

Given $(\xi, C)$ , a unit mass of identical users choose activity levels and a large population of adversaries decide whether to access the stored data. The resulting equilibrium (Proposition 1 of the paper, display (3)) has average user activity

\bar a^*(\xi, C) = \frac{C(1+\rho\xi)}{C(1-\beta)+\xi^2}, \qquad \bar a^*(0, C) = \frac{1}{1-\beta}.

The value at $\xi = 0$ is the activity when nothing is stored, the value the paper uses where (3) reads $0/0$ . From $\bar a^*$ one builds the consumer surplus (4), the business's profit (2) and the planner's objective (7):

\mathrm{CS}(\xi,C) = \tfrac12 \bar a^*(\xi,C)^2, \qquad \Pi(\xi,C) = (1-P)\,\bar a^*(\xi,C) + P\,\xi\,\bar a^*(\xi,C) - \psi C, \qquad W(\xi,C) = \alpha\,\mathrm{CS}(\xi,C) + (1-\alpha)\,\Pi(\xi,C).

The revenue model $P$ interpolates between a purely usage-driven business ( $P = 0$ , revenue proportional to activity) and a purely data-driven one ( $P = 1$ , revenue proportional to stored data $\xi \bar a^*$ ). A business optimum $(\xi^*, C^*)$ maximizes $\Pi$ over the feasible set $[0,1] \times [0,\infty)$ ; a social optimum $(\xi^W, C^W)$ maximizes $W$ over the same set. The business under-collects if $\xi^* \le \xi^W$ and over-protects if $C^* \ge C^W$ , and so on.

Formalization targets

Goal: Theorem 2, first two sentences

The paper's Theorem 2 (p. 13) reads:

Relative to the socially optimal strategy, the equilibrium data strategy of a purely usage-driven business (P = 0) prescribes under-collection and under-protection of users' data, i.e., ξ* ≤ ξ^W and C* ≤ C^W. The equilibrium data strategy of a business with any data-driven component in its revenue model (P > 0) never prescribes under-collection and over-protection of users' data i.e., it is never the case that ξ* ≤ ξ^W and C* ≥ C^W with at least one of the inequalities being strict. Any other direction in which the optimal business's data strategy deviates from the socially optimal strategy is the outcome for some specification of the business's revenue model and values of other model parameters.

The goal is its first two sentences, for every business optimum and every social optimum:

P = 0 \;\Longrightarrow\; \xi^* \le \xi^W \text{ and } C^* \le C^W,

P > 0 \;\Longrightarrow\; \neg\bigl(\xi^* \le \xi^W,\ C^* \ge C^W,\ \text{at least one strict}\bigr).

The third sentence is established numerically in the paper (Figure 3) and is not a target.

Milestones

Display (11), p. 34: under $\xi^* \le \xi^W$ and $C^* \ge C^W$ , the social optimum has weakly higher activity, $\bar a^*(\xi^W, C^W) \ge \bar a^*(\xi^*, C^*)$ .
Display (12), p. 34: under the same assumptions, $\bar a^*(\xi^W,C^W)\,\xi^W \ge \bar a^*(\xi^*,C^*)\,\xi^*$ .
Proposition 5(i), first claim (Online App. p. 8): for fixed $C$ and $P = 0$ , a collection level maximizes $\Pi(\cdot, C)$ on $[0,1]$ if and only if it maximizes $W(\cdot, C)$ .
The $P = 0$ step of the proof (App. A.4, p. 34): if $P = 0$ and $\xi^* > \xi^W$ , then $C^* > C^W$ .

Significance

The result. Theorem 2 identifies the one inefficiency that no revenue model produces: a business never stores too little data while protecting it too much. All other combinations occur for some parameters, so a regulator cannot infer the direction of a business's error without knowing its revenue model; but for a purely usage-driven business the direction is known, and it is too little protection. This underlies the paper's discussion of policy in §6, where the instruments considered (liability for data breaches, taxes on data) are compared by how they move $(\xi^*, C^*)$ towards $(\xi^W, C^W)$ .

The formalization. The result is proved in the paper (App. A.4, with Proposition 5 in Online App. C.5); it has not been machine-checked. The paper's argument for the purely usage-driven case refers to first-order conditions and does not treat the boundary strategies ( $\xi = 0$ , $C = 0$ ) or parameter corners ( $\rho = 0$ ) separately; a formal proof has to handle them. A complete development also yields reusable facts about the equilibrium activity $\bar a^*$ : its sign, its behaviour in $\xi$ for fixed $C$ , and the monotonicity in $C$ of the activity-maximizing collection level.

Difficulty

Both optima are defined only implicitly, as maximizers over a non-compact feasible set of a non-concave objective, and neither has a closed form that this mission may use. The comparison must therefore work from the optimality inequalities alone. The tempting approach, comparing first-order conditions, does not give a global statement: $\Pi$ and $W$ may have several local maxima, the maximizers need not be unique (both optima are $(0,0)$ in a whole region of parameters), and the constraint $\xi \le 1$ binds for large protection. In the purely usage-driven case the profit and welfare share their maximizers in $\xi$ for each fixed $C$ , but turning that into a comparison of $C^*$ with $C^W$ requires control of how the maximizing $\xi$ moves with $C$ , including at $C = 0$ .

Formalization scope

All objects are real-valued functions of explicit real parameters $\beta, \rho, \psi, P, \alpha$ and of the strategy $(\xi, C)$ , in the namespace DigitalPrivacy.Welfare, which imports $\bar a^*$ , CS, the feasible set and the business optimum from the shared module DigitalPrivacy.Strategy.Setting. The equilibrium activity takes the value $1/(1-\beta)$ at $\xi = 0$ for every $C$ , as in the paper; Lean's default $0/0 = 0$ is not used. Optima are predicates (IsBusinessOpt, IsSocialOpt): a feasible point at which the objective is at least its value at every feasible point. Theorem 2 quantifies over every pair of optima and asserts neither existence nor uniqueness. The P > 0 clause keeps the "at least one strict" condition; without it the clause is false, because both optima coincide at $(0,0)$ in part of the parameter space.

The standing assumptions are the paper's ranges $0 \le \beta < 1$ , $0 \le \rho < 1$ , $0 \le P \le 1$ , $\alpha \le 1$ , with two disclosed strengthenings: $\psi > 0$ (with $\psi = 0$ , $\rho = 0$ , $P = 0$ , every $(0, C)$ is both a business and a social optimum and the $P = 0$ sentence fails) and $\alpha > 0$ (with $\alpha = 0$ the planner's problem is the business's, and step (11) does not hold). Proposition 5(i) is stated with the printed ranges, $\alpha = 0$ included. No other hypothesis is added, so the hypotheses on the optima cannot be made vacuous by the encoding; a sanity check exhibits parameters at which $(0,0)$ is both a business and a social optimum.

A complete development needs elementary real analysis of the rational function $\bar a^*$ on $[0,1] \times [0,\infty)$ and nothing beyond Mathlib. Proofs of the milestones, of lemmas about $\bar a^*$ , and alternative arguments for the goal are all welcome. The paper's proofs are in App. A.4 (pp. 33–35) and Online App. C.5 (Online pp. 8–9).

Selected references

I. P. Fainmesser, A. Galeotti, R. Momot, Digital Privacy, Management Science 69(6):3157–3173, 2023. https://doi.org/10.1287/mnsc.2022.4513. Author manuscript, This Draft: April 2022, https://ssrn.com/abstract=3459274 (the version cited for all page and display numbers).

7 thms2 active usersReviewed

Completed

Analysis Operations Research Optimization+1·Captain: mikedeng1

Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality I: Feasible Solutions of the Continuous Stopping LP Can Be Improved to Threshold FormResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (p. 8)

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

t\,q^*(t,\ell)+\int_p^t\sum_{s\ge1}q^*(\tau,s)\,d\tau=1\ \ (t\ge t_\ell),\qquad q^*(t,\ell)=0\ \ (t<t_\ell),\tag{5–6}

q^*(t,\ell)=\begin{cases}T_i/t^{i+1}&t\in[t_i,t_{i+1}),\ \ell\le i,\\0&\text{else.}\end{cases}\tag{7}

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

8 thms2 active usersReviewed

Completed

Analysis Control Theory Economics+1·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost III: Condition 2, Medium Switching Cost, Always-Work Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships pay an agent per unit of output whose arrival is random: a salesperson closing deals, a call-centre worker resolving tickets, a contractor delivering jobs. When effort is unobservable, the classical tool for keeping an agent motivated is the threat of termination after poor performance. In practice firms often use a milder punishment, suspension: the agent is sent home for a while and later called back. Restarting work is not free, and each restart costs the firm a fixed switching cost.

P. Cao, P. Sun and F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost (Management Science, 2024), characterise the optimal dynamic contract in this setting. The optimal contract depends on the size of the switching cost: when it is large the firm should not hire, when it is moderate the firm should keep the agent working forever, and when it is small the firm uses a control-band contract with suspension episodes. Their proof is "guess and verify": a stochastic verification theorem (their Theorem 1) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value, and Propositions 2–7 exhibit such pairs in each parameter region.

This mission formalizes the certificate for the medium-switching-cost region under Condition 2 (Area II of the paper's Figure 2), where the agent is never suspended.

Setting

The principal faces a Poisson stream of arrivals, each worth revenue $R$ . Without effort the arrival rate is $\underline\mu\ge0$ ; an agent who exerts effort, at cost $b>0$ per unit time, raises it to $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's total cost rate while the agent works is $c\ge b$ , every start of work costs a switching cost $K>0$ , and the principal and agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ .

The paper's derived constants are

\beta=\frac{b}{\Delta\mu},\quad \bar w=\frac{\beta\mu}{\rho},\quad \underline v=\frac{\underline\mu R}{r},\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\quad \bar K_2=\bar V-\underline v-\bar w,

together with the revenue thresholds $\hat R$ (28) and $\bar R$ (34) and the switching-cost threshold $\underline K$ (33). Condition 2 is $\mu<\rho-r$ and $R\ge\hat R$ : the agent is much more impatient than the principal and revenue is high.

The state variable is the agent's promised utility $w\ge0$ . Two operators act on functions $f$ of $w$ , where $f'$ is the left derivative:

(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu.

The first is a delay-differential operator for the working state, the second a first-order operator for the suspended state. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) when $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$ .

The suspended-state equation $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ is solved by $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24). In the region of this mission the paper builds

V_\emptyset(w)=\begin{cases}V_{c_K}(w),&w\le\bar w,\\ \bar V-K,&w>\bar w,\end{cases}\qquad V_I(w)=\begin{cases}V_{c_K}(w),&w\le\underline\theta_K,\\ \bar V+m_K(w-\bar w),&\underline\theta_K<w\le\bar w,\\ \bar V,&w>\bar w,\end{cases}

from parameters $(c_K,m_K,\underline\theta_K)$ chosen so that $V_{c_K}$ pastes smoothly onto the line at $\underline\theta_K$ and ends at $\bar V-K$ at $\bar w$ .

Formalization targets

Goal: Proposition 5 (first claim)

Under Condition 2 and $K\in[\underline K,\bar K_2)$ , for every triple $(c_K,m_K,\underline\theta_K)$ with $\underline\theta_K\in(0,\bar w)$ , $c_K>0$ , $m_K\in[\frac{\rho-r}{\rho-r-\mu},\frac{\bar V-\underline v}{\bar w})$ and

V_{c_K}(\underline\theta_K)=\bar V+m_K(\underline\theta_K-\bar w),\qquad V'_{c_K}(\underline\theta_K)=m_K,\qquad V_{c_K}(\bar w)=\bar V-K,

the functions $V_I,V_\emptyset$ above satisfy (20)–(22).

Milestones

(EC.67): explicit $C^1(\underline\theta)$ and $m(\underline\theta)$ solve the value-matching and smooth-pasting equations at any $\underline\theta\in(0,\bar w]$ .
Lemma EC.3: $\psi_1(\underline\theta)=\bar V-\underline v-\bar w-C^1(\underline\theta)\bar w^{r/\rho}$ is continuous and strictly decreasing on $[0,\bar w]$ , so $\psi_1=K$ has a unique root $\underline\theta_K\in(0,\bar w)$ for $K\in(0,\bar K_2)$ ; the root decreases in $K$ and tends to $\bar w$ as $K\downarrow0$ .
Lemma 5: for every $K\in[\underline K,\bar K_2)$ the triple exists, and $c_K$ , $m_K$ , $\underline\theta_K$ are monotone in $K$ .

Lemma 5 guarantees that the goal is not vacuous.

Significance

Proposition 5 is the analytic half of the paper's Theorem 4: combined with the verification theorem, it shows that in Area II the principal's optimal value is attained by a contract that pays the agent $\beta$ per arrival and never suspends. The threshold $\underline K$ separates this region from the control-band region of Proposition 7, so the explicit formula for $\underline K$ is the boundary of the phase diagram.

The result is proved in the paper. No machine-checked version exists. A formal proof checks a delicate sign argument near $w=0$ , where $V_{c_K}$ has infinite slope, and it checks the threshold $\underline K$ , whose printed formula contains an error (see Formalization scope). The paper's companion identity (41), $U(\bar\Gamma)=\bar V-\bar w-K=V_\emptyset(\bar w)-\bar w$ , is about the utility of a contract and is not part of this mission; its deterministic half is immediate from (39).

Difficulty

The cases $w\in[\underline\theta_K,\bar w]$ and $w>\bar w$ are algebraic. The difficulty is $w\in(0,\underline\theta_K)$ : there $V_I$ is the curve $V_{c_K}$ , and $w+\beta$ lands beyond $\bar w$ (Condition 2 gives $\beta>\bar w$ ), so $\mathcal A_IV_I$ couples the curve with the constant $\bar V$ . Positivity there needs more than the sign of the smooth-pasting slope: it uses the lower bound on $m_K$ in (35), which is exactly where the threshold $\underline K$ enters. A direct sign check at $\underline\theta_K$ alone does not cover the interval. The existence lemma requires monotonicity of $\psi_1$ , whose expression mixes powers $\underline\theta^{r/\rho-1}$ with a linear factor.

Formalization scope

All functions are ℝ → ℝ and every quantifier ranges over $w\ge0$ ; powers are Real.rpow. The standing assumptions $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ , $R\Delta\mu>c$ are one hypothesis Standing; $\underline\mu\ge0$ and $b>0$ are read off the model and stated explicitly. The left derivative is derivWithin f (Set.Iic w) w, following the paper's convention on p. 15. Condition (20) is posed for $w>0$ only: at $w=0$ the right derivative of $V_{c_K}$ is $+\infty$ , so the paper's (20) there is an extended-real statement and Lean's junk derivative would make it false. (21) and (22) are posed as printed.

The threshold $\underline K$ of (33) is corrected: the printed bracket contains $\frac r\rho\beta$ , but the paper's own proof identifies $\underline K$ with $\check K_2$ of (EC.69), which gives $\frac{\rho-\mu}{\rho}\beta$ . With the printed term Lemma 5 fails (for $r=0.2,\rho=1.2,b=c=1,R=5,\mu=0.9,\underline\mu=0.1$ , the printed value is $-0.069$ , the corrected one $7.2533$ ). Equation (36) is printed with a free $w$ that should read $\underline\theta_K$ . The range $\underline\theta_K\in(0,\bar w)$ , given by the proof, is stated.

The goal quantifies over all triples satisfying Lemma 5's conclusions; such a triple is unique, so this is the paper's claim, and Lemma 5 rules out a vacuous goal. Dropping the bound $K$ in (21), the condition (22), or the lower bound on $m_K$ would trivialize or change the statement.

The development needs the derivative of $w\mapsto w^{r/\rho}$ , sign analysis of explicit real functions, and the intermediate value theorem. The Setting file is shared with the other missions of this series and will be consolidated. Proofs of the milestones in any order are welcome; (EC.67) is a self-contained calculus exercise.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845 (cited from the authors' manuscript and e-companion: §4.2 pp. 24–26, EC.3.7–EC.3.8 pp. ec32–ec34).
Y. Sannikov, A Continuous-Time Version of the Principal-Agent Problem, Review of Economic Studies 75(3), 2008. https://doi.org/10.1111/j.1467-937X.2008.00486.x
B. Biais, T. Mariotti, J.-C. Rochet, S. Villeneuve, Large Risks, Limited Liability, and Dynamic Moral Hazard, Econometrica 78(1), 2010. https://doi.org/10.3982/ECTA7261

6 thms2 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

Pricing in On-Demand and One-Way Vehicle-Sharing Networks 2: With Workload Budget K, Static Prices Earn a Demand-Independent 1 − O(1/√K) Fraction of the Fluid OptimumResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3, static half

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

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

Formalization scope

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

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

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

Selected references

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

11 thms2 active usersReviewed

Combinatorics Operations Research Optimization+2·Captain: mikedeng1

Pricing in On-Demand and One-Way Vehicle-Sharing Networks 3: The K/(N+K−1+Λ/μ) Guarantee Holds When Static Prices Split the Network into ComponentsResearch Paper

Motivation

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

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

Setting

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

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

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

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

Formalization targets

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

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

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

Milestones (p. 18–19)

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

A complete development needs:

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

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

Selected references

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

24 thms2 active users

Linear Optimization Markov Chain Operations Research+2·Captain: mikedeng1

Dynamic Matching: Characterizing and Achieving Constant Regret I: Under General Position the Exhaustive Resolving Policy Has Regret at Most Γ/ϵ at All TimesResearch Paper

Motivation

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

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

Setting

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

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

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

The static-planning problem is the linear program

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Mechanism Design+1·Captain: mikedeng1

Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail I: Under Centralized Dispute Resolution the Equilibrium Ransom Is Not Monotonically Decreasing in Efficiency γδResearch Paper

Review blackmail on online platforms

Online marketplaces depend on consumer reviews, and a single negative review can move a seller's future sales. Review blackmail exploits this: a consumer buys a product, posts a negative review, and offers to remove it in exchange for a payment. Platforms such as Amazon, eBay, Taobao and TripAdvisor respond with dispute resolution mechanisms that let sellers contest reviews. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) build a game-theoretic model of the seller, the blackmailer and the market's belief about product quality, and ask how the design of such a mechanism changes the blackmailer's leverage. Their first finding concerns a centralized mechanism, where the seller reports the review and the platform judges it: making the platform faster or more accurate does not always lower the ransom the blackmailer can extract. This mission formalizes that result together with the equilibrium analysis it rests on.

The model

A monopolist sells a product of unobservable quality $q\in\{l,h\}$ ; the market's prior that quality is high is $a\in(0,1)$ . A buyer of a high-quality product has gross utility $v_j$ with probability $\theta\in(0,1)$ and $0$ otherwise, with $v_j$ standard uniform; a low-quality product always gives $0$ . One consumer arrives.

With probability $\beta\in(0,1)$ he is malicious: he buys, posts a negative review $N$ , and demands a ransom $r$ for removing it.
Otherwise he is regular: at price $p$ he buys iff $a\theta v_j-p\ge0$ , which happens with probability $\rho=1-p/(a\theta)$ , and posts a truthful review, positive ( $P$ ) or negative ( $N$ ). No purchase means no review, written $R=0$ .

The market sees the review $R\in\{N,0,P\}$ , updates its belief to a posterior $a'$ by Bayes' rule, and the seller then earns a continuation payoff $\pi(a')$ , with $\pi$ nonnegative, convex and strictly increasing on $[0,1]$ .

Facing a ransom demand the seller can settle ( $s$ : pay $r$ , the review disappears), do nothing ( $n$ : the review stays), or report ( $c$ ) the review to the platform's centralized mechanism at a hassle cost $c\ge0$ . The platform investigates immediately with probability $\gamma\in[0,1]$ (timeliness) and identifies a malicious review correctly with probability $\delta\in[0,1]$ (accuracy); the review is removed with probability $\gamma\delta$ , the mechanism efficiency.

The market cannot observe the seller's interaction with the blackmailer. It holds a belief $i\in\{s,n,c\}$ about the seller's response, and this belief determines the posteriors: under belief $i$ a malicious review stays visible with probability $m_s=0$ , $m_n=1$ or $m_c=1-\gamma\delta$ , and $a^i_R$ is the Bayes posterior computed from the resulting review likelihoods. When the market believes $i$ and the seller plays $j$ , his payoff is $\pi(a^i_0)-r$ ( $j=s$ ), $\pi(a^i_N)$ ( $j=n$ ), or $\gamma\delta\,\pi(a^i_0)+(1-\gamma\delta)\pi(a^i_N)-c$ ( $j=c$ ). A response $i$ is an equilibrium if it is a best response to the belief $i$ ; among several equilibria, the seller-preferred one prevails. The malicious consumer buys iff some ransom $r>p$ is accepted in the prevailing equilibrium, and the equilibrium ransom $r^*$ is the greatest ransom at which settling prevails.

Formalization targets

Goal: Corollary 1 (p. 14)

If $c>0$ and $p<\pi(a)-\pi(a^n_N)-c$ , there are efficiencies $0\le e_1<e_2\le1$ at both of which the malicious consumer purchases, with

r^*(e_1)<r^*(e_2).

The equilibrium ransom is not monotonically decreasing in the efficiency $\gamma\delta$ .

Milestones

Lemma 2 (p. 11): $a^i_P=1$ , $a^i_0=a$ , $a^i_N\in[0,a]$ , and closed forms of $a^n_N$ , $a^c_N$ , $a^s_N$ .
Ordering (§4.1, p. 11): $a^s_N<a^c_N<a^n_N$ for $0<\gamma\delta<1$ .
Proposition 1(1)–(3) (p. 13): the exact conditions under which $n$ , $s$ and $c$ are equilibria, e.g.

i=n\ \text{is an equilibrium}\iff \pi(a^n_N)\ge\max\{\pi(a)-r,\ \pi(a)-c/\gamma\delta\}.

Proposition 2(1)–(2) (p. 13): the equilibrium ransom

r^*=\begin{cases}\pi(a)-\pi(a^n_N), & c\ge\gamma\delta(\pi(a)-\pi(a^n_N)),\\ (1-\gamma\delta)[\pi(a)-\pi(a^c_N)]+c, & c<\gamma\delta(\pi(a)-\pi(a^n_N)),\end{cases}

and the malicious consumer purchases iff $p<r^*$ .

Significance

Corollary 1 is the paper's headline message about centralized dispute resolution: improving the mechanism's timeliness or accuracy can raise the ransom. Below an efficiency threshold the mechanism is never used and the ransom equals the seller's loss from a visible negative review; just above it, the market expects the seller to report blackmail, which softens how it reads a negative review, and the blackmailer can ask for more. This is the motivation for the paper's second design, semi-decentralized dispute resolution, analysed in a companion mission. Proposition 2 is the complete characterization of the blackmailer's equilibrium behaviour under the centralized mechanism and is used again in the paper's pricing analysis (§4.4).

The results are proved in the paper (Appendix C). No machine-checked version exists. This mission produces Lean statements of the model, of the Bayes posteriors, of the equilibrium conditions, of the seller-preferred selection and of the ransom characterization, all derived from the primitive game rather than from the paper's closed forms.

Difficulty

Each step is elementary, but the chain is long and sign-sensitive. The equilibrium conditions require handling a belief-dependent payoff (the posterior depends on what the market believes, not on what the seller does), so a deviation changes the action without changing the posteriors. The ransom characterization needs a three-way comparison of equilibria and the tie-breaking in favour of settling at the boundary, where two equilibria give the same payoff. The corollary needs the jump at the threshold efficiency $c/(\pi(a)-\pi(a^n_N))$ to be strictly positive and to survive a small increase of the efficiency: the posterior $a^c_N$ moves with the efficiency, so a continuity argument for $\pi$ composed with the posterior is required, and $\pi$ is only assumed convex and strictly increasing on $[0,1]$ . The natural first idea, comparing the two closed forms of Proposition 2 at a single point, does not suffice, since at the threshold itself the two regimes coincide in value.

Formalization scope

Representation. One structure Model with fields $a,\theta,\beta,p,c$ and $\pi:\mathbb R\to\mathbb R$ ; inductive types for quality, reviews ( $N$ , Z for $R=0$ , $P$ ) and responses. The posterior post m R is Bayes' rule over the likelihood table with visibility probability $m$ of a malicious review; $a^i_R$ is post (keep (γ*δ) i) R.
Standing assumptions (Standing): $a,\theta,\beta\in(0,1)$ ; $\pi\ge0$ , convex and strictly increasing on $[0,1]$ ; $c\ge0$ ; and $0<p<a\theta$ . The last is implicit in the paper: it makes the purchase probability $1-p/(a\theta)$ that of a standard uniform valuation and keeps the event $R=0$ of positive probability. Every theorem also assumes $\gamma,\delta\in[0,1]$ .
Added hypotheses. $0<\gamma\delta<1$ in the ordering (strictness) and in Proposition 1 (the page divides by $\gamma\delta$ and $1-\gamma\delta$ ). $c>0$ in Corollary 1: at $c=0$ the corollary is false. Corollary 1's hypothesis, printed with a varying $\gamma\delta$ , is assumed at the threshold efficiency and required at both exhibited efficiencies.
Conventions. "Settling prevails" means settling is an equilibrium and no equilibrium pays the seller strictly more (ties go to settling, as in the paper's proof). $r^*$ is stated with IsGreatest of the set of ransoms at which settling prevails; purchase means some such ransom exceeds $p$ . "Not monotonically decreasing" means not nonincreasing.
Ruled out. Defining the posteriors by Lemma 2's closed forms, or $r^*$ by Proposition 2's formulas, would make the milestones definitional; both are defined from the game instead.
Infrastructure. Only Mathlib (ConvexOn, StrictMonoOn, IsGreatest). Proofs of the milestones in order, and reusable lemmas on the monotonicity of the posterior in the visibility probability, are welcome.

Selected references

Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (accepted manuscript: LBS Research Online, eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/)

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Mechanism Design+1·Captain: mikedeng1

Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail II: Under Semi-Decentralized Dispute Resolution with Penalty b the Equilibrium Ransom Has a Two-Regime Closed FormResearch Paper

Motivation

Online marketplaces rely on consumer reviews, and a negative review lowers what future buyers believe about a product. Review blackmail exploits this: a consumer buys, posts a negative review, and offers to remove it for a ransom. Platforms counter with dispute-resolution mechanisms. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) compare two of them in a Bayesian game between a seller, one consumer and the market. Under the centralized mechanism the seller reports the review and the platform decides whether to remove it. Under the semi-decentralized mechanism the seller removes the review himself, and the platform checks afterwards. If it judges the removal wrongful, it reinstates the review and fines the seller a penalty $b$ .

This mission covers the semi-decentralized mechanism. Its main result, Proposition 5, gives the ransom a blackmailer can extract in equilibrium in closed form and says when blackmail pays at all. A platform needs that answer when it chooses the penalty. Mission I of this series treats the centralized mechanism.

Setting

A product has quality $q\in\{l,h\}$ . The prior that $q=h$ is $a\in(0,1)$ . A buyer of a high-quality product gets a positive experience with probability $\theta\in(0,1)$ ; a low-quality product never gives one. With probability $\beta\in(0,1)$ the consumer is malicious. A malicious consumer buys at price $p$ , posts a negative review $N$ and demands a ransom $r$ . Otherwise the consumer is regular. A regular consumer buys with probability $\rho=1-p/(a\theta)$ (valuation $v_j$ uniform on $[0,1]$ ) and reviews truthfully: positive ( $P$ ) or negative ( $N$ ). No purchase means no review, written $R=0$ ; a removed review is also seen as $R=0$ .

The market observes $R\in\{N,0,P\}$ and forms the posterior $a'$ by Bayes' rule. The seller then earns $\pi(a')$ , where $\pi$ is nonnegative, convex and strictly increasing on $[0,1]$ .

Facing a ransom demand, the seller can settle ( $s$ : pay $r$ , review removed), do nothing ( $n$ ), or use the mechanism ( $d$ ). Under $d$ the platform judges immediately with probability $\gamma\in[0,1]$ (timeliness). It recognises a malicious review with probability $\delta\in[0,1]$ (accuracy). The review is therefore reinstated with probability $\gamma(1-\delta)$ , and the penalty $b\ge0$ is paid with probability $1-\delta$ . Write $a^i_R$ for the posterior after review $R$ when the market believes the seller's response is $i$ . The payoffs of the three responses are then

\pi(a^i_0)-r,\qquad \pi(a^i_N),\qquad (1-\gamma(1-\delta))\pi(a^i_0)+\gamma(1-\delta)\pi(a^i_N)-(1-\delta)b.

The market cannot see the interaction, so $i$ is an equilibrium at $r$ if no response pays more given the belief $i$ . The equilibrium ransom $r^*$ is the largest $r$ at which settling is an equilibrium and no equilibrium pays the seller more. The malicious consumer buys iff $p<r^*$ .

A seller could also use the mechanism against genuine negative reviews. Proposition 4 shows that this is deterred exactly when $b\ge\underline b:=(1-\gamma)[\pi(a)-\pi(a^s_N)]$ .

Formalization targets

Goal: Proposition 5 (p. 21)

Let $\delta<1$ and $T=\frac{1-\gamma(1-\delta)}{1-\delta}\big(\pi(a)-\pi(a^n_N)\big)$ .

If $b\ge T>\underline b$ :

r^*=\pi(a)-\pi(a^n_N),\qquad\text{and the malicious consumer buys iff } p<r^*.

If $\underline b\le b<T$ :

r^*=(1-\delta)\big(\gamma(\pi(a)-\pi(a^d_N))+b\big),\qquad\text{and the malicious consumer buys iff } p<r^*.

Milestones

(5), p. 21: the closed form of $a^d_N$ , together with $a^i_0=a$ .
§5.1, p. 21: the ordering $a^s_N<a^d_N<a^n_N$ .
Proposition 4, p. 20: genuine negative reviews are kept iff $b\ge\underline b$ .
Proof of Proposition 5, Step 1, pp. 41–42: the conditions under which $s$ , $n$ and $d$ are equilibria, one milestone each.

Significance

Proposition 5 has two regimes. If the penalty is high, the mechanism plays no part in blackmail: the seller would never use it, and the ransom equals the one with no mechanism at all. Below the threshold, the ransom is the seller's expected loss from using the mechanism. A lower ransom then means less blackmail, and it pushes the price at which blackmail stops paying downward. The threshold $T$ rises with the accuracy $\delta$ and falls with the timeliness $\gamma$ . The paper's later results on pricing and on the platform's penalty build on this characterization.

The result is proved in the paper (Appendix C, pp. 41–43). It has no machine-checked proof. Formalizing it pins down the equilibrium concept, including the selection among multiple equilibria. It also corrects a printed slip in the proof: the simplified condition for the mechanism to be an equilibrium drops a factor $1-\delta$ .

Difficulty

Each individual equilibrium condition is a rearrangement of payoff inequalities. The difficulty lies in selecting among equilibria. Several responses can be equilibria at the same ransom. Settling prevails only if no other equilibrium pays more, and the equilibria themselves depend on $r$ . So the set of ransoms at which settling prevails is not given by one inequality. Its greatest element must be found across three scenarios, comparing three thresholds that involve three different posteriors. Those comparisons require the posterior ordering $a^s_N<a^d_N<a^n_N$ , which comes from Bayes' rule and not from the payoff algebra. Reading the equilibrium condition for $s$ alone as the answer gives the wrong ransom in case 1.

Formalization scope

Everything lives in the namespace ReviewBlackmail.SemiDec, with one structure Model holding $a,\theta,\beta,p,\gamma,\delta,b$ and the payoff fut (the paper's $\pi$ ; Real.pi is never used). The predicate Standing collects the standing assumptions: $a,\theta,\beta\in(0,1)$ ; $\pi$ nonnegative, convex and strictly increasing on $[0,1]$ ; $\gamma,\delta\in[0,1]$ ; $b\ge0$ ; and the disclosed addition $0<p<a\theta$ , which makes the purchase probability $\rho$ lie in $(0,1)$ . Per-statement additions, each disclosed in the item:

$\delta<1$ on the goal and on Step 1 for $n$ and $d$ , which divide by $1-\delta$ ;
$0<\gamma(1-\delta)<1$ on the strict ordering;
$0<\gamma<1$ on the second half of Proposition 4.

Posteriors are defined by Bayes' rule over an explicit likelihood table with two visibility probabilities: $m$ for malicious and $g$ for genuine negative reviews. Proposition 4 needs beliefs in which genuine reviews are removed. The payoffs of Proposition 5 keep genuine reviews ( $g=1$ ), the case the paper reduces to via Proposition 4. Ties in the selection rule go to settling.

The posteriors $a^i_R$ are never defined by their closed forms, and $r^*$ is never defined by (6) or (7). The goal is stated with IsGreatest on the set of ransoms at which settling prevails, not with sSup, so neither the closed forms nor junk values of a supremum can make the goal trivial.

A complete development needs only Mathlib's ConvexOn, StrictMonoOn and IsGreatest and real-field algebra. The algebra of Bayes posteriors with two-point priors may be reusable. Proofs of the milestones and the goal are welcome, in any order.

Selected references

Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (cited from the accepted manuscript, LBS Research Online eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/).

8 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition III: Without Accelerability a Financially Constrained Monopoly Invests Less Than an Unconstrained OneResearch Paper

Motivation

Young innovative firms often fund research out of internal cash flow rather than external capital. Whether such financial constraints make firms invest less in research and development (R&D) is a long-standing question in corporate finance and the economics of innovation. Myers (1977) showed that the possibility of default leads to under-investment in growth options. Danmo Lin (Management Science, 2022) separates two ways in which spending more on a project can pay off: it can make the payoff larger (scalability) or make the discovery arrive sooner (accelerability). The paper's Corollary 1 says that the classical under-investment result holds exactly when the project is scalable but not accelerable, while acceleration can reverse it. This mission formalizes the under-investment half of that corollary.

Setting

A firm faces a one-time R&D opportunity. It chooses an investment intensity $R$ , a spending rate per unit of time, and pays it until discovery. Discovery is the first arrival of a Poisson process of rate $\lambda(R)$ , and on discovery the firm receives a payoff with mean $u(R)$ . As in the paper's equation (2),

u(R)=A\,R^{\beta},\qquad \lambda(R)=\eta\,R^{\gamma},\qquad A>0,\ \eta>0,\ \beta,\gamma\in[0,1),\ \beta+\gamma<1,

and intensities are at least $\underline R=1$ . The project is scalable if $u'>0$ (here $\beta>0$ ) and accelerable if $\lambda'>0$ (here $\gamma>0$ ). Future cash is discounted at rate $r>0$ .

An unconstrained (UC) firm can always pay $R$ . By the paper's Lemma 1, equation (5), its project value at intensity $R$ is the perpetuity

V_{uc}(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}.

A financially constrained (FC) firm pays $R$ out of an asset-in-place (AIP) cash flow $X_t$ , a geometric Brownian motion with drift $\mu$ and volatility $\sigma$ that starts at $X$ . It must abandon the project once $X_t<R$ . Lemma 1, equation (6), gives its project value as

V_{fc}(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}\Big(1-\big(\tfrac{X}{R}\big)^{\alpha}\Big),\qquad \alpha=\tfrac12-\tfrac{\mu}{\sigma^2}-\sqrt{\big(\tfrac12-\tfrac{\mu}{\sigma^2}\big)^2+\tfrac{2(\lambda(R)+r)}{\sigma^2}}.

The ranges of intensities are those of (7): $[1,\bar R]$ for the UC firm and $[1,\min\{\bar R,X\}]$ for the FC firm, with $\bar R=(A\eta)^{1/(1-(\beta+\gamma))}$ . The optimal intensities $R^*_{uc}$ and $R^*_{fc}$ are the sets of maximizers of $V_{uc}$ and $V_{fc}$ over these ranges.

Formalization targets

Goal: Corollary 1, first statement (p. 6)

If $\lambda'=0$ and $u'>0$ , then $R^*_{fc}<R^*_{uc}$ . Formally: under the standing assumptions, $r>0$ , $\sigma>0$ , $X\ge1$ , $\gamma=0$ , $\beta>0$ and $A\beta\eta>1$ , both optimal sets are nonempty and

x<y\qquad\text{for every } x\in R^*_{fc}\text{ and every } y\in R^*_{uc}.

Milestones (Appendix A.4, p. 20)

Without accelerability, every interior FC optimum ( $1<R<\min\{\bar R,X\}$ ) satisfies $u'(R)\lambda-1>0$ . This is the paper's consequence of the first-order condition (A.25).
Without accelerability and with $A\beta\eta>1$ , every UC optimum satisfies $u'(R)\lambda-1=0$ (in particular it is interior).

Significance

The statement pins down when the textbook under-investment effect of financing frictions holds: exactly when extra spending scales the prize but cannot speed it up. The paper contrasts it with the possibility of over-investment on accelerable projects (Corollary 1's second statement, supported by numerical exercises). Taken together, the two statements show that the R&D technology, not only the severity of the constraint, decides the direction of the distortion.

The result is proved in the paper (Appendix A.4); it has no machine-checked proof. A formal proof certifies the comparison for every pair of optima, without the paper's tacit assumption that optima are unique. It also makes explicit the interior-optimum condition $A\beta\eta>1$ under which the inequality is strict. The resulting facts about maximizers of products of a concave power-law profit and a decreasing survival factor are reusable for other real-options models with a survival discount.

Difficulty

The first idea is to compare the two first-order conditions. The UC optimum solves $u'\lambda=1$ , and at an interior FC optimum the derivative of the survival factor pushes $u'\lambda-1$ to be positive. Concavity of $f(R)=u(R)\lambda-R$ then orders the two. Turning this into a theorem about sets of maximizers needs more. The FC optimum can sit at a corner, either $R=1$ or the right end $\min\{\bar R,X\}$ , where no first-order condition holds, and the corners must be ruled out or handled separately. The survival factor $1-(X/R)^\alpha$ vanishes at $R=X$ . The UC value vanishes at $\bar R$ . When $X\le R^*_{uc}$ , the comparison is settled by the range rather than by the first-order condition. The strict inequality is false without an interior UC optimum: if $A\beta\eta\le1$ , both optimal sets equal $\{1\}$ .

Formalization scope

All objects are in the namespace AccelScal.FCMonopoly, in one definition file. It holds the parameter structure Tech $(A,\beta,\eta,\gamma)$ , the predicate Standing, $u$ , $\lambda$ , $\bar R$ , $\alpha$ , $V_{uc}$ (5), $V_{fc}$ (6), and the maximizer sets RstarUC, RstarFC over the ranges (7). Powers are Real.rpow, and $u'$ is Mathlib's deriv.

Committed conventions:

The reduced problems are the definitions. The FC firm's original problem (3) is an expectation over a geometric Brownian motion and its first-passage time below $R$ . That its value is (6) is the paper's Lemma 1 (Appendix A.12), which needs first-passage machinery absent from Mathlib, and it is not posed. The mission takes (6), and for symmetry (5), as the definitions of the two firms' problems, exactly as the paper's proof of Corollary 1 does. $V_{fc}$ is "the value of problem (3)" only through Lemma 1.
The random payoff is replaced by its mean $u(R)$ , and the AIP term of (3)/(4), which does not depend on $R$ , is dropped.
Standing assumptions: (2), plus the added condition $A\eta>1$ (investment takes place, so $V_{uc}(1)>0$ ). The goal adds $A\beta\eta>1$ , which is necessary for the strict inequality (the UC optimum is interior), and $X\ge1$ , which keeps the FC range nonempty. " $\lambda'=0$ , $u'>0$ " is encoded as $\gamma=0$ , $\beta>0$ , which is equivalent under (2). No sign condition on $\mu$ is imposed, and $\sigma>0$ .
The paper's single-valued $R^*$ is read as a set of maximizers. The inequality is claimed for every pair of optima.

Trivializing formalizations are ruled out. $R^*_{uc}$ is never defined by its closed form, and neither optimum is a selected value. The goal asserts that both optimal sets are nonempty. The FC range depends on $X$ through $\min\{\bar R,X\}$ . The conclusion is the strict " $<$ ", not " $\le$ ".

The paper's second and third statements of Corollary 1 (over-investment when $\lambda'>0$ , and when it is "more likely") are numerical or informal and are not posed. Contributions are welcome on both milestones and on the goal. Also welcome: general lemmas on the maximizers of a positive concave function times a decreasing positive factor, and a future formalization of Lemma 1 (6) from a geometric Brownian first-passage Laplace transform.

Selected references

D. Lin, Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition, Management Science, Articles in Advance, 2022. https://doi.org/10.1287/mnsc.2022.4503
S. C. Myers, Determinants of Corporate Borrowing, Journal of Financial Economics 5(2), 147–175, 1977. https://doi.org/10.1016/0304-405X(77)90015-0

4 thms2 active usersReviewed

Completed

Graph Theory Information Theory Probability+1·Captain: mikedeng1

Partial Recovery in the Graph Alignment Problem I: If D(P‖Q)/α = o(log n/n), No Algorithm Recovers a Fraction α of a Correlated Erdős–Rényi AlignmentResearch Paper

Motivation

Graph alignment asks for the correspondence between the vertices of two graphs that are noisy copies of each other with hidden labels. It arises in the de-anonymization of social networks, where an anonymized friendship graph is matched against a public one (Narayanan–Shmatikov 2009), and in computational biology, where protein–protein interaction networks of related species are aligned. The standard random model is the correlated Erdős–Rényi model of Pedarsani–Grossglauser 2011, for which exact recovery thresholds are known (Cullina–Kiyavash 2016) and almost-exact recovery is known to be impossible when $nqs=O(1)$ (Cullina–Kiyavash–Mittal–Poor 2018).

Hall and Massoulié (arXiv:2007.00533) study the weaker goal of partial recovery: output a permutation that agrees with the hidden one on a constant fraction $\alpha$ of the vertices. This mission formalizes their impossibility theorem; a companion mission (II) formalizes their possibility theorem.

Setting

Fix $n$ and scalars $0\le q<s\le1$ . A parent graph $G\sim G(n,q/s)$ is copied twice and each copy keeps every edge independently with probability $s$ , giving graphs $G_A$ and $G_{B'}$ with adjacency matrices $A$ and $B'$ . Every unordered pair $\{i,j\}$ of distinct vertices independently carries the pair $(A_{ij},B'_{ij})\in\{0,1\}^2$ with law $P$ (equation (3)):

p_{00}=1-2q+qs,\qquad p_{01}=p_{10}=q(1-s),\qquad p_{11}=qs .

Two independent edges of $G(n,q)$ have law $Q$ (equation (4)):

q_{00}=1-2q+q^2,\qquad q_{01}=q_{10}=q(1-q),\qquad q_{11}=q^2 .

The Kullback–Leibler divergence is $D(P\|Q)=\sum_{x\in\{0,1\}^2}P(x)\log\frac{P(x)}{Q(x)}$ .

A hidden permutation $\pi^*$ of the vertices, drawn uniformly from the $n!$ permutations, relabels $G_{B'}$ into $G_B$ : $B_{\pi^*(i)\pi^*(j)}=B'_{ij}$ . An algorithm sees only $(A,B)$ and returns a permutation $\hat\pi$ , possibly at random. Its quality is the overlap

\beta(\hat\pi,\pi^*)=\frac1n\sum_{i=1}^n\mathbf 1_{\hat\pi(i)=\pi^*(i)} .

The mutual information $I(\pi^*;(A,B))$ is that of the joint law of $\pi^*$ and the observation, and $M_\alpha=\max_{\pi^*}|\{\pi\mid\beta(\pi,\pi^*)\ge\alpha\}|$ counts the permutations that are $\alpha$ -close to a given one, out of $M=n!$ .

Formalization targets

Goal: Theorem 2.1 (p. 8)

Let $\alpha_n\in(0,1)$ , bounded below by a constant $c>0$ for large $n$ . If

\frac{D(P\|Q)}{\alpha_n}=o\Big(\frac{\log n}{n}\Big),

then for every sequence of algorithms,

\mathbb P\big[\beta(\hat\pi,\pi^*)<\alpha_n\big]\to1\qquad(n\to\infty).

Milestones

Theorem 3.1 (generalized Fano inequality): $\mathbb P[d(\hat Z,Z)>d]\ge1-\frac{I(Z;\hat X)+1}{\log(M/M_d)}$ for any Markov chain $Z\to\hat X\to\hat Z$ with $Z$ uniform.
Corollary 3.2: $\mathbb P(\beta(\hat\pi,\pi^*)<\alpha)\ge1-\frac{I(\pi^*;(A,B))+1}{\log(M/M_\alpha)}$ .
Proposition 3.3: $M/M_\alpha=\Omega(\lceil n\alpha\rceil!)$ .
Inequality (8): $I(\pi^*;(A,B))\le\mathbb E_{\pi^*}\big[D(\mathbb P((A,B)=\cdot\mid\pi^*)\,\|\,\mathcal Q)\big]$ , with $\mathcal Q$ the law of two independent $G(n,q)$ graphs.
The display after (8), p. 13: $I(\pi^*;(A,B))\le\binom n2D(P\|Q)$ .

Significance

The theorem gives a sufficient condition, in terms of a single per-pair divergence, under which no algorithm (efficient or not) recovers even a fraction $\alpha$ of the alignment. Together with the companion possibility result (Theorem 2.3: partial recovery is possible when $nqs$ exceeds an explicit constant under sparsity conditions), it brackets the partial-recovery threshold; the paper's Corollary 2.2 specializes it to $nqs=o(1)$ in the regime $n^{-k}\le q=o(n^{-1/2})$ .

On the formal side, the mission produces a finite, self-contained model of correlated random graphs with a planted permutation, a generalized Fano inequality for finite hypothesis classes with an arbitrary distance, and the bound of mutual information by a product divergence. The Fano inequality and the mutual-information bounds are reusable for other information-theoretic lower bounds (community detection, planted matching, testing). The paper proves the results on paper; none of them is formalized, and no Fano inequality is proved on the platform.

Difficulty

The Fano inequality (Theorem 3.1) is cited from Lemma 20 of Banerjee–Hegde–Massoulié (2012) and not proved in the paper, and the entropy calculus it rests on is not in Mathlib in a finite, real-valued form. The counting step (Proposition 3.3) concerns rencontres numbers; the paper uses the asymptotic $D_{n,k}\sim e^{-1}n!/k!$ , which is valid only for fixed $k$ , while the statement needs control uniform in $k$ . Bounding $I(\pi^*;(A,B))$ requires relating the conditional law of the observation, a relabelled product law, to the unlabelled reference law $\mathcal Q$ on a space of $4^{n^2}$ matrix pairs, most of which have probability zero.

A natural first idea for the goal, taking $\alpha$ arbitrary as printed, fails: if $\alpha_n=1/n$ , the identity algorithm succeeds whenever $\pi^*$ has a fixed point, with probability tending to $1-e^{-1}$ , even when the divergence condition holds. The argument needs $\log(M/M_\alpha)$ to grow like $n\alpha_n\log n$ , which needs $\alpha_n$ bounded below.

Formalization scope

Vertices are Fin n; a vertex pair is an off-diagonal element of Sym2 (Fin n); an edge state is a Bool × Bool with first coordinate $A$ , second $B'$ . The probability of a configuration is the product of $P$ over pairs, and $B$ is computed through $\pi^{*-1}$ . Every probability is a finite sum; logarithms are natural. Standing assumptions on the parameters are $0\le q<s\le1$ (pp. 5 and 7); the remark "we assume $s<1$ " of p. 6 is not used and not imposed.

Algorithms are real stochastic kernels from the observed pair $(A,B)$ to permutations, so randomized algorithms are included and deterministic ones are the 0/1 kernels. The algorithm's argument is the observation only: it does not see $\pi^*$ or $G_{B'}$ . Mutual information and Kullback–Leibler divergence are defined as finite sums (Lean's $0\cdot\log 0=0$ ).

Hypotheses added relative to the page, each disclosed in the item's note:

Theorem 2.1: $\alpha_n\ge c>0$ for large $n$ (the printed statement is false for $\alpha_n\to0$ fast).
Theorem 3.1 and Corollary 3.2: $M_d<M$ (resp. $M_\alpha<n!$ ), without which $\log(M/M_d)=0$ and the bound is meaningless.
Theorem 3.1: the observation space is finite; no metric axioms on $d$ are assumed.

Proposition 3.3 reads $(n\alpha)!$ as $\lceil n\alpha\rceil!$ .

Trivializing formalizations are ruled out: the algorithm cannot be given $\pi^*$ (an oracle wins) or nothing (the statement becomes empty); the little- $o$ hypothesis is a limit of a ratio, not an inequality; the configuration law is built from (3) and sums to 1, not chosen by the solver.

Infrastructure a complete development needs: finite entropy and mutual information with the chain rule and data processing; Gibbs' inequality; derangement and rencontres counts (numDerangements in Mathlib); Stirling-type lower bounds on $\log k!$ . Contributions are welcome on each milestone independently; the Fano inequality is the piece with the widest reuse.

The source is the arXiv preprint v5 (13 Jan 2022); its numbering is used throughout.

Selected references

G. Hall, L. Massoulié, Partial Recovery in the Graph Alignment Problem, arXiv:2007.00533v5, 2022; Operations Research, 2023. https://arxiv.org/abs/2007.00533
P. Pedarsani, M. Grossglauser, On the privacy of anonymized networks, KDD 2011. https://doi.org/10.1145/2020408.2020596
D. Cullina, N. Kiyavash, Improved achievability and converse bounds for Erdős–Rényi graph matching, SIGMETRICS 2016. https://arxiv.org/abs/1602.01042
D. Cullina, N. Kiyavash, P. Mittal, H. V. Poor, Partial recovery of Erdős–Rényi graph alignment via k-core alignment, arXiv:1809.03553, 2018. https://arxiv.org/abs/1809.03553
S. Banerjee, N. Hegde, L. Massoulié, The price of privacy in untrusted recommendation engines, Allerton 2012, pp. 920–927 (Lemma 20: the generalized Fano inequality); cited as [3] in the paper.
A. Narayanan, V. Shmatikov, De-anonymizing social networks, IEEE S&P 2009. https://doi.org/10.1109/SP.2009.22
T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006. https://doi.org/10.1002/047174882X

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Achieving High Individual Service Levels Without Safety Stock? Optimal Rationing Policy of Pooled Resources I: Capacity Is Asymptotically Feasible iff E[max Σ wⱼRⱼ] ≥ Σ wⱼβⱼ for All Weights w ≥ 0Research Paper

Motivation

Firms that serve several customers from shared capacity must decide which demands to fulfil after demand is observed. A customer-level service commitment constrains the allocation policy even when total capacity appears adequate: serving one customer can consume resources that another customer needs. The question in this mission is how to test a fixed capacity vector against all individual service targets without first specifying a particular rationing rule. Jiang, Wang, and Zhang give a characterization for a broad family of pooled-resource models, including inventory pooling, process flexibility, and assemble-to-order systems (SSRN preprint, §§1.1–2).

The authors' model allows service to mean more than the probability of completely filling an order. It can represent the probability of full service, a fulfilled fraction relative to expected demand, or a fulfilled fraction of realized demand. Their Theorem 1 addresses asymptotic feasibility: every target can be met to within any prescribed positive tolerance. It is distinct from exact feasibility, which the paper treats later under stronger conditions (Jiang, Wang, and Zhang, Theorems 1–2).

Setting

There are $n$ customers and $m$ resource types. A nonnegative capacity vector $c$ is fixed before a random, nonnegative demand vector $D$ is observed. The joint law of $D$ is $F$ and has a bounded second moment. After seeing $D$ , a decision consists of a vector $s$ of fulfilled customer demands and an allocation array $y$ recording the amount of each resource assigned to each customer. The paper's set $P(c,D)$ specifies all feasible pairs $(s,y)$ for that capacity and demand. It is a model input: the three operational examples use different feasible sets (§1.1, equations (1)–(4)).

For customer $j$ , a service measure $R_j(s_j,D_j)$ assigns a nonnegative score to fulfilled demand $s_j$ and demand $D_j$ . The customer has a target $\beta_j\in(0,1)$ . A deterministic policy chooses a feasible pair in $P(c,D)$ for each $D$ . A randomized policy chooses among deterministic policies. Its expected service to customer $j$ is denoted $S_j(\lambda)$ . The capacity is asymptotically feasible when, for every $\varepsilon>0$ , some randomized policy $\lambda_\varepsilon$ satisfies $S_j(\lambda_\varepsilon)\ge\beta_j-\varepsilon$ for every customer (Definition 1, equation (8)).

For nonnegative customer weights $w=(w_j)_j$ , define maximum weighted service at a realized demand by

M_w(D)=\max_{(s,y)\in P(c,D)}\sum_j w_jR_j(s_j,D_j).

The maximum uses only service, with zero allocation cost. The paper also introduces a linear allocation cost $f(y)$ , a deterministic Max-Weighted-Service minimization problem, and its expected dual functional; Lemma 1 concerns those general objects (§2, equations (14), (16)–(17)).

Formalization targets

Theorem 1: capacity characterization

Under Assumption 1, the target is the equivalence

c\text{ is asymptotically feasible} \quad\Longleftrightarrow\quad \mathbb E_F[M_w(D)]\ge\sum_jw_j\beta_j \quad\text{for every }w\ge0.

The weights range over the whole nonnegative orthant; they are not restricted to a simplex in the theorem. Assumption 1 requires each $R_j$ to be nondecreasing and upper semicontinuous in fulfilled demand at fixed realized demand, and each $P(c,D)$ to be compact (Theorem 1, equation (18)).

Milestones from the paper

Lemma 1 identifies the value of the pointwise Max-Weighted-Service rule: $\inf_\phi F(w,\phi)=F(w,\phi_w)=\mathbb E_F[g(w,c;D)]$ for a fixed $w\ge0$ . The proof of Theorem 1 then uses a minimax display over $W=\{w\ge0:\sum_jw_j\le1\}$ to obtain, for every $\varepsilon>0$ , a randomized policy whose weighted service shortfall is at most $\varepsilon$ throughout $W$ (equation (21)). Equation (22) gives the corresponding individual service bounds. These three source claims are the mission's milestones (Lemma 1 and proof of Theorem 1, pp. 12–14).

Significance

Theorem 1 supplies a test for a vector of simultaneous service targets using a family of deterministic, weighted allocation problems. It applies to any feasible-set model satisfying the stated assumptions, rather than only to one pooling network. It also delineates the strength of the conclusion: satisfying all weighted tests guarantees arbitrarily close service, while exact attainment requires the additional assumptions in the paper's next result (Theorems 1–2).

The statements in this mission compile as Lean declarations, but their proofs have not yet been machine checked. Completing the mission would provide a reusable formal interface for demand-dependent feasible sets, measurable rationing policies, finite policy randomization, service expectations, and pointwise weighted optimization. Those definitions can also support formal study of the paper's later exact-feasibility and policy-optimality results.

Difficulty

The forward implication compares service under one policy with a maximum over feasible decisions at every demand. The reverse implication is harder: a weighted inequality for each $w$ must yield one policy that serves all customers simultaneously to a common tolerance. A separate policy chosen for each weight does not itself meet the vector of targets. The optimization involves a set of demand-dependent policies, and the source's argument relies on properties of its attainable service vectors that need explicit representation in Lean (proof of Theorem 1, pp. 13–14).

Formalization scope

Customers and resources are Fin n and Fin m, with zero-based indices; the paper numbers them from one. A solution is a pair $(s,y)$ , and $P(c,D)$ remains an arbitrary feasible set. Deterministic policies are measurable functions of $D$ that select from $P(c,D)$ for every demand realization, at the theorem's fixed capacity. Randomized policies are finite probability mixtures of these selectors. Only finitely many expected services and costs occur in the statements, and finite mixtures represent the corresponding finite-dimensional expectation vectors of the paper's policy measures. The definition of asymptotic feasibility is made directly from these policies and their service values. The maximum in the theorem is made directly from $P(c,D)$ and $R$ , so the equivalence cannot follow from defining either side in terms of the other.

The paper defines $R_j$ on nonnegative pairs. Lean uses a total real-valued extension; the theorem requires it to be nonnegative, monotone and upper semicontinuous as specified, and jointly measurable. A common integrable envelope bounds every feasible service value, preventing a nonintegrable Bochner integral from silently taking Lean's default value of zero. A measurable maximizing selector is assumed for every nonnegative $w$ ; it ensures that the expectation of $M_w(D)$ and the policy behind the source's tie-breaking are meaningful. The demand law is a probability measure with bounded second moment and nonnegative demand, capacity is nonnegative, and $\beta_j\in(0,1)$ , matching the section's standing setup. Compactness alone permits an empty feasible set in Lean; the selector assumption ensures nonemptiness at each demand.

The definitions include the linear allocation-cost functional because Lemma 1 is stated with the paper's general $f$ . An integrable envelope also bounds its absolute value in that milestone. Reusable work includes measurable selection for a demand-dependent compact feasible set, integrability of finite policy mixtures, interchange of the pointwise optimum and expectation under the stated bounds, and the finite-dimensional minimax statement. Proofs or improvements to these interfaces are welcome as long as the source claims retain their stated strength.

Selected references

J. Jiang, S. Wang, and J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, SSRN preprint 3385089, version of 31 July 2021. SSRN.
J. Jiang, S. Wang, and J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, Operations Research, 2023. DOI: 10.1287/opre.2022.2386. The mission's labels and pages follow the SSRN preprint.

5 thms2 active usersReviewed

Combinatorics Graph Theory Probability+1·Captain: mikedeng1

Partial Recovery in the Graph Alignment Problem II: Under Explicit Sparsity Conditions with nqs Above a Constant, Some Algorithm Recovers a Fraction α of the AlignmentResearch Paper

Motivation

Graph alignment asks for the correspondence between the vertex sets of two graphs that are noisy copies of each other. It underlies the de-anonymisation of social networks, where an anonymised graph is matched to a public one (Narayanan, Shmatikov 2009), the comparison of protein–protein interaction networks across species, and matching problems in computer vision. The standard random model for studying when alignment is possible is the correlated Erdős–Rényi model (Pedarsani, Grossglauser 2011).

In that model, exact recovery of the hidden correspondence and almost exact recovery (all but a vanishing fraction of vertices) have sharp thresholds: exact recovery by Cullina, Kiyavash 2016 and 2017; almost exact recovery when $nqs = \omega(1)$ by Cullina, Kiyavash, Mittal and Poor (arXiv:1809.03553). Hall and Massoulié (arXiv:2007.00533v5, Operations Research 2023) study partial recovery, the recovery of a constant fraction $\alpha$ of the correspondence, in the sparse regime $nqs = \Theta(1)$ , where almost exact recovery is impossible. This mission formalizes their possibility result, Theorem 2.3. Its companion mission (Partial Recovery in the Graph Alignment Problem I) formalizes the impossibility result, Theorem 2.1.

Setting

Fix $n \ge 1$ and parameters $q, s$ with $0 \le q < s \le 1$ . A parent graph on $\{1, \dots, n\}$ includes each edge independently with probability $q/s$ . Two copies are made, and each copy keeps every edge independently with probability $s$ . The resulting graphs $G_A$ and $G_{B'}$ have adjacency matrices $A$ and $B'$ . For each unordered pair $\{i, j\}$ of distinct vertices, $(A_{ij}, B'_{ij})$ has the law $P$ of display (3):

p_{00} = 1 - 2q + qs, \qquad p_{01} = p_{10} = q(1-s), \qquad p_{11} = qs,

independently over the $\binom n2$ pairs. The covariance of $A_{ij}$ and $B'_{ij}$ is $\sigma^2 = q(s-q)$ (display (2)), which is positive when $q > 0$ .

A planted permutation $\pi^*$ relabels $G_{B'}$ into the observed graph $G_B$ : $B_{\pi^*(i)\pi^*(j)} = B'_{ij}$ . An algorithm sees $(A, B)$ and returns a permutation $\hat\pi$ . Its quality is the overlap

\beta(\hat\pi, \pi^*) = \frac1n \sum_{i=1}^n \mathbf 1\{\hat\pi(i) = \pi^*(i)\}.

For $0 < \alpha < 1$ , a permutation $\pi$ is good (Definition 2) if at least $n(1+\alpha)/2$ vertices $i$ have degree at least $nqs/2$ in the intersection of $G_A$ with $G_B$ relabelled by $\pi$ :

\sum_{i=1}^n \mathbf 1\Big\{\sum_{j \ne i} A_{ij} B_{\pi(i)\pi(j)} \ge \frac{nqs}{2}\Big\} \ge n\cdot\frac{1+\alpha}{2}.

In Lean, these objects are pLaw, Config, cfgProb, prob, A, B', B, overlap, good and Cond6 in GraphAlignment.Possible.

Formalization targets

Goal: Theorem 2.3 (pp. 8–9)

Let $0 < \alpha < 1$ and let $q = q_n$ , $s = s_n$ be sequences. Suppose there exist $\beta, \gamma > 0$ such that, for all large $n$ ,

nqs \ge \max\Big\{20,\ 84\log\frac{2}{1-\alpha},\ \frac{16}{\min(\gamma,\beta)(1-\alpha)}\Big\}, \quad s > \frac{8q}{1-\alpha}, \quad \frac{2q(1-s^2)}{s} \le n^{-\beta}, \quad qs \le n^{-2\gamma}. \tag{6}

Then some algorithm returns $\hat\pi$ with

\mathbb P\big[\beta(\hat\pi, \pi^*) \ge \alpha\big] \to 1 \qquad (n \to \infty).

Milestones

Lemma B.3: $M^n = \alpha^n \frac{M - \beta I}{\alpha - \beta} + \beta^n \frac{M - \alpha I}{\beta - \alpha}$ for a $2 \times 2$ matrix with distinct eigenvalues $\alpha, \beta$ .
Lemma B.2: for $n+1$ independent pairs with law $P$ and $W = A_0B_1 + \dots + A_nB_0$ ,

\mathbb E[e^{tW}] = \Big(\tfrac{T + \sqrt{T^2 - 4D}}{2}\Big)^{n+1} + \Big(\tfrac{T - \sqrt{T^2 - 4D}}{2}\Big)^{n+1}, \quad T = p_{11}(e^t - 1) + 1,\ D = \sigma^2(e^t - 1).

Lemma B.1: $(\alpha^k + \beta^k)^{n/k} \le (\alpha^2 + \beta^2)^{n/2}$ for $2 \le k \le n$ and $\alpha, \beta > 0$ .
Lemma 4.3: $\min_{z > 0} z^{-\tau} e^{q_2(z^2-1) + q_1(z-1)} \le \zeta^\tau$ , with $\zeta = \max\{\sqrt2 e q_1/\tau,\ 4e(q_2/\tau)^{1/2}\}$ , and the minimizer satisfies $z^{*2} = (\tau - q_1 z^*)/(2q_2) \le \tau/(2q_2)$ .
Display (10): for a permutation $p$ with a fraction $\epsilon$ of fixed points, $|S^1_2| \le n(1-\epsilon)$ and $|\bar S^2_2| \le \binom n2 - \binom{n\epsilon}2 \le \frac{n^2}2(1-\epsilon^2)$ .
Lemma A.2, in particular: $\mathbb P(\mathrm{Po}(2\lambda/3) \ge \lambda/2 - 1) \ge 0.7$ for $\lambda \ge 20$ .
Proposition 4.2: under (6), $\pi^*$ is good with probability tending to 1.
Proposition 4.4: under (6), $\mathbb P(\forall \pi,\ [\pi \text{ good} \Rightarrow \beta(\pi, \pi^*) > \alpha]) \to 1$ .

Significance

The result. Theorem 2.3 shows that partial alignment is information-theoretically achievable in the sparse regime $nqs = \Theta(1)$ , provided $nqs$ is above an explicit constant depending on $\alpha$ . Together with Theorem 2.1, it locates partial recovery between a necessary condition stated through the divergence $D(P\|Q)$ and a sufficient condition stated through $nqs$ . It complements the almost-exact-recovery results for $nqs = \omega(1)$ , which do not apply when $nqs$ stays bounded. The moment generating function computation of Lemma B.2 and the inequality of Lemma B.1 were reused for the sharp exact-recovery threshold by Wu, Xu, Yu (p. 9 of the source).

Formalizing it. The theorem is proved on paper; no part of it is machine-checked. The paper's route to Proposition 4.2 applies a $k$ -core theorem for $G(n, \lambda/n)$ with $\lambda$ fixed and $k$ an integer, at $\lambda = nqs$ and $k = nqs/2$ , which vary with $n$ and need not be integers. The statement of Proposition 4.2 remains true, but a formal proof needs a different argument. Proposition 4.4's union bound contains two repairable gaps: an infimum taken over $z > 0$ instead of $z > 1$ , and the bound $n! \le n^{\log n}$ . A formal development would settle the theorem under exactly the conditions (6).

Difficulty

The natural first step is to compute $\mathbb P(\pi \text{ good})$ for a fixed wrong permutation $\pi$ and take a union bound over all $n!$ permutations. The difficulty is that for $\pi \ne \pi^*$ the terms $A_{ij} B'_{p(i)p(j)}$ are not independent: an edge variable enters several terms along the cycles that $p$ induces on vertex pairs. A Chernoff bound therefore needs the moment generating function of a sum over each cycle of pairs. That is a transfer-matrix computation, and the per-cycle bounds must then be recombined uniformly in the cycle lengths. The resulting exponent must beat $\log n! \approx n \log n$ . This is where the sparsity conditions $2q(1-s^2)/s \le n^{-\beta}$ and $qs \le n^{-2\gamma}$ , and the constant $16/(\min(\gamma,\beta)(1-\alpha))$ , enter. Proposition 4.2 is a concentration statement for the number of vertices of degree at least $nqs/2$ in the intersection graph, an Erdős–Rényi graph $G(n, qs)$ , when $nqs$ is only a large constant.

Formalization scope

Everything is finite. Vertices are Fin n and permutations are Equiv.Perm (Fin n). A configuration assigns $(A_{ij}, B'_{ij}) \in$ Bool × Bool to each non-diagonal element of Sym2 (Fin n), and probabilities are finite sums of the product weights. They are not taken against a free measure, so the model is a genuine probability space whenever $0 \le q < s \le 1$ . The standing assumptions $0 \le q_n < s_n \le 1$ for every $n$ (p. 5 and the running assumption $s > q$ on p. 7) are hypotheses of the asymptotic statements. The paper's remark "we assume $s < 1$ " (p. 6) is used by neither result and is not imposed. Logarithms are natural, " $\to 1$ " is a limit along $n \to \infty$ , and the thresholds $nqs/2$ and $n(1+\alpha)/2$ are real numbers, not floored.

In the goal, an algorithm is a family of maps from the observed pair $(A, B)$ to a permutation. It is chosen before the planted permutations and may depend on $n$ , $q_n$ , $s_n$ , $\alpha$ , but never on $\pi^*$ . This rules out the trivial algorithm "output $\pi^*$ ". The theorem does not say how $\pi^*$ is drawn, so the limit is required for every sequence of planted permutations, which covers the uniform case. "Exponential time" is not formalized.

Three statements are posed in a corrected reading, each disclosed in its Formalization Note. In Lemma 4.3, $\tau, q_2 > 0$ and $z > 0$ : the paper allows $\tau = q_2 = 0$ and $z = 0$ , where $\zeta$ and (13) are undefined, and Lean's convention $0^{-\tau} = 0$ would make the bound trivial. Display (10) is stated for an arbitrary permutation $p$ . Only the "in particular" clause of Lemma A.2 is stated, because the paper's proof of the general normal-approximation bound does not hold as written. Lemma 4.1 (a $k$ -core theorem of Pittel, Spencer and Wormald) is not posed.

A complete development needs: Chernoff bounds for finite sums of dependent Bernoulli variables via the transfer-matrix formula, binomial and Poisson tail estimates, and the cycle decomposition of the action of a permutation on unordered pairs. Lemmas B.1, B.3 and 4.3 are general-purpose and reusable. Proofs of any milestone, and alternative proofs of Proposition 4.2 that avoid $k$ -cores, are welcome.

The source is the arXiv preprint v5, whose appendices contain the proofs that the main text defers to an electronic companion.

Selected references

G. Hall, L. Massoulié, Partial Recovery in the Graph Alignment Problem, Operations Research, 2023; preprint arXiv:2007.00533v5, 2022. https://arxiv.org/abs/2007.00533
D. Cullina, N. Kiyavash, P. Mittal, H. V. Poor, Partial Recovery of Erdős–Rényi Graph Alignment via k-Core Alignment, arXiv preprint, 2018. https://arxiv.org/abs/1809.03553
D. Cullina, N. Kiyavash, Exact Alignment Recovery for Correlated Erdős–Rényi Graphs, arXiv preprint, 2017. https://arxiv.org/abs/1711.06783
D. Cullina, N. Kiyavash, Improved Achievability and Converse Bounds for Erdős–Rényi Graph Matching, SIGMETRICS, 2016. https://arxiv.org/abs/1602.01042
B. Pittel, J. Spencer, N. Wormald, Sudden Emergence of a Giant k-Core in a Random Graph, J. Combin. Theory Ser. B, 1996. https://doi.org/10.1006/jctb.1996.0036
Y. Wu, J. Xu, S. H. Yu, Settling the Sharp Reconstruction Thresholds of Random Graph Matching, arXiv preprint, 2021. https://arxiv.org/abs/2102.00082
A. Narayanan, V. Shmatikov, De-anonymizing Social Networks, IEEE Symposium on Security and Privacy, 2009. https://doi.org/10.1109/SP.2009.22
P. Pedarsani, M. Grossglauser, On the Privacy of Anonymized Networks, KDD, 2011. https://doi.org/10.1145/2020408.2020596

12 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Secretaries with Advice 1: Under Non-Filtering and History-Irrelevance, an Optimal Stopping Policy Is MemorylessResearch Paper

Motivation

In the classical secretary problem, $n$ candidates arrive one at a time in random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones, and must irrevocably hire or pass. The goal is to hire the best candidate, and the optimal rule (wait for about $n/e$ arrivals, then take the first candidate better than all before) succeeds with probability about $1/e$ .

In many applications the decision maker also receives advice about each candidate: a noisy score, a prediction from a machine-learned classifier, or samples from the same distribution. Dütting, Lattanzi, Paes Leme and Vassilvitskii (arXiv:2011.06726, Mathematics of Operations Research, 2024) propose a single model covering these cases: each secretary carries a signal, ranks and signals have an arbitrary known joint distribution, and the question is which policies are optimal. Their first structural result says that, under two natural conditions on the distribution, the optimal policy can ignore almost all of the history: it needs only the current signal and whether the current secretary is the best so far. Such memoryless policies are simpler, store less, and are relevant where data retention is restricted.

Timeline. Dynkin (1963) gave the $1/e$ rule for the advice-free problem. Gilbert and Mosteller (1966) studied the full-information version, where the advice is the candidate's value drawn from a known distribution. Buchbinder, Jain and Singh (2014) wrote secretary problems as linear programs. Dütting et al. (arXiv 2020) extended this LP to general advice and proved Theorem 8, the result of this mission.

Setting

There are $n$ secretaries, arriving in the order $1,\dots,n$ , and a finite signal space $\mathcal S$ . An outcome consists of ranks $r_1,\dots,r_n\in[n]$ (ties allowed) and signals $s_1,\dots,s_n\in\mathcal S$ . A signaling structure is a known probability distribution $\mathbb P$ over outcomes such that, almost surely, some secretary has the top rank $r_i=n$ .

At round $i$ the algorithm sees the information $(\preceq_{1..i},s_1,\dots,s_i)$ : the relative order of the first $i$ arrivals and their signals, not the ranks themselves. A policy $q$ assigns to every round $i$ and every information value a stopping probability in $[0,1]$ . The policy stops at $i$ with probability $q_i\prod_{j<i}(1-q_j)$ , and its winning probability is the probability that it stops at some $i$ with $r_i=n$ .

The best-so-far event is $T_i=\{r_i\ge r_j\ \forall j<i\}$ . A policy is memoryless if its stopping probability at round $i$ depends only on $i$ , on whether $T_i$ holds, and on $s_i$ .

Two properties of $\mathbb P$ are assumed. Non-Filtering (NF): for $j<i$ , the conditional law of $(\preceq_{1..j},s_1,\dots,s_j)$ given $(T_j,s_j)$ is unchanged by additionally conditioning on $(T_i,s_i)$ . History-Irrelevance (HI): conditioned on $(T_i,s_i)$ , the information at round $i$ is independent of the event $r_i=n$ .

For $i\in[n]$ , $s,s'\in\mathcal S$ and $j<i$ let $a(i,s)=\mathbb P[r_i=n,\,s_i=s]$ and $c(i,s,j,s')=\mathbb P[T_j,\,s_j=s'\mid T_i,\,s_i=s]$ . The LP of §3 has variables $z(i,s)\ge0$ , constraint

z(i,s)\le 1-\sum_{j<i}\sum_{s'\in\mathcal S}z(j,s')\,c(i,s,j,s'),\tag{4}

and objective $\mathsf{Obj}=\sum_i\sum_s z(i,s)\,a(i,s)$ (5).

Formalization targets

Goal: Theorem 8

If $\mathbb P$ satisfies NF and HI, then there is a memoryless policy $m$ with

\mathbb P[m\text{ wins}]\ \ge\ \mathbb P[q\text{ wins}]\qquad\text{for every policy } q.

Milestones

Best-so-far reduction (§2, p. 6): every policy is dominated by one that stops only on best-so-far rounds.
Equation (2) (p. 8): under HI, $\mathbb P[r_i=n\mid\prec_{1..i},s_1,\dots,s_i]=\mathbb P[r_i=n\mid T_i,s_i]$ .
Equation (3) (p. 9): under HI, $\mathbb P[X\mid s_i,r_i=n]=\mathbb P[X\mid T_i,s_i]$ for every event $X$ of the round- $i$ information.
Proposition 9 (p. 10): under NF and HI, every policy yields $z\ge0$ satisfying (4) whose objective (5) is its winning probability.
Reconstruction claim (proof of Proposition 10, p. 11): for feasible $z$ , the policy (6) satisfies $\mathbb P[i\text{ is picked}\mid T_i,s_i=s]=z(i,s)$ .
Proposition 10 (p. 10): under NF and HI, every feasible $z$ is realized by a memoryless policy with winning probability $\mathsf{Obj}$ .

Significance

Theorem 8 reduces the search for an optimal policy from functions of the entire history, whose number grows exponentially in $n$ , to $n\cdot 2\cdot|\mathcal S|$ numbers, and with Propositions 9 and 10 it turns the problem into a linear program of polynomial size. The later sections of the paper build on it: threshold policies (§4), secretaries with samples (§5) and binary-classifier advice (§6) are all analysed through this LP. The examples satisfying NF and HI include the classical problem, the full-information problem, samples, and noisy classifier advice.

The paper gives a complete proof. As far as is known, none of it has been machine-checked, and Prove2Me has no formal model of secretary problems with advice. A formal development makes precise the parts the paper's argument leaves informal: the handling of conditioning on null events, of randomized policies, and of the existence of an optimum.

Difficulty

The obvious argument replaces a general policy by its conditional stopping probability given $(T_i,s_i)$ . This fails directly: the probability of reaching round $i$ depends on the whole history, so averaging the decision at round $i$ changes the distribution of the earlier stopping events, and the winning probability with it. The paper therefore goes through the LP. The variables $z(i,s)$ summarize a policy, NF is what makes constraint (4) depend only on the distribution and not on the policy, and HI is what makes the objective linear in $z$ . The reverse direction, Proposition 10, rebuilds a policy from $z$ through an induction over rounds in which the survival probability must be tracked exactly.

Formalization scope

Finite outcome space. Secretaries and ranks are Fin n, 0-based: Lean secretary $i$ is the paper's $i+1$ , and Lean rank $n-1$ is the paper's top rank $n$ . The signal space $S$ is a finite type, so every probability is a finite sum. Continuous signals (the paper's Example 2, $\mathcal S=\mathbb R$ ) and the non-NF Example 11 are out of scope. Ties are allowed, as in §2.
Information and policies. The information at round $i$ is the comparison table $r_a\le r_b$ for $a,b\le i$ together with the signals $s_0,\dots,s_i$ . A policy is a function of this information only and never sees the outcome. Policies are randomized, with values in $[0,1]$ ; the competitors in Theorem 8 range over all of them.
Conditioning. NF, HI, (2), (3) and the reconstruction claim are written cross-multiplied, so a null conditioning event imposes nothing. $c(i,s,j,s')$ is a quotient that Lean sets to $0$ when $\mathbb P[T_i,s_i=s]=0$ ; there $a(i,s)=0$ , so the objective is unaffected.
Optimality is stated as existence of a valid memoryless policy that beats every valid policy, not as a supremum. The paper presupposes that an optimum exists; with $S$ finite it does.
Departures from the page. Proposition 10 additionally asserts that the realizing policy is memoryless; this is the proof of Theorem 8's own observation about the policy (6). Proposition 9 is stated for every policy, as printed.
Not trivial. A Memoryless predicate that allowed dependence on the whole information, or a winning probability without the survival product, would make the goal empty. Neither is used here: a memoryless policy is a function of $(i,\mathbf 1_{T_i},s_i)$ only, and the winning probability includes $\prod_{j<i}(1-q_j)$ .
Welcome contributions. Lemmas on the finite probability calculus (prob, expectOn, cross-multiplied conditioning) and the identity $\prod_{j<i}(1-q_j)=1-\sum_{j<i}q_j\prod_{k<j}(1-q_k)$ are reusable well beyond this mission. Proving the milestones in the order listed follows the paper's proof. The running time of the LP and the paper's plots are out of scope.

Selected references

P. Dütting, S. Lattanzi, R. Paes Leme, S. Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2011.06726
E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Mathematics Doklady 4, 1963.
J. P. Gilbert, F. Mosteller, Recognizing the maximum of a sequence, Journal of the American Statistical Association 61, 1966. https://doi.org/10.1080/01621459.1966.10502008
N. Buchbinder, K. Jain, M. Singh, Secretary problems via linear programming, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0604

9 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Balancing Optimal Large Deviations in Ranking and Selection: The BOLD Allocation Learns the Large Deviations Optimality Conditions With Probability OneResearch Paper

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

Theorem 1 (consistency). Under Assumptions 1–3, $N^n_x \to \infty$ for every $x$ , almost surely.
Theorem 2. Under Assumptions 1–3, $\limsup_n N^n_x/N^n_y < \infty$ for all $x, y$ , almost surely.
Theorem 3. The total balance limit above.
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

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Probability·Captain: mikedeng1

Persuading Risk-Conscious Agents: A Geometric Approach I: The Sender's Persuasion Problem Is Solved by a Convex Program over Conv(P_a ∪ {0})Research Paper

Motivation

Bayesian persuasion studies a sender who observes a state of the world and commits in advance to a randomized disclosure rule, in order to influence the action of a receiver who updates her belief by Bayes' rule. Since Kamenica and Gentzkow (2011) the model has been applied to platform design, recommendation systems, queue information and rating systems. Almost all of this theory assumes the receiver is an expected-utility maximizer, so that her payoff from each action is linear in her belief.

Many receivers are not. A customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold has a utility that is nonlinear in her belief. Anunrojwong, Iyer and Lingenbrink (2023) call such receivers risk-conscious and show that, for them, the standard revelation-principle reduction to action recommendations fails. Their first main result replaces it with a convex program over the joint distribution of state and action. This mission formalizes that result and the lemmas leading to it.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega) \subseteq \mathbb{R}^{\Omega}$ the simplex of beliefs, with the Euclidean topology. Sender and receiver share a prior $\mu^* \in \Delta(\Omega)$ . The receiver chooses an action from a finite nonempty set $A$ . Her utility is an arbitrary function $\rho : \Delta(\Omega) \times A \to \mathbb{R}$ ; the sender's utility is $v : \Omega \times A \to \mathbb{R}$ .

For each action $a$ , the beliefs at which $a$ is optimal for the receiver form the set

P_a = \{\mu \in \Delta(\Omega) : a \in \arg\max_{a' \in A} \rho(\mu, a')\}.

The paper assumes throughout (Assumption 1) that every $P_a$ is closed.

A signaling scheme consists of a measurable signal space $S$ and a probability measure $\pi$ on $\Omega \times S$ whose $\Omega$ -marginal is $\mu^*$ . After signal $s$ the receiver holds the posterior $\mu_s \in \Delta(\Omega)$ given by Bayes' rule, and plays an optimal strategy $a(\cdot)$ , with $a(s) \in \arg\max_a \rho(\mu_s, a)$ , that is $\mu_s \in P_{a(s)}$ . The sender's persuasion problem (3) is to maximize $\mathbb{E}_\pi[v(\bar\omega, a(\bar s))]$ over signal spaces, schemes and optimal receiver strategies; when the receiver is indifferent, the sender picks the strategy she prefers.

A probability measure $\eta$ on $\Delta(\Omega)$ is Bayes-plausible if its mean is the prior: $\mathbb{E}_\eta[\bar s] = \mu^*$ .

Formalization targets

Goal: Theorem 1

The sender's problem (3) can be optimized by solving the convex program

\max_{\{t_a : a \in A\}} \sum_{\omega \in \Omega} \sum_{a \in A} t_a(\omega)\, v(\omega,a) \quad \text{s.t.} \quad \sum_{a \in A} t_a(\omega) = \mu^*(\omega)\ (\omega \in \Omega), \qquad t_a \in \operatorname{Conv}(P_a \cup \{0\})\ (a \in A). \qquad (7)

It is formalized as an equality of sets: the values achievable in (3) are exactly the objective values of feasible points of (7). This says that every scheme yields a feasible point of (7) with the same value, and every feasible point is realized by a scheme. In particular the supremum of (3) equals the maximum of (7), and an optimal solution of (7) gives an optimal scheme.

Milestones

Lemma 1 (Aumann–Maschler, Kamenica–Gentzkow): schemes whose signals are beliefs and satisfy $\mu_s = s$ correspond to Bayes-plausible measures.
Lemma 5: the belief-recommendation problem (4) is equivalent to problem (14) over Bayes-plausible measures.
Lemma 2: a Bayes-plausible measure and an optimal strategy give action probabilities $b_a \in [0,1]$ and mean-posteriors $m_a \in \operatorname{Conv}(P_a)$ with $\sum_a b_a m_a = \mu^*$ and the same sender value; the converse also holds.

Further result: Theorem 2

Let $\Upsilon_a$ be the states at which $a$ is sender-optimal, assume these sets partition $\Omega$ , and set $t^*_a = \mu^* \mathbb{1}_{\Upsilon_a}$ . Then the sender can fully persuade the receiver (almost surely, the receiver takes a sender-optimal action) if and only if $t^*$ is feasible for (7), i.e. $t^*_a \in \operatorname{Conv}(P_a \cup \{0\})$ for all $a$ .

Significance

The result. Problem (3) optimizes over arbitrary signal spaces and joint distributions, so it is not finite-dimensional. Program (7) has $|A|$ vector variables in $\mathbb{R}^{\Omega}$ , each in a convex set that depends only on the receiver's utility. Its variable $t_a(\omega)$ is the joint probability of state $\omega$ and action $a$ . The program gives the paper's bound on the number of signals needed (Proposition 1), its characterization of when persuasion helps (Proposition 2), the full-persuasion criterion (Theorem 2) and, after replacing $\operatorname{Conv}(P_a \cup \{0\})$ by a polytope, the linear program for binary persuasion (Theorem 3, the companion mission). For expected-utility receivers each $P_a$ is convex, and (7) reduces to the familiar obedience-constrained linear program.

Formalizing it. The results are proved in the paper; none is formalized. A formal development fixes what "can be optimized by solving" means as a set equality and handles general measurable signal spaces with posteriors defined only almost everywhere. It also exposes two places where the printed lemmas need correction (see the scope section).

Difficulty

The usual revelation-principle shortcut would merge all signals that lead to the same action. For a risk-conscious receiver this can change the response: averaging posteriors in $P_a$ can produce a belief outside $P_a$ , since $P_a$ need not be convex. The central geometric difficulty is relating a distribution of posteriors supported on a closed, potentially nonconvex $P_a$ to a finite-dimensional variable in $\operatorname{Conv}(P_a \cup \{0\})$ . The converse must preserve both Bayes plausibility and receiver optimality. With general signal spaces, the posterior is determined only almost everywhere, while the stated strategy condition applies at every signal.

Formalization scope

Representation. $\Omega$ and $A$ are Fintypes, $A$ nonempty, and $\Omega$ carries a measurable space in which singletons are measurable. Beliefs are functions $\Omega \to \mathbb{R}$ in stdSimplex ℝ Ω, Belief Ω is the simplex as a subtype, $\operatorname{Conv}$ is convexHull ℝ, and $0$ is the zero function. $\rho$ is a function on $\mathbb{R}^{\Omega}$ , used only on the simplex.
Signal spaces in (3) range over all measurable types. A scheme is a probability measure on $\Omega \times S$ with $\pi(\{\omega\} \times S) = \mu^*(\omega)$ .
Posteriors are any version of Bayes' rule: simplex-valued for every signal, measurable, and satisfying $\pi(\{\omega\} \times B) = \int_B \mu_s(\omega)\,\pi_S(ds)$ . Quotients $\pi(\omega,s)/\sum_{\omega'} \pi(\omega',s)$ with Lean's $x/0 = 0$ are not used. " $\mu_s = s$ " (Lemmas 1 and 5) means the identity is such a version, an almost-sure statement; the paper's "for all $s$ " in Lemma 1's converse is proved only almost surely.
Strategies are measurable (each event $\{a(\bar s) = b\}$ is measurable) and optimal at every signal. The sender's value is not computed with a fixed tie-breaking rule, so sender-preferred selection is kept.
Assumption 1 is a hypothesis of every statement that involves $\rho$ .
Corrections to Lemma 2. If some $P_a$ is empty, $\operatorname{Conv}(P_a)$ is empty and the printed forward direction fails, so $m_a$ is left free there; then $b_a = 0$ necessarily. The printed converse fails for pure strategies when two actions must share a posterior, so it is stated for optimal mixed strategies, which the paper allows on p. 11.
Ruled out: quantifying (3) only over belief signals with $\mu_s = s$ would turn Theorem 1 into Lemmas 5 and 2 and drop the coalescence step. The goal therefore quantifies over arbitrary signal spaces. Stating only "the optimal values are equal" through a real supremum would also be weaker, and is not done.
Infrastructure needed: means of probability measures on compact sets in $\mathbb{R}^n$ lying in the convex hull (Convex.integral_mem, compactness of convex hulls of compact sets), Carathéodory's theorem (convexHull_eq_union), finite discrete measures on $\Omega \times S$ , and conditional densities with respect to the signal marginal. The Bayes-plausibility and splitting lemmas are reusable in any persuasion development. Proofs of the milestones, of the goal, and of Theorem 2 are all welcome.

Selected references

J. Anunrojwong, K. Iyer, D. Lingenbrink, Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2208.03758v3
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
D. Bergemann, S. Morris, Bayes Correlated Equilibrium and the Comparison of Information Structures in Games, Theoretical Economics 11(2), 2016. https://doi.org/10.3982/TE1808

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Ride-Hailing Networks with Strategic Drivers: The Impact of Platform Control Capabilities on Performance: Centralized Control Has a Unique Driver Equilibrium and the Two-Step Solution Is OptimalResearch Paper

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

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$ .
Display (18): the closed form of $\pi_C(n)$ in the three zones.
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

7 thms2 active usersReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization II: A Large upper(p) Yields a New Valid Arc for Submodular Minimization over a Ring FamilyResearch Paper

Motivation

Submodular function minimization (SFM) asks for a set $S \subseteq V$ minimizing a function $f : 2^V \to \mathbb Z$ with diminishing marginal returns. It contains minimum cut, matroid intersection and many problems of combinatorial optimization, and the question of how fast it can be solved with a value oracle has a long history: Grötschel, Lovász and Schrijver (1981) gave the first polynomial algorithm via the ellipsoid method; Iwata, Fleischer and Fujishige (2001) and Schrijver (2000) gave the first combinatorial strongly polynomial algorithms; Orlin (2009) brought the bound to $O(n^5 \cdot \mathrm{EO} + n^6)$ .

Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) applied their faster cutting plane method to SFM and obtained an $\tilde O(n^3 \cdot \mathrm{EO} + n^4)$ strongly polynomial algorithm. Like several earlier strongly polynomial algorithms, theirs works over a ring family and repeatedly adds new valid arcs that shrink the family without losing a minimizer. The combinatorial core of that step is Lemma 79 (p. 84) and its mirror image Lemma 80 (p. 86), which the authors describe as new to their work. This mission formalizes Lemma 79 and the lemmas its proof uses.

Setting

Let $V = [n]$ and let $f : 2^V \to \mathbb Z$ be submodular (Definition 58): $f(T + i) - f(T) \le f(S + i) - f(S)$ whenever $S \subseteq T$ and $i \notin T$ , where $S + i = S \cup \{i\}$ . As in §13.1, $f(\emptyset) = 0$ .

For $y \in \mathbb R^n$ write $y(S) = \sum_{i \in S} y_i$ . The base polyhedron is

\mathcal B(f) = \{ y \in \mathbb R^n : y(S) \le f(S) \ \forall S \subseteq V,\ y(V) = f(V) \}.

Every permutation $v_1, \dots, v_n$ of $V$ defines a basic feasible solution (BFS) $h$ of $\mathcal B(f)$ by $h_{v_i} = f(\{v_1, \dots, v_i\}) - f(\{v_1, \dots, v_{i-1}\})$ (Theorem 62); $v_i$ precedes $v_j$ when $i < j$ .

A set $A$ of arcs on $V$ (an acyclic digraph) represents the ring family $\mathcal F_A$ of sets $S$ such that $i \in S$ implies $j \in S$ for every arc $(i, j) \in A$ . $R(i)$ and $Q(i)$ are the descendants and the ancestors of $i$ , both including $i$ . A permutation, or its BFS, is consistent with $A$ if for every arc $(i, j)$ the element $j$ precedes $i$ (Definition 74). A vector is non-degenerate if it has both a positive and a negative entry. Finally,

\mathrm{upper}(i) = f(R(i)) - f(R(i) - i), \qquad \mathrm{lower}(i) = f(V \setminus Q(i) + i) - f(V \setminus Q(i)).

An arc $(p, q)$ is valid if adding it keeps a minimizer of $f$ over $\mathcal F_A$ .

Formalization targets

Goal: Lemma 79 (new arc)

Let $y = \sum_k \lambda^{(k)} y^{(k)}$ be a non-degenerate convex combination of BFS's consistent with $A$ . If

\mathrm{upper}(p) > n^4 \max_j y_j,

then there is $q \notin R(p)$ such that every minimizer of $f$ over $\mathcal F_A$ that contains $p$ also contains $q$ .

Milestones, in the order of the proof

Lemma 65 (p. 77): a non-negative $h \in \mathcal B(f)$ makes $\emptyset$ a minimizer; a non-positive one makes $V$ a minimizer.
(15.2) (p. 85): moving $R(p)$ to the front of a consistent permutation gives a BFS $y'$ with $y'_p = \mathrm{upper}(p)$ , $y'_j \ge y_j$ on $R(p)$ and $y'_j \le y_j$ off $R(p)$ .
The restriction claim (p. 85): $f'(S) = f(S \cup R(p))$ on $V \setminus R(p)$ is submodular, $S_{\min} \setminus R(p)$ minimizes it over the induced ring family, and $y'$ restricted to $V \setminus R(p)$ lies in its base polyhedron.
(15.3) (p. 85): $y'(V \setminus R(p)) < (n - n^4) \max_j y_j$ .
Lemma 77 (p. 84): if $y \in \mathcal B(f)$ is non-degenerate and $y_i < -(n-1)\max_j y_j$ , then $i$ is in every minimizer over $\mathcal F_A$ .

The mission also contains Lemma 76 (the mirror of Lemma 77), Lemma 78 ( $\mathrm{lower}(i) \le h_i \le \mathrm{upper}(i)$ for consistent BFS's) and Lemma 80 (the mirror of Lemma 79, giving an arc $(q, p)$ with $q \notin Q(p)$ when $\mathrm{lower}(p) < n^4 \min_j y_j$ ).

Significance

Lemmas 79 and 80 are what make the paper's SFM algorithms strongly polynomial: each application adds one of at most $2\binom n2$ arcs, and the cutting plane method supplies, through its separating hyperplanes, exactly the convex combinations of consistent BFS's the lemmas take as input. Lemma 80 has no counterpart in earlier work, and the two lemmas are stated for general ring families, which the earlier versions were not. They are also a robust version of Lemma 65: a point of the base polyhedron that is only approximately degenerate still yields structural information about every minimizer.

The lemmas are proved in the paper; none of them is formalized. The mission produces machine-checked statements and proofs of the arc-adding step, in a form independent of the cutting plane machinery and reusable by any formalization of a ring-family SFM algorithm (Iwata–Fleischer–Fujishige, Orlin, or Lee–Sidford–Wong).

Difficulty

The inequality chain of each lemma is short; the work is in the combinatorics of permutations. Moving $R(p)$ to the front of a permutation must be shown to produce a permutation again, and the comparison (15.2) depends on knowing exactly which elements precede each $j$ before and after the move; the identity $y'_p = \mathrm{upper}(p)$ holds only because consistency puts all of $R(p) - p$ before $p$ , which needs an induction along paths of $A$ . The restriction to $V \setminus R(p)$ changes the ground set, so Lemma 77, stated on the full ground set, does not apply verbatim to the restricted problem. The paper's application of Lemma 77 also does not check that the restricted vector is non-degenerate, so that case has to be handled as well.

Formalization scope

The ground set is Fin n (0-based); sets are Finset (Fin n), $f$ is integer valued and vectors are real. A permutation σ : Equiv.Perm (Fin n) is a position map ( $u$ precedes $v$ iff σ u < σ v), and the BFS of a permutation is defined by the formula of Theorem 62; Theorem 62 itself (that these are the vertices of $\mathcal B(f)$ ) is not formalized and not needed. Arcs are a relation on Fin n; $R$ and $Q$ use its reflexive-transitive closure, and the digraph is assumed acyclic, as the paper does. Minimizers in Lemmas 76–80 are over the ring family $\mathcal F_A$ ; in Lemma 65 over all subsets. Constants $n^4$ , $n - 1$ and $n - n^4$ are real numbers.

Running-time and oracle-count clauses ("using $O(n \cdot \mathrm{EO})$ oracle calls and $O(n^2)$ time") are out of scope, as is the paper's main Theorem 31 and the bound $O(n)$ on the number of BFS's in the combination (the existence claim holds for any finite combination). Validity of the new arc is stated in the strong form proved on p. 85: every minimizer containing $p$ contains $q$ . The page's base polyhedron constraint " $\forall S \not\subseteq V$ " is read as $S \subseteq V$ . The restricted base polyhedron in the restriction claim uses the normalized $f' - f'(\emptyset)$ .

The hypotheses are satisfiable: with $n = 2$ , $A = \emptyset$ , $f(\{0\}) = f(\{1\}) = 1000$ , $f(\emptyset) = f(V) = 0$ , the combination $(\tfrac12 + \tfrac1{64})(1000, -1000) + (\tfrac12 - \tfrac1{64})(-1000, 1000)$ satisfies them for $p = 0$ . A modular $f$ never does, so the goal is not vacuous only because $f$ is genuinely submodular; a formalization in which the BFS's are not tied to $f$ , or in which non-degeneracy is non-strict, would change the statement and is ruled out.

Useful infrastructure: greedy vectors of a submodular function lie in its base polyhedron; reordering lemmas for permutations of Fin n; restriction of a set function to the complement of a set. Contributions of proofs of any milestone, and of Lemmas 76, 78 and 80, are welcome.

Selected references

Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, arXiv:1508.04874v2, 2015; FOCS 2015. https://arxiv.org/abs/1508.04874
M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981). https://doi.org/10.1007/BF02579273
A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000). https://doi.org/10.1006/jctb.2000.1989
S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001). https://doi.org/10.1145/502090.502096
J. B. Orlin, A faster strongly polynomial time algorithm for submodular function minimization, Math. Program. 118 (2009). https://doi.org/10.1007/s10107-007-0189-2
S. T. McCormick, Submodular function minimization, Handbooks in OR & MS 12 (2005). https://doi.org/10.1016/S0927-0507(05)12007-6

9 thms2 active users

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Economics of Permissioned Blockchain Adoption II: A Self-Financing Consumer Access Fee Sustains Full Blockchain Adoption for Large Horizontal DifferentiationResearch Paper

Motivation

A permissioned blockchain is a shared ledger to which only approved participants may write. In supply chains it is proposed as a way to make product information (origin, quality, which supplier fulfilled an order) verifiable to buyers. Iyengar, Saleh, Sethuraman and Wang (SSRN 3602376; Management Science 2023, doi:10.1287/mnsc.2022.4532) ask who gains from such adoption and who pays for it.

Their first main result (Proposition 4.8, the subject of the companion mission I) identifies an adoption failure: when products differ strongly in how well they match consumers' tastes, full adoption raises total welfare, yet no manufacturer adopts, because price competition leaves manufacturers no profit with which to recover the adoption cost while the information gain accrues to consumers. Their second main result, Proposition 4.9, the goal of this mission, shows that a simple self-financing mechanism removes the failure: charge consumers a fee for access to the blockchain's information and pass the proceeds to the manufacturers.

Setting

There are $4m$ manufacturers, $m\ge 2$ . Manufacturer $i$ has a horizontal type $q_i\in\{A,B\}$ and a vertical type $\xi_i\in\{h,l\}$ ; each of the four type classes has exactly $m$ members. Joining the blockchain costs manufacturer $i$ an amount $\chi_i>0$ ; $a_i\in\{0,1\}$ records the decision. A unit mass of consumers values a matching product at $H$ and a mismatched one at $L$ , with $0\le L<H$ , plus a vendor quality $h>l\ge 0$ ; the high-quality vendor has marginal cost $\gamma>0$ . Each consumer $k$ also has an outside option $\phi_k$ , drawn from a continuous distribution $G$ supported on $[0,\infty)$ . The parameter of interest is the horizontal differentiation $\Delta=H-L$ ; $L$ is held fixed and $H=L+\Delta$ .

Under full adoption, a consumer who has access to the blockchain's information finds a best product utility $\Delta+L+h-\gamma$ ; without access, only $\Delta/2+L+h-\gamma$ . A system of transfers $(\kappa,\{\tau_i\}_{i\in M})$ charges each consumer who wants access a fee $\kappa$ and pays manufacturer $i$ an amount $\tau_i\ge 0$ . A consumer pays ( $b_k=1$ ) when

\max\{\Delta+L+h-\gamma,\phi_k\}-\kappa\ \ge\ \max\Big\{\tfrac{\Delta}{2}+L+h-\gamma,\phi_k\Big\},

and $\mu_\kappa$ denotes the mass of paying consumers. The system is self-financing if

\kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i. \tag{14}

Manufacturer $i$ earns $\Pi(a_i,a_{-i})-\chi_i a_i+\tau_i a_i$ (15), where the gross profit $\Pi$ is zero because of price competition. The system overcomes adoption failures if full adoption ( $a_i=1$ for all $i$ ) is an equilibrium of this game.

The proof of Proposition 4.9 uses the fee $\kappa=\sum_i\chi_i/G(\phi)$ and the gain from access

h(\phi_k;\phi)=\max\{\Delta+L+h-\gamma,\phi_k\}-\frac{\sum_{i\in M}\chi_i}{G(\phi)}-\max\Big\{\frac{\Delta}{2}+L+h-\gamma,\phi_k\Big\}.

Formalization targets

Goal: Proposition 4.9 (p. 21)

\exists\,\Delta_0\ \forall\,\Delta>\Delta_0\ \exists\,\kappa,\{\tau_i\}:\quad \tau_i\ge 0,\quad \kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i,\quad a\equiv 1\ \text{is an equilibrium of (15)}.

The goal asserts the existence of a working scheme, as printed; it does not fix the scheme.

Milestones: Lemma B.1 (p. 38)

(a) For $\Delta>0$ and every $\phi$ , $\phi_k\mapsto h(\phi_k;\phi)$ is continuous and weakly decreasing on $[0,\infty)$ .

(b) For all sufficiently large $\Delta$ there is $\phi^*\ge 0$ with

h(\phi^*;\phi^*)=0,\qquad h(\phi_k;\phi^*)\ge 0\iff \phi_k\le\phi^*\quad(\phi_k\ge 0),

so that at the fee $\sum_i\chi_i/G(\phi^*)$ exactly the consumers with $\phi_k\le\phi^*$ pay.

Significance

Proposition 4.9 is the constructive half of the paper's message: an adoption failure driven by the split between who bears the cost and who reaps the benefit can be repaired without outside funding, by a fee on the side that benefits. The paper's scheme ( $\tau_i=\chi_i$ , $\kappa=\sum_i\chi_i/G(\phi^*)$ ) exactly reimburses adoption costs and is financed by a threshold set of consumers; Lemma B.1(b) is the fixed-point statement that makes this calibration consistent.

The result is proved in the paper (App. A.2, pp. 36–38, and App. B, pp. 38–41). It has no machine-checked proof. This mission produces one: a formal model of the access-fee mechanism in the reduced form the paper's proofs use, the threshold lemma, and the main proposition. The goal can be attacked through Lemma B.1(b) as in the paper, or by any other scheme meeting the definition.

Difficulty

The calibration is circular: the fee depends on the mass of paying consumers, and the mass of paying consumers depends on the fee. Lemma B.1(b) resolves this with a one-dimensional fixed point $h(\phi^*;\phi^*)=0$ , and the delicate points are positivity of $G$ at the relevant arguments (so that the fee is finite), the three-piece shape of $h(\cdot;\phi)$ , and choosing $\Delta$ large enough that the sign change happens inside the strictly decreasing piece. For the goal, the point to check is that the self-financing identity uses the actual mass of payers at the chosen fee: a fee too high drives the payers' mass, and with it the revenue, towards zero.

Formalization scope

Reduced form. The paper's full model is a signal game with Bertrand pricing whose equilibrium concept is not defined precisely; its proofs work with the closed-form outcome of Proposition A.1. The formalization does the same: consumer utilities are those computed in the proof of 4.9 ( $\Delta+L+h-\gamma$ with access, $\Delta/2+L+h-\gamma$ without), gross profit $\Pi$ is the constant $0$ in every profile (pp. 37–38, also for a deviating manufacturer), and "equilibrium" is a pure Nash equilibrium over unilateral switches of $a_i\in\{0,1\}$ . Signal accuracy is $\alpha=1/2$ , as in the paper's main text.
Encoding. Manufacturers are Fin 2 × Bool × Fin m; adoption profiles are Bool-valued. $G$ is ProbabilityTheory.cdf μ for a measure μ on ℝ. $\Delta$ is an argument of every object, with $H=L+\Delta$ .
Standing assumptions (one predicate Model.Standing): $m\ge 2$ , $0\le L$ , $0\le l<h$ , $\gamma>0$ , $\chi_i>0$ ; $\mu$ a probability measure without atoms, $\mu((-\infty,0))=0$ , and $\mu((a,b))>0$ for $0\le a<b$ (support $[0,\infty)$ ). No cost function $c_l$ , no Assumption 1 and no finite mean are needed or assumed. Lemma B.1(a) additionally assumes $\Delta>0$ , the model's $L<H$ .
Ties in the access decision go to paying, as in the proof's " $b_k=1$ iff $h\ge 0$ ".
Ruled out. $\mu_\kappa$ is the $\mu$ -measure of the paying consumers, not a free number in $[0,1]$ ; the equilibrium predicate and $\Pi$ are defined, not assumed; transfers are nonnegative; and no statement relies on Lean's value $0$ for a division by $G(\phi)=0$ .
Not formalized. The non-uniqueness clause of Lemma B.1(b) and Example B.1 (p. 40); the purchase-stage claims of the proof of 4.9 (market shares under transfers); Appendix C's symmetric-cost variant.
Infrastructure. Only Mathlib's measure theory and ProbabilityTheory.cdf; no new library is needed. Lemmas on CDFs of atomless, fully supported laws on $[0,\infty)$ are reusable beyond this mission. Proofs of the milestones and of the goal are welcome; the goal may be proved by any route.

Selected references

G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532

10 thms2 active users

Completed

Number Theory·Captain: Nickrobbins95

Irrationality measure of π is at most 7.101862832357 (Bai 2026)Research Paper

Y. Bai (arXiv:2609.11276, September 2026) proves that the irrationality measure of π is at most 7.101862832357, improving the Zeilberger–Zudilin bound 7.103205334137 (2020). The proof keeps the Zeilberger–Zudilin integral but gives its numerator two independent exponents, specialised at A₁ = A₂ = 1857/2785; the resulting integer linear forms in 1 and π, combined with Hata's lemma, give μ(π) ≤ 7.101862832357. This entry is the campaign template with the value 7.101862832357. Source: https://arxiv.org/abs/2609.11276

3 thms2 active usersReviewed

All missions

Operational Risk Management: Optimal Inspection Policy II: The Optimal Hybrid Inspection Policy Strictly Beats the Random Policy and Weakly Beats the Periodic PolicyResearch Paper

Why inspection timing matters

The model

Formalization targets

Goal: Proposition 5 (p. 20)

Milestones

Significance

Where the difficulty lies

Formalization scope

Selected references

Dynamic Optimal Reinsurance and Dividend Payout in Finite Time Horizon I: The HJB Variational Inequality Has a Unique Classical Solution with v_x ≥ 1, v_xx ≤ 0 and λv_x + v_xx ≥ 0Research Paper

Dividends, reinsurance and a finite horizon

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamic Optimal Reinsurance and Dividend Payout in Finite Time Horizon II: For Discrete Claims the Reinsurance Boundaries Are C¹, Start at 0 and Are Spaced Less Than (z_j − z_{j−1})/2c ApartResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Marketplace Leakage 1: With Uniform Switching Costs the Equilibrium Fee Is min{μ, v − c}, Leakage Is Positive but Partial, and the Marketplace's Profit Increases in μResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Direct Fidelity Estimation from Few Pauli Measurements 2: A Unit Vector Nearly Orthogonal to 2^{cd} Given States With Every Non-Identity Pauli Expectation ≤ √(72π³)·√(log d)/√dResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 1

Milestones (all p. 7)

Significance

Difficulty

Formalization scope

Selected references

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost IV: Low Switching Cost, Control-Band Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 7, first claim

Proposition 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Digital Privacy II: Against the Social Optimum, a Business Never Under-Collects While Over-Protecting Data, and a Purely Usage-Driven One Under-Collects and Under-ProtectsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2, first two sentences

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality I: Feasible Solutions of the Continuous Stopping LP Can Be Improved to Threshold FormResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 8)

Milestones

Significance

Difficulty