Probability

Why estimation risk matters for mean-variance portfolios

Mean-variance analysis (Markowitz, 1952) tells an investor which portfolio to hold once the mean vector $\mu$ and covariance matrix $\Sigma$ of asset returns are known. In practice both are estimated from a finite window of past returns, and the portfolio built from the estimates (the plug-in portfolio) performs badly out of sample: its weights are noisy and its realized utility is often far below the theoretical optimum. A long literature asks how to choose portfolio rules that take this estimation risk into account; Kan and Zhou (2007) treat the case with a risk-free asset.

Kan, Wang and Zhou (2022) study the case without a risk-free asset, where the investor must be fully invested in $N$ risky assets. There the optimal portfolio splits into the global minimum-variance (GMV) portfolio plus a scaled zero-investment portfolio, and estimation errors enter the two parts very differently. Their §2 derives the exact expected out-of-sample utility of the family of rules that rescale the estimated zero-investment part, and the coefficient that maximizes it. This mission formalizes that derivation.

Setting

An investor chooses weights $w \in \mathbb R^N$ with $1_N' w = 1$ to maximize the mean-variance utility

$$U(w) = w'\mu - \frac{\gamma}{2}\, w'\Sigma w,$$

where $\gamma > 0$ is the risk-aversion coefficient and $\Sigma$ is positive definite. The population quantities that matter are the GMV variance $\sigma_g^2 = 1/(1_N'\Sigma^{-1}1_N)$, the GMV mean $\mu_g = 1_N'\Sigma^{-1}\mu\,\sigma_g^2$, and the squared slope of the asymptote of the minimum-variance frontier, $\psi^2 = \mu'\Sigma^{-1}\mu - \mu_g^2/\sigma_g^2 \ge 0$.

The returns $r_1, \dots, r_h$ of an estimation window of length $h$ are independent and identically distributed $\mathcal N(\mu, \Sigma)$. The maximum-likelihood estimators are $\hat\mu_t = \frac1h\sum_s r_s$ and $\hat\Sigma_t = \frac1h\sum_s (r_s - \hat\mu_t)(r_s - \hat\mu_t)'$. From them come the sample GMV portfolio and the sample zero-investment portfolio

$$\hat w_{g,t} = \frac{\hat\Sigma_t^{-1}1_N}{1_N'\hat\Sigma_t^{-1}1_N}, \qquad \hat w_{z,t} = \hat\Sigma_t^{-1}(\hat\mu_t - 1_N\hat\mu_{g,t}),$$

with $\hat\mu_{g,t} = 1_N'\hat\Sigma_t^{-1}\hat\mu_t/(1_N'\hat\Sigma_t^{-1}1_N)$. For a constant combining coefficient $\tilde c$ the paper considers

$$\hat w_t(\tilde c) = \hat w_{g,t} + \frac{\tilde c}{\gamma}\,\hat w_{z,t};$$

$\tilde c = 1$ is the plug-in rule. The expected out-of-sample utility $E[U(\hat w_t(\tilde c))]$ evaluates $U$ at the true $\mu$, $\Sigma$ and averages over the sample. The five random quantities $\mu_{g,t} = \hat w_{g,t}'\mu$, $\mu_{z,t} = \hat w_{z,t}'\mu$, $\sigma^2_{g,t} = \hat w_{g,t}'\Sigma\hat w_{g,t}$, $\sigma^2_{z,t} = \hat w_{z,t}'\Sigma\hat w_{z,t}$ and $\sigma_{gz,t} = \hat w_{g,t}'\Sigma\hat w_{z,t}$ determine it.

Formalization targets

Goal: the optimal combining coefficient (§2.3, eqs. (20)–(21))

For $N \ge 2$ and $h > N + 3$, with

$$k = \frac{(h-N)(h-N-3)}{h(h-2)}, \qquad \tilde c^* = \frac{k\psi^2}{\psi^2 + \frac{N-1}{h}},$$

the coefficient $\tilde c^*$ is the unique maximizer of $\tilde c \mapsto E[U(\hat w_t(\tilde c))]$ over $\mathbb R$, and $0 \le \tilde c^* < 1$, with $\tilde c^* > 0$ when $\psi^2 > 0$.

Lemma 1 (eq. (17))

For $h > N + 3$ and every constant $\tilde c$,

$$E[U(\hat w_t(\tilde c))] = \mu_g - \frac{\gamma(h-2)\sigma_g^2}{2(h-N-1)} + \frac{h}{\gamma(h-N-1)}\left[\tilde c\psi^2 - \frac{\tilde c^2(h-2)(h\psi^2+N-1)}{2(h-N)(h-N-3)}\right].$$

The moments (A9)–(A13) and the auxiliary moments

$$E[\mu_{g,t}] = \mu_g,\quad E[\mu_{z,t}] = \frac{h\psi^2}{h-N-1},\quad E[\sigma^2_{g,t}] = \frac{(h-2)\sigma_g^2}{h-N-1},$$ $$E[\sigma^2_{z,t}] = \frac{h(h-2)(h\psi^2+N-1)}{(h-N)(h-N-1)(h-N-3)},\quad E[\sigma_{gz,t}] = 0,$$

together with the first and second moments of the auxiliary variables $y_1$, $y_2$ of Proposition 1 that the proof of Lemma 1 uses.

Significance

The result gives a closed-form, implementable-in-principle correction to the plug-in rule: since $\tilde c^* < 1$, the investor should always under-weight the estimated zero-investment portfolio, by a factor that depends only on $h$, $N$ and $\psi^2$. Replacing $\psi^2$ by an adjusted estimator gives the paper's feasible rules (§2.4, §3), which are compared empirically in §4. The moment formulas (A9)–(A13) are of independent use: they give the exact out-of-sample mean and variance of the sample GMV and zero-investment portfolios, which recur in the shrinkage literature (for instance Lassance, Martín-Utrera and Simaan, 2024, who build on this paper's Proposition 1).

The result is proved in the paper, but the proof rests on Proposition 1, a stochastic representation of the out-of-sample moments whose detailed proof is in an online appendix. No machine-checked proof exists. On Prove2Me, Proposition 1 is posed (Open) as RiskEU.OOSUVar.kan_representation in Lassance et al.'s restatement, together with special cases (eq_IA60, eq_IA49) of the combinations $\mu_{g,t} + (\kappa/\gamma)\mu_{z,t}$ and of the portfolio variance for $\kappa \in [0, 1]$ and $h > N + 7$. The closed-form vertex of the quadratic (17) is already proved there (RiskEU.RobustShrink.proposition_IA_1_3). What this mission adds is the statement about the actual expectation over the Gaussian sample, for all real $\tilde c$, under the paper's own threshold $h > N + 3$, with uniqueness of the maximizer.

Difficulty

Once Lemma 1 is available, the goal is the vertex of a concave quadratic. The difficulty is Lemma 1 itself: computing expectations of quadratic forms in $\hat\Sigma_t^{-1}$ and in the normalized vector $\hat\Sigma_t^{-1}1_N/(1_N'\hat\Sigma_t^{-1}1_N)$. The weights are ratios of dependent random quantities, so linearity of expectation does not apply directly, and inverse-Wishart moment formulas alone do not cover the ratio in $\hat w_{g,t}$. The threshold $h > N + 3$ is Lemma 1's hypothesis; the factor $h-N-3$ in the denominator of (A12) shows that it is what keeps the expected variance of the estimated zero-investment portfolio finite, so integrability is part of the content.

Formalization scope

The model is the published definition RiskEU.OOSUVar.Setting: Market N carries $\mu$, $\Sigma$, $\gamma$; sigmaG2, muG, psi2, U, sampleMean, sampleCov (divided by $h$), wHatG, wHatZ and IsGaussianSample are the objects above (that setting calls the window $T$; here it is $h$). The auxiliary family of Proposition 1 and $y_1$, $y_2$ come from the published RiskEU.OOSUVar.KanRepresentation. The mission's own definitions (KanCombine.Optimal.Model) add the standing assumptions, the combining portfolio, the five sample moments, the expected utility, $k$ and $\tilde c^*$.

Conventions committed to:

• $N \ge 2$, $\Sigma \succ 0$ and $\gamma > 0$ are explicit hypotheses (implicit in the paper); $h > N + 3$ is Lemma 1's. The $y$-moment milestone also assumes $N > 3$, as Proposition 1 does.
• $\tilde c$ ranges over all of $\mathbb R$, and "the optimal value" is stated as a unique maximizer.
• Every expectation identity asserts integrability: a Lean Bochner integral of a non-integrable function is $0$.
• Lean's matrix inverse is $0$ on singular matrices; $\hat\Sigma_t$ is almost surely nonsingular for $h > N$, so this does not change any expectation.
• The page's "$0 < \tilde c^* < 1$" fails at $\psi^2 = 0$, where $\tilde c^* = 0$; the goal states $0 \le \tilde c^* < 1$ and $\tilde c^* > 0$ under $\psi^2 > 0$.

The goal is about the integral over the Gaussian sample. Stating it about the closed-form right-hand side of (17) would reduce it to the vertex of a quadratic, which is already proved, and is ruled out. The hypotheses are satisfiable: $N = 2$, $h = 6$, $\mu = (0, 1)$, $\Sigma = I$, $\gamma = 1$ meets them with the product Gaussian sample, and gives $\tilde c^* = 1/8$.

A complete development needs Wishart and inverse-Wishart theory (the Bartlett decomposition, moments of chi-squared ratios) and a formal version of Proposition 1. These are reusable well beyond this mission; contributions proving (A9)–(A13) by any route, including directly from inverse-Wishart moments, are welcome.

Selected references

• R. Kan, X. Wang and G. Zhou, Optimal portfolio choice with estimation risk: No risk-free asset case, Management Science 68(3), 2022 (cited from the submitted manuscript, November 2020). https://doi.org/10.1287/mnsc.2021.3989 ; https://ssrn.com/abstract=2819254
• R. Kan and G. Zhou, Optimal portfolio choice with parameter uncertainty, Journal of Financial and Quantitative Analysis 42(3), 2007. https://doi.org/10.1017/S0022109000004129
• H. Markowitz, Portfolio selection, Journal of Finance 7(1), 1952. https://doi.org/10.1111/j.1540-6261.1952.tb01525.x
• N. Lassance, A. Martín-Utrera and M. Simaan, The risk of expected utility under parameter uncertainty, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.00178
• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982. https://doi.org/10.1002/9780470316559

Motivation

Firms carry risks they cannot insure directly. A farmer's revenue depends on local yield and on local price; an airline's cost depends on jet fuel at a specific airport; an energy retailer's margin depends on load and on weather. Exchange-traded derivatives are written on standardized indices, so the exposure that matters is only partly claimable. Guiotto and Roncoroni (Operations Research 2022) study the design of a combined custom hedge: one over-the-counter claim written on the claimable part $X$ of the firm's risk, plus a second claim written on a side index $I$ that is correlated with the unclaimable part. The question is when such a pair is well defined, that is, when the firm's mean–variance hedging problem has one and only one optimal pair of claims.

Single-claim custom hedging goes back to Chowdhry and Howe (1999) and Caldentey and Haugh (2006; 2009, Operations Research 57(1)), whose framework prices claims through a pricing kernel $dQ/dP$ known to the firm; that framework is adopted here. With two claims on two different random elements the optimal pair is coupled, and existence and uniqueness are no longer automatic.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying three random elements, valued in arbitrary measurable spaces: the claimable term $X$, the nonclaimable term $Y$ and the side index $I$. Write $\mathcal F_X=\sigma(X)$ and $\mathcal F_I=\sigma(I)$. The firm's business position is $\pi=\pi(X,Y)$ for a Borel revenue function $\pi$, assumed square-integrable.

A claim on $X$ is a random variable $H$ that is $\mathcal F_X$-measurable and has finite variance; the set of such claims is $\mathcal H_X$, and $\mathcal H_I$ is defined likewise. The centered subspace $\mathbb H_X\subseteq\mathcal H_X$ consists of claims with $\mathbb E[H]=0$.

Claims are priced by a pricing kernel $dQ/dP$, the density of an equivalent martingale measure $Q$: it is positive almost surely, has mean one and is square-integrable, and $\mathbb E_Q[Z]=\mathbb E[Z\,dQ/dP]$. The firm ranks positions by the mean–variance criterion

$$\mathcal U(Z)=\varrho\,\mathbb E[Z]-\tfrac a2\operatorname{Var}[Z],\qquad \varrho\ge 0,\ a>0 .$$

The value-centered design problem is

$$\max\Big\{\mathcal U\big(\pi+[H+G]\big)\ :\ H\in\mathcal H_X,\ G\in\mathcal H_I,\ \mathbb E_Q[H]=\mathbb E_Q[G]=0\Big\}.\qquad(4)$$

A maximizer $(H^*,G^*)$ is an optimal combined claim pair. The dependence between $X$ and $I$ is measured by the maximal correlation

$$r_{XI}=\sup\big\{\rho(\phi,\psi)\ :\ \phi\in\mathbb H_X,\ \psi\in\mathbb H_I\big\}\in[0,1],\qquad(6)$$

with $\rho$ the Pearson correlation. Finally $\mathcal K=\pi+(\varrho/a)\,dQ/dP$ is the optimal hedging kernel, $\Pi^X_0=-\mathbb E\big[\mathcal K-\mathbb E[\mathcal K\mid\mathcal F_I]\mid\mathcal F_X\big]$, and $T[Z]=\mathbb E\big[\mathbb E[Z\mid\mathcal F_I]\mid\mathcal F_X\big]$.

Formalization targets

Goal: Theorem 1 (p. 11)

If $r_{XI}<1$, then

1. an optimal combined claim pair $(H^*,G^*)$ of (4) exists;
2. it is unique up to $P$-null sets, and so is the hedge $H^*+G^*$;
3. the value-centered optimal claim $H^*_0=H^*-\mathbb E[H^*]$ solves

$$H^*_0=\Pi^X_0+\mathbb E\big[\mathbb E[H^*_0\mid\mathcal F_I]\mid\mathcal F_X\big].\qquad(7)$$

Milestones

• Proposition 1 (p. 9): every optimal pair is $H^*=H^*_0-\mathbb E_Q[H^*_0]$, $G^*=G^*_0-\mathbb E_Q[G^*_0]$ with $P$-centered $(H^*_0,G^*_0)$ solving the first-order system (5).
• (EC.25)–(EC.26) (p. ec24): a centered solution of (5) satisfies $H_0=\Pi_0+T[H_0]$.
• $T$ on $\mathbb H_X$ (p. ec24): $\mathbb E[T[Z]]=\mathbb E[Z]$, $T(\mathbb H_X)\subseteq\mathbb H_X$, and $\Pi_0\in\mathbb H_X$.
• Inner-product bound (p. ec25): $\langle\mathbb E[\phi\mid\mathcal F_I],\psi\rangle\le r_{XI}\|\phi\|_2\|\psi\|_2$ for $\phi\in\mathbb H_X$, $\psi\in\mathbb H_I$.
• (EC.28) (p. ec25): $\|\mathbb E[\phi\mid\mathcal F_I]\|_2\le r_{XI}\|\phi\|_2$.
• $\|T\|\le r_{XI}$ (p. ec25) on $\mathbb H_X$.
• (EC.27) (p. ec25): if $r_{XI}<1$, $H_0=\Pi_0+T[H_0]$ has a unique solution in $\mathbb H_X$.

Significance

The result. Theorem 1 makes the combined hedge an object: without it the optimal pair may fail to exist or may be non-unique (the paper points to Appendix EC.1(F) for non-uniqueness), and the paper's later results, the design integral equation (Theorem 2) and the value of combining claims (Theorem 3 and Definitions 1–3), are stated for the optimal pair whose existence and uniqueness Theorem 1 provides. Equation (7) separates the optimal claim into a part determined by the kernel $\mathcal K$ alone and a cross-claim feedback through $I$. The condition $r_{XI}<1$ is checkable: for jointly lognormal $(X,I)$ it reduces to $|\rho_{Z,W}|<1$ for the underlying normals (Example 4).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof needs a Hilbert-space treatment of conditional expectations onto two σ-algebras, a formal maximal-correlation index, and an existence argument for the maximization problem itself, which the paper's proof leaves implicit (see below). The intermediate statements are general facts about pairs of σ-algebras with maximal correlation below one and are reusable outside hedging.

Difficulty

The optimal pair is coupled: the claim on $X$ depends on the conditional expectation of the claim on $I$ given $X$ and conversely, so neither can be computed first. When $X$ and $I$ share information, the two claim spaces overlap and the sum $\mathcal H_X+\mathcal H_I$ need not be closed in $L^2$; a maximizing sequence can then escape, and two different pairs can produce the same hedge. The condition $r_{XI}<1$ excludes this, and the work lies in turning it into a quantitative bound on the alternating conditional-expectation operator.

A second difficulty is a gap in the printed argument. The paper derives the first-order system (5) as a necessary condition and then proves that the resulting fixed-point equation has a unique solution. It does not show that the pair built from that solution is optimal for (4), so existence of a maximizer needs a separate argument that the first-order condition is also sufficient or that the maximum is attained. The goal is stated for maximizers of (4), so this step cannot be skipped.

Formalization scope

Everything lives in the namespace CustomHedge.Exist. A Market bundles $P$, $X$, $Y$, $I$, the revenue function, the kernel D $=dQ/dP$, rho $=\varrho$ and a; Standing collects the assumptions above. Conventions:

• Claims are random variables $\Omega\to\mathbb R$, strongly measurable for $\sigma(X)$ (resp. $\sigma(I)$) and in $L^2(P)$, not payoff functions $x\mapsto H(x)$.
• Optimality is maximization of U over all feasible pairs; uniqueness and the equations (5), (7), (EC.25), (EC.27) hold $P$-almost surely.
• $\mathbb E_Q$ centers the budget constraint; $\mathbb E=\mathbb E_P$ centers $H^*_0$, $\mathbb H_X$ and the maximal correlation.
• The paper allows $a\ge0$; the formalization requires $a>0$, because $\mathcal K$ divides by $a$ and with $a=0$ problem (4) generally has no maximizer. $\varrho=0$ is allowed.
• The maximal correlation is a real supremum over pairs with positive variances (where $\rho$ is defined), with $\sup\emptyset=0$; the set is bounded by one.
• $\|Z\|_2=(\mathbb E[Z^2])^{1/2}$; conditional expectation is Mathlib's condExp.

A trivializing formalization is ruled out: the goal quantifies over maximizers of (4), not over solutions of the first-order system or of (EC.27), which are separate milestones. A sorry-free check confirms the standing assumptions and $r_{XI}<1$ hold together with a non-trivial $\sigma(X)$.

Needed infrastructure: $L^2$ conditional expectation as an orthogonal projection, the identity $\mathbb E[\mathbb E[\phi\mid\mathcal G]\psi]=\mathbb E[\phi\psi]$ for $\mathcal G$-measurable $\psi$, Banach's fixed-point theorem on a closed subspace of $L^2$, and concave maximization over a closed affine subspace. The maximal-correlation file is reusable beyond this mission. Proofs of individual milestones, and a proof of the goal by any route, are welcome.

Selected references

• P. Guiotto and A. Roncoroni, Combined custom hedging: optimal design, noninsurable exposure, and operational risk management, Operations Research 70(3), 2022. https://doi.org/10.1287/opre.2021.2133 (cited from manuscript OPRE-2019-01-058.R3)
• R. Caldentey and M. Haugh, Optimal control and hedging of operations in the presence of financial markets, Mathematics of Operations Research 31(2), 2006. https://doi.org/10.1287/moor.1060.0193
• B. Chowdhry and J. T. B. Howe, Corporate risk management for multinational corporations: financial and operational hedging policies, European Finance Review 2, 229–246, 1999 (as cited in the paper; no link verified).
• A. Rényi, On measures of dependence, Acta Mathematica Academiae Scientiarum Hungarica 10, 1959. https://doi.org/10.1007/BF02024507
• B. Schweizer and E. F. Wolff, On nonparametric measures of dependence for random variables, Annals of Statistics 9(4), 1981. https://doi.org/10.1214/aos/1176345528

Motivation

Restaurants that take orders online promise each customer a pickup time when the order is placed. A static quote promises every customer the same lead time $\delta$, the form in common use. Once the promise is fixed, the kitchen still decides when to start each order. Starting too early means the food waits and cools (an earliness cost). Starting too late breaks the promise (a tardiness cost). Farahani, Dawande and Janakiraman (SSRN 3557605; published in Operations Research, 2022, doi:10.1287/opre.2021.2203) model this as a single-server queue and propose simple threshold policies. To judge those policies against the unknown optimum they need lower bounds on the optimal long-run average cost, and their first such bound is the subject of this mission.

The bound uses a clairvoyant relaxation: a decision maker who knows every future arrival and service time can do no worse than one who does not. Relaxations of this kind are standard for finite-horizon stochastic dynamic programs, where the relaxed problem is deterministic and its expected value can be estimated by Monte Carlo simulation (Brown, Smith and Sun, 2010, doi:10.1287/opre.1090.0796). Brown and Haugh (2017, doi:10.1287/opre.2017.1631) extended them to discounted infinite-horizon problems. The queue here is an undiscounted infinite-horizon problem: the clairvoyant problem involves an infinitely long sample path, which cannot be simulated directly. Theorem 4 of the paper resolves this by showing that the clairvoyant cost per customer over any finite number of customers is already a valid lower bound.

Setting

A probability space carries inter-arrival times $T_1, T_2, \dots$ and service times $x_1, x_2, \dots$. The $T_n$ are identically distributed with mean $1/\lambda$, the $x_n$ are identically distributed with mean $1/\mu$, the whole family is mutually independent, and $\lambda < \mu$ (the queue is stable). Customer $n \ge 1$ arrives at

$$t_n = T_1 + \cdots + T_n$$

and is due at $d_n = t_n + \delta$, where $\delta \ge 0$ is the quote time. The arrival rate is $\lambda = 1/\mathbb E[T_1]$.

A schedule assigns to each customer $n$ a service start time $y_n$, which may depend on the sample path. It is FCFS-feasible if on every sample path

$$y_n \ge t_n, \qquad y_{n+1} \ge y_n + x_n \qquad (n \ge 1).$$

Customer $n$ departs at $D_n = y_n + x_n$ and pays $g(D_n - d_n)$, where

$$g(\xi) = c_e(-\xi)^+ + c_d(\xi)^+, \qquad c_e, c_d \ge 0.$$

The long-run average cost of a schedule is (the paper's form (4))

$$C(y) = \lambda \limsup_{N \to \infty} \mathbb E\Big[\frac1N \sum_{n=1}^N g(y_n + x_n - d_n)\Big].$$

The perfectly-clairvoyant cost of customers $i, \dots, j$ on a sample path $\omega$ (program (12)) is

$$\gamma_{i:j}(\omega) = \inf_y \sum_{n=i}^j g(y_n + x_n - d_n) \quad \text{s.t.} \quad y_n \ge t_n \ (i \le n \le j), \quad y_{n+1} \ge y_n + x_n \ (i \le n < j).$$

In Lean these are StaticQuote.Clairvoyant.Model with Standing, rate, arrival, due, g, IsFCFSSchedule, cost, IsSchedule and gamma.

Formalization targets

Goal: Theorem 4 (p. 18)

For every FCFS-feasible schedule $y$ and every $N \ge 1$,

$$C(y) \ \ge\ \lambda\, \mathbb E\Big[\frac{\gamma_{1:N}(\omega)}{N}\Big].$$

The paper writes the left side as $C^{\pi^*}$, the optimal cost. The statement here holds for every schedule, so it covers the optimum whenever one exists.

Milestones (in the order of the printed proof, pp. 18–19)

1. Sample-path bound: $\gamma_{1:M}(\omega)/M \le \sum_{n=1}^M g(D_n - d_n)/M$ on every path.
2. (14): $\limsup_M \lambda\, \mathbb E[\gamma_{1:M}/M] \le C(y)$.
3. Superadditivity: $\gamma_{1:2N}(\omega) \ge \gamma_{1:N}(\omega) + \gamma_{N+1:2N}(\omega)$.
4. Block stationarity: $\mathbb E[\gamma_{1:N}] = \mathbb E[\gamma_{N+1:2N}]$.
5. Doubling: $\mathbb E[\gamma_{1:2N}] \ge 2\,\mathbb E[\gamma_{1:N}]$.
6. Dyadic bound: $k \mapsto \mathbb E[\gamma_{1:2^kN}/2^kN]$ is non-decreasing and $\mathbb E[\gamma_{1:N}/N] \le \limsup_k \mathbb E[\gamma_{1:2^kN}/2^kN]$.
7. (15): $\mathbb E[\gamma_{1:N}/N] \le \limsup_M \mathbb E[\gamma_{1:M}/M]$.

Significance

The result. Theorem 4 turns an infinite-horizon lower bound into a finite computation: for any $N$, the deterministic clairvoyant problem over $N$ customers can be solved on simulated sample paths, and the sample mean, scaled by $\lambda$, estimates a lower bound on the optimal long-run cost. The paper uses this bound, with its refinements (Theorems 5 and 6), to certify the numerical quality of its threshold policies (§7). Without it, the only available benchmark is the asymptotic clairvoyant cost, which cannot be computed.

Formalizing it. The paper proves the theorem with an informal argument. No machine-checked proof of this bound, or of the sample-path GI/G/1 objects it needs, is known to exist. The mission produces a sample-path model of a single-server queue with due dates, a clairvoyant value defined as an extended-real infimum, and the measure-theoretic step that the clairvoyant cost of a block of customers has the same expectation as that of the first block.

Difficulty

Most steps are monotonicity of integrals and of $\limsup$. The substantive step is block stationarity (milestone 4). $\gamma_{N+1:2N}$ and $\gamma_{1:N}$ are not functions of the same random variables, and $\gamma_{N+1:2N}$ depends on the absolute arrival times $t_{N+1}, \dots, t_{2N}$, which carry the whole history $T_1, \dots, T_N$. The equality of expectations needs the clairvoyant value to be expressed as a function of relative arrival times and service times only. It also needs that function to be measurable (it is an infimum over uncountably many schedules) and the joint law of a block of an i.i.d. family to be invariant under shifting the block. The doubling argument then has to pass from horizons $2^kN$ to all horizons $M$, which in the extended reals needs no integrability.

Formalization scope

• Source. The statements follow the SSRN author version of 2021-08-05 (abstract 3557605), whose page and equation numbers are cited throughout; the published article's numbering is not used.
• Indices start at $1$: $t_n = T_1 + \cdots + T_n$; the coordinates $T_0, x_0$ are unused and carry no hypothesis. $N \ge 1$ in the goal, in the dyadic bound and in (15) (the paper's $\mathbb N$ starts at $1$; the ratios are $0/0$ at $N = 0$).
• Sample paths. The outcome $\omega$ is the full sample path of inter-arrival and service times; the page calls it "a sample path of inter-arrival times" on p. 18 and "of inter-arrival and service times" on p. 19.
• Policy class. The paper's admissible, FCFS and Loynes stable policy classes are not modelled. The Loynes class asks for $L^1$ convergence of the waiting times $W^\pi_n$. For a nondegenerate GI/G/1 queue these converge only in law, so the class may be empty, and an infimum over it would be vacuous. Every statement instead quantifies over all schedules that are FCFS-feasible on every sample path. That class contains every policy the paper considers, so the statements imply the paper's. No measurability or adaptedness of $y$ is required: the bound holds without it.
• Cost. $C(y)$ is defined by the per-customer form (4), not by the calendar-time form (1); the paper passes from (1) to (4) by citing Whitt (1991), and the proof of Theorem 4 uses (4) only.
• Extended reals. $\gamma$ is an infimum in $[0, \infty]$ (the page writes $\min$, which is attained but not proved to be). Costs, expectations (lower Lebesgue integrals) and $\limsup$s are in $[0, \infty]$. Each cost term is $\max(g, 0)$, which is exact because $g \ge 0$.
• Standing assumptions. The paper leaves some conditions implicit; they are made explicit: durations are nonnegative almost surely, $\delta, c_e, c_d \ge 0$, and "mean $1/\lambda$, mean $1/\mu$" means $0 < \mathbb E[T_1] < \infty$ and $0 < \mathbb E[x_1] < \infty$. Stability $\lambda < \mu$ ($\mathbb E[x_1] < \mathbb E[T_1]$) is kept as the paper's standing assumption although Theorem 4 does not use it. A one-point model ($T \equiv 1$, $x \equiv 1/2$, $\delta = c_e = c_d = 1$) satisfies all of them and has finite $\gamma_{1:N}$.
• Ruled out. A real-valued $\gamma$, cost, expectation or $\limsup$ (junk value $0$ on unbounded or non-integrable input); a policy class that may be empty; dropping the i.i.d. or independence hypotheses (milestone 4 and the goal fail without them); $N = 0$; and $\lambda$ as a free parameter (it is $1/\mathbb E[T_1]$).
• Infrastructure. A complete development needs measurability of the clairvoyant value, invariance of block laws for i.i.d. families, and the comparison of a $\limsup$ along a subsequence with the full $\limsup$ in $[0, \infty]$. The block-law invariance and the sample-path queue model can be reused in other missions. Proofs of any milestone, and lemmas towards milestone 4, are welcome.

Selected references

• M. H. Farahani, M. Dawande, G. Janakiraman, Order Now, Pickup in 30 Minutes: Managing Queues with Static Delivery Guarantees, SSRN 3557605, version of 2021-08-05; published in Operations Research, 2022. https://ssrn.com/abstract=3557605, https://doi.org/10.1287/opre.2021.2203
• D. B. Brown, J. E. Smith, P. Sun, Information relaxations and duality in stochastic dynamic programs, Operations Research 58(4), 785–801, 2010. https://doi.org/10.1287/opre.1090.0796
• D. B. Brown, M. B. Haugh, Information relaxation bounds for infinite horizon Markov decision processes, Operations Research 65(5), 1355–1379, 2017. https://doi.org/10.1287/opre.2017.1631
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036094
• W. Whitt, A review of L = λW and extensions, Queueing Systems 9(3), 235–268, 1991. https://doi.org/10.1007/BF01158466

Motivation

Optimal stopping asks when to halt a stochastic process so as to maximize an expected reward. Examples are exercising an American option, selling an asset, or ending a clinical trial. The optimal policy is the solution of a dynamic program over the whole state space. In high dimension it cannot be computed exactly, and the usual approximations (regression on basis functions, as in Longstaff–Schwartz) produce policies that are hard to read: a decision maker cannot see why the policy stops in a given state.

Ciocan and Mišić (Interpretable Optimal Stopping, Management Science 2022; arXiv:1812.07211) propose to restrict the search to tree policies. These are binary decision trees whose split nodes compare one state variable with a threshold and whose leaves say stop or go. The tree is fitted by maximizing the average reward over a finite set of simulated trajectories, which is a sample average approximation (SAA) of the true problem. This mission formalizes the consistency guarantee that justifies the method: as the number of trajectories grows, the optimal SAA value over trees of bounded depth converges almost surely to the optimal true value over the same trees.

Setting

The state of the system is a vector $\mathbf x\in\mathcal X=\mathcal X_1\times\cdots\times\mathcal X_n\subseteq\mathbb R^n$. The process $\mathbf x(1),\dots,\mathbf x(T)$ runs for $T$ periods and starts at a fixed state $\mathbf x(1)=\bar{\mathbf x}$. Stopping in period $t$ in state $\mathbf x$ pays $g(t,\mathbf x)$, and rewards are discounted by a factor $\beta\in[0,1]$ per period.

A stationary policy is a map $\pi:\mathcal X\to\{\mathbf{stop},\mathbf{go}\}$. Its stopping time on a path is $\tau_\pi=\min\{t:\pi(\mathbf x(t))=\mathbf{stop}\}$, and $\tau_\pi=+\infty$ if the policy never stops. Its value is

$$J^\pi(\bar{\mathbf x})=\mathbb E\big[\beta^{\tau_\pi-1}g(\tau_\pi,\mathbf x(\tau_\pi))\big],$$

where a path on which $\pi$ never stops earns $0$. Given trajectories $\mathbf x(\omega,\cdot)$ for $\omega=1,\dots,\Omega$, the sample-average value $\hat J^\pi(\bar{\mathbf x})$ is the average of the same discounted reward over the $\Omega$ trajectories.

A tree policy $\pi(\cdot;\mathcal T,\mathbf v,\boldsymbol\theta,\mathbf a)$ is given by four things:

• a binary tree topology $\mathcal T$;
• for each split node $s$, a split variable index $v(s)$;
• for each split node $s$, a real split point $\theta_s$;
• for each leaf $\ell$, an action $a(\ell)$.

A state descends to the left child of $s$ when $x_{v(s)}\le\theta_s$ and to the right child otherwise, and receives the action of the leaf it reaches. $\Pi_{\mathrm{tree}}(d)$ is the class of tree policies of depth at most $d$. Once $d$ is fixed, the skeletons $(\mathcal T,\mathbf v,\mathbf a)$ form a finite set, but the split points $\boldsymbol\theta\in\mathbb R^{\mathbf{splits}}$ range over a continuum.

The paper's standing assumptions are:

1. Assumption 1: $\mathcal X$ is totally bounded and $\|\mathbf x-\mathbf y\|_\infty\le1$ on $\mathcal X$.
2. Assumption 2: $0\le g(t,\mathbf x)\le G$ for all $t$ and $\mathbf x\in\mathcal X$.
3. Assumption 3: there is a function $f$, strictly increasing and continuous with $f(0)=0$, such that $\Pr[\mathbf x(t)\in A]\le f(\lambda(A))$ for every period $1<t\le T$, where $\lambda$ is Lebesgue measure.

Formalization targets

Goal: Corollary 1 (p. 10)

Fix a depth $d$ and $\epsilon>0$. With probability one there is a finite $\Omega_0$ such that for all $\Omega\ge\Omega_0$,

$$\Big|\sup_{\pi\in\Pi_{\mathrm{tree}}(d)}J^\pi(\bar{\mathbf x})-\sup_{\pi\in\Pi_{\mathrm{tree}}(d)}\hat J^\pi(\bar{\mathbf x})\Big|\le\epsilon.$$

This is the paper's headline consistency result: the optimal SAA value converges almost surely to the optimal tree-policy value.

Milestones

1. Slab bound (proof of Lemma EC.2, p. ec3): $\Pr[x_{v(s)}(t)\in[\min\{\theta_{1s},\theta_{2s}\},\max\{\theta_{1s},\theta_{2s}\}]]\le f(|\theta_{1s}-\theta_{2s}|)$ for $t>1$.
2. Lemma EC.2: if two split-point vectors give the same skeleton and both continue at $\bar{\mathbf x}$, then $|J^{\pi_{\boldsymbol\theta_1}}-J^{\pi_{\boldsymbol\theta_2}}|\le GT\sum_{s}f(|\theta_{1,s}-\theta_{2,s}|)$.
3. Lemma EC.3: the deterministic sample analogue, $|\hat J^{\pi_{\boldsymbol\theta_1}}-\hat J^{\pi_{\boldsymbol\theta_2}}|\le\frac G\Omega\sum_\omega\sum_{t\ne1}\sum_s\mathbb I\{x_{v(s)}(\omega,t)\in\text{slab}_s\}$.
4. Fixed-policy strong law (EC.1.1, p. ec1): for one tree policy, $\hat J^\pi\to J^\pi$ almost surely.
5. Lemma EC.1: for one skeleton, almost surely $\sup_{\boldsymbol\theta}|J^{\pi_{\boldsymbol\theta}}-\hat J^{\pi_{\boldsymbol\theta}}|\le\epsilon$ for all large $\Omega$.
6. Theorem 1 (p. 10): the same, uniformly over all of $\Pi_{\mathrm{tree}}(d)$.

Significance

Corollary 1 is what makes the SAA tree-fitting procedure a consistent estimator of the best interpretable policy. A decision maker who optimizes a depth-$d$ tree on enough simulated trajectories obtains an in-sample value that approximates, to any precision, the true value achievable by depth-$d$ trees. The paper also shows (Section EC.1.2) that the conclusion fails when the depth is unbounded, so the depth restriction is part of the result and not a convenience. Theorem 1, the uniform law behind it, has its own uses: it also controls the out-of-sample value of the SAA-optimal tree.

The results are proved in the paper's electronic companion. To our knowledge they have no machine-checked proof. Formalizing them yields a reusable model of finite-horizon stopping with stationary policies and decision-tree policies, and a uniform strong law for a class of indicator-type functionals that is discontinuous in its parameters. The latter is a pattern that recurs in empirical-risk results for trees and threshold rules.

Difficulty

The strong law gives convergence for one policy at a time, outside a null set that depends on the policy. Uncountably many split points mean uncountably many null sets, so the pointwise law does not yield Theorem 1. The usual fix, a Lipschitz or continuity argument in the parameter, fails because $\hat J^\pi$ is a step function of $\boldsymbol\theta$: moving one threshold past a sampled state changes a decision and the sample value jumps. The jumps of the true value must instead be controlled by the probability that the process visits the thin slab between two thresholds, which is where Assumption 3 enters. The jumps of the sample value must be controlled by the empirical frequency of such visits, uniformly in the thresholds. The first period is excluded throughout, because $\mathbf x(1)=\bar{\mathbf x}$ is deterministic and Assumption 3 does not apply to it.

Formalization scope

• States and paths. States are Fin n → ℝ, whose Mathlib norm is the sup norm $\|\cdot\|_\infty$. Paths are Fin T → (Fin n → ℝ), and periods are 0-indexed (k : Fin T is period $t=k+1$, so $\beta^{\tau-1}$ is β ^ k).
• The process. The process is its path law μ, a probability measure, with $\mathbf x(1)=\bar{\mathbf x}$ and $\mathbf x(t)\in\mathcal X$ almost surely.
• Rewards. $\beta\in[0,1]$ and the rewards g k are measurable. Both are readings of "discounted" and of the expectation on the page.
• The sample. The sample is an i.i.d. sequence of random paths with law μ, measurable and mutually independent (iIndepFun). The page says only "trajectories of the process" and its proofs use the strong law. $\hat J$ averages the first m samples, and "with probability one" is ∀ᵐ.
• Assumption 3. It is imposed on measurable sets of finite Lebesgue measure. The printed codomain $f:[0,\infty)\to[0,1]$ is dropped. As printed, the assumption cannot hold for $n\ge1$, $T\ge2$: a box containing $\mathcal X$ has probability $1$, which forces $f\equiv1$ on a half-line. Dropping the codomain costs nothing, because $r\mapsto f(r)+r$ converts any admissible $[0,1]$-valued $f$.
• Trees. A tree is an inductive skeleton with split variables Fin n and leaf actions. Split points are a function of the node address. A split sends ties left ($x_i\le\theta$). A leaf has depth $0$. $\Pi_{\mathrm{tree}}(d)$ is the type of (skeleton of depth $\le d$, split points), and the suprema in Corollary 1 are real suprema over it. They are genuine suprema because the type is nonempty and the values are bounded in $[0,G]$ (for $\hat J$, almost surely).
• Readings of the lemmas. Lemma EC.2 carries Assumption 1, which its proof uses, although its statement names only Assumptions 2 and 3. The page's "$\boldsymbol\theta\in\mathcal X$" in Lemmas EC.1–EC.3 is read as $\boldsymbol\theta\in\mathbb R^{\mathbf{splits}}$, the stronger statement.

The statements cannot be met by a degenerate policy class or a junk value. $J$ is the expectation under the true law, $\hat J$ the average over i.i.d. trajectories, and the suprema range over every tree of depth at most $d$ with arbitrary real split points. The hypotheses are jointly satisfiable with a nonconstant reward and a split that changes the action. One example is $n=1$, $T=2$, $\mathcal X=[0,1]$, $\mathbf x(2)$ uniform, $g(t,x)=x$ and $f(r)=r$.

A complete development needs:

• measurability of the reward of a tree policy;
• integrability from boundedness;
• the Lebesgue measure of product boxes;
• finiteness of the set of skeletons of bounded depth;
• a covering argument for the bounded range of split points;
• Mathlib's strong_law_ae.

Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 through Glivenko–Cantelli or VC-type arguments.

Selected references

• D. F. Ciocan and V. V. Mišić, Interpretable Optimal Stopping, Management Science, 2022. Preprint arXiv:1812.07211v2. https://arxiv.org/abs/1812.07211
• F. A. Longstaff and E. S. Schwartz, Valuing American Options by Simulation: A Simple Least-Squares Approach, Review of Financial Studies 14(1), 2001. https://doi.org/10.1093/rfs/14.1.113
• A. J. Kleywegt, A. Shapiro and T. Homem-de-Mello, The Sample Average Approximation Method for Stochastic Discrete Optimization, SIAM Journal on Optimization 12(2), 2002. https://doi.org/10.1137/S1052623499363220

Motivation

Emergency departments (EDs) are crowded in part by patients whose condition could have been treated by a primary care provider (PCP), while other patients first visit a PCP, are found to be critical, and are sent on to the ED, paying for two visits. Teletriage — a nurse telephone line that assesses symptoms and recommends where to seek care — is widely offered by health systems and insurers as a remedy for both. It is not error-free: a nurse can undertriage a critical patient (advise primary care) or overtriage a sick one (advise the ED). Whether such an imperfect advisor reduces ED usage, or merely sends more worried-but-well patients to the ED, is the question this mission formalizes.

Çakıcı and Mills (M&SOM, 2020; accepted manuscript at SSRN 2849635) model a patient who does not know whether she is merely sick or critical, chooses between the PCP, the ED and a teletriage call, and updates her belief after the call. Their Proposition 3 answers the question in closed form when every patient calls: teletriage reduces ED usage exactly when the overtriage rate is below an explicit threshold, and reduces double-dipping exactly when the undertriage rate is below another.

Setting

A patient is in one of two states, sick ($S$) or critical ($C$), and holds a belief $b\in[0,1]$, the probability that she is critical. Three actions are available.

• PCP: copay $c_P$. A critical patient seen at the PCP is sent on to the ED, so she also pays $c_E$; this is double-dipping. The expected cost is $c_P+b\,c_E$.
• ED: copay $c_E$, which ends the episode.
• Teletriage (TT): copay $c_T$. The line predicts sick (PS) or critical (PC) with undertriage rate $\alpha=\Pr(PS\mid C)$ and overtriage rate $\beta=\Pr(PC\mid S)$. The patient updates her belief by Bayes' rule to $b_{PS}=\alpha b/(\alpha b+(1-\beta)(1-b))$ or $b_{PC}=(1-\alpha)b/((1-\alpha)b+\beta(1-b))$, and then takes the better of PCP and ED at her posterior. She cannot call twice.

Without teletriage the patient's cost is $V_0(b)=\min\{c_E,\,c_P+b\,c_E\}$, minimized by the ED exactly when $b\ge b_0=1-c_P/c_E$. With teletriage it is

$$\tilde V_0(b)=\min\bigl\{c_E,\;c_P+b\,c_E,\;c_T+(\alpha b+(1-\beta)(1-b))V_0(b_{PS})+((1-\alpha)b+\beta(1-b))V_0(b_{PC})\bigr\}.$$

Teletriage is informative when $\alpha+\beta<1$. Proposition 2 of the paper identifies an interval where calling is strictly optimal, bounded by two thresholds

$$\underline b_0=\frac{\beta b_0+\frac{c_T}{c_P}(1-b_0)}{\beta b_0+(1-\alpha)(1-b_0)},\qquad \bar b_0=\frac{(1-\beta)b_0-\frac{c_T}{c_P}(1-b_0)}{(1-\beta)b_0+\alpha(1-b_0)}.$$

Write $\pi^{ED}(b)$ and $\pi^{DD}(b)$ for the probabilities that a patient with belief $b$ who acts optimally ends up at the ED, resp. double-dips, without teletriage, and $\tilde\pi^{ED}(b)$, $\tilde\pi^{DD}(b)$ with it. When beliefs are uniform on $[l,u]$, the population rates are the averages $\pi^{ED}=\frac1{u-l}\int_l^u\pi^{ED}(s)\,ds$, and likewise for the others.

Formalization targets

Goal: Proposition 3

Assume informative teletriage, beliefs uniform on $[l,u]\subseteq[0,1]$, and $\underline b_0<l<b_0<u<\bar b_0$: with teletriage everyone calls, and without it some patients go to the PCP and some to the ED. Then

$$\pi^{ED}-\tilde\pi^{ED}>0\iff\beta<\beta^0=\frac{u-\frac{u^2}{2}-\bigl(b_0-\frac{b_0^2}{2}\bigr)}{u-\frac{u^2}{2}-\bigl(l-\frac{l^2}{2}\bigr)},\qquad \pi^{DD}-\tilde\pi^{DD}>0\iff\alpha<\alpha^0=\frac{b_0^2-l^2}{u^2-l^2}.$$

Milestones

1. The no-teletriage threshold at $b_0$ (§4.1).
2. Proposition 1, informative case: $b_{PS}<b<b_{PC}$ for $0<b<1$, $\alpha+\beta<1$.
3. Steps of the proof of Proposition 2: the auxiliary thresholds $\underline{\underline b}_0\le\underline b_0$, $\bar b_0\le\bar{\bar b}_0$ and where the posteriors fall; the cost of calling outside $(\underline{\underline b}_0,\bar{\bar b}_0)$; the two linear comparisons inside it.
4. Proposition 2.
5. The closed forms of $\pi^{ED},\pi^{DD}$ and $\tilde\pi^{ED},\tilde\pi^{DD}$ (display on p. 11).
6. The closed forms of $\pi^{ED}-\tilde\pi^{ED}$ and $\pi^{DD}-\tilde\pi^{DD}$ (proof of Proposition 3).

Significance

The result separates the two failure modes of a triage line. Overtriage alone governs whether ED visits fall, and undertriage alone governs whether double-dipping falls, with thresholds that depend only on the copays (through $b_0$) and the belief range. A health system can therefore read off, for a given patient population, the overtriage rate a teletriage service must achieve before it relieves the ED. In the paper's example ($c_E=5c_P$, beliefs uniform on $[0.15,0.85]$), $\beta^0=0.025$: with an overtriage rate of 2.5% or more, teletriage does not reduce ED usage even though every patient calls.

The result is proved in the paper; no machine-checked version exists. Formalizing it means checking the full chain from the patient's optimization to the population averages: that the argmin of $\tilde V_0$ produces the threshold structure of Proposition 2 with the stated thresholds, that the per-belief probabilities on p. 11 follow from the optimal actions (including the boundary cases the page leaves implicit), and that the integrals evaluate as claimed. Two printing slips in the proofs (a right-hand side $c_P+b_{PS}c_E$ for $c_P+b\,c_E$, and a denominator $u-l-(\frac{u^2}2+\frac{l^2}2)$ for $u-l-(\frac{u^2}2-\frac{l^2}2)$) are corrected in the milestone statements.

Difficulty

The final integrals are elementary once the integrands are known. The work is in the integrands. $\tilde\pi^{ED}(b)$ is not given; it comes from which of three costs is smallest at $b$, and, for a caller, which provider is chosen at each of two posteriors that are rational functions of $b$. On the calling range the patient must go to the PCP after the prediction sick and to the ED after critical, i.e. $b_{PS}<b_0<b_{PC}$, and this is what makes $\tilde\pi^{ED}(b)=b+\beta(1-b)$. That in turn needs the inequalities $\underline{\underline b}_0\le\underline b_0$ and $\bar b_0\le\bar{\bar b}_0$, which use $c_T\ge0$ and informativeness, and the linearization of the teletriage cost in the middle range. Reading $\tilde\pi^{ED}$ off the display on p. 11 skips exactly this argument.

Formalization scope

Everything lives in the namespace Teletriage.OneShot and in ℝ. A single definition file holds the parameters $(c_P,c_E,c_T,\alpha,\beta)$, the standing assumptions, the posteriors, the costs, the optimal actions, the probabilities, the uniform average and all thresholds.

Conventions:

• Standing assumptions $0<c_P<c_E$, $0\le c_T$, $\alpha,\beta\in[0,1]$. The first three are added. The thresholds divide by $c_P$; $c_P<c_E$ is stated only in passing (p. 12) and makes $b_0\in(0,1)$; $c_T$ is a copayment, and with $c_T<0$ the display of $\tilde\pi^{ED}$ is false. Informativeness $\alpha+\beta<1$ is a separate hypothesis, inherited by Proposition 3 from Proposition 2.
• Ties in the argmin are broken ED ≻ teletriage ≻ PCP (and ED over PCP without teletriage), matching the displays on p. 11. Proposition 2 is stated in its strict open-region reading: at $c_T=0$ teletriage ties the PCP at low beliefs, so the page's "if and only if" at the endpoints is false under any tie rule.
• Probabilities are computed from the optimal actions, never defined by the closed forms on p. 11. Defining $\tilde\pi^{ED}$ or $\tilde\pi^{DD}$ by those displays, or the teletriage cost by its middle-range linear form, would make the goal a calculus exercise and is ruled out.
• Averages are $\frac1{u-l}\int_l^u g$, the paper's $\int_0^1 g f$ with the Uniform$[l,u]$ density. No integrability hypotheses are added: the integrands are piecewise linear, and proving their integrability is part of the work.
• Lean's division returns $0$ on a zero denominator. The posteriors are only used multiplied by the probability of their prediction, so a junk value never enters a cost or a probability.

Not in scope: the traditional-access model (Propositions 4–5), the open- vs traditional-access comparisons (Propositions 6–7, Corollaries 1–2), the sequential POMDP (Lemma 1, Propositions 8–9), and the uninformative cases of Proposition 1.

Welcome contributions: proofs of the milestones in any order. The algebra of milestones 3–4 is self-contained and reusable for the traditional-access analogue (Proposition 4).

Selected references

• Ö. E. Çakıcı and A. F. Mills, On the Role of Teletriage in Healthcare Demand Management, Manufacturing & Service Operations Management, 2020. https://doi.org/10.1287/msom.2020.0908 (accepted manuscript: https://ssrn.com/abstract=2849635)
• T. Ayer, O. Alagoz and N. K. Stout, OR Forum—A POMDP Approach to Personalize Mammography Screening Decisions, Operations Research 60(5), 2012. https://doi.org/10.1287/opre.1110.1019

Motivation

Loot boxes are a selling format for virtual items in video games and digital collectibles: the customer pays a fixed price for a box whose content is a random item from a catalog. They generate a large share of revenue in the game industry and have drawn regulatory attention because the customer does not know what they are buying. From the seller's side they are a form of probabilistic selling, close to bundling: a box is a lottery over the catalog, and repeated purchases let a customer assemble a collection.

Chen, Elmachtoub, Hamilton and Lei (Loot Box Pricing and Design, Management Science 2021; the mission follows the authors' manuscript submitted in August 2019) compare two designs. A unique box never repeats an item the customer owns; a traditional box draws uniformly from the whole catalog, so duplicates occur. Their headline asymptotic results are that, as the catalog grows, the optimal unique box earns the mean valuation $\mu$ per item, as much as the grand bundle (Theorem 2), while the optimal traditional box earns exactly a fraction $1/e$ of it (Theorem 3). This mission formalizes the traditional-box result.

Setting

A monopolist sells $N \ge 1$ distinct virtual items. A customer's valuations $V_1, \dots, V_N$ are i.i.d. with a law $F$ on $[0,\infty)$ with mean $\mu$ and finite variance $\sigma^2$. A second copy of an item is worth nothing.

The seller offers a traditional box at a fixed price $p > 0$ in every period. Each box contains an item drawn uniformly at random from $[N]$, independently of the valuations and of earlier draws. Let $S_t$ be the set of distinct items owned before the $t$-th box, so $S_1 = \emptyset$. The expected utility of the $t$-th box is

$$U_t = \frac{1}{N}\sum_{i \in [N]\setminus S_t} V_i \;-\; p .$$

The customer is myopic: they buy the $t$-th box if and only if $U_t \ge 0$, and the first time $U_t < 0$ they leave for good. The normalized revenue at price $p$ and the optimal normalized revenue are

$$R_{TB}(p) = \frac{p \cdot \mathbb E[\#\text{ of traditional box purchases}]}{N}, \qquad R_{TB} = \sup_{p>0} R_{TB}(p).$$

The milestones use a random walk. For i.i.d. $w_0, w_1, \dots$ with law $F$, the first passage above a level $t$ is $r(t) = \inf\{j \ge 1 : t \le w_0 + \dots + w_{j-1}\}$; the paper's $r_N$ is $r(Np)$. Also $\zeta_N = \sum_{i=1}^N 1/i - \log N - \gamma$, where $\gamma$ is the Euler–Mascheroni constant.

Formalization targets

Goal: Theorem 3, the limit clause (p. 13)

$$\lim_{N\to\infty} R_{TB} = \frac{\mu}{e}.$$

It holds for every valuation law in the model, with no condition on the shape of $F$ beyond non-negativity and a finite variance.

Milestones (proof of Theorem 3, pp. 33–34)

1. Eq. (16), index corrected. The revenue identity $R_{TB}(p) = p\,\mathbb E\big[\sum_{k=r_N}^{N} 1/k\big]$.
2. Eq. (17). $\frac{Np}{\mu} \le \mathbb E[r_N] \le \frac{Np}{\mu} + 1 + \frac{\sigma^2}{\mu^2}$ when $\mu > 0$.
3. Eq. (21). $R_{TB}(\mu/e) \ge \frac{\mu}{e}\log\Big(1\big/\big(\frac1e + \frac{1+\sigma^2/\mu^2}{N}\big)\Big)$, the finite-$N$ lower bound of Theorem 3 at an explicit price.
4. Eq. (22). $\mathbb P\big(r_N \le (1-\epsilon)Np/\mu\big) \le \sigma^2\big/\big(\frac{\epsilon^2}{1-\epsilon}Np\mu\big)$ for $0<\epsilon<1$.
5. Eqs. (24)–(26), corrected. For $0 < \epsilon < 1$,

$$R_{TB} \le \frac{\mu e^{\zeta_N-1}}{1-\epsilon} + \frac{\mu}{(1-\epsilon)N} + \frac{(1-\epsilon)\sigma^2(1+\log N)}{\epsilon^2\mu N},$$

whose right-hand side tends to $\mu/e$ when $\epsilon = N^{-1/3}$.

Significance

The result. Theorem 3 quantifies the price of duplicates. A traditional box loses a factor $e$ against the unique box, the grand bundle and the upper bound $\mu$ of the paper's Proposition 1, for every valuation distribution, so in large catalogs the unique box earns about $0.63\mu$ more per item. The constant $1/e$ comes from the interplay between the coupon-collector waiting times $N/(N-j)$ and the price at which the myopic customer stops; the identity and the bounds expose that interplay as a statement about the first passage of a random walk.

Formalizing it. The result is proved on paper, not formalized. Two of the printed steps of the proof need repair: the harmonic-number rewriting in (16) drops one term, and the per-price upper bound (25) derived from it is false at small prices (for $V \equiv 1$, $N = 1000$, $p = 1/N$ the revenue is $\approx 0.007485$ while (25) gives $\approx 0.007014$); its maximization also ignores prices above $\mu/(1-\epsilon)$. The milestones state the corrected claims, and the limit survives. A machine-checked proof therefore settles the headline result independently of the printed argument.

Difficulty

The number of boxes a myopic customer buys depends on all valuations and on the random order in which distinct items arrive, and the index at which the customer stops is not a stopping time of the forward purchase process: whether the customer continues depends on valuations of items not yet collected. Applying Wald-type identities directly to the purchase sequence therefore fails. The revenue identity (16) also mixes two sources of randomness, the coupon-collector waiting times and the values in order of collection, whose independence must be established rather than assumed. On the upper side, the expected first-passage index needs an overshoot bound for renewal processes (Lorden's inequality), which Mathlib does not contain, and the limit needs an upper bound that is uniform over all prices, including prices far above $\mu$ where the per-price estimate of the paper breaks down.

Formalization scope

All declarations live in the namespace LootBox.TB. The valuation law is a probability measure F : Measure ℝ with F (Set.Iio 0) = 0 and MemLp id 2 F; $\mu$ is ∫ x, x ∂F and $\sigma^2$ the centred second moment. The sample space for $N$ items is valuations × draws, (Fin N → ℝ) × (ℕ → Fin N), with the product of Measure.pi of $F$ and Measure.infinitePi of the uniform law on Fin N; draw $t$ is the item of the $(t+1)$-th box. The purchase count is the first $t$ with $U_{t+1}<0$, valued in ℕ∞; expectations are lower Lebesgue integrals and revenues live in ℝ≥0∞, so no expectation is truncated by toReal. The paper's $\max_p$ is a supremum over $p > 0$. The goal is indexed by $N = n + 1$ so that the uniform law is defined. The page's backward walk $C_j$, extended by virtual i.i.d. variables, is represented by the partial sums of an i.i.d. sequence under walkLaw F = Measure.infinitePi (fun _ => F).

The hypothesis $\mu > 0$ appears in the milestones that divide by $\mu$, not in the goal: when $\mu = 0$ nothing is bought and both sides of the limit are $0$. A formalization in which revenue is a real number obtained by toReal, or in which prices may be $0$ (where a customer with zero valuations buys forever), could make bounds vacuous; neither is used here.

A complete development needs the coupon-collector decomposition of the purchase count, the exchangeability of the values in order of collection, Wald's identity and Lorden's overshoot bound for i.i.d. non-negative walks, Chebyshev's inequality (meas_ge_le_variance_div_sq), Jensen's inequality for $-\log$, and the bounds $\log(n+1) \le H_n \le 1 + \log n$ and $\zeta_N \to 0$ (Mathlib's NumberTheory/Harmonic). Wald's identity and Lorden's bound are reusable well beyond this mission. Proofs of individual milestones, and of the renewal-theoretic lemmas they need, are welcome.

Selected references

• N. Chen, A. N. Elmachtoub, M. L. Hamilton, X. Lei, Loot Box Pricing and Design, Management Science 67(8), 2021. https://doi.org/10.1287/mnsc.2020.3748
• G. Lorden, On excess over the boundary, Annals of Mathematical Statistics 41(2), 1970. https://doi.org/10.1214/aoms/1177697092
• Y. Bakos, E. Brynjolfsson, Bundling Information Goods: Pricing, Profits, and Efficiency, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1613
• A. Gut, Stopped Random Walks: Limit Theorems and Applications, 2nd ed., Springer, 2009. https://doi.org/10.1007/978-0-387-87835-5