Operations Research

Motivation

Networks of autonomous sensors — machines on a factory floor, vehicles, devices in the Internet of Things — each measure a common environment with their own noise and can improve their estimates by asking other sensors for theirs. Communication capacity is limited, so each sensor must decide whom to ask, and the answer it receives is useful only to the extent that it understands how the other sensor turns measurements into estimates. Saghafian, Tomlin and Biller (SSRN 3124417, version of October 16, 2020; published in Manufacturing & Service Operations Management, 2021) model this as a dynamic target-selection problem and ask which communication network forms in the long run. Their abstract leads with the answer: each sensor eventually settles on a constant target set, which is sample-path dependent. With known, pairwise distinct qualities this target set is a single sensor (Proposition 4, p. 21). This mission formalizes that result.

Setting

There are $n$ sensors $N = \{1, \dots, n\}$. Sensor $i$ has a quality $q_i > 0$: its measurement of the state has noise variance $1/q_i^2$. Sensor $i$ starts with initial familiarities $v_{ij0}, w_{ij0} > 0$ with each other sensor $j$, the precisions of its initial Gaussian beliefs about $j$'s inference parameters. A sample path $S_\infty = (s_0, s_1, s_2, \dots)$ is the sequence of realized states, an arbitrary sequence of reals.

The familiarity function of $i$ with $j$ in period $t$ is a function $\psi_{ijt} : \mathbb R \to \mathbb R$. It starts at

$$\psi_{ij1}(s) = \frac{v_{ij0}^2 w_{ij0}^2}{w_{ij0}^2 + v_{ij0}^2 s^2} \qquad (12)$$

In period $t$, after $s_{t-1}$ is revealed, sensor $i$ targets the sensor of least signal variance

$$j^*_{it} = \arg\min_{j \in N\setminus\{i\}} \frac{q_j^2 + 1/\psi_{ijt}(s_{t-1})}{q_j^4}, \qquad (10)\text{–}(11)$$

with ties broken toward the lower index (footnote 11). Writing $a_{ijt} = 1$ if $j^*_{it} = j$ and $0$ otherwise, the familiarity grows by the stickiness factor:

$$\psi_{ij,t+1}(s) = \psi_{ijt}(s) + f(q_i,q_j)\,a_{ijt}, \qquad f(q_i,q_j) = \frac{1+q_i^2}{q_j^2(1+q_i^2+q_j^2)}. \qquad (14)$$

The long-run contacts of $i$ along $S_\infty$ are (Definition 2)

$$T_i(S_\infty) = \{\, j \in N\setminus\{i\} : \lim_{t\to\infty} \psi_{ijt}(s_{t-1}) = \infty \,\}. \qquad (20)$$

In Lean these are Instance (q, v, w), psi1, sigma2, stick, lowArgmin, the joint recursion fam/target, count and longRunContacts in IoTFusion.KnownQuality.

Formalization targets

Goal: Proposition 4 (p. 21)

If the qualities are asymmetric ($q_j \neq q_{j'}$ for $j \ne j'$, Definition 3), then for every sample path

$$|T_i(S_\infty)| = 1 \qquad \text{for all } i \in N.$$

No hypothesis on the state process is involved: the statement holds path by path.

Milestones

1. Proposition 2 (p. 15): the closed form $\psi_{ij,t+1}(s) = \psi_{ij1}(s) + f(q_i,q_j)\sum_{l=1}^{t} a_{ijl}$ (15).
2. Remark 1 (p. 20): $j \in T_i(S_\infty)$ iff $i$ targets $j$ infinitely often.
3. Lemma 2 (p. 21): for every $\epsilon > 0$ there is a fixed threshold $\bar\psi_\epsilon$ such that $\psi_{ijt}(s_{t-1}) > \bar\psi_\epsilon$ and $q_j/q_{j'} > 1+\epsilon$ imply $j^*_{it} \ne j'$.

Supporting items: $T_i(S_\infty) \ne \emptyset$ for $n \ge 2$ (long_run_contacts_nonempty); each sensor eventually targets one fixed sensor (eventually_constant_target, the wording of p. 5); and the rank-one precision identity (EC.66).

Significance

Proposition 4 says that, with known and distinct qualities, the long-run communication network is a functional graph — every sensor has out-degree one — although which graph forms depends on the realized states, and a sensor's eventual partner need not be the highest-quality sensor available. The paper builds on it its description of the long-run network as a random directed graph (Propositions 5–6) and its managerial discussion of early-period "momentum" in familiarity.

The result is proved in the paper; nothing in it is machine-checked. The work here is a formal proof of the deterministic core, including the existence half $T_i \neq \emptyset$, which the printed proof (p. ec22) does not give: it shows only $|T_i| \le 1$.

Difficulty

Every statement is elementary in isolation; the difficulty is that the target sequence is defined by a feedback loop. The target of period $t$ depends on familiarities, which depend on all earlier targets, which depend on earlier states. Statements about "infinitely often" therefore cannot be reduced to the behavior of any single function of $t$ fixed in advance.

The tempting argument "the highest-quality sensor eventually wins" is false: a sensor that becomes familiar early with a lower-quality partner can keep choosing it forever, so no fixed candidate for the unique contact exists. The uniqueness argument must instead compare two putative long-run contacts with each other, using a familiarity threshold that does not depend on the familiarity with the worse one (Lemma 2), and the existence half needs a separate counting argument over the finitely many possible targets.

Formalization scope

• Sensors are Fin n (0-based) with $n \ge 2$ on the existence statements; for $n = 1$ there is no other sensor and $T_i = \emptyset$.
• Periods are 0-based: Lean step $k$ is the paper's period $k+1$, the target at step $k$ uses the state $s_k$, and fam P i s k is $\psi_{ij,k+1}$.
• $q_i > 0$, and $v_{ij0}, w_{ij0}$ finite and positive, are theorem hypotheses (the paper's standing assumptions; its limiting case "fully knows", $v = w = \infty$, is not posed).
• Ties go to the lower index; "$\lim = \infty$" is Filter.Tendsto … atTop atTop; $|T_i|$ is Set.ncard; asymmetry is Function.Injective q.
• The familiarity function is defined by (12) and (14), the paper's familiarity dynamics. The paper derives (14) by Bayesian updating of the scalar $\hat\alpha_j + \hat\beta_j s_{t-1}$. Under the joint Gaussian beliefs, the update is exact for the precision at the realized state $s_{t-1}$ (the item (EC.66)), but at other states $s$ the posterior precision grows by less than $f$. Proposition 2(i) "for any $s$" is therefore a modelling choice. Every later result of the paper is derived from (15), so the dynamics (12) + (14) is the paper's operative model. Whether Proposition 4 survives under the exact bivariate posterior is open and not posed.
• Not posed: Propositions 5–6. Proposition 5's step "(EC.87): at $t^*$ the sets $T_i(S_\infty)$ are all determined" does not follow. Even with Gaussian innovations, a continuation of the path through a state near $0$ after any $t^*$ can make a never-targeted higher-quality sensor the unique long-run contact, so the printed claim fails without further assumptions on the state process. Lemma 1, Proposition 3 and Proposition 7 (unknown qualities) are outside this mission.
• Lemma 2's threshold depends on the pair $(j, j')$ in the paper's proof; the statement fixes the instance first and asks for one threshold per $\epsilon$, uniform over paths, sensors and periods (the maximum over the finitely many pairs).
• Trivializations ruled out: the target ranges over $j \neq i$ only, with a specified tie-break; familiarity and target form one trajectory determined by the instance, the sensor and the path, with no free history argument; $T_i$ is defined by divergence of $\psi_{ijt}(s_{t-1})$, not by target counts; the goal is $|T_i| = 1$, not $\le 1$; and it quantifies over every real path, with no AR(1) or typicality hypothesis.
• Infrastructure: none beyond Mathlib (finite sets, filters, $2\times2$ matrices for (EC.66)). Proofs of the milestones, of the existence half and of the goal are welcome in any order. A general lemma that "a sequence in a finite set takes some value infinitely often" with the matching Set.ncard bookkeeping would be reusable.

Selected references

• S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, SSRN 3124417, version of October 16, 2020. https://ssrn.com/abstract=3124417
• S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0958

Motivation

Firms increasingly delegate the generation of new concepts (product designs, advertising campaigns, engineering prototypes) to outside providers such as design agencies and engineering consultancies. The client cannot dictate how hard the provider works; it can only decide when to stop asking for new solutions. Two practices are common. Under a flexible stopping policy the client keeps the right to stop or continue after each submitted solution. Under a committed stopping policy the client commits in advance to stop, and pay, as soon as a feasible solution arrives. Classical search theory says that keeping options open is never harmful, so flexibility should dominate. Yet committed contracts are widespread in practice.

Rahmani and Ramachandran (2021) explain this by two features that the classical benchmarks omit: a deadline on the number of rounds, and a provider who adjusts its effort from round to round in response to the client's policy. In two benchmark settings, an unlimited number of rounds or a fixed provider effort, flexibility (weakly) dominates (their Lemmas 1 and 2). With a deadline and strategic effort, commitment can be strictly better, and the paper characterizes exactly when.

Setting

A client delegates a project of $T = 2$ rounds to a provider. In each round $t$ in which the client asks for a solution, the provider chooses an effort $\mu_t \in \{\mu_l, \mu_h\}$, at cost $c_l$ or $c_h$, and submits a solution of quality $v_t \ge 0$. The client pays an evaluation cost $c_I$ for each submitted solution. When the project stops with a feasible solution ($v > 0$), the client implements the best solution received and pays the provider a fixed payment $p$; if no feasible solution is found by the deadline, nothing is paid.

Quality under effort $\mu$ has distribution function

$$\Phi_\mu(x) = 1 - \mu e^{-x/k}, \qquad x \ge 0,$$

where $k > 0$ is the provider's capability: with probability $1-\mu$ the solution is infeasible ($v = 0$), and otherwise it has density $\frac{\mu}{k}e^{-v/k}$ on $(0,\infty)$. The expected quality is $k\mu$. The standing assumptions are

$$0 < \mu_l < \mu_h < 1, \qquad 0 \le c_l < c_h, \qquad c_h/\mu_h \ge c_l/\mu_l .$$

Under the committed policy, the project stops after round 1 if $v_1 > 0$. Under the flexible policy, after a feasible $v_1$ the client compares $v_1 - p$ with the expected value of a second round and stops when stopping is at least as good. The provider anticipates this and chooses its efforts by backward induction: round-2 efforts $\mu^C_2$, $\mu^{F+}_2$ (after a feasible first solution), $\mu^{F-}_2$ (after an infeasible one), then round-1 efforts $\mu^C_1$, $\mu^F_1$. Write $\Pi^C_1$ and $\Pi^F_1$ for the client's equilibrium expected profits under the two policies.

Formalization targets

Goal: Proposition 4 (a)

Fix $\mu_l,\mu_h,c_l,c_h$ satisfying the standing assumptions and a payment $p > 0$. There exist thresholds $\hat c_I(k)$ and $\bar c_I(k)$ such that for all $k > 0$ and $c_I > 0$,

$$\Pi^F_1 < \Pi^C_1 \iff \hat c_I(k) < c_I < \bar c_I(k) \ \text{ and } \ p \ge \frac{c_h - c_l}{\mu_h - \mu_l}.$$

Commitment is strictly better exactly for an intermediate range of evaluation costs, and never when the payment is below $(c_h - c_l)/(\mu_h - \mu_l)$. The thresholds are left existential, as in the paper.

Milestones

1. §3.2, property (2): the expected quality under effort $\mu$ is $k\mu$.
2. Proposition 2 (a)–(b): the flexible client stops after a feasible $v_1$ if and only if $v_1 \ge v^F_s$, for a unique threshold $v^F_s \ge 0$.
3. Proposition 3 (a): under commitment, $(\mu^C_1,\mu^C_2)$ is $(\mu_l,\mu_l)$, $(\mu_l,\mu_h)$, $(\mu_h,\mu_h)$ as $p$ crosses thresholds $\underline p \le \bar p^C$.
4. Proposition 3 (b): under flexibility, $\mu^{F+}_2 = \mu_l$, and $(\mu^F_1,\mu^{F-}_2)$ switches at $\underline p$ and $\bar p^F$.
5. Proposition 3 (c): $\bar p^C \le \bar p^F$, and $\bar p^F - \bar p^C$ is nondecreasing in $k$ and nonincreasing in $c_I$.
6. Proposition 2 (c): $v^F_s$ is nondecreasing in $k$ and nonincreasing in $c_I$.
7. Lemma 2 at $T = 2$: with the same effort in every round, $\Pi^C_1 \le \Pi^F_1$.

Significance

Proposition 4 reverses the conventional wisdom that retaining decision rights cannot hurt the decision maker. The mechanism is strategic: flexible stopping lowers the provider's expected reward for a good first solution, because the client may continue the search instead of accepting it, and so it weakens the provider's first-round effort (Proposition 3). When the payment is in $[\bar p^C, \bar p^F)$, commitment induces high first-round effort that flexibility does not, and whether this outweighs the option value of a second round depends on the evaluation cost. The result gives contract designers in innovation procurement a concrete criterion in terms of evaluation cost, capability and payment.

The paper's proofs are in an online appendix. No machine-checked version of any result in this model exists. The mission produces a formal model of a dynamic principal–agent stopping game with an atom-plus-density quality law, a verified threshold structure for the client's stopping rule, and the full equilibrium effort characterization, all of which carry over to related delegation and contest models.

Difficulty

The goal compares two equilibrium profits, each determined by a nested backward induction in which the provider's round-1 effort depends on the client's stop rule, which in turn depends on the provider's round-2 effort. The obvious approach, comparing the two policies at the same efforts, proves only Lemma 2 and points the wrong way. The comparison must instead track which of the effort regimes of Proposition 3 each policy induces, as a function of $p$ and $c_I$. The profits are piecewise in $c_I$ (the stopping threshold is zero for large $c_I$), and the claim that the strict-improvement set in $c_I$ is a single open interval requires a monotonicity argument across these pieces, uniformly in $k$. The case $p < (c_h-c_l)/(\mu_h-\mu_l)$ must be shown to give no improvement at all.

Formalization scope

The Lean development models exactly the two-round game ($T = 2$), the case the paper analyzes in §4. Effort levels form a two-element inductive type; parameters $(\mu_l,\mu_h,c_l,c_h,k)$ form a record, with $c_I$ and $p$ separate arguments. The standing assumption $c_h/\mu_h \ge c_l/\mu_l$ is written cross-multiplied; $c_l \ge 0$ is the reading that costs are non-negative. The paper's Stieltjes integrals $\int_a^\infty g\,d\Phi_\mu$ are Bochner integrals of $g$ against the density over the open ray $(a,\infty)$; the atom at $0$ appears in the separate $\Phi_\mu(a)$ terms, so no payment is charged on infeasible solutions. Ties are broken as on the page: the provider takes high effort, and the flexible client stops. The paper's restriction to payments "neither too high nor too small" (Lemma A-1 of its online appendix) is not available; every statement is posed for all $p > 0$, for which it remains true. Evaluation costs satisfy $c_I > 0$.

The model defines no stopping threshold and no effort in closed form: the stopping threshold $v^F_s$ is a theorem (Proposition 2), $\mu^{F+}_2$ is computed from the provider's objective, and the goal compares profits at the efforts the model computes, not at efforts supplied as arguments. A formalization that defined $v^F_s = k\log(k\mu_l/c_I)$, fixed $\mu^{F+}_2 = \mu_l$, or compared the policies at exogenous efforts would make the milestones trivial or prove a different theorem, and is ruled out.

A complete development needs integrals of polynomial-times-exponential functions on rays, the closed forms of the round-2 values, and finite case analysis over effort profiles. Contributions to the comparative statics (Propositions 2 (c), 3 (c)) are welcome independently of the goal.

Not formalized: Proposition 4 (b) (its $\hat c_I$ half fails under the main-text model, e.g. at $\mu_l = 1/2$, $\mu_h = 4/5$, $c_l = 1/2$, $c_h = 1$, $p = 7/2$, $c_I = 9/10$, $k \in \{6, 8\}$); Lemma 1 (infinite horizon); Proposition 1 (general finite $T$); Proposition 5 (dependent solutions); Propositions 6–8 (endogenous payments); the numerical study.

Selected references

• M. Rahmani and K. Ramachandran, Delegating Innovation Projects with Deadline: Committed vs. Flexible Stopping, Management Science 67(10):6317–6332, 2021. https://doi.org/10.1287/mnsc.2020.3800
• C. Terwiesch and C. Loch, Collaborative prototyping and pricing of custom-designed products, Management Science 50(2):145–158, 2004 (cited by the paper as the source of the infinite-round and fixed-effort benchmarks).

Why platforms share demand information

Online retail platforms such as Amazon, Alibaba's Tmall and JD.com host thousands of third-party sellers and observe every customer interaction with each of them. From these interactions the platform learns about market demand far better than any single seller can, and it sells or gives away part of that knowledge through analytics tools (Alibaba's Business Advisor is the example in the source paper). The platform earns a commission on every seller's revenue, so it cares about the sellers' total profit, and it has to decide what each seller is told.

The classic literature on information sharing in oligopoly points the other way. Gal-Or (1985) showed that Cournot competitors facing a common demand shock never voluntarily pool their private demand signals: shared information makes their strategies more correlated, and the resulting competition destroys more value than the better forecasts create. Li (2002) and others refined the conditions. Liu, Zhang and Zhang (Manufacturing & Service Operations Management, 2023; SSRN 3258109) change who decides: the signals belong to the platform, which chooses what each seller learns in order to maximize its commission. Their headline result for the unconstrained ("asymmetric full sharing") format is that the platform shares everything it knows, without any added noise, but only with a limited number of sellers, and that number is determined by the substitution between products alone.

The model

There are $N \ge 1$ sellers of substitutable products. Given quantities $q_1, \dots, q_N$, seller $i$'s price is

$$p_i = a - q_i - b\sum_{d \ne i} q_d + u, \qquad 0 < b \le 1,$$

where $u \sim N(0, \sigma)$ is a common demand shock with prior variance $\sigma > 0$. The platform observes, for each seller $i$, a signal $x_i = u + e_i$ with $e_i \sim N(0, t)$, $t > 0$, independent of everything else.

A noise matrix $M = (m_{ij})$ with entries in $[0, +\infty]$ is the platform's sharing strategy. Seller $j$ receives the noisy copy $\hat x_{ij} = x_i + \epsilon_{ij}$, $\epsilon_{ij} \sim N(0, m_{ij})$ independent, for every $i$ with $m_{ij} < +\infty$; $m_{ij} = 0$ is truthful sharing and $m_{ij} = +\infty$ means $x_i$ is withheld from seller $j$. Seller $j$'s information $y_j(M)$ is the $\sigma$-algebra generated by what he receives.

Each seller chooses a quantity measurable with respect to his information to maximize his expected profit $\pi_i = E[(1 - \alpha) q_i p_i]$, where $\alpha \in (0,1)$ is the platform's commission rate. A Bayesian equilibrium under $M$ is a profile of such strategies from which no seller gains by deviating. The platform's expected profit is $\Pi = E[\alpha \sum_i q_i p_i]$, and it chooses $M$ before the signals are realized.

Under Asymmetric Full Sharing (AFS) each seller $j$ receives all $N$ signals with one common noise level $\eta_j = m_{ij}$ (for all $i$), and the levels may differ across sellers. The benchmark is no sharing, $m_{ij} = +\infty$ for all $i, j$, with platform profit $\Pi_{NS} = \alpha N a^2/[2 + b(N-1)]^2$.

Formalization targets

Goal: Proposition 2 (optimal asymmetric full sharing)

Let $m = \min\{2/b - 1, N\}$. Among all AFS noise matrices in $[0,+\infty]^{N \times N}$ and all equilibria, an optimal strategy is to share $\{x_1, \dots, x_N\}$ truthfully with sellers $1, \dots, K^*$ and nothing with the others, where

$$K^*_{AFS} \in \big\{\lfloor m \rfloor, \lceil m \rceil\big\}, \qquad \Pi^*_{AFS} = \frac{\alpha N a^2}{[2 + b(N-1)]^2} + \frac{\alpha K^*_{AFS}\,\sigma^2}{[2 + b(K^*_{AFS} - 1)]^2\,(\sigma + t/N)}.$$

The platform and every seller do weakly better than without sharing, and every optimal truthful group has size $\lfloor m \rfloor$ or $\lceil m \rceil$.

Milestones

1. Eq. (5): under full sharing with noise $\eta$, $E[u \mid y_j] = \frac{\sigma}{\sigma + (t + \eta)/N}\cdot\frac1N\sum_i \hat x_{ij}$.
2. Eq. (4): a profile is an equilibrium iff $q_i = \frac12\big(a - b\sum_{d\ne i}E[q_d \mid y_i] + E[u \mid y_i]\big)$ for all $i$.
3. Lemma 1: the no-sharing equilibrium quantities $a/(2 + b(N-1))$ and profit $\Pi_{NS}$.
4. A seller who receives nothing earns exactly his no-sharing profit (p. 13).
5. Under AFS, an interior noise level for one seller is strictly beaten by $0$ or $+\infty$ (p. 16).
6. Proposition 1 (AFS half): optimal AFS matrices have $m^*_{ij} \in \{0, +\infty\}$.
7. Eq. (8) at every group size $K \le N$.
8. The integer maximizers of $K \mapsto K/[2 + b(K-1)]^2$ on $\{0,\dots,N\}$ lie in $\{\lfloor m \rfloor, \lceil m \rceil\}$ (p. 18).
9. Informed sellers strictly gain and the others earn the benchmark (p. 19).

Significance

The result separates two levers of information design, precision and audience, and shows that in this linear-Gaussian Cournot setting only the audience matters: the platform never degrades a signal, it only chooses how many sellers see it. The optimal audience size $\min\{2/b - 1, N\}$ depends only on the substitution parameter once the market is large, and equals one seller when products are perfect substitutes. This reverses the Gal-Or no-sharing result by changing who decides, and it explains why a commission-earning platform may rationally treat its sellers asymmetrically, which is the tension the paper's later sections on fairness and privacy constraints study.

The paper's proofs are in an online appendix. No part of this model has a machine-checked proof. The mission produces a reusable Lean layer for Bayesian games with designed Gaussian signals: information $\sigma$-algebras generated by noisy copies of shared signals, Bayesian Nash equilibrium over square-integrable strategies, and its characterization by first-order conditions in conditional expectations. Mathlib has Gaussian measures, conditional expectation and independence, but not the projection formula for jointly Gaussian vectors that eq. (5) needs.

Difficulty

The closed forms are routine once one assumes that equilibria are linear in the received average signal. The difficulty lies in what that assumption skips. First, eq. (5) is a statement about conditional expectation with respect to a $\sigma$-algebra generated by $N$ correlated Gaussian variables; it needs the Gaussian conditioning (projection) theorem, not a computation with densities. Second, the goal quantifies over all equilibria, so existence and uniqueness of the equilibrium must be proved for every noise matrix, including those with infinite entries; the paper solves the first-order condition and never discusses uniqueness. Third, Proposition 1 is an optimization over $[0,+\infty]^N$: the platform's profit is not concave in the noise levels, and the endpoint property for one seller (with the others fixed at arbitrary levels) is the step that rules out partial sharing. Restricting attention to truthful groups from the outset assumes away exactly this step.

Formalization scope

All declarations live in the namespace RetailInfoShare.AFS, with one definitions file RetailInfoShare.AFS.Model. Conventions:

• $\sigma$, $t$ and $m_{ij}$ are variances (gaussianReal 0 σ), as eq. (3) of the paper requires.
• The primitives $u$, $e_i$ and standard normals $\xi_{ij}$ are measurable and mutually independent on one probability space; the added noise is $\epsilon_{ij} = \sqrt{m_{ij}}\,\xi_{ij}$. The paper's "cov = 0" is read as independence, as its text says.
• Noise levels are in ℝ≥0∞; a signal with $m_{ij} = \top$ never enters the receiving seller's information $\sigma$-algebra.
• Equilibrium is the ex-ante best-response property over square-integrable strategies measurable for the seller's information; this is equivalent a.e. to the interim maximization of eq. (2).
• The platform's profit is the unconditional expectation (the matrix is chosen before the signals).
• Added standing hypotheses: $0 < \alpha < 1$ (never stated in the paper), and $\sigma > 0$, $t > 0$, $N \ge 1$ made explicit. Sellers are Fin N, so the paper's sellers $1,\dots,K$ are indices $0,\dots,K-1$.
• Profits and equilibria are defined from the model, never by the closed forms (4) or (8); a formalization that defined $\Pi$ by eq. (8) or optimized only over truthful groups would reduce the goal to milestone 8 and is ruled out.

Out of scope: the AIS half of Proposition 1, Proposition 3 and Lemma 2 (privacy-constrained sharing), the symmetric formats of §5, the pricing mechanism of §6, and the appendix extensions. Contributions of general infrastructure are welcome: the Gaussian conditioning theorem in Mathlib form, and existence and uniqueness of equilibria in linear-quadratic Bayesian games with Gaussian information.

Selected references

• Z. Liu, D. J. Zhang, F. Zhang, Information Sharing on Retail Platforms, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2020.0915 (preprint: SSRN 3258109, https://ssrn.com/abstract=3258109)
• E. Gal-Or, Information Sharing in Oligopoly, Econometrica 53(2), 1985. https://doi.org/10.2307/1911241
• L. Li, Information Sharing in a Supply Chain with Horizontal Competition, Management Science 48(9), 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
• L. Li, Cournot Oligopoly with Information Sharing, RAND Journal of Economics 16(4), 1985. https://doi.org/10.2307/2555502

Motivation

A manufacturer selling through several retailers rarely publishes the terms it gives each of them. Wholesale prices, slotting fees and rebates are negotiated bilaterally, and a retailer usually sees its own contract but not its rival's. Much of the supply-chain contracting literature nevertheless assumes observable contracts, and under that assumption a well-known ranking holds: the manufacturer, the channel and social welfare do better with two-part tariffs (a fixed fee plus a marginal wholesale price), while the retailers do better with plain wholesale-price contracts.

The industrial-organization literature has long known that secrecy changes the manufacturer's problem. Hart and Tirole (1990), O'Brien and Shaffer (1992) and McAfee and Schwartz (1994) showed that a manufacturer that cannot commit publicly to the terms it offers each retailer is tempted to undercut itself bilaterally: it offers one retailer a better deal, at the expense of the others, and the retailers anticipate this. Li and Liu (Manufacturing & Service Operations Management, SSRN 3339702) ask what this does to the ranking of contract types in a simple model of price competition. Their answer, Proposition 3, is that the ranking reverses when competition is intense: the manufacturer prefers wholesale prices once the competition parameter reaches $2\sqrt2$, the retailers always prefer them, and the whole industry prefers them once the parameter reaches $\sqrt3 - 1$.

Setting

A manufacturer with zero unit cost sells one product through two retailers $i \in \{1,2\}$. Retailer $i$ charges price $p_i$ and faces demand

$$D_i = 1 - p_i + \theta\,(p_j - p_i), \qquad j \ne i,$$

where $\theta \ge 0$ measures how intensely the retailers compete.

The manufacturer offers each retailer a contract $C_i = (K_i, w_i)$, a fixed fee $K_i$ and a marginal wholesale price $w_i$. In the two-part tariff game contracts range over $\{(K,w): w \ge 0\}$; in the wholesale-price game over $\{(0,w): w \ge 0\}$. The contract type is common knowledge, but retailer $j$ does not observe the terms offered to retailer $i$.

Each retailer, seeing only its own contract, accepts or rejects and chooses a price $p_i \ge 0$ and an order $Q_i \ge 0$. A retailer holding the belief $\tilde p_j$ about its rival's price conjectures the profit

$$\tilde\pi_i = p_i \min\bigl(Q_i,\ 1 - p_i + \theta(\tilde p_j - p_i)\bigr) - w_i Q_i - K_i ,$$

and $0$ if it rejects. The manufacturer earns $w_i Q_i + K_i$ from each retailer that accepts.

Because no proper subgame exists, the solution concept is the contract equilibrium with passive beliefs: a pair of contracts $(C_1^*, C_2^*)$ and, for each retailer, a strategy $\sigma_i$ giving an action at every contract of the class, such that

1. at every contract $C$, $\sigma_i(C)$ maximizes $\tilde\pi_i$ for the belief $\tilde p_j$ equal to the rival's equilibrium price, the price in $\sigma_j(C_j^*)$, so an unexpected offer does not change the belief;
2. no pair of contracts gives the manufacturer more total profit when each retailer responds to its own contract through $\sigma_i$.

The equilibrium profits are the manufacturer's $\Pi$, retailer $i$'s $\pi_i$ (computed with the actual prices), and the industry's $\Pi + \pi_1 + \pi_2$.

Formalization targets

Goal: Proposition 3

For every $\theta \ge 0$, both games have a passive-belief equilibrium, and for every equilibrium $E^T$ of the tariff game and $E^W$ of the wholesale-price game,

$$\Pi(E^T) \le \Pi(E^W) \iff \theta \ge 2\sqrt2, \qquad \pi_i(E^T) < \pi_i(E^W)\ (i = 1,2), \qquad \Pi_{\mathrm{ind}}(E^T) \le \Pi_{\mathrm{ind}}(E^W) \iff \theta \ge \sqrt3 - 1,$$

together with the strict versions of the two equivalences ($<$ iff $>$). At the thresholds the two profits coincide.

Milestones

1. Equation (2), p. 13: an accepting retailer with belief $\tilde p$ and contract $(K,w)$ charges $p = \frac{1+\theta\tilde p}{2+2\theta} + \frac w2$ and orders its conjectured demand.
2. Two-part tariffs, bilateral optimum, p. 14: against a retailer with a fixed belief, the manufacturer's best tariff is $\bigl(\frac{(1+\theta\tilde p)^2}{4(1+\theta)}, 0\bigr)$.
3. Wholesale prices, bilateral optimum, p. 17: the best wholesale price is $\frac{1+\theta\tilde p}{2(1+\theta)}$.
4. Proposition 1, p. 14: under unobservable two-part tariffs every equilibrium has $(K_i,w_i) = \bigl(\frac{1+\theta}{(2+\theta)^2}, 0\bigr)$, $p_i = \frac1{2+\theta}$, $\Pi = \frac{2(1+\theta)}{(2+\theta)^2}$, $\pi_i = 0$.
5. Proposition 2, p. 16: under unobservable wholesale prices every equilibrium has $w_i = \frac2{4+\theta}$, $p_i = \frac3{4+\theta}$, $\Pi = \frac{4(1+\theta)}{(4+\theta)^2}$, $\pi_i = \frac{1+\theta}{(4+\theta)^2}$.

Significance

Proposition 3 shows that the textbook ranking of supply-chain contracts depends on an observability assumption that is often false in practice. Under secret contracts the fixed fee loses its usual advantage: a manufacturer offering two-part tariffs cuts marginal wholesale prices to zero, retail competition becomes as fierce as possible, and all profit has to be collected through fees out of a shrinking pie. A wholesale price keeps marginal costs, and therefore retail prices, high. For $\theta \ge 2\sqrt2$ this "win-win" makes both the manufacturer and the retailers better off; as $\theta \to \infty$ the manufacturer's gain approaches 100 percent and the industry's 200 percent (p. 18).

The proposition is proved in the paper's Online Appendix. No machine-checked proof of it, or of the underlying equilibria, is known. A formalization would fix the solution concept precisely (quantification over off-path contracts, the tie-break at zero conjectured profit, the domain of contracts), establish uniqueness of the equilibria, which the page asserts only implicitly, and provide a reusable encoding of contract equilibria with passive beliefs for later missions on vertical contracting.

Difficulty

The closed forms of Propositions 1 and 2 make Proposition 3 a comparison of rational functions. The work is in the equilibrium layer. The retailers' strategies must be optimal at every contract, including contracts never offered, and the manufacturer's deviation is evaluated against those off-path responses while the rival's action is held fixed. Each retailer's belief is pinned to the rival's equilibrium price, so the equilibrium is a fixed point of a belief map composed with two optimization problems, the retailer's and the manufacturer's bilateral one. Uniqueness of the equilibrium is part of the claim, and the retailer's problem is non-smooth because of the $\min$ in sales and the accept/reject choice. At a zero marginal price the optimal order is not unique, so order quantities cannot be pinned down.

Formalization scope

Everything lives in the namespace ContractUnobs.Compare, with one definitions module, ContractUnobs.Compare.Model. Retailers are indexed by Fin 2 with rival 1 - i; all quantities are real. A contract is a structure with fields K and w; a retailer's action records accept : Bool, a price p and an order Q. IsPassiveEq θ cls E is the equilibrium condition above for a contract class cls (tariffClass or wholesaleClass); mfrProfit, retProfit and industryProfit are the realized profits.

Conventions committed to, each disclosed in the item statements:

• wholesale prices are nonnegative in both classes ($w < 0$ makes the retailer's order problem unbounded);
• retail prices are nonnegative (the paper assumes prices induce nonnegative demand, p. 11), and sales are $\min(Q, \max(0, D))$;
• a retailer whose best conjectured profit is exactly $0$ accepts (as on p. 13);
• the manufacturer is paid for quantities ordered;
• "in equilibrium" is read as a statement about every equilibrium, together with existence;
• in Proposition 3, "higher when $\theta \ge 2\sqrt2$" is read as an equivalence (weak at the threshold, strict beyond it), with the converse shown in the paper's figures.

Stating Proposition 3 with the closed-form values of Propositions 1 and 2 substituted for the equilibria is a different, nearly trivial theorem and is not the goal; the goal quantifies over equilibrium profiles, and its existence conjuncts exclude a vacuous reading.

The observable benchmark (Lemmas 1–3), the corollaries, and the extensions of §6 (buyback contracts, asymmetric retailers, downstream merger) are not part of this mission. Contributions welcome: proofs of the milestones, a general lemma on maximizing $(p-w)(A-Bp)$ over $p \ge 0$, and a reusable treatment of passive-belief contract equilibria.

Selected references

• X. Li and Q. Liu, Contract Unobservability and Downstream Competition, Manufacturing & Service Operations Management; SSRN preprint 3339702. https://ssrn.com/abstract=3339702 (published version: https://doi.org/10.1287/msom.2020.0905)
• O. Hart and J. Tirole, Vertical Integration and Market Foreclosure, Brookings Papers on Economic Activity: Microeconomics, 1990, 205–286. https://doi.org/10.2307/2534783
• D. P. O'Brien and G. Shaffer, Vertical Control with Bilateral Contracts, RAND Journal of Economics 23(3), 1992, 299–308. https://doi.org/10.2307/2555895
• R. P. McAfee and M. Schwartz, Opportunism in Multilateral Vertical Contracting: Nondiscrimination, Exclusivity, and Uniformity, American Economic Review 84(1), 1994, 210–230. https://www.jstor.org/stable/2117980

Why estimation risk matters for mean-variance portfolios

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

Lemma 1 (eq. (17))

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Conventions committed to:

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

The value-centered design problem is

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

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

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

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

Formalization targets

Goal: Theorem 1 (p. 11)

If $r_{XI}<1$, then

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4 (p. 18)

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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