Operations Research

Motivation

Distributionally robust optimization (DRO) guards a data-driven decision against misspecification of the model that generated the data. In its penalized form, the decision maker replaces the sample-average problem $\max_x \mathbb E_{\mathbb P_n}[f(x,Y)]$, where $\mathbb P_n$ is the empirical distribution of the data $Y_1,\dots,Y_n$, by

$$\max_x\ \min_{\mathbb Q}\Big\{\mathbb E_{\mathbb Q}[f(x,Y)]+\frac1\delta\,\mathcal H_\phi(\mathbb Q\,|\,\mathbb P_n)\Big\},$$

where $\mathcal H_\phi$ is a $\phi$-divergence and $\delta\ge0$ controls how far an adversary may move the distribution. Such models are used in operations research, statistics and machine learning (Ben-Tal et al. 2013; Lam 2016; Duchi and Namkoong 2019), and a practitioner must choose $\delta$. Gotoh, Kim and Lim (arXiv:1711.06565, Operations Research 2021) study this calibration problem. Their first contribution, on which the rest of the paper builds, is an exact description of what the robust model penalizes for small $\delta$: the worst-case loss of expected reward is, to first order, the variance of the reward divided by the curvature $\phi''(1)$ of the divergence. This mission formalizes that theorem (Theorem 2.2) together with its proof chain in Appendix F.

Setting

A decision $x$ is fixed throughout, so the data enter only through the reward vector $f=(f_1,\dots,f_n)$ with $f_i=f(x,Y_i)$. The nominal distribution is a probability vector $\mathbb P_n=(p_1,\dots,p_n)$ with every $p_i>0$; the empirical distribution of distinct data points is $p_i=1/n$. Write

$$\mathbb E_{\mathbb P_n}[f]=\sum_{i=1}^n p_if_i,\qquad \mathbb V_{\mathbb P_n}[f]=\sum_{i=1}^n p_i\big(f_i-\mathbb E_{\mathbb P_n}[f]\big)^2 .$$

The divergence generator is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ satisfying Assumption 2.1: $\phi$ is closed (lower semicontinuous) and convex, $\phi(z)\ge\phi(1)=0$ for $z\ge0$, $\phi(z)=+\infty$ for $z<0$, and $\phi$ is twice continuously differentiable on a neighbourhood of $z=1$ with $\phi''(1)>0$. Kullback–Leibler ($z\log z-z+1$), modified $\chi^2$ ($(z-1)^2$) and Burg ($-\log z+z-1$) generators all qualify.

For $\delta>0$, the worst-case measures $\mathbb Q(\delta)$ of (2.7) are the minimizers, over probability vectors $q=(q_1,\dots,q_n)$, of

$$J_\delta(q)=\sum_{i=1}^n q_if_i+\frac1\delta\sum_{i=1}^n p_i\,\phi\Big(\frac{q_i}{p_i}\Big),$$

and $\mathbb Q(0)=\mathbb P_n$. The worst-case sensitivity (2.8) of the expected reward is

$$\mathcal S_{\mathbb P_n}(f)=-\lim_{\delta\downarrow0}\frac{\mathbb E_{\mathbb Q(\delta)}[f]-\mathbb E_{\mathbb P_n}[f]}{\delta}.$$

The proof uses the convex conjugate $\phi^*(\zeta)=\sup_z\{\zeta z-\phi(z)\}$ (F.5) and a Lagrange multiplier $c^\star(\delta)$ for the constraint $\sum_iq_i=1$.

Formalization targets

Goal: Theorem 2.2 (p. 8)

For every $\phi$ satisfying Assumption 2.1, every $\mathbb P_n$ with positive weights and every $f$, worst-case measures exist for each $\delta>0$, and for every choice of them

$$\mathcal S_{\mathbb P_n}(f)=\frac{1}{\phi''(1)}\,\mathbb V_{\mathbb P_n}[f].$$

Milestones (Appendix F, in proof order)

1. (F.4), p. 48. $\phi'$ has a continuously differentiable local inverse near $\zeta=0$, with $[\phi']^{-1}(0)=1$ and $[\phi']^{-1}(\zeta)=1+\zeta/\phi''(1)+o(\zeta)$.
2. p. 49. $\phi^*$ is finite and twice continuously differentiable near $0$, $[\phi^*]'=[\phi']^{-1}$ there, $[\phi^*]'(0)=1$ and $[\phi^*]''(0)=1/\phi''(1)$.
3. (F.7)–(F.8), p. 49. For small $\delta>0$ the first-order condition $\sum_ip_i[\phi^*]'(\delta(-f_i-c))=1$ has a unique solution $c^\star(\delta)$ near $-\mathbb E_{\mathbb P_n}[f]$, and $c^\star(\delta)\to-\mathbb E_{\mathbb P_n}[f]$ as $\delta\downarrow0$.
4. Proposition F.1, (F.1)–(F.2), p. 47. For small $\delta>0$ the worst-case measure is unique, $q^*_i(\delta)=p_i[\phi']^{-1}(\delta(-f_i-c^\star(\delta)))$, and $c^\star(\delta)$ maximizes the dual function $-\frac1\delta\sum_ip_i\phi^*(\delta(-f_i-c))-c$.
5. Proposition F.1, (F.3), p. 47. $q^*_i(\delta)=p_i\{1-\delta(f_i-\mathbb E_{\mathbb P_n}[f])/\phi''(1)\}+o(\delta)$.

Significance

Theorem 2.2 identifies penalized DRO, for small $\delta$, with a mean–variance trade-off: the robust objective is (by the expansion (2.6), which the paper cites) $\mathbb E_{\mathbb P_n}[f]-\frac{\delta}{2\phi''(1)}\mathbb V_{\mathbb P_n}[f]+o(\delta)$, and the theorem gives the derivative of the worst-case mean that underlies that expansion. The paper's calibration method (§§4–6) rests on this: since in-sample robustness acts by penalizing variance, $\delta$ is chosen by trading an out-of-sample reduction in variance against a loss in mean.

The result is proved in the paper; to the best of current searches it has no machine-checked proof. The mission produces a complete formal proof of Theorem 2.2 under the paper's own assumption, a formal treatment of the conjugate duality for penalized $\phi$-divergence problems on finite supports, and corrected versions of three steps of the printed argument (see Formalization scope).

Difficulty

The theorem is a first-order expansion of an argmin, and the obvious route is to differentiate the optimality conditions at $\delta=0$ by the implicit function theorem. That step fails under Assumption 2.1: the system defining the multiplier $c^\star(\delta)$ involves $[\phi^*]'$ evaluated at $\delta(-f_i-c)$, and its partial derivative in $\delta$ at $\delta=0$ requires a third derivative of $\phi$, which is not assumed. For $\phi(z)=(z-1)^2+|z-1|^{5/2}$ the multiplier satisfies $c^\star(\delta)+\mathbb E_{\mathbb P_n}[f]\approx0.036\sqrt\delta$, so it is not differentiable at $0$, although Theorem 2.2 still holds. A proof therefore has to extract the first-order behaviour of $\mathbb Q(\delta)$ from continuity of $c^\star$ at $0$ alone. Further work lies in showing that the minimizer is interior and unique for small $\delta$ when $\phi$ is only locally smooth, and in handling extended-real values of $\phi$ and $\phi^*$.

Formalization scope

• $\phi$ is a function ℝ → EReal satisfying Assumption21: lower semicontinuity, pointwise convexity on $\mathbb R$ (with $0\cdot(+\infty)=0$), $0\le\phi(z)$ for $z\ge0$, $\phi(1)=0$, $\phi(z)=\top$ for $z<0$, finiteness and $C^2$ smoothness of the real part on an open interval around $1$, and $\phi''(1)>0$. Assumption 2.1 is the only hypothesis on $\phi$: no third derivative, no finiteness on $(0,\infty)$, and no separate $\phi'(1)=0$ (it follows from the assumption).
• Derivatives of $\phi$ and $\phi^*$ are those of their real parts (EReal.toReal); every statement that differentiates also asserts or implies finiteness where it differentiates.
• The data are indexed by Fin n. The weights are general, $p_i>0$ and $\sum_ip_i=1$; the paper's empirical distribution is $p_i=1/n$, and its variance $\frac1n\sum_i(f_i-\mathbb E_{\mathbb P_n}[f])^2$ is the special case. The paper's (2.4) also allows zero weights; these are excluded.
• $\mathbb Q(\delta)$ ranges over the minimizers of $J_\delta$ on Mathlib's stdSimplex. The goal asserts that minimizers exist for every $\delta>0$ and that the limit holds for every selection of minimizers; it is not a statement about an arbitrary function constrained by hypotheses, and the existence clause rules out a vacuous reading.
• The sensitivity (2.8) is stated as a one-sided limit along $\delta\downarrow0$, so the branch $\mathbb Q(0)=\mathbb P_n$ is not needed.
• Corrected readings: (F.4) prints $\phi^{-1}$ and $\phi''(0)$ for $[\phi']^{-1}$ and $\phi''(1)$; p. 49 prints $[\phi^*]''(0)=1/\phi''(0)$ for $1/\phi''(1)$; the claim that $c^\star$ is continuously differentiable at $\delta=0$ is false under Assumption 2.1, and milestone 3 states continuity at $0$ instead. The clause "$\mathbb Q(\delta)$ is continuously differentiable near $\delta=0$" of Proposition F.1 is not stated; (F.3) is.
• Out of scope: the asymptotic out-of-sample analysis of §§3–5 (Proposition 3.2, Theorem 3.3, Propositions 4.1, 4.2, 5.2, Theorem 5.3), the bootstrap calibration algorithm of §6 and the experiments of §7. Those results either apply cited limit theorems, or expand moments of quantities known only in distribution without the integrability that would justify it.
• Everything beyond the local definitions is in Mathlib: EReal, LowerSemicontinuous, stdSimplex, deriv, ContDiffOn, HasDerivAt, Filter.Tendsto. A reusable by-product is the local theory of the convex conjugate of a $C^2$ convex function near a point of positive curvature. Contributions of proofs of any milestone are welcome.

Selected references

• J. Gotoh, M. J. Kim, A. E. B. Lim, Calibration of Distributionally Robust Empirical Optimization Models, Operations Research, 2021; read as arXiv:1711.06565v2, 2020. https://arxiv.org/abs/1711.06565
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• H. Lam, Robust Sensitivity Analysis for Stochastic Systems, Mathematics of Operations Research 41(4), 2016. https://doi.org/10.1287/moor.2015.0776
• J. C. Duchi, H. Namkoong, Variance-based Regularization with Convex Objectives, Journal of Machine Learning Research 20, 2019. https://arxiv.org/abs/1610.02581

Motivation

A firm can sell utility tokens before it has produced the good those tokens will buy. The sale supplies cash for production, but the firm can keep some or all of that cash instead. Speculators anticipate both the later value of a token and this diversion incentive when deciding whether to buy. Gan, Tsoukalas and Netessine study the resulting financing and production decisions in a three-period model of an initial coin offering (ICO). Their utility-token analysis identifies a value-to-cost threshold below which the ICO cannot raise cash and, above it, a unique equilibrium design under the paper's demand condition. Gan, Tsoukalas and Netessine, SSRN author version, §§2–3 and Appendix B.1.

The question matters to operations and finance because the funds obtained before production change the firm's later incentive to produce. Selling more tokens supplies a larger budget but leaves the firm with fewer tokens to sell after demand is realized. The model makes that tension quantitative through the ICO cap, production quantity and market token price. Gan, Tsoukalas and Netessine, pp. 7–14.

Setting

The firm initially has no wealth and owns $m>0$ utility tokens, redeemable for its future product. It chooses an ICO price $\tau\ge0$ and a cap $n\in[0,m]$ on tokens sold to speculators. There are $z\ge m$ potential speculators. Each wants at most one token and arrives simultaneously. If $s$ tokens sell, the firm may produce $Q$ units at unit cost $c>0$, subject to $0\le Q\le\tau s/c$. Customer demand $D$ has probability law $\mu$ and cumulative distribution function $F$; customers value each unit at $v>c$. Token counts and quantities are represented by real numbers, as in the paper's continuous optimization. Gan, Tsoukalas and Netessine, §2, pp. 7–10.

The market-clearing price of a token after demand is realized is $(v/m)\min\{Q,D\}$. Write $S(Q)=\mathbb E_\mu[\min\{D,Q\}]$ for expected sales. Conditional on $s$ sales, the firm maximizes $(m-s)(v/m)S(Q)-cQ$ over the production budget. A production rule $Q(\tau,s)$ selects a maximizer at every feasible history; it is determined by this optimization problem rather than prescribed by a closed formula. At the ICO stage a speculator's expected utility is

$$u_\tau(s)=\frac{s}{z}\left(\frac vm S(Q(\tau,s))-\tau\right).$$

The participation rule sells all $n$ offered tokens when $u_\tau(n)\ge0$, and otherwise sells none. The firm's expected terminal wealth is ICO receipts less production cost plus the market value of its unsold tokens. An equilibrium consists of production optimality after every feasible history and a pair $(\tau,n)$ maximizing this wealth over all $\tau\ge0$ and $0\le n\le m$. The market-clearing and participation rules are the model's interpretations of Lemma 1 and Lemma 2(i). Gan, Tsoukalas and Netessine, (1)–(3), (10), pp. 8–10, 12, 34.

Formalization targets

Proposition 1 identifies the optimal production quantity in two regimes. Proposition 2 identifies when a cap can support positive sales at a positive ICO price. Lemma 2 and Propositions 12–13 supply the participation and optimal-cap statements recorded as milestones. The main target is Proposition 3, including every part of its conclusion. Gan, Tsoukalas and Netessine, pp. 11–14, 34–35.

If $v\le2c$, no feasible ICO design raises cash. If $v>2c$, the equilibrium ICO price $\tau^*$ and cap $n^*$ exist and are unique. With

$$Q^*=F^{-1}\!\left(1-\frac{m}{m-n^*}\frac cv\right),$$

the cap is the unique point in $(mc/v,m/2)$ satisfying

$$\frac{vn^*}{cm}S(Q^*)=Q^*.$$

The remaining conclusions are $\tau^*=(v/m)S(Q^*)$, all $n^*$ tokens sell, market-period token price equals $(v/m)\min\{Q^*,D\}$ with expectation $\tau^*$, and the full ICO proceeds are used for production: $cQ^*=\tau^*n^*$. Gan, Tsoukalas and Netessine, Proposition 3, pp. 13–14.

Significance

The result gives a precise failure threshold for a utility-token ICO and ties the successful design to demand, production cost and the amount of tokens retained by the firm. In particular, its cap is below half of the total token supply, and at the optimum the production budget binds. These are statements about the model's incentive problem, with the demand condition required for its uniqueness result. Gan, Tsoukalas and Netessine, discussion after Proposition 3, p. 14.

The paper proves these results mathematically. This mission records their Lean statements as open goals; it does not yet supply machine-checked proofs. Completing the formalization would also develop reusable facts about expected truncated demand, inverse distribution functions, and optimization under a cash budget. The equity-token comparison, extensions and numerical experiments remain separate from this target. Gan, Tsoukalas and Netessine, §§4, 6 and Appendix C.

Difficulty

The firm controls the ICO price and cap before the production decision, while speculator participation responds to the production rule. Raising the cap increases possible receipts but can lower the firm's incentive to produce and therefore the resale value speculators expect. A production optimum for fixed sales does not by itself identify which sales level will occur. The firm's wealth also changes regime when the production budget ceases to bind, so a single smooth optimization statement does not cover the entire feasible set. The uniqueness claim depends on the demand-density condition stated before Proposition 12. Gan, Tsoukalas and Netessine, §§3.1–3.4 and Appendix B.1.

Formalization scope

Demand is one probability measure $\mu$ on $\mathbb R$: $F$ is its cumulative distribution function and $S(Q)$ is the integral of $\min(D,Q)$ against that same measure. The inverse expression is the infimum of nonnegative $x$ with $F(x)\ge y$. The paper's $F^{-1}(0)=0$ is represented by $F(x)=0$ for $x\le0$ and $F(x)>0$ for $x>0$. Because the proofs and the Appendix B.1 condition use a density and its derivative, the formal setting requires a positive differentiable density wherever $x>0$ and $F(x)<1$. The paper's informal $z\gg m$ is represented by $m\le z$. These choices are explicit added assumptions or readings of the source's conventions. Gan, Tsoukalas and Netessine, pp. 8–9, 34, 37–38, 46–48.

The Appendix B.1 condition on $f'/f^2$ is applied at interior quantiles $0<y<1-2c/v$, avoiding the support boundary where the paper does not define the derivative. Lemma 2(ii)–(iii) is stated at $\tau>0$, because at zero price its printed conclusions fail. The positive boundary price in Proposition 12 is considered on the open viable-cap interval; its printed upper endpoint has no positive solution. Its “unique solution” is the unique positive solution, since zero also solves the first displayed equation. The participation equality there is evaluated at full sales $s=n$: evaluated after abstention at $s=0$, it would hold automatically. These boundary readings follow the paper's own adjacent analysis. Gan, Tsoukalas and Netessine, pp. 12–13, 34–35, 45–47.

The production rule is quantified over every rule that truly optimizes the budgeted production subgame. Expected sales is the integral against $\mu$, never a free function unrelated to $F$. The equilibrium optimizes over all feasible prices and caps; the narrow interval for $n^*$ is a conclusion. The work needed includes measure-theoretic sales identities, quantile behavior, and the firm's regime-dependent optimization. Contributions establishing these facts or proving the named milestones fit this mission. The model here is the base utility-token, simultaneous-arrival model; equity tokens, sequential arrival, the §6 extensions and numerics are outside its scope.

Selected references

• J. R. Gan, G. Tsoukalas and S. Netessine, Initial Coin Offerings, Speculation, and Asset Tokenization, SSRN author version 3361121, June 29, 2020; published in Management Science (2020). SSRN author version, DOI.

Motivation

Digital platforms (marketplaces, payment networks, sharing services) need large up-front investments in capacity before any revenue arrives, and their founders typically finance them by selling equity to venture capitalists. Since 2017 an alternative has been available: issuing a platform-specific cryptocurrency (a utility token) in an initial coin offering (ICO), and running the platform on a blockchain whose fee rules are fixed in a smart contract. Whether this is merely a new funding channel or a better business model is a question for operations management, corporate finance and platform economics alike.

J. Chod, N. Trichakis and S. A. Yang (Platform Tokenization: Financing, Governance, and Moral Hazard, Management Science, 2022) answer it in a model in which the entrepreneur's effort is not contractible. They show that the answer depends on the cost of building capacity: when capacity is expensive, equity wins (their Proposition 1), and when it is cheap, tokens win (their Proposition 2). This mission formalizes the second result.

Setting

An entrepreneur builds a platform of capacity $Q$ at cost $C(Q)=KQ^k$ and exerts effort $e$ at private cost $\gamma e$. Buyers' inverse demand is $d(e,q)=e^aq^{-b}$ and sellers' supply curve is $s(q)=mq^n$, with $0<a<b<1$, $m,n\ge0$ and $k>(1-b)/(1-a)$. Sellers pay a one-time cost $c$ to join, cash flows are discounted by $\delta\in(0,1)$, and each token is used $v\ge1$ times per period. The per-period surplus is

$$\mathcal F(e,q)=q\bigl(d(e,q)-s(q)\bigr),$$

with partial derivatives $\mathcal F_e$, $d_e$ in $e$. The entrepreneur's objective in both models is the net present value

$$\frac{\mathcal F(e,Q)}{1-\delta}-cQ-C(Q)-\gamma e .$$

In the traditional model the entrepreneur sells an equity share $\alpha$ to a venture capitalist and can raise the fee once sellers have sunk their joining cost (holdup), which forces a first-period subsidy. Its equilibrium payoff \Pi^\$$ is the maximum of the objective subject to (1-\alpha)\mathcal F_e/(1-\delta)=\gamma$, where$\alpha$is the VC's break-even share, (17)–(20). In the **blockchain-based model** she sells a fraction$\alpha$of the tokens and commits to the fee; the payoff$\Pi^B$is the maximum subject to$\mathcal F_e/(1-\delta)-\alpha\frac1v d_eQ=\gamma$and$\alpha,d(e,Q)Q=vC(Q)$with$\alpha\le1$, (33)–(36). Corollary 1 rewrites both as one program with effort factors$\beta^$$,$\beta^B$, the blockchain one carrying the extra cap$d(e,Q)Q\ge vC(Q)$.

Formalization targets

Goal: Proposition 2

With all other parameters fixed and $c>0$ or $m>0$, there is $\varepsilon>0$ such that for every $K\in(0,\varepsilon]$ both suprema are finite and $\Pi^B>\Pi^\$\qquad\text{unless}\qquad\Pi^B=\Pi^\$=0 .$ No value of $\varepsilon$ is fixed: the goal asserts only the existence of a cheap-capacity regime.

Milestones

1. Corollary 1 for $i=B$ and $i=$$: Lemmas 2–3's programs equal (37)–(40).
2. (B.19)–(B.20): for small $K$ the token cap (39) does not bind.
3. Claim (i): $h(e,Q)>g(e,Q)$, i.e. \beta^B>\beta^\$$ wherever d>s$.
4. (B.29): e^\(Q)<e^B(Q)<e^*(Q)$, in root form.
5. Claim (ii): the objective is strictly concave in $e$ with unique maximizer $e^*(Q)$.

Significance

Proposition 2 is the paper's headline. It isolates two advantages of tokenization that hold even without any cost or technology difference: token investors are exposed to platform revenue rather than profit, which is less sensitive to effort, so the entrepreneur internalizes more of the marginal value of her effort; and a fee committed on a blockchain removes the holdup problem and with it the subsidy the traditional platform must finance. Together with Proposition 1 it delineates when a platform should tokenize.

The result is proved in the paper (Appendix B, pp. 19–20). It has not been machine-checked. The proof is short but leaves two steps informal: the relaxation of the cap (39) "by continuity", and the existence of optimal solutions behind the printed "max". A formal proof settles both, and fixes the exact hypotheses under which the claim holds (see the scope section).

Difficulty

The algebra of Corollary 1 and of Claim (i) is routine. The difficulty is analytic. The naive argument compares the two programs pointwise in $Q$ at their largest effort roots, but the payoffs are suprema over non-compact feasible sets, and the comparison only transfers to the suprema if the traditional supremum is attained, or approached at capacities bounded away from $0$ and $\infty$. The relaxation of (39) requires a bound, uniform in small $K$, showing that points violating the cap cannot approach the relaxed supremum; this is where $c>0$ or $m>0$ enters, since with $c=m=0$ the objective near such points is not controlled as $K\to0$.

Formalization scope

Parameters are a structure Params with real fields $a,b,m,n,K,k,c,\gamma,\delta,v$; Params.Standing collects the printed assumptions ($0<a<b<1$, $m,n\ge0$, $k>(1-b)/(1-a)$, $v\ge1$) and four the paper uses without stating ($0<\delta<1$, $c\ge0$, $\gamma>0$, $K\ge0$). Powers are Real.rpow, with Lean's $0^y=0$ for $y\ne0$; the partials $\mathcal F_e=ae^{a-1}Q^{1-b}$, $d_e=ae^{a-1}Q^{-b}$ are closed forms, certified by two HasDerivAt helper theorems, and $e^*(Q)$ is a closed form certified as the argmax by Claim (ii).

\Pi^\$$ and \Pi^B$are *defined* by the programs of Lemmas 2 and 3; the underlying dynamic game is not modelled. Each payoff is$\max{0,\sup(\text{objective over the feasible set})}$: the supremum replaces the printed max, never shown attained, and$0$ is the outside option of not starting the venture, invoked in the last paragraph of the paper's proof.

Departures from the printed statement, all disclosed in the items:

• $K\in(0,\varepsilon]$ instead of $[0,\varepsilon]$: at $K=0$ the Corollary 1 payoff programs coincide on the branch $c\le d-s$ (e.g. $c=0$, $m=1$), contradicting the printed strict claim. Lemma 2's literal $0<\alpha$ constraint omits that zero-investment boundary, so this mission states the common positive-$K$ regime.
• The added hypothesis $c>0$ or $m>0$: with $c=m=0$, \beta^\=\beta^B$and the blockchain program is the traditional one plus a cap, so$\Pi^B\le\Pi^$$for every$K>0$.
• Corollary 1 for i=\$$ is posed for K>0$and as an equality of payoffs: at$K=0$, (19) gives$\alpha=0$, which (20) excludes.

The goal cannot be met vacuously: it asserts that both objective images are bounded above, so the suprema are not Lean's junk value $0$, and the helper piTrad_pos_example states \Pi^\>0$at the Figure 1 parameters ($k=1$,$K=0.01$), ruling out an empty traditional program.

A complete development needs real-power calculus, the intermediate value theorem, strict concavity of $e\mapsto e^a$, and a compactness or coercivity argument for the suprema. The coercivity bounds for programs of the form "maximize a concave revenue minus a power cost subject to a first-order condition" are reusable for other effort-and-capacity models. Proofs of any milestone are welcome, as are proofs of the helpers.

Selected references

• J. Chod, N. Trichakis, S. A. Yang, Platform Tokenization: Financing, Governance, and Moral Hazard, Management Science, Articles in Advance, 2022. https://doi.org/10.1287/mnsc.2021.4225
• M. C. Jensen, W. H. Meckling, Theory of the Firm: Managerial Behavior, Agency Costs and Ownership Structure, Journal of Financial Economics 3(4), 1976. https://doi.org/10.1016/0304-405X(76)90026-X

Motivation

Sellers sometimes offer a customer a choice among individual products and a product whose final item is revealed only after purchase. Airlines, for example, can sell a fixed itinerary alongside a discounted option that leaves one feature unspecified. The seller must decide whether this opaque product earns enough to justify limiting how much individual item prices can differ. Elmachtoub and Hamilton study this question for unit-demand customers who know their own values for the possible items. Their 2021 paper identifies two conditions under which the best menu of opaque products earns at least as much as the best separate item prices.

The comparison matters because the opaque menu uses less item-specific pricing information. The seller gives every item one price and gives opaque products of equal size the same price. The theorem says that this constrained format can still match discriminatory pricing when the valuation law is symmetric and either customers assess opaque products pessimistically or valuations have only two levels. The paper also supplies counterexamples outside those conditions; the symmetry and customer-type hypotheses are substantive.

Setting

There are $N\ge2$ items. A customer has a nonnegative valuation vector $v=(v_1,\ldots,v_N)$, sampled from a probability law $F$. A menu option has a price and a valuation. Its utility is valuation minus price. The customer buys one option of greatest utility when that utility is nonnegative. If several options have greatest utility, the customer buys one with the highest price. Remaining ties at the same price do not affect revenue. A customer may also buy nothing, yielding zero revenue.

In discriminatory pricing (DP), the seller assigns a nonnegative price $p_i$ to each item and offers only the individual items. Write $R_{\mathrm{DP}}(p_1,\ldots,p_N)$ for expected revenue and $R_{\mathrm{DP}}$ for its optimum over item-price vectors.

In opaque selling (OPQ), the seller offers the items at a common price $p$ and also offers every set $S$ of at least two items. A set of size $k$ costs $p^k$, independent of which items it contains. A pessimistic customer values $S$ at $\min_{i\in S}v_i$; a risk-neutral customer values it at $|S|^{-1}\sum_{i\in S}v_i$. Both value a singleton at its item value. A customer is pessimistic with probability $\alpha$ and risk-neutral with probability $1-\alpha$, independently of the valuation vector. The expected revenue of a price menu is $R_{\mathrm{OPQ}}^\alpha(p,p^2,\ldots,p^N)$; its optimum is $R_{\mathrm{OPQ}}^\alpha$.

A law $F$ is exchangeable if permuting the coordinates of $v$ leaves its joint distribution unchanged. Coordinates may be correlated, and they need not be independent. A law is two-valued when there are real numbers $a<b$ such that almost every valuation vector has every coordinate in $\{a,b\}$. This says the same pair applies to the entire vector, rather than allowing a different pair at each coordinate.

Formalization targets

Theorem 1: revenue dominance

For exchangeable $F$, nonnegative valuations, and $0\le\alpha\le1$, the target is

$$\bigl(\alpha=1\ \text{or}\ F\text{ is two-valued}\bigr) \quad\Longrightarrow\quad R_{\mathrm{OPQ}}^\alpha\ge R_{\mathrm{DP}}.$$

The first case covers any exchangeable law, including discrete laws with ties, when all customers are pessimistic. The second covers every mix of customer types when the valuations take two common values. Neither case requires independent item values. This mission retains both cases in one goal because that is Theorem 1 as stated in the paper.

The milestones trace the two cases. They identify the equal probabilities of valuation-order events, the value of the best opaque subset at a fixed size, the pessimistic dominance case, the three candidate DP price vectors under two values, the conditional revenue identity printed as display (1), the opaque price ladder's revenue for both customer types, and the two-valued dominance case. Each milestone is attached to a passage in the proof of Theorem 1.

Significance

The theorem gives a comparison of optimal revenues, not just a comparison of one chosen menu with one chosen price vector. For a seller with exchangeable valuations, it guarantees that size-based opaque prices can recover at least the revenue available from item-specific prices in either named regime. Outside those regimes, the paper's counterexamples prevent extending that guarantee merely by relaxing the hypotheses.

The result is proved in the cited paper; the goal here is a machine-checked version of its statement and proof. A formal development would establish the choice rule for finite menus, expectations for discrete and continuous valuation laws, permutation symmetry, finite order statistics, and the behavior of size-based menus at utility and price ties. These components are reusable in later formalizations of unit-demand pricing and opaque-product models. The present mission starts with unproved Lean theorem statements; compiling those statements does not certify the paper's argument.

Difficulty

One tempting argument treats the opaque menu as discriminatory pricing with the valuation order known to the seller. That comparison overlooks a restriction: the same price must be attached to each product size, so a price that is useful for the highest-valued item need not be useful for every realized ordering. The paper explicitly notes that the apparent information advantage alone would also suggest dominance in settings where dominance fails.

Ties create another obstacle. The probability formulas displayed for DP and OPQ in the selling-model section use inequalities that can count a tied purchase more than once. The paper sets aside ties for exposition in that section, yet the two-valued case necessarily has them. A faithful proof has to use the stated customer choice rule and the highest-price tie-break, rather than treating those displayed sums as definitions for discrete laws. The two-valued case also requires tracking how revenue changes with the number of high valuations, without assuming independent coordinates.

Formalization scope

Items are represented by Fin N and valuation profiles by functions Fin N → ℝ; the paper's item indices start at one, while Lean's start at zero. The probability law is a measure on profiles with a probability-measure instance and almost-sure nonnegative coordinates. Exchangeability means invariance of this law under every coordinate permutation. Two-valued support is an almost-sure condition on the whole profile. No independence or density assumption is included.

The menu contains every nonempty item set. Singletons stand for the ordinary items at their common price; sets of equal larger size share an opaque price. All seller prices are nonnegative. Revenue is the highest price among options with maximal nonnegative utility, with zero when no option qualifies. This directly represents the rule on page 8, including discrete laws. The pessimistic valuation is a finite minimum and the risk-neutral valuation a finite average. Customer type is mixed independently of the valuation law, so the OPQ expectation is the $\alpha$-weighted sum of the two type-specific expectations.

Expected revenues and optimal revenues use extended nonnegative reals $[0,\infty]$. The optima are suprema over nonnegative prices; existence of a maximizing price vector is not assumed. This avoids default values for an unbounded real supremum and records possible infinite revenue. Prices for unused cardinalities are nonnegative but have no effect on the menu. The order statistic sorts the coordinates with multiplicity; it is not defined through the subset identity it is meant to satisfy.

The goal is not implied by a degenerate model: the revenue function charges the highest price among utility maximizers and sells only at nonnegative utility; the optimal revenues range over nonnegative prices; exchangeability is invariance under every coordinate permutation. Contributions toward the finite-menu choice lemmas, permutation-invariant integration, order-statistic identity, two-valued DP structure, and the two cases are within scope.

Selected references

• A. N. Elmachtoub and M. L. Hamilton, The Power of Opaque Products in Pricing, Management Science, 2021, doi:10.1287/mnsc.2020.3750. This mission uses the author's 54-page manuscript, pinned locally by SHA-256 ccd5b53ae01d607eca3b7df8549f418f52245b99bb2dfa050b6f5c4878a3cffe; its printed and PDF page numbers agree.

Motivation

Stress testing and data-driven decision making often combine two samples: observations $X_1,\dots,X_n$ of the quantity of interest and additional scenarios $Y_1,\dots,Y_m$ (stress scenarios supplied by a regulator, or unlabeled data). Blanchet and Kang (arXiv:1605.01340v4, 2020; later in Operations Research, 2021) propose to measure how far the empirical distribution of the observations is from the set of distributions that live on the merged sample and satisfy a hypothesis about a parameter, such as "the mean is $\theta$". The distance is an optimal-transport (Wasserstein) cost, and the resulting statistic is the sample out-of-sample (SOS) profile function.

The construction is the transport analogue of empirical likelihood (Owen 1988), whose central result is a Wilks-type theorem (Wilks 1938): $-2\log$ of the likelihood ratio at the true mean is asymptotically $\chi^2$. Empirical likelihood can only reweight the observed points. The SOS function can also move mass to out-of-sample scenarios, which is what makes it usable for stress testing. Confidence regions require the asymptotic law of the statistic at the true parameter. That law is the subject of this mission: the paper's main theorem for means, Theorem 1 (pp. 15–16).

Setting

Let $l\ge1$. Observations $X_1,X_2,\dots$ and scenarios $Y_1,Y_2,\dots$ are random vectors in $\mathbb R^l$, all mutually independent, with Lebesgue densities $f_X$ and $f_Y$. A ratio $\kappa\in[0,\infty)$ fixes the number of scenarios $m=\lfloor\kappa n\rfloor$ used with $n$ observations. The standing assumptions A1)–A4) (p. 14) are: the samples are i.i.d. with these densities; $\mathbb E\|X_1\|_2^2+\mathbb E\|Y_1\|_2^2<\infty$; $f_X,f_Y>0$ everywhere; and, if $l\ge2$, $f_X,f_Y$ are differentiable with bounded gradients.

The merged sample is $\mathcal Z_{n+m}=(Z_1,\dots,Z_{n+m})=(X_1,\dots,X_n,Y_1,\dots,Y_m)$. For $\theta\in\mathbb R^l$ the SOS function (Definition 1, in the linear-programming form (21)) is

$$R_n^W(\theta)=\min\Big\{\sum_{i=1}^n\sum_{j=1}^{n+m}\pi(i,j)\|X_i-Z_j\|_2^2:\ \pi\ge0,\ \sum_j\pi(i,j)=\tfrac1n\ \forall i,\ \sum_j\Big(\sum_i\pi(i,j)\Big)Z_j=\theta\Big\}.$$

It is the least squared transport cost from the empirical measure $\mu_n$ of the $X_i$ to a probability measure supported on $\mathcal Z_{n+m}$ with mean $\theta$. The statistic of interest is $R_n^W(\theta_*)$ at the true mean $\theta_*=\mathbb E X_1$. Write $\mathrm{Var}(X)=\mathbb E[(X_1-\theta_*)(X_1-\theta_*)^{\mathsf T}]$ and $\tilde Z\sim N(0,\mathrm{Var}(X))$.

The limits involve a mixed exponential variable. With the rate $\Lambda(x,\lambda)=[f_X(x+\lambda/2)+\kappa f_Y(x+\lambda/2)]\,\pi^{l/2}/\Gamma(l/2+1)$, the variable $\tau(\lambda)$ satisfies $\mathbb P[\tau(\lambda)>t]=\mathbb E[\exp(-\Lambda(X_1,\lambda)t)]$. From $\tau(0)$ one defines $\tilde g(x)=\mathbb P(\tau(0)\le\|x\|_2^2)$, $\tilde\eta(x)=\mathbb E[\max(1-\tau(0)/\|x\|_2^2,0)]$, the solution $\rho(z)>0$ of $1/\rho=\tilde g(\rho z)$, and $c_0=\mathbb E[\Lambda(X_1,0)]$.

Formalization targets

Goal: Theorem 1 (pp. 15–16)

As $n\to\infty$,

$$l=1:\quad nR_n^W(\theta_*)\Rightarrow\sigma^2\chi_1^2=\text{law of }\|\tilde Z\|_2^2,\qquad \sigma^2=\mathrm{Var}(X);$$ $$l=2:\quad nR_n^W(\theta_*)\Rightarrow\rho(\tilde Z)\big(2-\tilde\eta(\rho(\tilde Z)\tilde Z)\,\rho(\tilde Z)\big)\|\tilde Z\|_2^2;$$ $$l\ge3:\quad n^{1/2+3/(2l+2)}R_n^W(\theta_*)\Rightarrow\frac{2l+2}{l+2}\cdot\frac{\|\tilde Z\|_2^{1+1/(l+1)}}{c_0^{1/(l+1)}} .$$

The goal is the paper's theorem in all three regimes. The $l=2$ case is stated with $\tilde\eta(\rho\tilde Z)$, a correction of the printed $\tilde\eta(\tilde Z)$ (see Formalization scope).

Milestones (in attack order)

1. (21)–(22), pp. 35–36: LP duality, $R_n^W(0)=\max_{\lambda,\gamma\ge0}\{-\lambda^{\mathsf T}\bar X_n-\frac1n\sum_i\gamma_i\}$ subject to $-\lambda^{\mathsf T}X_i-\gamma_i\le\inf_j\{-\lambda^{\mathsf T}Z_j+\|X_i-Z_j\|_2^2\}$.
2. §7.2.1, p. 38: the closest-point bound, $\inf_a\{-\lambda^{\mathsf T}a+\|x-a\|_2^2\}=-\lambda^{\mathsf T}x-\|\lambda\|_2^2/4$, attained at $x+\lambda/2$.
3. (27), p. 41: $R_n^W(0)=\max_\lambda\{-2\lambda^{\mathsf T}\bar X_n-\frac1n\sum_i\max(\|\lambda\|_2^2-D_i(\lambda),0)\}$, with $D_i(\lambda)$ the squared distance from $X_i+\lambda$ to the nearest other point of $\mathcal Z_{n+m}$.
4. Lemma 1, p. 40 (two bounds): $\limsup_n\mathbb E\sup_{t\le T}|n^{-1/2}\sum_i(\cdot-\mathbb E\,\cdot)|<\infty$ for $I(T_i(n,\lambda)\le t)$ and for $\max(t^2-T_i(n,\lambda)^\alpha,0)$, where $T_i(n,\lambda)$ is the first-arrival time of the counting process of other sample points near $X_i+\lambda/2$.
5. Lemma 2, p. 41 (first clause): $\mathbb P[T_i(n,\lambda)\le t]-\mathbb P[\tau(\lambda)\le t]=O(t^{1+1/l}/n^{1/l})$.
6. (31), p. 45: $1/\rho=\tilde g(\rho z)$ has a unique solution for $z\ne0$ ($l=2$).
7. §7.2.5, p. 45: $\max_\zeta\{-2\zeta^{\mathsf T}z-\|\zeta\|_2^2\tilde\eta(\zeta)\}=\rho(z)(2-\tilde\eta(\rho(z)z)\rho(z))\|z\|_2^2$, attained at $-\rho(z)z$.
8. §7.2.6, pp. 47–48: $\max_\zeta\{-2\zeta^{\mathsf T}z-\frac{2C}{l+2}\|\zeta\|_2^{l+2}\}=\frac{2l+2}{l+2}\|z\|_2^{1+1/(l+1)}/C^{1/(l+1)}$.

Significance

Theorem 1 calibrates the SOS method. Its quantiles define the radius of a confidence region for the mean, and through the paper's Theorems 2–3 for estimating equations and for stochastic programs whose uncertainty set must cover out-of-sample scenarios. Unlike empirical likelihood, the limit depends on the dimension and on the densities $f_X,f_Y$: more dispersed scenarios give smaller distances and smaller quantiles (§4.1.1). The theorem also shows that the scaling itself changes with $l$, from $n$ for $l\le2$ to $n^{1/2+3/(2l+2)}$ for $l\ge3$.

The result is proved in the paper; nothing here is an open problem. As far as we know, none of it has been formalized. A formal development adds:

• a checked version of a proof that is informal in places: it passes $o_p(1)$ terms through maxima over unbounded dual variables;
• the correction of the $l=2$ limit;
• reusable pieces: a duality theorem for finite transport problems with a mean constraint, a binomial-to-Poisson estimate for nearest-neighbour counts, and empirical-process bounds for dependent nearest-neighbour statistics.

Difficulty

The obvious approach is a Wilks-type expansion: take the dual of the LP, find the dual multiplier $\lambda_n\approx c\,\bar X_n$ by a quadratic approximation, and read off a $\chi^2$ limit. This works only for $l=1$. In higher dimensions the transport may only move mass to sample points, and the constraint for observation $i$ is controlled by the distance from $X_i+\lambda/2$ to the nearest other sample point. That distance is of order $n^{-1/l}$, so it competes with $\|\lambda\|^2$ at a dimension-dependent scale. The quadratic approximation therefore fails: the dual objective becomes, after rescaling, an average of $\max(\|\zeta\|^2-T_i^{2/l},0)$ over $n$ dependent first-arrival times, which share the same merged sample.

Three steps carry the weight. (a) The dependent array $T_i(n,\lambda)$ needs a uniform $n^{-1/2}$ empirical-process bound (Lemma 1); i.i.d. tools such as the Dvoretzky–Kiefer–Wolfowitz inequality do not apply. (b) A quantitative Poisson approximation (Lemma 2) needs the bounded density gradients. (c) The random concave objective must converge to a deterministic one uniformly enough that its maximiser converges (argmax continuity). Step (c) also needs a multivariate central limit theorem for $\sqrt n\bar X_n$, which Mathlib does not yet provide.

Formalization scope

Representation. Points live in EuclideanSpace ℝ (Fin l). The samples are infinite sequences on a probability space $(\Omega,\mathbb P)$, jointly independent (iIndepFun over $\mathbb N\sqcup\mathbb N$), with laws volume.withDensity. The $n$-th statistic uses the first $n$ observations and the first $\lfloor\kappa n\rfloor$ scenarios; $m=[\kappa n]$ is read as the floor, and $\kappa=0$ is allowed. The SOS function is a real infimum over couplings $\pi:\{1..n\}\times J\to\mathbb R$ of indexed families. Convergence in distribution is Mathlib's TendstoInDistribution, with limit the image of multivariateGaussian 0 Var(X) under an explicit map $\varphi_l$. The goal is a conjunction of three clauses, $l=1$, $l=2$, $l\ge3$.

Conventions and disclosed readings.

• The $l=2$ limit uses $\tilde\eta(\rho(\tilde Z)\tilde Z)$. Theorem 1 prints $\tilde\eta(\tilde Z)$, but the derivation on p. 45 evaluates $G(\zeta,n)=\|\zeta\|^2\tilde\eta(\zeta)+o(1)$ at $\zeta^*_n=-\rho Z_n$, and the two laws differ for every $\tilde Z\ne0$. Milestone 7 isolates this computation.
• When $\theta_*$ is outside the convex hull of the merged sample, the LP is infeasible; $R_n^W$ is then $0$ by convention, where the paper has $+\infty$. The event has probability tending to zero, and no feasibility hypothesis is added to the goal.
• $\rho(0):=0$ (the equation has no solution at $0$, which is a null event for $\tilde Z$), and $\tilde\eta(0)=1$ is never used.
• In (27), after $\lambda\leftarrow2\lambda$, the nearest-point distance is centred at $X_i+\lambda$; the page keeps the symbol $T_i(n,\lambda)$.
• "$Z_j\ne X_i$" in the counting process is a condition on values.
• Lemma 1's $\overline{\lim}$ is a $\limsup$ of a lower Lebesgue integral.
• Lemma 2 is posed at fixed $t$, with the constant allowed to depend on $t$. Its second clause ($O(1/n^l)$) is not posed: it is not supported by the estimate (26) its proof cites. For $l=1$ Lemma 2 adds the density regularity that A4) requires only for $l\ge2$.
• In §7.2.6 the sign of $G$ is read as $+$, and the scaling $n^{1/2+5/(4l+2)}$ printed on p. 48 is read as $n^{1/2+3/(2l+2)}$ (Theorem 1).

Ruled out. The following are not acceptable formalizations: a feasibility hypothesis on every sample; a limit law left as a parameter or quantified existentially; $\rho$, $\tilde g$ or $\tilde\eta$ given by closed forms rather than from the law of $\tau(0)$ and the fixed-point property; the printed $\tilde\eta(\tilde Z)$ presented as proved; Lemma 2 with a constant uniform in $t$; Lemma 1 with a Bochner integral, which would be a default $0$ for a non-integrable supremum.

Infrastructure. A full proof needs: finite LP strong duality (Farkas), absent as a packaged theorem; binomial/Poisson estimates for small-ball counts; a pathwise Burkholder–Davis–Gundy inequality (Beiglböck and Siorpaes 2015) or another route to Lemma 1; dominated-convergence differentiation of $\mathbb E\max(\|\zeta\|^2-\tau,0)$; a multivariate CLT; and argmax-continuity for random concave functions. The LP duality and the multivariate CLT are reusable well beyond this mission. Contributions to any milestone are welcome; milestones 1, 2, 6, 7 and 8 are deterministic and independent of the probabilistic core.

Selected references

• J. Blanchet, Y. Kang, Sample Out-of-Sample Inference Based on Wasserstein Distance, arXiv:1605.01340v4, 2020; Operations Research, 2021. https://arxiv.org/abs/1605.01340
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, Journal of Applied Probability 56(3), 2019. https://arxiv.org/abs/1610.05627
• A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
• S. S. Wilks, The large-sample distribution of the likelihood ratio for testing composite hypotheses, Annals of Mathematical Statistics 9(1), 1938. https://doi.org/10.1214/aoms/1177732360
• M. Beiglböck, P. Siorpaes, Pathwise versions of the Burkholder–Davis–Gundy inequality, Bernoulli 21(1), 2015. https://arxiv.org/abs/1305.6188

Motivation

A clinical trial that compares several treatments for the same condition must decide, patient by patient, which treatment the next patient receives. When the treatments are related (doses of one drug, drugs of one class), an outcome observed on one arm is informative about the others, and a good allocation rule should exploit that correlation. Chick, Gans and Yapar (SSRN 3184758, version of August 31, 2020; later in Management Science) model this as Bayesian sequential sampling with a correlated Gaussian prior and propose the cPDE allocation policy, which samples the arm with the largest value of an adaptive-lookahead optimal-stopping index. Their one theorem, Theorem 1, says that cPDE is asymptotically consistent: run forever, it learns every arm's mean and identifies the best arm.

Consistency is the minimal guarantee asked of an allocation heuristic: a rule that can stop sampling an arm whose value is still uncertain may settle on the wrong treatment forever. The argument follows the consistency proof of Xie, Frazier and Chick (Operations Research 64(2):542–559, 2016; "XFC") for one-step knowledge-gradient (cKG) policies, extended to an index whose lookahead is itself an optimal stopping time.

Setting

There are $M\ge2$ arms. Arm $i$ has unknown mean $\theta_i$; an observation of arm $i$ is $Y\mid\theta_i\sim N(\theta_i,\lambda_i)$ with known $\lambda_i>0$, independent across observations. The prior is $\theta\sim N(\mu^0,\Sigma^0)$ with $\Sigma^0$ positive definite, and sampling arm $i$ costs $c_i>0$. After $t$ observations the belief is $(\mu^t,\Sigma^t)$; one observation $y$ of arm $i$ updates it by Bayes' rule (8):

$$\mu'=\mu+\frac{y-\mu_i}{\lambda_i+\Sigma_{i,i}}\Sigma e_i,\qquad \Sigma'=\Sigma-\frac{\Sigma e_ie_i^\top\Sigma}{\lambda_i+\Sigma_{i,i}}.$$

From a belief $(\mu,\Sigma)$, imagine sampling arm $i$ alone. The predictive change $Z^\tau_i=\mu^{t+\tau}_i-\mu^t_i$ after $\tau$ samples is a centred Gaussian with variance $\lambda_i\tau/(n_i(n_i+\tau))$, $n_i=\lambda_i/\Sigma_{i,i}$ ((9)–(10)). The cPDE allocation index is (EC.8):

$$\nu^*_i(\mu,\Sigma)=\sup_{T_i\ge1}\mathbb E\Big[-T_i+\frac1{c_i}\max_j\Big\{\mu_j+\frac{\Sigma_{i,j}}{\Sigma_{i,i}}Z^{T_i}_i\Big\}\Big]-\frac1{c_i}\max_j\mu_j,$$

the supremum over stopping times of the sampling of arm $i$. The one-step index $\nu^{cKG_1}_i$ is the same expression with $T_i\equiv1$ ((EC.6)). The cPDE policy allocates observation $t+1$ to an arm maximizing $\nu^*_i(\mu^t,\Sigma^t)$; the trial never stops.

Formalization targets

Goal: Theorem 1 (p. 13)

For each arm $i$, almost surely,

$$\Sigma^T_{i,i}\to0,\qquad \nu^*_i(\mu^T,\Sigma^T)\to-1,\qquad \mu^T_i\to\theta_i\ \text{(also in }L^2),$$

and almost surely $\theta$ has a unique maximizer which, for all large $T$, is also the unique maximizer of $\mu^T$.

Milestones

1. Prop. 3 (p. 12): $Z^\tau_i$ is a uniformly integrable martingale and $\mathbb E[Z^{T}_i]=0$ for a.s. finite stopping times.
2. Lemma EC.1, first inequality (p. ec3): $\nu^{cKG_1}_i\le\nu^*_i$.
3. Lemma EC.3 (p. ec6): if $\liminf_T\nu^{cKG_1}_i(\mu^T,\Sigma^T)=-1$ for all $i$, then every $\Sigma^T_{i,i}\to0$.
4. Lemma EC.4 (p. ec7): an arm sampled infinitely often has $\Sigma^T_{i,i}\to0$, and $\Sigma^T_{i,i}\to0$ forces $\nu^*_i(\mu^T,\Sigma^T)\to-1$.
5. Lemma EC.5 (p. ec7): if $\liminf_T\nu^*_i(\mu^T,\Sigma^T)=-1$ for all $i$, then every $\Sigma^T_{i,i}\to0$.

Significance

Theorem 1 is the only theoretical guarantee the paper gives for cPDE; the rest of the paper is computational (bounds, comparators, experiments). It also covers, through the same sandwich argument, the cheaper variants cPDELower and cPDEUpper (Corollary 1), which are not part of this mission. A consistent policy cannot lock onto a wrong treatment, which is the property a trial designer needs before comparing finite-horizon performance.

The result is proved on paper but has no machine-checked proof. Formalizing it requires a correlated-Gaussian Bayesian learning model, optimal stopping indices defined as suprema over stopping times, and the XFC consistency argument, none of which exist in Lean. The paper's proof also routes Lemma EC.4 through an upper bound that is false as printed (see below), so a checked proof replaces that step with a correct one.

Difficulty

The obvious route bounds $\nu^*_i$ above by a one-step index with a fixed lookahead $\bar\tau$, as the paper's Lemma EC.1 does. That bound fails: $\bar\tau$ of (EC.11) changes under a change of currency while every index is invariant. For $M=2$, $\mu=(0,10^{-3})$, $\Sigma=\mathrm{diag}(10^{-6},10^{-6})$, $\lambda=(10^{-4},10^{-4})$, $c=(10^{-7},10^{-7})$, the formula gives $\bar\tau=1$ and $\nu^{cKG_1:1}_1\approx-1$, while the lookahead $T\equiv242$ already yields a value above $240$. Any upper bound on $\nu^*_i$ must instead be uniform over stopping times of unbounded length, and showing that it tends to $-1$ needs $(\Sigma^T_{i,j})^2/\Sigma^T_{i,i}\to0$ along posterior covariances, not only $\Sigma^T_{i,i}\to0$.

The second difficulty is the "finitely sampled arms" half of the argument (Lemmas EC.3, EC.5): an arm whose variance stays positive must keep a one-step value of sampling bounded away from zero, even while correlated arms are learned. This uses almost sure convergence of the posterior means and the structure of the piecewise linear terminal reward.

Formalization scope

Arms are Fin M (0-based) and time $t$ counts observations, $t=0$ being the prior. The trial lives on the canonical space $\theta\in\mathbb R^M$ times an array of standard normal noises $\varepsilon_{i,k}$, with law multivariateGaussian µ0 Σ0 times an infinite product of gaussianReal 0 1; the $k$-th sample of arm $i$ is $\theta_i+\sqrt{\lambda_i}\,\varepsilon_{i,k}$. The index $\nu^*_i$ is built on its own auxiliary space (a prior draw of $\theta_i-\mu_i$ and i.i.d. noise), not as a conditional expectation on the trial space.

Committed conventions, each a disclosed reading of the page:

• $\nu^*_i$ is (EC.8). The printed definition (15) omits $-\frac1{c_i}\max_j\mu_j$; with (15) Theorem 1 ii) would be false.
• The supremum in (EC.8) is a real sSup over stopping times of the auxiliary filtration with $1\le T_i\le N$ for some $N$; this has the paper's value and keeps every expectation finite.
• Ties in the cPDE argmax go to the least index (the paper: randomly). Every arm is eligible at every time ($\mathcal M_t=\mathcal M$), so Assumption 1 iii) is trivial.
• Theorem 1 ii) and Lemmas EC.4–EC.5 are read with $(\mu^T,\Sigma^T)$. Theorem 1 iv) is uniqueness of the maximizer of $\theta$ plus eventual agreement of the unique maximizer of $\mu^T$. The $L^2$ claim is MemLp plus eLpNorm → 0.
• "liminf $=-1$" in Lemmas EC.3, EC.5 is "for every $\varepsilon>0$, the index is below $-1+\varepsilon$ infinitely often"; since both indices are $\ge-1$ this is the printed hypothesis. Lemma EC.4 is stated for every sample path.

Trivializing formalizations are ruled out: $\nu^*_i$ is defined from $(\mu,\Sigma,\lambda_i,c_i)$, not a parameter, a fixed-lookahead index or a supremum over non-adapted times; the policy is defined, not assumed; $\mu^t$ and $\Sigma^t$ both come from (8); the $L^2$ part does not use an integral that is $0$ for non-integrable functions; iv) asserts uniqueness; and the false upper bound of Lemma EC.1 is not posed or used.

A complete development needs Gaussian conditioning for the update (8) (that $\mu^t=\mathbb E[\theta\mid\mathcal F_t]$), the closed form $\Sigma^t=(\Sigma_0^{-1}+\mathrm{diag}(n^t_k/\lambda_k))^{-1}$, optional stopping for uniformly integrable martingales, measurability of the index, and the XFC argument. The Gaussian-update and optional-stopping parts are reusable for other Bayesian ranking-and-selection results; contributions of those as separate lemmas are welcome.

Selected references

• S. E. Chick, N. Gans, Ö. Yapar, Bayesian Sequential Learning for Clinical Trials of Multiple Correlated Medical Interventions, SSRN 3184758 (INSEAD Working Paper 2020/40/TOM/ACGRE), version of August 31, 2020. https://ssrn.com/abstract=3184758
• J. Xie, P. I. Frazier, S. E. Chick, Bayesian Optimization via Simulation with Pairwise Sampling and Correlated Prior Beliefs, Operations Research 64(2):542–559, 2016.
• P. I. Frazier, W. B. Powell, S. Dayanik, The Knowledge-Gradient Policy for Correlated Normal Beliefs, INFORMS Journal on Computing 21(4):599–613, 2009.
• S. E. Chick, P. I. Frazier, Sequential Sampling for Selection with Economics of Selection Procedures, Management Science 58(3):550–569, 2012.
• D. Williams, Probability with Martingales, Cambridge University Press, 1991.