Operations Research

Motivation

Social-media influencers earn money by endorsing products to their followers. An endorsement of a product that does not fit the audience brings in money today but costs followers, and followers are also what spreads awareness of the influencer to new people. Nistor, Selove and Villas-Boas (Influencer Authenticity: To Grow or to Monetize, Management Science, 2024) model this trade-off as a deterministic, infinite-horizon, discounted optimal-control problem with a single binary control. In their base model (§3) the optimal policy is to grow first and monetize later: authentic while awareness is small, permanently inauthentic once awareness passes a threshold.

Section 4.2 of the paper asks how this changes when the audience is not permanent: users join and leave the platform, or the influencer covers a topic that interests people only for a while. With follower turnover the influencer never reaches full awareness, and Proposition 3 says that if turnover is fast enough she never monetizes at all. The model gives a testable prediction: influencers on platforms with rapid user turnover, or in product categories with short-lived interest, should stay authentic.

Setting

Time is $t \in [0, \infty)$. There is a unit mass of potential followers, and $A_t \in [0,1]$ is the share of them who are aware of the influencer, starting from $A_0$. At each time she is either authentic or inauthentic. Following Table 1 of the paper:

• authentic: $F_t = A_t$ followers and instantaneous profit $\pi_t = A_t$;
• inauthentic: $F_t = \gamma A_t$ followers and profit $\pi_t = \gamma\varphi A_t$,

with $0 < \gamma < 1$ and $\varphi > 1$. These are the reduced-form parameters of §3.1: a fraction $\gamma$ of aware people follow an inauthentic influencer, who earns $\varphi$ per follower, and authentic profit per follower is normalized to $1$. The paper assumes $\gamma\varphi > 1$ "for the remainder of the paper", so that being inauthentic pays more today.

Potential followers leave and are replaced at a turnover rate $x \in (0, \beta)$, and awareness follows equation (6):

$$\frac{dA_t}{dt} = \beta F_t (1 - A_t) - x A_t ,$$

where $\beta > 0$ is the word-of-mouth rate. Under the always-authentic policy this is the logistic equation $\frac{dA_t}{dt} = A_t(\beta - x - \beta A_t)$, with steady state $\frac{\beta - x}{\beta}$. The influencer maximizes the discounted profit (2), $\int_0^\infty e^{-rt}\pi_t\,dt$, with discount rate $r > 0$.

In the Lean development (namespace InfluencerAuth.Turnover) a policy is a measurable set $S \subseteq \mathbb R$ of the times at which she is inauthentic, so $S = \emptyset$ is "always authentic". IsPath β γ x A₀ S A says $A$ is an admissible awareness path, discountedProfit γ φ r S A is (2) at time $0$, and IsOptimalFrom β γ φ r x A₀ S A says that $(S, A)$ earns at least as much as every measurable policy with any admissible path from the same $A_0$. authValue β x r is the closed form $\overline V$ of Lemma 5, and Condition2 γ φ β r x is

$$\frac{(1-\gamma)x}{r + \beta - x} > \gamma\varphi - 1 .$$

Formalization targets

Goal: Proposition 3 (p. 9)

Under the standing assumptions $0<\gamma<1$, $\varphi>1$, $\gamma\varphi>1$, $\beta>0$, $r>0$, with $0 < x < \beta$ and Condition 2,

$$\forall A_0 \in \Bigl(0, \tfrac{\beta - x}{\beta}\Bigr),\quad \exists A,\ \ (\emptyset, A) \text{ is optimal from } A_0 .$$

The range of $A_0$ is the paper's set of "all feasible levels of awareness". The statement fixes no constant beyond those of Condition 2.

Milestone: Lemma 5 (p. 9)

For $0 < A_0 < 1$ and every admissible always-authentic path $A$ from $A_0$,

$$\int_0^\infty e^{-rt} A_t\,dt = \overline V(A_0) = \int_0^\infty \frac{e^{-rs}}{\frac{\beta}{\beta - x} + \frac{1 - A_0\beta/(\beta - x)}{A_0} e^{-(\beta - x)s}}\,ds .$$

Milestone: display (7) (p. 9)

$$\left.\frac{d\overline V(A)}{dA}\right|_{A = \frac{\beta - x}{\beta}} = \int_0^\infty e^{-(r + \beta - x)s}\,ds = \frac{1}{r + \beta - x}.$$

Significance

Proposition 3 is the paper's result on when the grow-then-monetize pattern of the base model breaks down. Without turnover the influencer always monetizes once she is large enough (Proposition 1, §3). With turnover there is a whole parameter region, given by Condition 2, where monetizing is never optimal. The condition compares the extra current profit from being inauthentic, $\gamma\varphi - 1$, with the awareness lost by being inauthentic, $(1-\gamma)x$, valued at the marginal value of awareness at the steady state, $1/(r+\beta-x)$ from (7).

The proofs are in an online appendix that is not part of the published article, and this result has no machine-checked proof. The mission provides a precise statement of the control problem: optimality over every measurable switching pattern, with the dynamics in integral form. It also gives the closed-form always-authentic value and its derivative as separate targets. A complete development would be one of the first formal optimality proofs for an infinite-horizon, discounted, continuous-time deterministic control problem.

Difficulty

Optimality is claimed against every measurable policy, not only against constant or threshold policies. The natural argument is a verification theorem: show that $\overline V$ satisfies the Hamilton–Jacobi–Bellman inequality on the feasible range, then integrate along an arbitrary competitor path. Condition 2 is stated only at the steady state $(\beta-x)/\beta$, where (7) gives the marginal value of awareness. At a lower awareness level the inequality comparing the two actions involves $\overline V'(A)$ at that level, so it does not follow from Condition 2 alone; it needs control of $\overline V'$ on the whole interval. A competitor path may also switch infinitely often, so its awareness is only absolutely continuous, and the comparison must work almost everywhere. Above the steady state the always-authentic policy is in general not optimal, so any argument must use the restriction $A_0 < (\beta - x)/\beta$.

Formalization scope

• Policies and dynamics. A policy is a measurable Set ℝ. An admissible path is continuous on $[0,\infty)$, starts at $A_0$, stays in $[0,1]$, and satisfies $A_t = A_0 + \int_0^t (\beta f_S(s) A_s(1-A_s) - xA_s)\,ds$ for $t \ge 0$, with $f_S = \gamma$ on $S$ and $1$ off $S$. This is the Carathéodory form of (6). A derivative everywhere is not required, because that would exclude every switching policy. The clause $A_t\in[0,1]$ follows from the equation and is stated to make integrability explicit.
• Objective. discountedProfit is $\int_{(0,\infty)} e^{-rt} p_S(t) A_t\,dt$ with $p_S = \gamma\varphi$ on $S$ and $1$ off $S$; the paper's value from time $t$ is the same object after the shift $s = u - t$. No optimal value is defined as a real supremum; optimality is a comparison with every competitor.
• Hypotheses. The goal carries every standing assumption of the paper: $0<\gamma<1$, $\varphi>1$, $\gamma\varphi>1$, $\beta>0$, $0<x<\beta$. It also assumes $r>0$, which is how "discount rate $r$" is read and which makes (2) finite. The milestones drop $\gamma$, $\varphi$ and their assumptions, which the always-authentic value does not involve.
• No trivialization. The goal produces the optimal path existentially, so it cannot hold for lack of an admissible path. The competitor class is nonempty (the logistic solution is admissible), and every competitor's profit is the integral of a bounded measurable function, so no competitor collapses to the junk value $0$. Widening $A_0$ to $(0,1)$ would make the statement false, not stronger.
• Infrastructure. The development needs the explicit logistic solution with turnover, differentiation under the integral sign for $\overline V$, and a comparison or verification argument for scalar ODEs with measurable coefficients. The verification lemma for discounted bang-bang control of a one-dimensional state is reusable for chunk 1 of this series and for similar marketing-diffusion models. Proofs of either milestone, a sanity proof that the logistic path is admissible, and the verification argument are all welcome contributions.

Selected references

• C. Nistor, M. Selove, J. M. Villas-Boas, Influencer Authenticity: To Grow or to Monetize, Management Science, Articles in Advance, 2024. https://doi.org/10.1287/mnsc.2023.03479
• F. M. Bass, A New Product Growth for Model Consumer Durables, Management Science 15(5), 1969, 215–227. https://doi.org/10.1287/mnsc.15.5.215
• W. H. Fleming, R. W. Rishel, Deterministic and Stochastic Optimal Control, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7

Why scoring rules for multivariate distributions

A probabilistic forecast issues a whole distribution $P_X$ for an uncertain quantity $Y\in\mathbb R^d$ rather than a single number: wind and wave heights at several sites, demand for several products, the joint returns of several assets. Forecasts of this kind are compared and estimated with a scoring rule $S(P_X,y)$, a number assigned to the forecast once the realization $y$ is observed. A scoring rule is proper if a forecaster who knows the true distribution $P_Y$ minimizes the expected score by reporting it, and strictly proper if $P_Y$ is the only minimizer (Gneiting and Raftery 2007). Properness is what makes a score usable for model ranking and for M-estimation: an improper score rewards systematic misreporting.

For univariate distributions the continuous ranked probability score (CRPS) and the quadratic score are standard. In several dimensions the choices are thinner: the quadratic score needs a density and is sensitive to its spikes, and the energy score and the multivariate CRPS (MCRPS) were treated as separate constructions. Meng, Taylor, Ben Taieb and Li (arXiv:2002.09578v6, Operations Research, 2025) give one family, the L² scoring rules, which contains the quadratic score, the CRPS and the MCRPS as special cases and produces new ones, such as a score based on lower partial moments. Their Theorem 1 says these rules are proper. This mission formalizes that theorem.

Setting

Work on $\mathbb R^d$ with Lebesgue measure $\mathcal L^d$ and the componentwise order. A distribution is a probability measure $P$ on $\mathbb R^d$; the paper writes it through a generalized density $f_P$ (a PDF, a PMF or a mixture), and every integral $\int g(s)f_P(s)\,ds$ below is $\int g\,dP$. The forecasts range over a class $\mathcal V^d$ of distributions.

Fix a kernel $w:\mathbb R^d\to\mathbb R$ and a weight $h\ge0$ that is integrable. The smoothed density of $P$ is the convolution

$$(f_P*w)(z)=\int_{\mathbb R^d} w(z-s)\,dP(s).$$

For the Heaviside kernel $u(z)=\mathbb 1\{z\ge0\}$ it is the CDF $F_P(z)=P\{s\le z\}$.

The two L² scoring rules are, for a forecast $P_X$ and a realization $y$,

$$S(P_X,y;w,h)=\int_{\mathbb R^d}\big((f_X*w)(z)-w(z-y)\big)^2h(z)\,dz \qquad (2)$$ $$S'(P_X,y;w,h)=\int_{\mathbb R^d}(f_X*w)^2(z)h(z)\,dz-2\int_{\mathbb R^d}(f_X*w)(z)\,w(z-y)\,h(z)\,dz. \qquad (3)$$

The realization $y$ is treated as a point mass, whose convolution with $w$ is $w(\cdot-y)$. The divergence of a score is $\mathbb E_{P_Y}[S(P_X,\bullet)]-\mathbb E_{P_Y}[S(P_Y,\bullet)]$, and the paper's candidate is the weighted L² distance between smoothed densities,

$$\int_{\mathbb R^d}\big((f_X*w)(z)-(f_Y*w)(z)\big)^2h(z)\,dz. \qquad (1)$$

Assumption 1 (p. 32) collects the integrability under which all these integrals are finite.

Formalization targets

Goal: Theorem 1 (p. 8)

Under Assumption 1, for all $P_X,P_Y\in\mathcal V^d$,

$$\mathbb E_{P_Y}[S(P_X,\bullet)]-\mathbb E_{P_Y}[S(P_Y,\bullet)]=\mathbb E_{P_Y}[S'(P_X,\bullet)]-\mathbb E_{P_Y}[S'(P_Y,\bullet)]=\int\big(f_X*w-f_Y*w\big)^2h\,dz\ \ge 0,$$

so both rules are proper. If in addition $h\ne0$ $\mathcal L^d$-a.e. and $f_Y*w$ determines $P_Y$ within $\mathcal V^d$, both are strictly proper. The goal fixes no kernel and no weight: it holds for every pair $(w,h)$ meeting the assumption.

Milestones

1. The relation between (2) and (3): $S=S'+\int w^2(z-y)h(z)\,dz$, a term that does not depend on the forecast (p. 8).
2. The Fubini step of the proof: $\int\!\int g(z)w(z-s)h(z)\,dz\,dP_Y(s)=\int g\,(f_Y*w)\,h\,dz$ (p. 32).
3. The divergence display: the divergence of (2) equals (1) and is nonnegative (p. 32).
4. The strict step: a vanishing divergence with $h\ne0$ a.e. forces $f_X*w=f_Y*w$ a.e. (p. 32).
5. MCRPS (5) and MCRPS′ (6) are strictly proper for all distributions when $h\ne0$ a.e. (p. 11).
6. Lower partial moments of any order $k$ determine the distribution (Appendix, p. 34).

Significance

Theorem 1 is the paper's justification for its whole family of scores. With $w=u$ it shows that the MCRPS is proper; with $w$ the kernel of lower partial moments it shows that a new LPM score is proper; and in Section 4 of the paper the same smoothed densities $f_Y*w$ define the level sets whose scoring functions are the subject of the companion mission (Mission II of this series). Strict properness reduces to one question about the kernel: whether $f_Y*w$ determines $P_Y$. Milestones 5 and 6 answer it for the CDF and for lower partial moments.

The result is proved in the paper (appendix, pp. 32 and 34). To our knowledge none of it is formalized: Mathlib has no scoring rules, and the platform has no proper scoring rule for distributions, no multivariate CRPS and no lower partial moment. The formalization adds the integrability bookkeeping the paper leaves implicit, a machine-checked uniqueness theorem for the multivariate CDF (Mathlib's ext_of_Iic covers linear orders only, i.e. $d=1$), and the same for lower partial moments.

Difficulty

The algebraic core of Theorem 1 is the expansion of a square, and the obvious argument is the paper's. The cost lies elsewhere. Every expectation is an iterated integral of a function of $(s,z)$, and exchanging the order (Fubini) and splitting an integral of a difference require the integrability that Assumption 1 states only as "then (2) is well-defined and finite". The proof also uses $\int dP_Y=1$ when it integrates the $y$-free terms against $P_Y$.

For the companions the obstacle is measure-theoretic. An a.e. equality of multivariate CDFs must first be upgraded to equality everywhere, by right-continuity in each coordinate, and then measures that agree on lower orthants must be shown equal, a π-system argument in $\mathbb R^d$. For lower partial moments the paper differentiates $k$ times under the integral; a rigorous version has to control the finiteness of the lower-order moments.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with its product Lebesgue measure volume and the Pi order, so $y\le z$ is componentwise and lower orthants are Set.Iic z. $d$ is any natural number; at $d=0$ the strict clauses are vacuous, as in the paper.
• Distributions are measures with IsProbabilityMeasure; the class $\mathcal V^d$ is a set of such measures. Its convexity (§2) is never used and is not imposed.
• Standing assumptions. The kernel $w$ is a measurable function. The paper also allows a local Borel measure, so that $w=\delta_0$ gives the quadratic score (4); that case is not covered. $h$ is measurable, nonnegative and integrable, not normalized to a density.
• Assumption 1 made explicit. Its clauses (b) and (c) are formalized as integrability hypotheses, each labelled with its clause: $(f_Y*w)^2h$ and $w(\cdot-y)^2h$ integrable; $(s,z)\mapsto w(z-s)^2h(z)$ integrable for $P_Y\otimes\mathcal L^d$; $(f_X*w)\,w(\cdot-y)\,h$ integrable; and $(s,z)\mapsto(f_X*w)(z)\,w(z-s)\,h(z)$ integrable for $P_Y\otimes\mathcal L^d$. Clause (a) adds that $f_Y*w$ is well defined.
• "$f_X*w=f_Y*w$" is an $\mathcal L^d$-a.e. equality. "$f_Y*w$ uniquely characterizes any $P_Y\in\mathcal V^d$" is a property of the whole class $\mathcal V^d$, not of the pair at hand. "$h$ nonzero $\mathcal L^d$-a.e." is used with the paper's quantifier. The theorem's printed "$f_{\mathbf y}*w$" is read as $f_Y*w$.
• Lower partial moments are defined from the explicit kernel printed in (7), $\prod_j (z_j-s_j)^k\mathbb 1\{z_j\ge s_j\}/k!$, for $k\in\mathbb N$, not as a convolution power of $u$. Milestone 6 states equality of the LPMs implying $P_X=P_Y$, the claim of its opening sentence.
• Ruling out trivial readings. A Bochner integral of a non-integrable function is $0$ in Lean, so every expectation in every statement carries the integrability that makes it the paper's integral. Without it, properness could hold because both sides are $0$. The characterization hypothesis is never assumed for the pair $(P_X,P_Y)$ alone.
• Needed infrastructure: product-measure Fubini (integral_integral_swap), integrability of products and squares, and uniqueness of measures from a generating π-system. A general lemma "a multivariate CDF determines its measure" would be reusable well beyond this mission and is welcome as a separate contribution.

Selected references

• X. Meng, J. W. Taylor, S. Ben Taieb, S. Li, Scores for Multivariate Distributions and Level Sets, Operations Research, 2025; preprint arXiv:2002.09578v6, 2023. https://arxiv.org/abs/2002.09578v6
• T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 359–378, 2007. https://doi.org/10.1198/016214506000000437
• T. Gneiting, R. Ranjan, Comparing Density Forecasts Using Threshold- and Quantile-Weighted Scoring Rules, Journal of Business & Economic Statistics 29(3), 411–422, 2011. https://doi.org/10.1198/jbes.2010.08110

Motivation

Risk sharing asks how a total loss $X$ should be split among $n$ agents, each of whom evaluates its share with its own risk measure, so that the sum of their assessments is as small as possible. The smallest achievable sum is the inf-convolution of the agents' risk measures, and an allocation that attains it is an optimal allocation. For Value-at-Risk, the risk measure of the Basel framework, this problem was solved by Embrechts, Liu and Wang (2018) and extended to agents with heterogeneous beliefs by Embrechts, Liu, Mao and Wang (2020).

Lambda Value-at-Risk ($\Lambda\mathrm{VaR}$), introduced by Frittelli, Maggis and Peri (2014), replaces the fixed confidence level of VaR by a function $\Lambda$ of the loss threshold, so that the tolerated exceedance probability may depend on the size of the loss. Liu and Schied (2025) study $\Lambda\mathrm{VaR}$ when probabilities are replaced by capacities, which model ambiguity about the underlying distribution: a capacity can be the upper envelope of a family of probability measures. Their Section 5.1 answers the question of what the inf-convolution of such risk measures is, which earlier work had settled for constant $\Lambda$ under capacities (Choquet quantiles, Liu, Mao and Wang 2024) and for $\Lambda\mathrm{VaR}$ under probability measures (Liu 2025; Liu, Tsanakas and Wei 2025).

Setting

$(\Omega,\mathcal F)$ is a measurable space and $\mathcal X$ a set of random variables containing every bounded one. A capacity is a map $w:\mathcal F\to[0,1]$ that is increasing for inclusion with $w(\emptyset)=0$ and $w(\Omega)=1$; it is continuous if $w(A_n)\to0$ whenever $A_n\downarrow\emptyset$. For a function $\Lambda:\mathbb R\to(0,1)$ (the class $\mathcal H$; increasing members form $\mathcal H_I$) and a capacity $w$,

$$\Lambda\mathrm{VaR}^w(X)=\inf\{x\in\mathbb R:\ w(X>x)\le\Lambda(x)\},\qquad\inf\emptyset=+\infty,$$

a value in $[-\infty,\infty]$. $\mathcal H^*_I$ ($\mathcal H^*_D$) denotes the increasing (decreasing) functions $\mathbb R\to(0,1]$.

The allocations of $X$ are $\mathbb A_n(X)=\{(X_1,\dots,X_n)\in\mathcal X^n:\sum_iX_i=X\}$, and the inf-convolution of $\rho_1,\dots,\rho_n$ is

$$\mathop{\square}_{i=1}^n\rho_i(X)=\inf\Big\{\sum_{i=1}^n\rho_i(X_i):(X_1,\dots,X_n)\in\mathbb A_n(X)\Big\}.$$

A downset is a collection $\mathcal A\subseteq\mathcal F$ containing $\emptyset$ and closed under taking measurable subsets. A family $\{\mathcal A_x\}_{x\in\mathbb R}$ of downsets induces the risk measure $\rho(X)=\inf\{x:\{X>x\}\in\mathcal A_x\}$. For $\boldsymbol\Lambda=(\Lambda_1,\dots,\Lambda_n)$ and $\mathbf w=(w_1,\dots,w_n)$ the paper defines

$$\mathcal A^{\boldsymbol\Lambda,\mathbf w}_x=\Big\{\bigcup_{i=1}^nA_i:\ w_i(A_i)\le\Lambda_i(y_i),\ i\in[n],\ \textstyle\sum_iy_i=x\Big\},$$

and $\Pi_n(\Omega)$ denotes the measurable partitions of $\Omega$ into $n$ (possibly empty) parts.

Formalization targets

Goal: Proposition 8

For $\Lambda_i\in\mathcal H$ with $\lambda^-_i=\inf\Lambda_i>0$ and continuous capacities $w_1,\dots,w_n$:

$$\mathop{\square}_{i=1}^n\Lambda_i\mathrm{VaR}^{w_i}(X)=\inf\{x\in\mathbb R:\{X>x\}\in\mathcal A^{\boldsymbol\Lambda,\mathbf w}_x\};$$

if this infimum is attained at $x^*$, then $X_i=(X-x^*)\mathbb 1_{A^*_i}+y^*_i$ is optimal for every $(y^*_i)$ with $\sum_iy^*_i=x^*$ and $(A^*_i)\in\Pi_n(\Omega)$ with $w_i(\{X>x^*\}\cap A^*_i)\le\Lambda_i(y^*_i)$ (and such data exist); and if all $\Lambda_i$ are increasing, the inf-convolution equals $\Lambda\mathrm{VaR}^w$ for some $\Lambda\in\mathcal H^*_I$ and capacity $w$.

Milestones

• Remark 1: under a continuous capacity, $\Lambda\mathrm{VaR}^w(X)<\infty$ when $\inf\Lambda>0$ or $\Lambda\in\mathcal H_I$.
• Theorem 3 (7): for risk measures $\rho_i$ induced by families of downsets $\{\mathcal A^{(i)}_x\}$ with values in $[-\infty,\infty)$, $\mathop{\square}\rho_i(X)=\inf\{x:\{X>x\}\in\widetilde{\mathcal A}_x\}$, where $\widetilde{\mathcal A}_x=\bigcup_{y_1+\dots+y_n=x}\{\bigcup_iA_i:A_i\in\mathcal A^{(i)}_{y_i}\}$.
• Theorem 3 (8): a minimizer of (7) yields the optimal allocation $(X-x^*)\mathbb 1_{A^*_i}+y^*_i$.
• Theorem 3, monotonicity: $\{\widetilde{\mathcal A}_x\}$ is increasing (decreasing) when all input families are.
• Theorem 1 (i): $\rho$ is a $\Lambda\mathrm{VaR}^w$ with $\Lambda\in\mathcal H^*_I$ iff it is induced by an increasing family of downsets.
• Theorem 1 (ii): the decreasing, left-continuous counterpart.

Significance

Proposition 8 shows that risk measures of $\Lambda\mathrm{VaR}$ type, under possibly different capacities for different agents, are closed under inf-convolution when all $\Lambda_i$ increase, and it gives explicit optimal allocations: each agent pays a fixed amount $y^*_i$ and carries the excess $X-x^*$ on one cell of a partition. It contains as special cases the inf-convolution of VaR (Embrechts et al. 2018), of VaR with heterogeneous beliefs (Embrechts et al. 2020) and of Choquet quantiles (Liu, Mao and Wang 2024). Via the paper's Corollary 4 it yields risk sharing for robust $\Lambda\mathrm{VaR}$ over sets of probability measures.

The result is proved in the preprint; it has no machine-checked proof. A formalization adds a verified account of the extended-real bookkeeping that the paper leaves implicit, and it pins down which printed claims hold: two claims in the preprint are false (see Formalization scope), which a formal development has to avoid.

Difficulty

The individual risk measures are not real-valued: $\Lambda_i\mathrm{VaR}^{w_i}$ can be $-\infty$, and without the finiteness of Remark 1 it can be $+\infty$, in which case a sum over agents is meaningless. Every step of (9) therefore has to be carried out in the extended reals, and the identity has to hold in the degenerate cases (an empty or unbounded threshold set) as well as the generic one. Capacities are neither additive nor continuous from above in general, so the familiar quantile arguments for probability measures do not transfer.

The last claim of the goal is not a consequence of (9) alone: it needs the representation Theorem 1 (i), whose converse direction must produce a $\Lambda$ and a capacity from an abstract increasing family of downsets, including degenerate families in which $\Omega$ itself is eventually admissible or no nonempty event ever is. The natural first idea, that the decreasing case is symmetric, fails: the convolved family of downsets need not be left-continuous, and the decreasing analogue of the claim is false.

Formalization scope

Lean namespace LambdaVaRAmb.InfConv. Random variables are measurable maps $\Omega\to\mathbb R$; the domain $\mathcal X$ is any set of functions that contains all bounded measurable functions, consists of measurable functions, and is closed under $X\mapsto(X-c)\mathbb 1_A+d$ and under $X\mapsto f(X)$ for increasing 1-Lipschitz $f$ with $f(0)=0$. This is the disclosed reading of the paper's "good enough properties"; bounded and all measurable functions both qualify. Capacities are real set functions whose axioms are imposed on measurable sets. $\Lambda\mathrm{VaR}$, induced risk measures and the inf-convolution are valued in EReal, with $\inf\emptyset=+\infty$. Agents are indexed by Fin n with $n\ge1$ (implicit in the paper). "Increasing" is Monotone; left-continuity of $\Lambda$ is continuity within $(-\infty,x]$; "admits a minimizer" is attainment of the infimum (IsLeast).

Not posed, because false: the claim of Theorem 3 that $\{\widetilde{\mathcal A}_x\}$ is left-continuous when all input families decrease, and the decreasing branch of Proposition 8. With $w_1=w_2$ Lebesgue measure on $[0,1]$, $\Lambda_1$ equal to $0.4$ on $(-\infty,0)$ and $0.1$ on $[0,\infty)$, and $\Lambda_2(y)=0.1+0.4/(1+e^y)$, the convolved family is not left-continuous and the inf-convolution is not a $\Lambda\mathrm{VaR}^w$ with decreasing $\Lambda$. The goal states the increasing branch only.

Trivializing encodings are ruled out: infima are taken in EReal (a real sInf would collapse unbounded sets to $0$); the finiteness hypothesis of Theorem 3 keeps $+\infty$ and $-\infty$ out of the sums; the domain $\mathcal X$ is constrained so that the tail allocations lie in it; downsets consist of events; the allocation clause comes with an existence clause so that it cannot hold vacuously; and the representing pair $(\Lambda,w)$ is chosen uniformly in $X$. Sanity checks (not part of the mission) confirm that the hypotheses of Proposition 8 are satisfiable and that $\Lambda\mathrm{VaR}$ of a constant is that constant.

Contributions welcome: Remark 1 and the monotonicity milestone are short and independent; Theorem 3 is reusable for any risk measure induced by downsets; Theorem 1 is a general representation result for $\Lambda\mathrm{VaR}$ under capacities.

Selected references

• P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv preprint, 2025. https://arxiv.org/abs/2511.00717v1
• M. Frittelli, M. Maggis and I. Peri, Risk measures on $\mathcal P(\mathbb R)$ and Value at Risk with probability/loss function, Mathematical Finance 24(3), 442–463, 2014.
• P. Embrechts, H. Liu and R. Wang, Quantile-based risk sharing, Operations Research 66(4), 936–949, 2018. https://doi.org/10.1287/opre.2017.1716
• P. Embrechts, H. Liu, T. Mao and R. Wang, Quantile-based risk sharing with heterogeneous beliefs, Mathematical Programming Series B 181(2), 319–347, 2020. https://doi.org/10.1007/s10107-018-1313-1
• P. Liu, Risk sharing with Lambda value at risk, Mathematics of Operations Research 50(1), 313–333, 2025.
• P. Liu, T. Mao and R. Wang, Quantiles under ambiguity and risk sharing, arXiv preprint, 2024. https://arxiv.org/abs/2412.19546v1
• P. Liu, A. Tsanakas and Y. Wei, Risk sharing with Lambda Value-at-Risk under heterogeneous beliefs, Finance and Stochastics, forthcoming. https://arxiv.org/abs/2408.03147

Motivation

Ranking and selection (R&S) asks which of $k$ simulated systems has the largest mean performance when every observation is costly. It is a basic tool of simulation optimization: choosing a staffing level, an inventory policy or a network design from a large catalogue of candidates that can only be evaluated by noisy simulation. In the fixed-budget formulation a total of $B$ observations is spent sequentially and one alternative is selected at the end; procedures are compared by their probability of correct selection (PCS).

Cloud and parallel computing have made problems with thousands to millions of alternatives routine, and the relevant question is how the budget must grow with $k$. A procedure is sample optimal if a budget $B = ck$, linear in $k$, keeps its PCS bounded away from zero as $k \to \infty$; a total budget of order $k$ is clearly necessary. Li, Fan and Hong (arXiv:2303.02951) show that the simplest procedure of all, the greedy procedure, which always samples the alternative with the largest current sample mean, is sample optimal. They also show that its PCS limit is strictly below one under the slippage configuration, however large $c$ is: the greedy procedure is not consistent. This mission formalizes the remedy: an exploration phase of $n_0$ observations per alternative before the greedy phase makes the procedure consistent.

Setting

There are $k$ alternatives. Alternative $i$ produces independent observations $X_{i1}, X_{i2}, \dots \sim N(\mu_i, \sigma_i^2)$, independent across alternatives, and alternative 1 is the unique best. The running average after $n$ observations is $\bar X_i(n) = \frac1n\sum_{j=1}^n X_{ij}$.

Assumption 1 (p. 12). There are constants $\gamma > 0$ and $\bar\sigma^2 > 0$ such that $\mu_1 - \max_{i \ge 2}\mu_i \ge \gamma$ and $\max_i \sigma_i^2 \le \bar\sigma^2$, regardless of how large $k$ is.

The explore-first greedy (EFG) procedure (Procedure 2, p. 21) with exploration size $n_0$ and budget $B$:

1. take $n_0$ observations from every alternative, and set $n_i = n_0$;
2. while $\sum_i n_i < B$, take one more observation from $\arg\max_i \bar X_i(n_i)$;
3. select $\arg\max_i \bar X_i(n_i)$.

With $B = ck$ the exploration phase uses $n_0 k$ observations and the greedy phase $n_g k$, where $n_g = c - n_0$. The greedy procedure is the case $n_0 = 1$.

Crossing times. Let $Z_1, Z_2, \dots$ be iid standard normal, $\bar Z(n) = \frac1n\sum_{j=1}^n Z_j$, and

$$\tilde N(x; n_0) = \inf\{n \ge n_0 : \bar Z(n) < x\}, \qquad C(x; n_0) = \mathrm E\big[\tilde N(x; n_0)\big] \in [0, \infty],$$

with $\inf \emptyset = \infty$. $C(\cdot\,; n_0)$ is finite exactly on $(0, \infty)$, where it is strictly decreasing and continuous.

Consistency (Definition 2, p. 21): A sample-optimal fixed-budget R&S procedure is consistent if the PCS of the procedure satisfies that, for any $\alpha \in (0,1)$, there exists a constant $c>0$ such that $\liminf_{k\to\infty} \mathrm{PCS} \ge \alpha$, for $B = ck$.

Formalization targets

Goal: Theorem 4 (p. 24)

Suppose Assumption 1 holds. Let $\alpha \in (0,1)$ and $\gamma_0 \in (0, \gamma)$. Let $n_0 \ge 1$ satisfy

$$\Pr\Big\{\min_{n \ge n_0} \bar X_1(n) > \mu_1 - \gamma_0\Big\} \ge \alpha \tag{5.3}$$

and let $n_g \ge C\big(\tfrac{\gamma - \gamma_0}{\bar\sigma}; n_0\big) - n_0$. If $B = (n_0 + n_g)k$, then the PCS of the EFG procedure satisfies

$$\liminf_{k \to \infty} \mathrm{PCS} \ \ge\ \alpha .$$

Milestones

1. Lemma 3 (p. 22): $\bar Z(n)$, $n \ge n_0$, attains its minimum at a finite time almost surely.
2. (5.1) (p. 22): $\tilde N(x) \le \tilde N(x; n_0) \le n_0 \inf\{m \ge 1 : \bar Z(mn_0) < x\}$, and the last crossing time is distributed as $\tilde N(\sqrt{n_0}\,x)$ (scaling corrected, see below).
3. Lemma 4 (p. 22): $\tilde N(x;n_0)$ is a.s. finite with finite mean for $x > 0$; finite with probability strictly between 0 and 1, with infinite mean, for $x < 0$; a.s. finite with infinite mean for $x = 0$.
4. Lemma 7 (p. ec6): $C(x; n_0)$ is strictly decreasing and continuous on $(0, \infty)$.
5. (5.2) (p. 23): $\mathrm{PCS} \ge \Pr\big\{\sum_{i=2}^k N_i(\bar X_1^*(n_0); n_0) + N_1^*(n_0) \le B\big\}$, where $\bar X_1^*(n_0)$ and $N_1^*(n_0)$ are the minimum and argmin of $\bar X_1(n)$ over $n \ge n_0$, and $N_i(b; n_0)$ is the first $n \ge n_0$ with $\bar X_i(n) < b$.
6. Theorem 3 (p. 23, first sentence): if $B/k = n_0 + n_g$ and $n_g > C(\gamma/\bar\sigma; n_0) - n_0$, then $\liminf_k \mathrm{PCS} \ge \Pr\{\min_{n\ge n_0}\bar X_1(n) > \mu_1 - \gamma_0\}$, where $\gamma_0 \in (0, \gamma)$ solves $C\big(\tfrac{\gamma-\gamma_0}{\bar\sigma}; n_0\big) = n_g + n_0$.
7. Lemma 5 (p. 24): for every $\gamma_0 > 0$ and $\alpha \in (0,1)$ some finite $n_0 \ge 1$ satisfies (5.3).

Significance

The result. Theorem 4 shows that a one-line change to the greedy procedure, a fixed number of initial observations per alternative, turns a sample-optimal but inconsistent procedure into one that is both sample optimal and consistent. Any PCS target is reached with a budget that grows only linearly in the number of alternatives, without variance estimates, elimination rules or pairwise comparisons. Together with (5.4) (p. 24) it also gives a recipe for choosing $n_0$ and $n_g$ when $\gamma$ and $\bar\sigma^2$ are known, which converts the fixed-budget procedure into a fixed-precision one.

Formalizing it. The results are proved in the paper, but Lemma 4 and Theorem 4 have their proofs omitted ("straightforward"), and Theorem 3's proof refers to "almost the same analysis" as Theorem 1. A machine-checked development makes these steps explicit. It also corrects the scaling in (5.1), which is misprinted in the source. No part of it is formalized on the platform. The boundary-crossing inequality (5.2) and the crossing-time lemmas for the Gaussian running average are reusable in the companion missions of this series and for other greedy procedures.

Difficulty

The obvious approach is to bound each inferior alternative's sample size by the number of observations it needs to fall below alternative 1, and to sum. It fails because alternative 1's running average is itself random, may drop below its mean, and can lose the lead at any time before it reaches its minimum. The boundary must be the random minimum $\bar X_1^*(n_0)$, and the crossing times of the other alternatives are then dependent through it. The step from (5.2) to Theorem 3 needs crossing times dominated by iid copies of $\tilde N(\cdot\,; n_0)$ on the event that the minimum is high, a strong law over the growing array, and the continuity of $C(\cdot\,; n_0)$ (Lemma 7) to pass to the limit in the level. Lemma 4 needs fluctuation facts for the Gaussian random walk (finite expected crossing time for $x>0$, infinite mean at $x=0$) that are not in Mathlib.

Formalization scope

• Model. Observations form an array $X_{ij}$ indexed by $\mathbb N \times \mathbb N$ on a probability space, mutually independent, with $X_{ij} \sim N(\mu_i, \sigma_i^2)$ and $\sigma_i^2 > 0$. Problem $k$ uses alternatives $0, \dots, k-1$; Lean's alternative $0$ is the paper's alternative 1. One array serves every $k$, which does not change any PCS.

• Procedure. The EFG procedure is a deterministic map from the observation array to the selected index. Ties in every arg max go to the smallest index, which is a null event under the model. The greedy loop runs $B - n_0k$ times (none if $B \le n_0k$).

• Budget. $B = (n_0 + n_g)k$ is read as $\lfloor (n_0+n_g)k \rfloor$. Conditions involving $C(\cdot\,; n_0) - n_0$ are written additively in $[0, \infty]$.

• Crossing times, argmins and $C$. These take values in $\mathbb N \cup \{\infty\}$ and $[0, \infty]$. A path that never crosses has crossing time $\infty$, and $C(0; n_0) = \infty$ is literal. "$\min_{n \ge n_0} \bar X_1(n) > a$" means that the path is bounded below from $n_0$ on and its infimum exceeds $a$. The minimum is attained a.s. (Lemma 3).

• Probabilities and limits. These are extended nonnegative reals. The liminf is taken in $[0, \infty]$.

• (5.1) correction. The paper derives $\tilde N(x;n_0) \le n_0\tilde N(x/\sqrt{n_0})$ from "$\bar Z(mn_0) = \sqrt{n_0}\,\bar Z(m)$ statistically". In fact $\bar Z(mn_0) \overset{d}{=} \bar Z(m)/\sqrt{n_0}$, so the milestone states the bound with $\tilde N(\sqrt{n_0}\,x)$. The printed form is false for $x < 0$ and $n_0 \ge 2$.

• Theorem 3. The existence of $\gamma_0$, implicit in the paper, is a conclusion of the statement, so the lower bound cannot hold vacuously. The slippage-configuration limit in its second sentence is not stated.

• Ruled out. None of the following can make the statements trivial, because the encodings above exclude them:

  • an $\mathbb N$-valued crossing time with $\inf\emptyset = 0$;
  • a real infimum of an unbounded path read as $0$;
  • an unsolvable equation for $\gamma_0$.

• Infrastructure needed. A complete development needs the following, all reusable beyond this mission:

  • laws of crossing times of the Gaussian random walk;
  • the strong law for iid $\mathbb N\cup\{\infty\}$-valued variables;
  • a coupling of the crossing times with iid copies;
  • a pathwise induction over the run of the procedure for (5.2).

  Contributions to any milestone are welcome.

• Source. The source is the authors' arXiv preprint, version 3 (11 Dec 2023), and all numbering follows it.

Selected references

• Z. Li, W. Fan, L. J. Hong, The (Surprising) Sample Optimality of Greedy Procedures for Large-Scale Ranking and Selection, arXiv:2303.02951v3, 2023; Management Science, 2025. https://arxiv.org/abs/2303.02951
• R. E. Bechhofer, A single-sample multiple decision procedure for ranking means of normal populations with known variances, Annals of Mathematical Statistics 25(1):16–39, 1954. https://doi.org/10.1214/aoms/1177728845
• S.-H. Kim, B. L. Nelson, A fully sequential procedure for indifference-zone selection in simulation, ACM Transactions on Modeling and Computer Simulation 11(3):251–273, 2001. https://doi.org/10.1145/502109.502111

Motivation

Ranking and selection (R&S) asks how to spend a fixed budget of simulation runs on $k$ competing system designs so that the design with the largest mean performance is identified with high probability. When $k$ runs into the thousands or millions, the relevant question is how the total budget must grow with $k$. Li, Fan and Hong (arXiv:2303.02951v3, published in Management Science, 2025) showed that the simplest adaptive rule, the greedy procedure, is sample optimal: a budget linear in $k$ keeps the probability of correct selection (PCS) bounded away from zero (their Theorem 1, p. 15). This mission formalizes their second main result: under the least favorable configuration of means and variances, the PCS lower bound of Theorem 1 is exactly the limit, so it cannot be improved for the greedy procedure.

The result also explains the paper's later design choices. Corollary 1 (p. 18) deduces from it that the greedy procedure is not consistent: however large the constant $c$ in $B = ck$, its worst-case PCS stays below a constant less than one. This is why §5 of the paper introduces an explore-first variant.

Setting

There are $k$ alternatives. Alternative $i$ produces independent observations $X_{i1}, X_{i2}, \dots \sim N(\mu_i, \sigma_i^2)$, independent across alternatives, and alternative $1$ is the unique best. The running average of alternative $i$ after $n$ observations is $\bar X_i(n) = \frac1n \sum_{j=1}^n X_{ij}$.

The greedy procedure (Procedure 1, p. 10) takes one observation from each alternative, then repeatedly takes one more observation from the alternative with the largest current running average, until $B$ observations have been taken in total; it selects the alternative with the largest final running average. PCS is the probability that it selects alternative $1$, and PICS $= 1 -$ PCS.

The slippage configuration with a common variance (SC-CV, §4.3, p. 16) is

$$\mu_1 - \mu_i = \gamma > 0 \quad (i = 2, \dots, k), \qquad \sigma_i^2 = \sigma^2 > 0 \quad (i = 1, \dots, k):$$

the non-best alternatives share one mean and all alternatives share one variance.

The constant governing the analysis is

$$C(x) = \exp\Big( \sum_{n=1}^\infty \frac1n \Phi(-\sqrt n\, x) \Big), \qquad x > 0,$$

where $\Phi$ is the standard normal distribution function. By Lemma 2 of the paper, $C(x)$ is the expected first time $n$ at which the running average of iid $N(0,1)$ variables drops below $x$; it is continuous and strictly decreasing on $(0, \infty)$ and tends to $\infty$ as $x \to 0^+$.

Formalization targets

Goal: Theorem 2 (p. 16)

If $B = ck$ and $c > C(\gamma/\sigma)$, let $\gamma_0 \in (0, \gamma)$ solve $C((\gamma - \gamma_0)/\sigma) = c$. Under the SC-CV,

$$\lim_{k\to\infty} \mathrm{PCS} = \Pr\Big\{ \min_{n\ge1} \bar X_1(n) > \mu_1 - \gamma_0 \Big\} = \Big[C\Big(\frac{\gamma_0}{\sigma}\Big)\Big]^{-1}.$$

The goal asserts both that some such $\gamma_0$ exists and that the limit holds for every solution.

Milestones, in the order of the proof (EC.1.4, pp. ec3–ec5)

1. (EC.1.8), p. ec4: with $m_\epsilon$ the first time $\bar X_1$ drops below a level $\mu_1 - \gamma_\epsilon^+$, PICS is at least the probability that the budget suffices to reach $m_\epsilon$ but not to push every other alternative below the new minimum of $\bar X_1$.
2. (EC.1.11), p. ec5, with $\gamma_\epsilon^\pm$ from (EC.1.7): $\liminf_k \mathrm{PICS} \ge \Pr\{ m_\epsilon < \infty, \min_{1\le n\le m_\epsilon-1} \bar X_1(n) \ge \mu_1 - \gamma_\epsilon^- \}$.
3. (EC.1.6), p. ec3: $\liminf_k \mathrm{PICS} \ge \Pr\{\exists n \ge 1 \text{ s.t. } \bar X_1(n) < \mu_1 - \gamma_0\}$.
4. Theorem 1 under the SC-CV, p. 15: $\liminf_k \mathrm{PCS} \ge \Pr\{\min_{n\ge1} \bar X_1(n) > \mu_1 - \gamma_0\} = [C(\gamma_0/\sigma)]^{-1} > 0$.

Milestones 3 and 4 bound the PCS from above and below by the same quantity, up to the null event $\{\min_n \bar X_1(n) = \mu_1 - \gamma_0\}$. Corollary 1 (p. 18, $\lim \mathrm{PCS} \le [C(\gamma/\sigma)]^{-1} < 1$) is included as a separate theorem after the goal; it is not a milestone.

Significance

The result. Theorem 1 gives a lower bound on the asymptotic PCS that holds for every configuration satisfying a gap and a variance bound. Theorem 2 shows the bound is attained under the SC-CV, so it is the exact worst-case asymptotic PCS of the greedy procedure on a linear budget. It also identifies the slippage configuration as least favorable for this procedure. Corollary 1, which follows from it, shows that the greedy procedure is sample optimal without being consistent. The paper uses this to motivate the explore-first greedy procedure of §5, which is consistent.

Formalizing it. The theorem is proved in the paper; none of it is formalized. A formal proof requires a precise, total definition of the greedy procedure as a map from an observation array to a selected alternative, a pathwise analysis of that map (milestone 1), the strong law of large numbers for iid crossing times with values in $\mathbb N \cup \{\infty\}$, and a limiting argument in $\epsilon$ that uses the continuity and strict monotonicity of $C$. The identity $\Pr\{\min_n \bar X_1(n) > \mu_1 - \gamma_0\} = [C(\gamma_0/\sigma)]^{-1}$ is the Gaussian case of Spitzer's identity, which Mathlib does not have.

Difficulty

The lower half is Theorem 1. The upper half needs a different pathwise argument. Showing that the greedy procedure can succeed only requires bounding the budget the inferior alternatives consume. Showing that it must fail requires an event on which alternative 1 has fallen below a level and the remaining budget cannot lift it back. The paper conditions on such an event, $B_\epsilon$. On $B_\epsilon$, two families of crossing times, measured against two different random levels (the running minimum of $\bar X_1$ before and at $m_\epsilon$), are compared with deterministic multiples of $k$. Both comparisons need the strong law, and the event $B_\epsilon$ must survive the limit $\epsilon \to 0$. The obvious first idea is to copy the proof of Theorem 1 with the inequalities reversed. It fails because the inclusion (3.2) behind Theorem 1 is one-sided: a large budget forces a correct selection, but a small budget alone does not force an incorrect one.

Formalization scope

• Model. Alternatives are indexed from $0$ in Lean: Lean's alternative $0$ is the paper's alternative $1$. Observations form one infinite array $X_{ij}$ on a probability space, mutually independent over all pairs $(i, j)$, with $X_{ij} \sim N(\mu_i, v_i)$. The problem with $k$ alternatives reads rows $0, \dots, k-1$. PCS for $k$ alternatives depends only on the law of those rows, so this coupling changes no PCS.
• Procedure. The procedure is a deterministic function of the array. Ties in every arg max go to the smallest index; ties have probability zero under normality. With fewer than $k$ observations of budget, no greedy step is taken.
• Budget. "$B = ck$" is read as $B = \lfloor ck \rfloor$.
• Values. Probabilities, limits and liminfs are taken in $[0, \infty]$. Crossing times take values in $\mathbb N \cup \{\infty\}$, with $\infty$ when no crossing occurs. "$\min_{n\ge1} \bar X_1(n) > a$" means the running average is bounded below and its infimum exceeds $a$; the minimum is attained almost surely.
• The constant $C$. It is defined by the series above. Every statement evaluates it only at positive arguments ($\gamma/\sigma$, $(\gamma - \gamma_0)/\sigma$, $\gamma_0/\sigma$), where the series converges.
• Disclosed generalization. Milestone 1 is stated for an arbitrary level and for arbitrary means with positive variances, since the inclusion uses neither the SC-CV nor the event $B_\epsilon$.

Three trivializations are ruled out. Crossing times typed in $\mathbb N$ would be $0$ when no crossing occurs. Junk values of tsum or of the infimum on unbounded sets would make the statements meaningless. A $\gamma_0$ that no value can satisfy would make the goal vacuous, which is why the goal also asserts that $\gamma_0$ exists.

Infrastructure needed: the strong law for iid $\mathbb N \cup \{\infty\}$-valued variables with finite mean, Spitzer's identity for Gaussian random walks, and continuity of $C$. These would be reusable in any boundary-crossing analysis of sequential procedures. Contributions toward any milestone, or toward these general lemmas, are welcome. The source PDF is the arXiv v3 preprint (11 Dec 2023), and all page and equation numbers refer to it.

Selected references

• Z. Li, W. Fan, L. J. Hong, The (Surprising) Sample Optimality of Greedy Procedures for Large-Scale Ranking and Selection, arXiv:2303.02951v3, 2023; Management Science, 2025. https://arxiv.org/abs/2303.02951
• F. Spitzer, A combinatorial lemma and its application to probability theory, Trans. Amer. Math. Soc. 82 (1956), 323–339. https://doi.org/10.1090/S0002-9947-1956-0079851-X
• R. E. Bechhofer, A single-sample multiple decision procedure for ranking means of normal populations with known variances, Ann. Math. Statist. 25 (1954), 16–39. https://doi.org/10.1214/aoms/1177728845

Motivation

Fake follower accounts are sold openly to social media influencers, who buy them because advertisers and new followers read a large follower count as a sign of quality. Platforms respond with antifake effort: detection, removal and registration hurdles that make fake accounts more expensive to operate, but that also impose a nuisance cost on legitimate users (more CAPTCHAs, more false flags). Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game and ask how fake-account purchases respond to the platform's effort and to contextual factors such as social media literacy and antifake technology.

A finding of the paper that runs against intuition concerns the high-quality influencer. In a costly separating equilibrium the high type buys fake accounts defensively, so that a low-quality influencer cannot afford to mimic its follower count. This contrasts with Chen and Papanastasiou (2021), where only the low type manipulates. Proposition 3 of the paper describes how this defensive purchase moves with every parameter, and in particular that raising the antifake effort can increase it. This mission formalizes Proposition 3 and the steps the paper uses to explain it.

Setting

An influencer is of high type $H$ or low type $L$, with content qualities $q_H>q_L>0$. A unit mass of consumers has valuation $\theta\sim U[0,1]$ and follows when $\theta q\ge c$. A fraction $l\in(0,1)$ of consumers, the social media literacy, know the type; the rest infer it from the early follower count, which the influencer can inflate with fake accounts. Advertising yields revenue $\mu$ per real follower, of which the influencer keeps a share $\lambda_i$.

The platform chooses an antifake effort $d\ge0$. With antifake technology level $\tau\in[0,1)$, base price $p_0$, opportunity cost $c_0\ge0$ and nuisance coefficient $c_1\ge0$, the unit price of fake accounts and the cost of following are

$$p_f=p_0+\frac{d}{1-\tau},\qquad c=c_0+c_1(1-\tau)d .$$

A type of quality $q$ has $n_{in}=l(1-c/q)$ informed followers, and, when its type is revealed, $n_{un}=(1-l)(1-c/q)$ uninformed ones. With $\eta_2=\frac1l\lambda_i\mu(1-l^2)$ and $d_2=(1-\tau)(\eta_2-p_0)$, Lemma 2 of the paper gives the costly separating equilibrium for $d\le d_2$, in which the H-type's early-follower count is

$$n_2^{csep}=\frac1{p_f}\lambda_i\mu\big[(1-l)(n_{in}^H-n_{in}^L)+(n_{un}^H-n_{un}^L)\big]+n_{in}^L \quad(17)$$

and its defensive purchase is $x_H^{csep}=n_2^{csep}-n_{in}^H$. In the pooling equilibrium the low type's offensive purchase is $x_L^{pool}=n_{in}^H-n_{in}^L$. In Lean the parameters are fields mu lamI lamP rho l qH qL c0 c1 tau p0 gamma of a structure Params, and the quantities above are price, cost, nIn, nUnSep, eta2, d2, nCsep2, xCsepH, xPoolL.

Formalization targets

Goal: Proposition 3(c)

Assume $c_0>0$, $p_0>0$ and Assumption 3 ($p_0<\eta_2$). Let (22) be the condition

$$c_1(1-\tau)^2\le\frac{\lambda_i\mu(1-l^2)c_0}{p_0[\lambda_i\mu(1-l^2)-p_0l]} .$$

If (22) holds, $d\mapsto x_H^{csep}(d)$ is strictly decreasing on $[0,d_2]$. Otherwise there is $\hat d\in(0,d_2)$ with $x_H^{csep}$ strictly increasing on $[0,\hat d]$ and strictly decreasing on $[\hat d,d_2]$.

Milestones

1. The closed form (20): $x_H^{csep}=\frac1{p_f}[\lambda_i\mu(1-l^2)-p_fl](c/q_L-c/q_H)$.
2. The marginal effects: $dx_H^{csep}/dd=m_1+m_2$, with $m_1$ the higher fake-account price effect and $m_2$ the higher nuisance cost effect, as displayed on p. 8875.
3. $m_2=0$ at $d=d_2$, and $x_H^{csep}$ is strictly decreasing on a left neighbourhood of $d_2$.
4. Proposition 3(a): $x_H^{csep}$ strictly decreases in $l$, in $p_0$, in the quality ratio $R=q_L/q_H$ and in $\tau$ (four milestones).
5. Proposition 3(b): $x_H^{csep}$ strictly increases in $\lambda_i$.

A companion theorem, not a milestone, states Proposition 2(a)–(b) for the offensive purchase $x_L^{pool}$.

Significance

Proposition 3(c) says that the platform's main instrument against fake accounts can backfire: below a threshold on the technology level, a moderate increase in antifake effort makes high-quality influencers buy more fake accounts, because the higher nuisance cost widens the follower gap the low type would have to close. Proposition 3(a) identifies the levers that reduce defensive purchases unambiguously: literacy, the base price, and antifake technology. Together with Proposition 2, these results underlie the paper's policy discussion of when an antifake campaign reduces the number of fake accounts at all.

The results are proved in the paper's Online Appendix; none of them is machine-checked. The formalization makes every hypothesis explicit: positivity of $c_0$ and $p_0$, the exact domain on which each monotonicity claim is strict, and the reading of the informal remark "$m_2\to0$", which is false as $d\to\infty$ and true at the edge $d_2$ of the costly separating range. It also yields a reusable closed form for the equilibrium purchase that other statements about this model can cite.

Difficulty

The closed form and the derivative are algebra and calculus over rational functions of $d$, with care about $p_f\ne0$. The content is the dichotomy in (c). On $[0,d_2)$ the two marginal effects have opposite signs, $m_1<0<m_2$, and both depend on $d$ through $p_f$ and through $c$. The paper's informal argument ("$m_2\to0$, so $m_1$ dominates eventually") settles only the right end of the range. What the goal requires is the sign of $m_1+m_2$ on the whole interval: that it changes sign at most once, that (22) is exactly the condition for it to be nonpositive at $d=0$, and that in the other case the change of sign happens strictly inside $(0,d_2)$. Strictness of the parameter comparative statics also fails at the edges ($d=0$ for $\tau$, $d=d_2$ for $R$), so each domain has to be chosen exactly.

Formalization scope

All quantities are real-valued closed forms; no probability spaces are introduced, since the paper's expectations over $\theta$ are already the closed forms (8)–(9). The parameter bundle carries the standing ranges of §3 and Table 1: $\mu>0$, $\lambda_i,\lambda_p>0$, $\lambda_i+\lambda_p<1$, $0<\rho<1$, $0<l<1$, $0<q_L<q_H$, $c_0,c_1\ge0$, $0\le\tau<1$, $\gamma>0$. The readings of the paper fixed by the formalization are:

• Assumptions 1 and 2 ($q_L>c$, $\lambda_i>p_f/(\mu+p_f)$) depend on $d$ and are not imposed; the follower formulas are used untruncated, as in the paper. This strengthens every statement.
• Added hypotheses $c_0>0$ (needed for strictness) and $p_0>0$ ((22) divides by $p_0$; $p_f>0$ at $d=0$); Assumption 3 where the paper uses it.
• The quality ratio $R$ is never defined in the paper; it is $q_L/q_H$ with $q_H$ fixed, as the text after Proposition 3 says.
• Domains. Proposition 3(c) is stated on $[0,d_2]$; when a pooling range exists, the costly separating range is $(d_1,d_2]$ and the peak of the second case may lie below $d_1$. The $\tau$ claim needs $d>0$ and $p_f\le\eta_2$; the $R$ claim needs $d<d_2$. The $l$, $p_0$ and $\lambda_i$ claims hold for every value in the open range, a strengthening.
• "$m_2\to0$" is formalized as $m_2(d_2)=0$ plus strict decrease near $d_2$.
• Proposition 2(c) ("unaffected by $p_0$ or $\lambda_i$") is not posed: it holds by definition.

$x_H^{csep}$ is defined as $n_2^{csep}-n_{in}^H$ through (17), not by the right side of (20); a definition by (20) would make the closed-form milestone trivial. The goal must be proved about this function on $[0,d_2]$, not about a sign condition on an abstract derivative. The proofs are in the paper's Online Appendix, which is not used here; every milestone is a statement or display of the main text. Contributions of proofs of any milestone are welcome, as are lemmas on single-crossing of the derivative.

Selected references

• Z. Huang and D. Liu, Economics of Social Media Fake Accounts, Management Science 71(10):8865–8883, 2025. https://doi.org/10.1287/mnsc.2022.02616
• L. Chen and Y. Papanastasiou, Seeding the Herd: Pricing and Welfare Effects of Social Learning Manipulation, Management Science 67(11):6734–6750, 2021.
• X. Guo, G. Xiao and F. Zhang, Effect of Consumer Awareness on Corporate Social Responsibility under Asymmetric Information, SSRN preprint, 2017. https://doi.org/10.2139/ssrn.3039862
• G. J. Mailath, M. Okuno-Fujiwara and A. Postlewaite, Belief-Based Refinements in Signalling Games, Journal of Economic Theory 60(2):241–276, 1993.