Operations Research

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

Why ad blockers matter to platforms

Ad blockers remove advertising from web pages, and with it the revenue that pays for free content. By the time of this paper a large share of desktop users ran one, and publishers had three responses at hand: tolerate ad blockers, block access to users who run one (an adblock wall), or move behind a paywall. The common view was that ad blockers can only hurt ad-funded platforms.

Despotakis, Ravi and Srinivasan (SSRN 3083119, version of November 28, 2017; published in Management Science in 2020, doi:10.1287/mnsc.2020.3653) model this choice as competition between two platforms and show that ad blockers can raise platform revenue. The mechanism is a segmentation effect: users who would install an ad blocker are typically the most ad-averse, and competition over them pushes ad intensities down for everyone. Letting them block ads takes them out of the ad market, so competition for the remaining users is softer. This mission formalizes the paper's first main result, Proposition 1, together with the case analysis of its proof.

Setting

Two platforms sit at the endpoints $0$ and $1$ of a Hotelling line. Users are spread uniformly on $[0,1]$; a user at position $x$ gets intrinsic value $1-x$ from platform 1 and $x$ from platform 2, plus a common value $m$ large enough that every user joins exactly one platform (full coverage). There are two user segments:

• non-adblock users, of mass $\lambda$ and ad sensitivity $\beta$;
• adblock users, of mass $\mu$ and ad sensitivity $\gamma$, who block ads whenever a platform allows it.

The price sensitivity of all users is $1$. Each platform $i$ chooses a plan:

• Ban: ad blockers are banned, everyone sees ads of intensity $a_i \ge 0$, and the platform earns $a_i$ per user;
• Allow: ad blockers are allowed; non-adblock users see ads of intensity $a_i \ge 0$ and the platform earns $a_i$ per such user, while adblock users see nothing and generate no revenue;
• Fee: no ads, a subscription fee $p_i \ge 0$ paid by every user.

At platform 1 a non-adblock user suffers disutility $\beta a_1$ under Ban and Allow and $p_1$ under Fee; an adblock user suffers $\gamma a_1$ under Ban, $0$ under Allow and $p_1$ under Fee. Platform 2 is symmetric. Within a segment, platform 1's share is the length of the set of users who prefer it,

$$s(d_1, d_2) = \max\Big\{0, \min\Big\{1, \tfrac{1 + d_2 - d_1}{2}\Big\}\Big\},$$

where $d_1, d_2$ are the two disutilities, and the revenue $r_i$ is the sum over the segments of mass × share × payment per user.

The game has two stages. Platforms first choose plans $(s_1, s_2)$; then they choose decision values $(d_1, d_2)$, and a stage-2 equilibrium is a pure Nash equilibrium of the resulting revenue game over $d_i \ge 0$. A plan profile with its decision values is an equilibrium if the decision values form a stage-2 equilibrium and, after any unilateral change of plan by either platform, the new subgame has a stage-2 equilibrium in which the deviator earns no more.

The benchmark is the world without ad blockers: plans are Ads (identical to Ban: everyone sees ads, the adblock-prone segment keeps sensitivity $\gamma$) and Fee.

Formalization targets

Goal: Proposition 1

For $\lambda, \mu, \beta, \gamma > 0$:

1. if

$$\beta \le \frac{\lambda(3\lambda+4\mu)^2}{(\lambda+\mu)(3\lambda+2\mu)^2} \quad\text{and}\quad \frac{\lambda+\mu\,\gamma/\beta}{(3\lambda+4\mu\,\gamma/\beta)^2} \le \frac{\lambda}{(3\lambda+2\mu)^2},$$

then (Allow, Allow) with $a_1 = a_2 = 1/\beta$ is an equilibrium, each platform earning $\lambda/(2\beta)$; 2. if $\gamma/\beta \ge 2 + \mu/\lambda$ and $\beta \le \lambda/(\lambda+\mu)$, then the same holds and $\lambda/(2\beta)$ is at least each platform's revenue in every symmetric stage-2 equilibrium of the benchmark subgames (Ads, Ads) and (Fee, Fee).

Milestones

The milestones follow the numbered cases of the appendix proof: the share formula (case 1), the benchmark subgames (Ads, Ads) and (Fee, Fee) (cases 1–2), the on-path subgame (Allow, Allow) (case 5), the deviation subgames (Ban, Allow) and (Fee, Allow) (cases 8–9), and the three algebraic facts of p. 44 that turn revenue comparisons into conditions on $\beta$ and $\gamma/\beta$.

Significance

Proposition 1 is the paper's answer to whether ad blockers must hurt publishers: in a region of parameters both platforms prefer to let ad blockers in, and both earn more than without ad blockers. It underlies the paper's welfare result (Proposition 2) and the extensions with an intermediate segment, whitelisting and content investment, which all build on the same equilibrium.

The result is proved on paper by first-order conditions of interior solutions. It is not formalized anywhere. A machine-checked version has to deal with what the first-order derivation leaves out: corner responses where a platform abandons a segment, global rather than local optimality of each response, and uniqueness where it is needed. Two of the paper's intermediate claims fail as printed in parts of the parameter region (see Difficulty), and one threshold on p. 44 contains a typo; the formal statements here are the corrected versions, so a completed proof also certifies the corrected thresholds.

Difficulty

The obvious argument solves the first-order system $\partial r_1/\partial d_1 = \partial r_2/\partial d_2 = 0$ in every subgame. That gives candidate points, not equilibria. With clipped shares the revenue of a platform is only piecewise quadratic in its decision, and a platform can do better by moving to a corner, for example by raising its ad intensity until it serves no adblock user at all.

This happens in exactly the region where Proposition 1 matters. In the (Ban, Allow) deviation subgame the interior point printed in the paper is not a stage-2 equilibrium for large $\gamma/\beta$: at $(\lambda,\mu,\beta,\gamma) = (1,2,1/10,1)$ the Ban platform earns about $0.75$ there but about $2.97$ by serving only non-adblock users. The proof must therefore find the right stage-2 equilibrium regime by regime and check every unilateral deviation globally over $[0,\infty)$. Similarly, the benchmark (Ads, Ads) point is not an equilibrium for large $\gamma/\beta$, which is why the benchmark comparison quantifies over actual equilibria.

Formalization scope

• All parameters and decision values are real numbers; $\lambda, \mu, \beta, \gamma > 0$ are hypotheses of the goal; each milestone assumes positivity of the parameters it uses, and decision values range over $[0,\infty)$.
• Market shares are clipped to $[0,1]$. A formalization with the unclipped share $(1 + d_2 - d_1)/2$ is ruled out: it turns every revenue into a global quadratic, makes every printed first-order point an equilibrium, and trivializes the corner analysis that the result actually requires.
• The intrinsic value $m$ cancels under full coverage and appears only in the share milestone, which identifies the clipped share with the Lebesgue measure of the users preferring platform 1.
• Platform 2's revenue is platform 1's with the roles exchanged.
• The equilibrium notion requires a stage-2 equilibrium on the path and, after each unilateral plan deviation, some stage-2 equilibrium leaving the deviator no better off; play after joint deviations is unconstrained.
• The benchmark is the main game with plans restricted to Ban (= Ads) and Fee. Its comparison is with every symmetric stage-2 equilibrium; when (Ads, Ads) has none, that clause is vacuous, while (Fee, Fee) always has the unique equilibrium $p_1 = p_2 = 1$.
• "Better off" is the weak inequality, as in the paper's conditions.

The development needs only real analysis of piecewise quadratic functions and Lebesgue measure of intervals. The model definitions (Hotelling share with full coverage, pure Nash equilibrium over nonnegative reals) are reusable for other duopoly models. Proofs of individual milestones are welcome independently; the goal follows from them by the case analysis described above.

Selected references

• A. Despotakis, R. Ravi, K. Srinivasan, The Beneficial Effects of Ad Blockers, SSRN working paper 3083119, version of November 28, 2017. https://ssrn.com/abstract=3083119
• A. Despotakis, R. Ravi, K. Srinivasan, The Beneficial Effects of Ad Blockers, Management Science, 2020. https://doi.org/10.1287/mnsc.2020.3653
• H. Hotelling, Stability in Competition, The Economic Journal 39(153), 41–57, 1929. https://doi.org/10.2307/2224214

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

Why customized returns matter

Many sellers accept returns of standard goods but restrict returns of customized goods. A customized item is more likely to fit its buyer, yet it may be harder for the seller to recover value when it comes back. Choosing a return policy therefore changes both what customers buy and how many units they return. Esenduran, Letizia, and Ovchinnikov study this tradeoff in a two-product market and show that permitting customized-product returns can, for some parameters, raise the firm's profit while reducing its total return volume (accepted manuscript, Proposition 2, p. 11). The result is an existence statement about a firm's optimal policy, not a claim that permissive returns always have this effect.

Consumers, products, and the firm's policy

A unit mass of consumers has taste $t$ uniformly distributed over $[0,1]$. The standard product is located at $t=1$ and has baseline willingness to pay $\mathrm{WTP}_s(t)=t$. The customized product changes both a direct-value attribute and a taste-related attribute; its baseline willingness to pay is $\mathrm{WTP}_c(t)=1+\alpha_c-(1-\beta_c)(1-t)$. Here $\alpha_c$ may have either sign, while $0<\beta_c\le1$ measures the taste improvement. These are the paper's normalized expressions, with the reservation value set to one (§2.2, pp. 5–6).

Product $i\in\{c,s\}$ matches a consumer's needs with probability $m_i$; after a mismatch, the consumer values it at only $\theta\mathrm{WTP}_i(t)$, where $0\le\theta<1$. The firm chooses a nonnegative price $p_i$ and a nonnegative return fee $f_i$ for each product. A buyer learns whether the product matches after buying and keeps it exactly when keeping gives at least the payoff $-f_i$ from returning it. Before purchase, the consumer compares the two expected utilities, including this return option, and buys only if the best one is positive. A tie between products goes to the standard product. These rules determine the buyer volumes $Q_i$, the mismatch-return segments $Q_i^R$, and the keep segments $Q_i^K$. The expected number of returns is $R_i=(1-m_i)Q_i^R$ (§2.3, p. 7; problem (3), p. 10).

With production cost $k_i$ and recovered value $r_i$ on a returned unit, the firm's expected profit and total return volume are

$$\Pi(p,f)=\sum_{i\in\{c,s\}}\bigl[Q_i(p_i-k_i)+R_i(f_i+r_i-p_i)\bigr], \qquad R_{\mathrm{tot}}=R_c+R_s.$$

An optimal policy maximizes this profit over all nonnegative prices and fees. In the paper's disallow counterfactual, the standard product's price and fee remain at the original optimal policy's values, while the customized price and fee are chosen to maximize profit subject to $R_c=0$. The proof writes this as problem (5) in the Solution 2 region (Online Appendix pp. 14–15).

Formalization targets

The goal is Proposition 2. There exist admissible parameters and an original optimum such that customized returns occur, and for every original optimum and every associated disallow-counterfactual optimum,

$$R_c^*>0,\qquad \Pi^*>\Pi_{\mathrm{no\ }c\mathrm{\ returns}}^*,\qquad R_{\mathrm{tot}}^*<R_{\mathrm{tot,no\ }c\mathrm{\ returns}}^*.$$

Both optimization problems must attain their maxima. The quantified claim is what “can increase profits and reduce total returns” means in this model; it does not replace an optimum by a preselected formula.

Three milestones trace the part of the paper used for this existence result. Solution 2 characterizes an original optimum with positive customized-return and standard-return segments, a positive standard-keep segment, and no customized-keep segment. Solution 2b characterizes the corresponding optimum when customized returns are disallowed and the standard terms stay fixed. Their returns identity expresses the difference in total return volumes as a factor containing $W=m_s(1-m_c)-m_c(1-m_s)(1-\beta_c)$; away from the boundary $r_s=r_s^{SB2}(r_c)$, that difference is negative exactly when $W<0$ (Online Appendix pp. 4–5, 15).

What the result establishes

The paper's claim separates the total number of returns from the permissiveness of one product's return policy. A permissive customized policy may induce some consumers to switch away from standard goods. Since customized goods match preferences more often, those switches can outweigh returns from newly served buyers; profit can rise at the same time. Thus a firm cannot infer total return volume by looking only at the customized product's own returns (§3.2, p. 11).

The paper proves the result analytically. This mission records its model, optimization comparison, and three central statements in Lean; the theorem proofs are open formalization work. A completed development would certify the global optimum comparison, including existence and all admissible nonnegative policies, as well as the algebraic segment identity. The definitions of consumer choice, return volumes, and the constrained counterfactual can also support formalizations of the paper's other solution regions and robustness results.

Where the formalization is difficult

The return option makes each consumer's expected utility piecewise linear in taste. Which product a consumer buys depends on the upper envelope of two such functions and zero, so the volumes change formula when thresholds cross. The firm's objective is consequently piecewise rather than one differentiable expression on the full policy space. A stationary formula for one segment ordering is insufficient to establish a global optimum; the proof must account for policies on other orderings and their boundaries. The paper's displayed Solution 2 region also includes parameter points where a fee becomes negative or a segment leaves $[0,1]$, so those expressions alone do not characterize the intended interior policy (Online Appendix A.2, pp. 3–5).

Formalization scope

Lean represents every parameter, price, fee, threshold, profit, and segment size as a real number. Consumer volumes are Lebesgue measures of subsets of $[0,1]$; a consumer purchases only when expected utility is strictly positive. The latter convention follows the proof of Proposition B1 and Table 2, which exclude a buyer with nonpositive expected utility. The paper's p. 7 prose uses a weak inequality; at a zero fee that choice could create a positive-volume tie incompatible with its return accounting. The standard product wins ties between products. The standard product has $\alpha_s=\beta_s=0$ in the definitions (Table 1, p. 7; Online Appendix p. 11).

The standing assumptions include Table 1's parameter ranges, the ordering condition $m_s>\mu_c(1-\beta_c)$, $\mu_i>k_i$, and $m_i+r_i(1-m_i)>k_i$. The lower bounds $m_s\ge0$ and $k_s\ge0$ are made explicit. Milestone formulas that divide by $\theta$ or $1-\beta_c$ assume $\theta>0$ and $\beta_c<1$. The Solution 2 and 2b milestones additionally require an interior feasible region: positive return segments, a positive standard-keep segment, nonnegative standard fee, and less than full market coverage. These added conditions select the solution described in the appendix. The displayed customized price of Solution 2 is not used: at the rational consistency witness it conflicts with the displayed segment sizes. The statements retain those segment sizes and the standard terms, which are the quantities needed for Proposition 2.

The goal quantifies over the firm's actual feasible policies and asserts that both optima exist. Defining “optimal” through a closed-form candidate, omitting the disallow maximum, or using a zero-volume population would erase the comparison. Contributions may address global optimality, the consumer threshold and measure calculations, the counterfactual optimum, or the returns identity. The measure and piecewise optimization results would be reusable for other product-line models.

Selected references

• Esenduran, G., P. Letizia, and A. Ovchinnikov, Customization and Returns, accepted manuscript, Management Science, accepted December 13, 2021. SSRN 3444244. This mission cites the manuscript's printed pages and its Online Appendix.
• Esenduran, G., P. Letizia, and A. Ovchinnikov, Customization and Returns, Management Science, 2022. DOI: 10.1287/mnsc.2022.4305. The typeset pagination is not used for the formal statements.

Motivation

A seller choosing a simple way to sell several items faces a problem when one buyer values both individual items and combinations. Pricing each item or offering the entire set as one bundle is easy to describe; an optimal lottery menu can use many more options. The question is how much revenue this simplicity can cost. Eden, Feldman, Friedler, Talgam-Cohen and Weinberg give a guarantee controlled by how many potentially valuable combinations contain any one item. Their result applies to valuations with complements and feasibility constraints that also create substitutes. The preprint used here is arXiv:1612.04746v2; its theorem and page numbers are the source for this mission.

The paper's lower-bound examples show that dependence on the complementarity degree is needed, up to constants, for the mechanisms under study (§6, pp. 13–15). The mission targets the upper bound, including its stated constant. It does not claim that the stronger lower-bound examples have already been formalized.

Setting

Let $M$ be a finite set of items. A hyperedge $T\subseteq M$ represents a combination with a nonnegative bonus $w(T)$. A fixed feasible family $C\subseteq 2^M$ is downward closed and contains the empty set. A buyer receiving bundle $S$ can obtain the bonuses of a feasible subset $T\subseteq S$, so the induced valuation is

$$v_w(S)=\max_{T\subseteq S,\ T\in C}\sum_{U\subseteq T}w(U).$$

Each weight $w(T)$ is sampled independently from a distribution $D'_T$ with finite support; together they induce a population $D$ of valuations. As in §2, pp. 4–5, weights outside $C$ are zero, and $w(\varnothing)=0$ normalizes the empty bundle's value. The population has complementarity degree at most $d$ when every item belongs to at most $d$ hyperedges for which a positive weight is possible.

A mechanism gives each reported valuation in the finite type space $V$ a lottery over bundles and a payment. The buyer evaluates a lottery by expected value. The mission uses incentive compatibility and individual rationality for truthful mechanisms: a buyer prefers their own report, and participating gives nonnegative utility. Let $\operatorname{Rev}(m)$ be such a mechanism's expected payment.

BREV is the best expected revenue from a single price $p$ for the grand bundle, namely $\sup_p p\Pr[v_w(M)\ge p]$. SREV* is a conservative separate-price benchmark. At item prices $\vec p$, item $i$ contributes its price only when some bundle containing $i$ has strictly positive surplus and every bundle omitting $i$ has nonpositive surplus. The supremum is over all real price vectors; it is the paper's $\operatorname{SREV}^{*}$, rather than a favorable tie-breaking convention for an ordinary item-pricing menu (§2, p. 5).

Formalization targets

The goal is Theorem 3.2, p. 6. For every population of degree at most $d$ and every truthful mechanism $m$,

$$\operatorname{Rev}(m)\le(4d+16)\max\{\operatorname{BREV}(D),\operatorname{SREV}^{*}(D)\}.$$

The milestones follow the paper's two benchmark terms. Corollary 3.1, p. 6 bounds revenue by NON-FAVORITE plus SINGLE. Theorem 4.6, pp. 9–10 specifies a partition of hyperedges returned by Partition-Edges, and Proposition 4.1, p. 7 bounds SINGLE by $4d\operatorname{SREV}^{*}+4\operatorname{BREV}$. For NON-FAVORITE, Lemma 5.1, p. 10 introduces the CORE and TAIL terms at a cutoff $t$; Propositions 5.5 and 5.7, pp. 12–13 bound those terms; and Proposition 5.10, p. 13 gives $\operatorname{NON\text{-}FAVORITE}\le12\operatorname{BREV}$. These seven statements are the mission's intermediate targets.

Significance

The theorem gives a concrete revenue guarantee for two simple selling formats even though the valuation can contain overlapping complementary bonuses and feasibility constraints. It says that, within the stated finite-support model, the better simple benchmark captures at least a $1/(4d+16)$ fraction of the revenue of any truthful, individually rational lottery mechanism. The paper also establishes lower bounds showing that a factor growing with $d$ is inherent for its simple-mechanism comparison (§6).

The mathematical result is proved in the paper. The Lean goal and milestones here are statements awaiting proofs; compilation checks their types and definitions, not their truth. Completing them would create a reusable finite product model for mechanism-design arguments, an explicit version of the strict separate-sale benchmark, and a machine-checked combinatorial partition theorem. Those pieces can support later work on revenue bounds with constrained bundles.

Difficulty

The first apparent shortcut is to compare revenue directly with the best bundle price. It cannot account for instances where value is spread among item prices, while item pricing alone cannot account for large complementary bonuses. The paper therefore has to control two different contributions to its revenue benchmark. In the favorite-hyperedge contribution, overlapping edges make independently chosen bundle prices interact. In the nonfavorite contribution, large weights require a different estimate from bounded weights. The duality benchmark also uses ironed virtual values for discrete distributions; replacing them by un-ironed slopes can change SINGLE. These are specific obstacles to closing the Lean goal, beyond the routine finite-sum bookkeeping (§§3–5).

Formalization scope

The Lean model uses Finset bundles, a downward-closed finite family $C$, and positive masses on finite supports for each hyperedge law. A finite product support gives the expectation and probability operators. The valuation is computed from a realized hypergraph; mechanisms operate on the resulting finite valuation type space. The goal quantifies over each valid mechanism. It does not use a real supremum over mechanism revenues, whose default value on an unbounded set would make the statement misleading. BREV and SREV* do use real suprema over all real prices, matching the paper's price domains.

Favorite regions compare nonempty hyperedges, with an injective rank resolving ties. The paper specifies a lexicographic tie rule; quantifying over ranks includes that choice. SINGLE uses the slope of the least concave majorant of the finite revenue curve, the discrete ironed virtual value implicit in the paper. Figure 1 is represented by its actual sweep and loop, and Theorem 4.6 excludes the empty hyperedge because that input prevents the stated procedure from terminating. Proposition 5.5 specifies $t\ge0$, the domain on which its printed inequality holds. These conventions and the explicit individual-rationality requirement prevent zero-valued or arbitrary-payment cases from trivializing the target.

Contributions toward the published milestones are welcome, including the duality and ironing argument behind Corollary 3.1, the combinatorial theorem for Figure 1, and the finite-support estimates for CORE and TAIL. The listed milestones do not include every supporting lemma from the paper; the remaining posted-price, concentration, and independent-event results may be developed as reusable lemmas where needed. No milestone is weakened to make its proof fit the current library.

Selected references

• A. Eden, M. Feldman, O. Friedler, I. Talgam-Cohen and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for a Buyer with Complements, arXiv:1612.04746v2, 2017; published in Operations Research, 2021. Preprint.

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

When a bank or firm in a network of mutual obligations cannot meet its liabilities, some rule must decide how much each debtor pays each creditor. The rule used almost universally in the systemic-risk literature is the proportional rule of Eisenberg and Noe (2001): every agent pays its liabilities in full if it can, and otherwise distributes its whole asset value over its creditors in proportion to their claims. Central banks and regulators use it to measure contagion in interbank markets; Elsinger, Lehar and Summer (2006) apply it to the 881 banks reporting to the Austrian Central Bank, and Upper (2011) surveys fifteen such studies.

The rule is usually taken as given. Csóka and Herings (2021) ask which properties of a bankruptcy rule single it out, without assuming in advance that payments depend only on an agent's asset value and liabilities. Their answer is an axiomatization: five basic axioms together with one axiom on splitting an agent into identical copies.

For claims problems (one estate, several claimants) the proportional rule has classical characterizations through nonmanipulability by merging and splitting claims (O'Neill 1982, de Frutos 1999, Moreno-Ternero 2006, Ju, Miyagawa and Sakai 2007). Csóka and Herings show that the network analogue of nonmanipulability is too strong (no rule satisfies it together with the basic axioms) and replace it by invariance to mitosis.

Setting

Agents are natural numbers. A financial network $F = (N, z, L)$ consists of a nonempty finite set $N \subseteq \mathbb N$ of agents, endowments $z_i > 0$ for $i \in N$, and a nonnegative liability matrix $L$ on $N \times N$ with $L_{ii} = 0$; $L_{ij}$ is what $i$ owes $j$. The class of all financial networks is $\mathfrak F$. The relative liability matrix is $\Pi_{ij} = 0$ if $L_{ij} = 0$ and $\Pi_{ij} = L_{ij}/\sum_{k \in N} L_{ik}$ otherwise.

A payment matrix is an element of $\mathcal M(N)$, the nonnegative $N \times N$ matrices with zero diagonal; $P_{ij}$ is the amount $i$ pays $j$. Agent $i$'s asset value is $a_i(N,z,P) = z_i + \sum_{j \in N} P_{ji}$ and its equity is $e_i(N,z,P) = a_i(N,z,P) - \sum_{j \in N} P_{ij}$. For rows, $P_i < L_i$ means $P_{ij} \le L_{ij}$ for all $j$ with strict inequality for some $j$.

A bankruptcy rule $b$ assigns to each $F \in \mathfrak F$ a payment matrix $b(F) \in \mathcal M(N)$ (Definition 2.1). The proportional rule $p$ assigns the solution of

$$P_{ij} = \min\Big\{\Pi_{ij}\Big(z_i + \sum_{k \in N} P_{ki}\Big),\ L_{ij}\Big\}, \qquad i, j \in N. \tag{2.1}$$

The axioms, in the order of the paper:

• claims boundedness: $b(F) \le L$;
• limited liability: $e_i(N,z,b(F)) \ge 0$;
• priority of creditors: $b_i(F) < L_i$ implies $e_i(N,z,b(F)) = 0$;
• continuity: $b(F^n) \to b(F)$ whenever $F^n \to F$, where convergence means that the populations eventually coincide and endowments and liabilities converge;
• impartiality: $L_{ij} = L_{ik}$ implies $b_{ij}(F) = b_{ik}(F)$;
• invariance to mitosis: if agent $j$ is split into $|K|+1$ identical agents $\{j\} \cup K$, each receiving the fraction $1/(|K|+1)$ of $j$'s endowment, liabilities and claims and none toward each other, then the total payments of the copies to, and from, each other agent equal $j$'s original payments, and payments among the other agents do not change.

Formalization targets

Goal: Theorem 4.2

$$\text{(a)}\quad \forall F \in \mathfrak F,\ \exists!\, P \text{ solving (2.1) for } F,$$ $$\text{(b)}\quad b \text{ satisfies the six axioms} \iff \forall F,\ b(F) \text{ solves (2.1) for } F .$$

Part (a) makes $p$ a well-defined bankruptcy rule; part (b) says that $p$ satisfies the axioms and that every rule satisfying them is $p$.

Milestones

1. Uniqueness and existence of the solution of (2.1) (Eisenberg–Noe, Theorem 2, cited on p. 2801).
2. Every solution of (2.1) gives nonnegative equities, and zero equity to any agent not paying in full (Part (I), p. 2808).
3. A limit of solutions of (2.1) along converging networks solves (2.1) for the limit network (Part (I), p. 2808).
4. The split payment matrix (A.1) solves (2.1) for the split network (Part (I), pp. 2808–2809).
5. Part (I): the proportional rule satisfies the six axioms.
6. Lemma A.1: under impartiality and invariance to mitosis, $L_{ij} = (q/r) L_{ik}$ implies $b_{ij}(F) = (q/r) b_{ik}(F)$.
7. Part II for rational liabilities, without continuity; then Part II in general.

Significance

The theorem justifies the proportional rule by properties rather than by convention. Because the axioms make no assumption on the form of the rule, consequences such as the absence of pairwise netting are derived, not assumed. Together with the paper's Theorem 5.3 (no rule satisfies the basic axioms and full nonmanipulability), it shows that invariance to mitosis is the strongest splitting requirement compatible with the basic axioms.

The result is proved on paper; no part of it, and no part of the Eisenberg–Noe clearing theory, has a machine-checked proof on this platform. A formalization contributes a reusable layer for clearing payments in financial networks: the system (2.1), its existence and uniqueness under strictly positive endowments, nonnegativity and zero-equity properties of clearing vectors, and their continuity in the data. These are the objects every stress-testing model on top of Eisenberg–Noe starts from.

Difficulty

Existence and uniqueness of a solution of (2.1) is a fixed-point statement about a nonlinear, non-contracting map; uniqueness holds only because every endowment is strictly positive, and fails without it (two agents owing each other one unit with no endowments admit both $P = 0$ and $P = L$).

In the characterization direction, impartiality only equalizes payments to equal claims, and invariance to mitosis only relates networks that differ by splitting one agent into identical copies. Neither axiom speaks directly about payments to unequal claims, and splitting reaches only ratios of positive integers. Passing from rational to real liabilities needs continuity of the rule and continuity of $p$, and the latter rests on uniqueness of the clearing vector, so the two halves of the theorem are not independent.

Formalization scope

• Model. Agents are natural numbers and populations are nonempty Finset ℕ; a fixed finite type cannot express mitosis, which creates fresh agents. Endowments, liabilities and payment matrices are functions on $\mathbb N$ (resp. $\mathbb N \times \mathbb N$) that vanish outside the population, as part of the network structure and of $\mathcal M(N)$. All quantities are real.
• Conventions. $\Pi$ is written with the page's case split. Continuity is sequential, exactly in the paper's convergence criterion (eventual equality of populations, coordinatewise convergence of endowments, liabilities and payments); the paper's topology is first countable, so this is continuity. The split network of Axiom 4.1 is a predicate fixing every coordinate of the new network; $K$ is a finite set of fresh agents and may be empty. The divisor $|K|+1$ is real.
• Added hypothesis. In Lemma A.1, $q$ and $r$ are required to be positive integers; the page writes $q, r \in \mathbb N$ and its proof splits agents into $q$ and $r$ copies.
• Goal shape. "$b = p$" is expressed as "$b(F)$ solves (2.1) for every $F$", and the goal also asserts that (2.1) has a unique solution. Without part (a) the iff would be compatible with an empty class of rules satisfying (2.1); a formalization that drops it, or that defines $p$ by choice from an unproved existence claim, is not the theorem.
• Out of scope. Nonmanipulability (Axiom 5.1, Theorem 5.3), the independence examples of Section 6 and Appendix B, and the linear-programming characterization (2.2).
• Welcome contributions. A general Knaster–Tarski proof of existence for (2.1) via Mathlib's OrderHom.lfp, the uniqueness argument under positive endowments, and lemmas on the split network (sums over the copies, the relative liabilities of copies) that serve both Part (I) and Lemma A.1.

Selected references

• P. Csóka, P. J.-J. Herings, An Axiomatization of the Proportional Rule in Financial Networks, Management Science 67(5):2799–2812, 2021. https://doi.org/10.1287/mnsc.2020.3700
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2):236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• H. Elsinger, A. Lehar, M. Summer, Risk Assessment for Banking Systems, Management Science 52(9):1301–1314, 2006. https://doi.org/10.1287/mnsc.1060.0531
• C. Upper, Simulation Methods to Assess the Danger of Contagion in Interbank Markets, Journal of Financial Stability 7(3):111–125, 2011. https://doi.org/10.1016/j.jfs.2010.12.001
• B. O'Neill, A Problem of Rights Arbitration from the Talmud, Mathematical Social Sciences 2(4):345–371, 1982. https://doi.org/10.1016/0165-4896(82)90029-4
• B. Moreno-Ternero, Proportionality and Non-Manipulability in Bankruptcy Problems, International Game Theory Review 8(1):127–139, 2006. https://doi.org/10.1142/S0219198906000825