Probability

Motivation

Optimal stopping with samples sits between two classical problems. In the secretary problem a decision maker sees items in random order, knows nothing about their values, and must stop on one; the best guarantee is $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant $\alpha^*\approx0.745$: Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017) showed that it is achieved. Real decision makers usually have neither nothing nor everything: they have a history of past observations.

Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) model this as $p$-DOS (sample-driven optimal stopping): each of $N$ items is independently placed in a history set with probability $p$, the decision maker sees the history first and then the remaining items online, and must stop on one online item. At $p=0$ this is the secretary problem; as $p\to1$ the history reveals the distribution and the problem approaches the i.i.d. prophet setting. This mission formalizes the paper's Theorem 8, which makes the second statement precise: the optimal guarantee tends to $\alpha^*$.

Timeline. Hill and Kertz (1982) compared stop-rule and supremum expectations for i.i.d. variables; Kertz (1986) completed the comparison, giving the worst-case constant $\approx0.745$ through the integral equation used below; Correa et al. (2017) gave a matching algorithm. Kaplan, Naori and Raz (2020) studied the sample-driven model with a weaker bound for small $p$; Correa, Dütting, Fischer and Schewior (2019) and Rubinstein, Wang and Weinberg (2020) studied i.i.d. values with samples from an unknown distribution. The present paper (2020–2021) gives the exact limit program and Theorem 8.

Setting

Fix $p\in(0,1)$. A stopping rule is a nonnegative function $q(t,\ell)$ of a time $t\in[p,1]$ and a rank $\ell\ge1$. For $k\ge1$ let

$$F_k(q)=\sum_{\ell=1}^{k}\int_p^1 q(t,\ell)\sum_{j=\ell}^{k}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^{\ell}\,dt .$$

The limit program SDCLP$_p$ maximizes $\alpha\in[0,1]$ over pairs $(q,\alpha)$ with

$$t\,q(t,\ell)+\int_p^t\sum_{s\ge1}q(\tau,s)\,d\tau\le1\quad(t\in[p,1],\ \ell\ge1),\qquad \alpha\le\frac{F_k(q)}{1-p^k}\quad(k\ge1).$$

Its optimal value is $\alpha(p)$. The paper obtains SDCLP$_p$ as the limit $N\to\infty$ of the linear programs that describe the best algorithm for $p$-DOS with adversarial values (§4.1–4.2); Theorem 8 is a statement about the program's value.

Two constants are defined by equations. $\tilde\alpha(p)$ is the unique root in $(0,1)$ of

$$\ln p+\frac{\tilde\alpha(1-p)^2}{p}=\sum_{i=1}^{\infty}\frac{\ln\bigl(1-\tilde\alpha+\tilde\alpha[(i+1)p^i-ip^{i+1}]\bigr)}{i(i+1)},\qquad(19)$$

and $\alpha^*$ is the solution of $\int_0^1\frac{dy}{y(1-\ln y)+1/\alpha^*-1}=1$. A threshold rule (12) is given by times $p=t_1\le t_2\le\cdots\le1$ with $T_i=\prod_{j\le i}t_j$: on $[t_i,t_{i+1})$ it equals $T_i/t^{i+1}$ for ranks $\ell\le i$ and $0$ for larger ranks.

Formalization targets

Goal: Theorem 8

$$0\le\tilde\alpha(p)\le\alpha(p)\le\alpha^*\quad(p\in(0,1)),\qquad \lim_{p\to1^-}\tilde\alpha(p)=\lim_{p\to1^-}\alpha(p)=\alpha^*.$$

Milestones, in the order the proof uses them

1. B.4: $\sum_{\ell=1}^{j}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^\ell=t$.
2. Lemma 4: a maximal $\alpha$ satisfies $\alpha\ge\inf_{k\ge1}\frac{1}{1-p^k}\sum_{j\le k}\int_p^1 t\,q(t,j)\,dt$ when $q$ is non-increasing in $\ell$.
3. Lemma 5: for a threshold rule, the system "every term of that infimum equals $\alpha$" is equivalent to explicit equations (15)–(16).
4. Lemma 6 (i), (ii): the times $t_1=p$, $t_2=pe^{\alpha(1-p)^2/p}$, $(t_k/t_{k+1})^{k-1}=\gamma_k/\gamma_{k-1}$ increase, and their limit is at most $1$ exactly under condition (18).
5. B.6: $T_i/t_i^{i-1}=p\gamma_{i-1}$ and $\mu_k=p(1-\alpha+\alpha p^{k-2})/(k-2)$.
6. Lemma 6 (iii): under (18) the threshold rule is feasible with value $\alpha$.
7. Lemma 7: (19) has a unique root, continuous in $p$.
8. B.8: the ratio $h(p,\eta)$ of the two sides of (19) tends to $\int_0^1\frac{dy}{y(1-\ln y)+1/\eta-1}$ as $p\to1$.

Significance

The result. Theorem 8 shows that sample access interpolates continuously between the secretary and prophet worlds and that, with almost full information, no more than the known-distribution guarantee $\alpha^*$ is lost or gained. The explicit rule behind $\tilde\alpha(p)$ is a concrete threshold algorithm, and the companion Theorem 9 of the paper ($\tilde\alpha(p)\ge\alpha^*p$, a separate mission) turns it into sample-complexity bounds: $O(n/\varepsilon)$ samples suffice for $\alpha^*-O(\varepsilon)$.

Formalizing it. The result is proved on paper; no part of it is machine-checked. A formal proof contributes a verified treatment of an infinite-dimensional linear program over $L^1([p,1]\times\mathbb N)$, of series defined through implicit equations, and of a Riemann-sum limit obtained by l'Hôpital's rule. One clause, $\alpha(p)\le\alpha^*$, is not proved in the paper: it is imported from the i.i.d. prophet inequality literature via the interpretation of $\alpha(p)$ as a competitive ratio. A formal proof of that clause directly from SDCLP$_p$ would be new.

Difficulty

The lower bound $\tilde\alpha(p)\le\alpha(p)$ needs an explicit feasible point of an infinite program; checking feasibility of the threshold rule requires exact telescoping of series with products of the times $t_k$, which are defined recursively through fractional powers. The limit $\tilde\alpha(p)\to\alpha^*$ is a $0/0$ limit of infinite series whose terms change scale as $p\to1$: every individual term tends to zero, so termwise passage to the limit gives no information, and the integral in the defining equation of $\alpha^*$ appears only in an aggregate limit of the whole series. The upper bound $\alpha(p)\le\alpha^*$ cannot come from evaluating any single solution: it is a statement about every feasible $q$, and the paper obtains it only through an external argument.

Formalization scope

• A stopping rule is q : ℝ → ℕ → ℝ; ranks are 1-based (values at rank $0$ are never used), and constraints are imposed pointwise on $[p,1]$ as printed. The integral of the series in (10) is a lower Lebesgue integral of an $[0,\infty]$-valued series, so it cannot collapse to a junk value; each $q(\cdot,\ell)$ is required integrable on $[p,1]$.
• $\alpha(p)$ is sSup of the set of feasible $\alpha$; it contains $0$ and is bounded by $1$, so it is the true supremum (checked in a sorry-free verification file). The program ranges over all feasible $q$, never only threshold rules.
• (11) is quantified over $k\ge1$ only, so $1-p^k\neq0$.
• Threshold rules use the half-open intervals $[t_i,t_{i+1})$ of (7); (12) prints closed intervals, which overlap at the $t_i$.
• The series in (18), (19), (26) and $\mu_k$ are written with the summation index shifted to start at $0$; with $p,\alpha\in(0,1)$ every logarithm's argument lies in $[1-\alpha,1]$, so they converge absolutely and tsum is the true sum.
• Lemma 6's recursion is $t_{k+1}=t_k(\gamma_{k-1}/\gamma_k)^{1/(k-1)}$ for $k\ge2$, the unique positive solution of (17).
• $\tilde\alpha$ and $\alpha^*$ are predicates (IsAlphaTilde, IsAlphaStar), not chosen functions; the goal holds for every root selection. Existence and uniqueness of $\alpha^*$ (with $\beta=1/\alpha^*$) is already posed as the open item CorreaThreshold.Adaptive.beta_star_existsUnique and is not posed again.
• "$p\to1$" is the one-sided filter 𝓝[<] 1.
• Lemma 6 (iii) carries hypothesis (18), which the paper states in the sentence after the lemma; without it the claim is false.

Trivializing formalizations are ruled out: replacing $\alpha(p)$ by $\tilde\alpha(p)$ or by the value of a truncated program, fixing $p$, restricting $q$ to threshold rules in the definition of $\alpha(p)$, or replacing $\alpha^*$ by $0.745$ each changes the theorem and is not done.

A complete development needs: binomial identities, interval integrals of $t^{-i}$ and of piecewise-defined functions, real powers and logarithms of recursively defined sequences, summability of series in $\ell^1$, continuity of the root of a monotone family of equations, and limits of Riemann-type sums on $(0,1]$. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021. https://arxiv.org/abs/2011.06516v2
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, The Annals of Probability 10(2), 336–345, 1982 (reference [26] of the paper).
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19, 88–112, 1986 (reference [28]).
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms for a random stream of customers, ACM EC 2017 (reference [17]).
• H. Kaplan, D. Naori, D. Raz, Competitive analysis with a sample and the secretary problem, SODA 2020 (reference [27]).
• J. Correa, P. Dütting, F. Fischer, K. Schewior, Prophet inequalities for i.i.d. random variables from an unknown distribution, ACM EC 2019 (reference [15]).
• A. Rubinstein, J. Z. Wang, S. M. Weinberg, Optimal single-choice prophet inequalities from samples, ITCS 2020 (reference [40]).

Motivation

Hiring is a pipeline: a firm with $k$ openings and a large pool of applicants cannot interview everyone, so it must decide whom to interview, in what order, and whether to hire on the spot. The ProbeTop-k problem models this. Each applicant has a random value with a known distribution, an interview reveals the value, at most $T$ interviews may be conducted, and at most $k$ applicants are hired. The firm maximises the expected total value of its hires.

The same structure appears in stochastic probing, sequential testing and assortment problems, and its benchmark, the best adaptive, non-committed policy (one that may choose the next interview after seeing earlier values and may hire only at the end), is hard to compute. Practical policies are non-adaptive (fix the interview order in advance) and committed (hire or reject right after each interview). Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) ask how much is lost by restricting to such policies, and answer with an LP-rounding algorithm whose guarantee improves with $k$.

Setting

An instance $I = (k, T, n, F)$ has $1 \le k \le T \le n$. Applicant $i \in [n]$ has value $V_i$ supported on finitely many non-negative values $r_1, \dots, r_J$, with $q_{ij} = \Pr(V_i = r_j)$; values are independent across applicants.

The linear relaxation $\mathrm{LP}_{ptk}(I)$ has variables $y_i$ (probability of interviewing $i$) and $x_{ij}$ (probability of hiring $i$ when $V_i = r_j$):

$$\mathrm{LP}_{ptk}(I) = \max \sum_{i=1}^n \sum_{j=1}^J r_j x_{ij} \quad \text{s.t.}\quad x_{ij} \le y_i q_{ij},\ \ \sum_i y_i \le T,\ \ \sum_{i,j} x_{ij} \le k,\ \ x_{ij} \ge 0,\ \ 0 \le y_i \le 1 .$$

From a solution $(x, y)$ define

$$p_i = \frac{\sum_j x_{ij}}{y_i}, \qquad v_i = \frac{\sum_j r_j x_{ij}}{\sum_j x_{ij}},$$

each $0$ when its denominator is $0$.

The algorithm ALGptk solves the LP and takes a basic optimal solution $(x, y)$. It then draws the interview set $S$ by the dependent rounding DR: applicants with $y_i = 1$ are always in $S$; a single fractional $y_a$ puts $a$ in $S$ with probability $y_a$; two fractional $y_a + y_b = 1$ put exactly one of them in $S$, $a$ with probability $y_a$. ALGptk interviews $S$ in decreasing order of $v_i$, and on observing $V_i = r_j$ hires $i$ with probability $x_{ij}/(y_i q_{ij})$ if a position is still open. Its expected reward is $R_{ALG_{ptk}}(I)$.

Formalization targets

Goal: Theorem 1

$$R_{ALG_{ptk}}(I) \;\ge\; \Big(1 - \frac{e^{-k}k^k}{k!}\Big)\, \mathrm{LP}_{ptk}(I) \qquad \text{for every valid instance } I \text{ with } k \text{ positions.}$$

The factor is $1 - 1/e$ at $k = 1$ and tends to $1$ as $k \to \infty$.

Milestones

The paper's own steps, in attack order:

1. Lemma 2 (p. 16): a basic feasible solution has at most two fractional $y_i$, and two fractional ones sum to $1$.
2. (P1), (P2) (p. 17): DR has marginals $\mathbb{E}(Y_i) = y_i$ and never exceeds $T$ interviews.
3. $\mathbb{E}(P_i) = p_i$ (p. 18): the hiring coin has mean $p_i$.
4. Lemma 3 (p. 18): $R_{ALG_{ptk}}(I) = \sum_i v_i\, \mathbb{E}(\mathbf 1\{N_{i-1} < k\} Z_i)$, where $Z_i = Y_i P_i$, the $P_i$ are independent Bernoulli($p_i$) indicators, and $N_{i-1}$ counts the earlier applicants with $Z_\ell = 1$.
5. Lemma 4 (p. 18): with two fractional components, this quantity under DR is at least its value under independent rounding of $y$.
6. LP identity (p. ec8): $\sum_{i,j} r_j x_{ij} = \sum_i y_i v_i p_i$.
7. Proposition EC.1 (Yan 2011; p. ec2): the weighted rank function of a $k$-uniform matroid has correlation gap at most $(1 - e^{-k}k^k/k!)^{-1}$.
8. Independent version (p. ec8): with independent rounding, the reward is at least $(1 - e^{-k}k^k/k!)\,\mathrm{LP}_{ptk}(I)$.

A companion milestone, Lemma 5 (p. 21), states that for weighted Bernoulli instances the LP has an optimal solution with $x_i = y_i q_i$. It does not feed Theorem 1.

Significance

Theorem 1, combined with the fact that $\mathrm{LP}_{ptk}$ bounds every adaptive, non-committed policy (Lemma 1 of the paper), shows that a policy that is both non-adaptive and committed earns at least a fraction $1 - e^{-k}k^k/k!$ of the optimal adaptive, non-committed reward; the lost fraction $e^{-k}k^k/k!$ vanishes as $k$ grows. The factor is tight for this LP (App. B.6). The theorem also underlies a PTAS for ProbeTop-k (Corollary 1) and, through Lemma 5, the same guarantee for the Sequential Offering problem of Purohit et al. (Corollary 2).

The result is proved in the paper; to our knowledge nothing in it is machine-checked. A formalization would add to the platform:

• an LP relaxation with basic feasible solutions as extreme points of a polytope;
• an explicit model of a randomised, committed selection algorithm as a finite expectation;
• the correlation gap of $k$-uniform weighted rank functions, a tool that recurs across prophet inequalities, posted pricing and stochastic probing.

Proposition EC.1 is a cited result (Yan 2011), not proved in the paper. Formalizing it is part of the work.

Difficulty

The obvious argument compares the algorithm with the LP term by term, $\Pr(i \text{ hired}) \ge c\, y_i p_i$ for each $i$. This fails because hiring is capped at $k$: applicants late in the order are hired only if few earlier ones were. The guarantee must be obtained in aggregate, which is what the correlation gap does.

Two steps carry the weight:

• Proposition EC.1 is a genuine extremal inequality over all distributions on subsets with given marginals.
• Lemma 4 must show that the negative correlation DR introduces between the two fractional applicants never hurts a committed, order-dependent selection. It is a case analysis over sample paths that uses the decreasing order of $v_i$.

Lemma 3 is a conditional-expectation identity, but in a fully explicit model it requires marginalising out the values and coins of all other applicants.

Formalization scope

Lean namespace HiringLP.ProbeTopK.

Representation.

• Applicants are Fin n and support points Fin J. All quantities are real.
• Instances are valid when $1 \le k \le T \le n$, $r_j \ge 0$, $q_{ij} \ge 0$ and $\sum_j q_{ij} = 1$.
• Basic feasible solutions are Set.extremePoints ℝ of the feasible set in $(x, y)$-space. An optimal solution is feasible and objective-maximal among feasible points, and $\mathrm{LP}_{ptk}(I)$ is the objective at it.

Conventions.

• $p_i$, $v_i$ and the hiring probability $x_{ij}/(y_i q_{ij})$ are $0$ when their denominators vanish (the paper's footnote 2).
• The interview order is a permutation required to be non-increasing in $v_i$, with ties in any order.
• DR is an explicit formula for the probability of each interview set.

The expected reward. $R_{ALG_{ptk}}(I)$ is a finite sum over the interview set, the value vector (independent, law $q$) and the vector of hiring coins (independent given the values). Applicant $i$ is hired exactly when it is interviewed, its coin succeeds, and fewer than $k$ earlier interviewed applicants had successful coins. The reward collects the realised values $r_{V_i}$.

Ruled out.

• Defining the reward as $\sum_i v_i\, \mathbb{E}(\mathbf 1\{N_{i-1} < k\} Z_i)$. That is Lemma 3, which would make the goal a statement about its own proof.
• Comparing with the objective at an arbitrary feasible point instead of an optimal one.

Infrastructure and contributions. The weighted rank function, independent rounding and marginals are separate, reusable definitions. Contributions are welcome on each milestone, especially Proposition EC.1. So is general infrastructure: extreme points of polytopes as basic solutions, and finite product distributions.

Selected references

• B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, Operations Research, 2024; preprint arXiv:2210.04059v3, 2023. https://arxiv.org/abs/2210.04059
• Q. Yan, Mechanism design via correlation gap, Proceedings of the 22nd ACM-SIAM Symposium on Discrete Algorithms (SODA), 710–719, 2011. Proceedings volume: https://doi.org/10.1137/1.9781611973082
• S. Agrawal, Y. Ding, A. Saberi, Y. Ye, Correlation robust stochastic optimization, Proceedings of the 21st ACM-SIAM Symposium on Discrete Algorithms (SODA), 1087–1096, 2010. Proceedings volume: https://doi.org/10.1137/1.9781611973075
• R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3):324–360, 2006. https://doi.org/10.1145/1147954.1147956
• M. Purohit, S. Gollapudi, M. Raghavan, Hiring under uncertainty, Proceedings of the 36th International Conference on Machine Learning (PMLR 97), 5181–5189, 2019. https://proceedings.mlr.press/v97/purohit19a.html

Motivation

Retailers that run predictable promotions teach their customers to wait for them. A customer who knows that a discount will come next week has no reason to buy at the list price today. Firms therefore lose margin on exactly the customers who would have paid in full. One response, documented in practice by Moon, Bimpikis and Mendelson (2017), is to randomize promotions: commit to a distribution of prices, draw a fresh price every period, and let customers know only the distribution. A customer cannot time a discount that arrives at random. Whether waiting is worthwhile then depends on how patient the customer is.

The classical deterministic answer to strategic waiting is cyclic pricing: Conlisk, Gerstner and Sobel (1984) showed that a durable-goods monopolist facing a stream of arriving customers lowers its price periodically. Besbes and Lobel (2015) characterized optimal deterministic policies when customers differ in valuation and patience. Randomized prices as a model of sales go back to Varian (1980) in a competitive setting. Chen, Hu and Wu (SSRN 3223844, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1194) ask the monopoly question directly: which price distribution should a seller commit to when two customer segments differ in both valuation and waiting cost? This mission formalizes their answer for the two-segment base model.

Setting

A monopolist sells one product over an infinite horizon. A fraction $\alpha\in(0,1)$ of arriving customers are low-valuation customers, who value the product at $v_L$ and pay a waiting cost $c_L$ per period; the remaining $1-\alpha$ are high-valuation customers, with valuation $v_H>v_L$ and waiting cost $c_H$. Assumption (S) of the paper is $0<c_L<v_L$ and $0<c_H<v_H$.

The firm announces a price distribution: a random price $P$ with finitely many possible values $p$ and probabilities $f(p)\ge0$ summing to one. Each period an independent price is drawn from it. Write $F(x)=\sum_{p\le x}f(p)$ for the distribution function, $\mathbb E[P\mid P\le x]$ for the mean price conditional on $P\le x$, and $\mathbb E[(v-P)^+]=\sum_p f(p)\max(v-p,0)$ for the expected one-period surplus of a customer with valuation $v$. The purchase threshold of a customer with waiting cost $c$ is

$$\underline p=\max\{v'\mid \mathbb E[(v'-P)^+]\le c\}.$$

A customer whose valuation exceeds her threshold waits and buys at the first price not above it.

The paper reduces the firm's choice to the regime where low-valuation customers wait and high-valuation customers buy on arrival. The firm's long-run profit per arriving customer is then the objective of problem (2):

$$\max_{F}\ \alpha\,\mathbb E[P\mid P\le \underline p^L]+(1-\alpha)F(v_H)\,\mathbb E[P\mid P\le v_H]\quad\text{s.t.}\quad \mathbb E[(v_L-P)^+]>c_L,\ \ \mathbb E[(v_H-P)^+]\le c_H,$$

where $\underline p^L$ is the low type's threshold. Replacing $\underline p^L$ by $v_L$ in the objective gives the relaxation, problem (3). The key constants are

$$\Delta_R=\sqrt{\frac{\alpha c_L}{(1-\alpha)(v_H-v_L)}},\qquad U_1=\alpha v_L+(1-\alpha)v_H-(1-\alpha)c_L-2(1-\alpha)(v_H-v_L)\Delta_R,$$ $$U_2=\alpha v_L+(1-\alpha)v_H-(1-\alpha)c_H-\alpha c_L\frac{v_H-v_L}{c_H-c_L}.$$

In Lean the parameters are vL vH cL cH α, a law is w : ℝ →₀ ℝ with IsPriceDist w, and the objects above are cdf, condExp, gain, thresh, Feas, obj2, obj3, ΔR, bnd $=(c_H-c_L)/(v_H-v_L)$, U1, U2. Here $\underline p^L$ is written p^L in milestone text.

Formalization targets

Goal: Proposition 3 (p. 16)

Assume $c_L<c_H$ and $\Delta_R<1$, and let $U=U_1$ if $\Delta_R<\frac{c_H-c_L}{v_H-v_L}$ and $U=U_2$ otherwise. Then every price distribution feasible for (2) earns at most $U$ in (2), and there is $\eta$ with $\eta(\delta)\to0$ as $\delta\searrow0$ such that the two-point law

$$f(p)=\begin{cases}\beta^* & p=\underline p^*,\\ 1-\beta^* & p=v_H,\end{cases}\qquad \beta^*=\min\Big\{\Delta_R,\frac{c_H-c_L}{v_H-v_L}-\delta\Big\},\quad \underline p^*=v_L-\frac{c_L}{\beta^*}-\eta(\delta),$$

is feasible for (2) for all small $\delta>0$ and its profit tends to $U$. This is the $\epsilon$-optimality of the paper's Definition 1.

Milestones

1. §3.2.2: for every law feasible for (2), $\mathbb E[P\mid P\le\underline p^L]\le\mathbb E[P\mid P\le v_L]$, so (3) relaxes (2).
2. §3.2.2: every feasible law has $F(v_L)<\frac{c_H-c_L}{v_H-v_L}$.
3. Lemma 5, in the form its proof establishes: moving all mass above $v_L$ to $v_H$ preserves feasibility and does not lower the objective of (3).
4. Lemma 6(ii)(a) and (b): every feasible law earns at most $U_1$, respectively $U_2$, in (3).
5. Lemma 6(i), the complementary regime $\Delta_R\ge1$: no feasible law beats the static profit $\max\{v_L,(1-\alpha)v_H\}$.

Significance

The result says that, in this model, the optimal randomized promotion is the simplest one. The firm posts the regular price $v_H$ most of the time and runs a promotion at $\underline p^*$ with probability $\beta^*$. High-valuation customers buy on arrival; low-valuation customers wait for the promotion. The discount below $v_L$, of size $c_L/\beta^*$, is the price of keeping low types in the market. The closed forms $U_1,U_2$ quantify the profit lost relative to perfect discrimination $\alpha v_L+(1-\alpha)v_H$. The paper uses them to compare randomized with static and cyclic pricing (Propositions 4 and 8) and generalizes the structure to myopic customers and to $n$ segments.

The result is proved on paper; no machine-checked version exists. The mission produces a formal statement of the firm's problem over all finitely supported price laws on $\mathbb R$, a verified upper bound on its value, and a verified family that attains it in the limit. It also records three points the printed statements leave implicit (below).

Difficulty

The decision variable is an entire distribution, and the objective of (2) depends on it through the threshold $\underline p^L$, itself defined by a maximization over the distribution. The obvious approach, guessing the two-point law and checking first-order conditions, gives no upper bound over all laws. The upper bound has to hold for laws with arbitrarily many support points, of either sign and above $v_H$, and both incentive constraints enter it. Problem (3) has a strict constraint and no maximizer, so every statement about "the optimal profit" has to be read as a supremum. The attainment half then needs the threshold of the two-point law, computed from its definition, to sit exactly $\eta(\delta)$ below $v_L$.

Formalization scope

• Distributions. A price law is w : ℝ →₀ ℝ with nonnegative masses summing to one (finite support, as the paper assumes on p. 9). Prices range over all of $\mathbb R$: $\underline p^*$ can be negative under the hypotheses, and with prices restricted to $[0,\infty)$ Proposition 3 is false for some admissible parameters.
• Standing assumptions, hypotheses of every theorem: Assumption (S), $v_L<v_H$ (printed on p. 9), and $0<\alpha<1$ (added; $\Delta_R$ divides by $1-\alpha$).
• Added hypothesis of the goal: $c_L<c_H$. Without it $\beta^*<0$ and the two-point law is not a distribution.
• Conventions. $\mathbb E[P\mid P\le x]$ is a quotient that Lean sets to $0$ when $F(x)=0$; this never happens for feasible laws. $\underline p^L$ is the real supremum of $\{v'\mid\mathbb E[(v'-P)^+]\le c_L\}$, which is a maximum for every price law. "The optimal expected profit is no more than $U$" is read as a bound on every feasible law. "Optimal" in Proposition 3 is $\epsilon$-optimality for (2), stated as the upper bound plus the approaching family, with $\eta$ existential.
• Lemma 5 as printed quantifies over optimal solutions of (3), which do not exist; the milestone states the dominance that its proof (Online Supplement p. 8) establishes.
• Ruled out. The profit and the threshold of the two-point law are not given in closed form: they are the general obj2 and thresh applied to it. The upper bound ranges over all feasible laws, not two-point laws or laws on $[0,v_H]$. "Optimal" is not read as "beats static pricing" (that is Proposition 4) or as an attained maximum, and $\eta$ may not depend on the competing law.
• Not in the mission. The customer's optimal-stopping model (Lemma 1, Proposition 1, Lemma 2) is the paper's justification of the objective of (2); the mission states problem (2) as printed. Cyclic and Markovian pricing, myopic customers and $n$ segments are not posed.
• Needed infrastructure. Finite sums over Finsupp supports, monotonicity and continuity of $v\mapsto\mathbb E[(v-P)^+]$, and the elementary concavity argument for $\beta\mapsto U(\beta)$. A general library of finitely supported real price laws (distribution function, partial expectations, expected surplus) would be reusable for other pricing papers. Proofs of any milestone are welcome.

Selected references

• H. Chen, M. Hu, J. Wu, Intertemporal Price Discrimination via Randomized Promotions, SSRN preprint 3223844 (revision of 2022-11-16); Manufacturing & Service Operations Management, 2023. https://ssrn.com/abstract=3223844, https://doi.org/10.1287/msom.2023.1194
• J. Conlisk, E. Gerstner, J. Sobel, Cyclic pricing by a durable goods monopolist, Quarterly Journal of Economics 99(3), 1984. https://doi.org/10.2307/1885961
• O. Besbes, I. Lobel, Intertemporal price discrimination: Structure and computation of optimal policies, Management Science 61(1), 2015. https://doi.org/10.1287/mnsc.2014.2049
• H. Varian, A model of sales, American Economic Review 70(4), 1980. https://www.jstor.org/stable/1803562
• X. Su, Intertemporal pricing with strategic customer behavior, Management Science 53(5), 2007. https://doi.org/10.1287/mnsc.1060.0628
• K. Moon, K. Bimpikis, H. Mendelson, Randomized markdowns and online monitoring, Management Science, 2017.

Motivation

Many proof-of-stake blockchains do not let every participant produce blocks. Instead, token holders elect a small committee of block producers, and the committee runs a Byzantine agreement protocol among itself. EOS, for example, elects 21 producers by approval voting: each token holder approves a set of candidates, and the 21 candidates with the most approvals form the committee. Byzantine agreement protocols are safe only while a large enough fraction of the committee is honest, typically more than two thirds, so the security of the whole chain rests on a question of social choice: does approval voting, with voters who see only noisy information about the candidates, elect a committee with enough honest members?

Benhaim, Falk and Tsoukalas (arXiv:2110.08673v2, Management Science 2023) model this election and analyse it. Their main result, Theorem 3, shows that whatever strategies the voters use, as long as the honest candidates are approved with probability at least a fixed margin $\delta$ above the dishonest ones, the probability of electing an honest committee converges to one exponentially fast in the number of voters. This mission formalizes that result.

Setting

There are $n$ voters and $m$ candidates (block producers), and a committee of size $k\le m$ is to be elected. Each voter $i$ submits an approval ballot $\mathcal C_{v_i}$, a subset of the candidates. The score of candidate $j$ is the number of voters approving it,

$$\operatorname{score}(j)=X_j=\bigl|\{\,i : j\in\mathcal C_{v_i}\}\bigr| .$$

The elected committee $\mathbb T$ consists of $k$ candidates with the highest scores. When several candidates tie at the lowest elected score, or when fewer than $k$ candidates have a non-zero score, the paper resolves the choice adversarially. Formally, a set $T$ of candidates is an admissible committee if $|T|=k$ and $X_b\le X_a$ for every $a\in T$ and $b\notin T$.

Each candidate is honest or dishonest. Let $\mathcal M$ denote the set of dishonest candidates. For a tolerance $p\in[0,1]$ (for instance $p=1/3$), the committee is honest, written $\mathbb T=H$, if it has at least $\lceil(1-p)k\rceil$ honest members. Because ties and filling are adversarial, $\mathbb T=H$ means that every admissible committee has at least $\lceil(1-p)k\rceil$ members outside $\mathcal M$.

The ballots are random: they are drawn on a probability space, independently across voters, while the approvals inside a single ballot may depend on each other in any way. The vote probability $p_{ij}=\Pr[j\in\mathcal C_{v_i}]$ is the probability that voter $i$ approves candidate $j$. The candidates' types are fixed throughout, and all randomness is in the ballots.

Formalization targets

Goal: Theorem 3 (p. 22)

Suppose there are a set $\mathcal H$ of honest candidates with $|\mathcal H|\ge(1-p)k$ and a $\delta>0$ with $\min_{i,\,j\in\mathcal H}p_{ij}\ge\max_{i,\,j\in\mathcal M}p_{ij}+\delta$. Then

$$\Pr[\mathbb T=H]\ \ge\ 1-2m^2e^{-\delta^2 n/2}.$$

Milestones (in the order the proof on p. 48 uses them)

1. Opening claim of the proof (p. 48). If every member of $\mathcal H$ outscores every member of $\mathcal M$, then $\mathbb T=H$ (deterministic).
2. Theorem 1 (pp. 15–16). Each vote count is Poisson binomial:

$$\Pr[X_j=x]=\sum_{|A|=x}\ \prod_{i\in A}p_{ij}\prod_{i\notin A}(1-p_{ij}).$$

3. Theorem 6 (p. 50). Chernoff–Hoeffding for a Poisson binomial $X$ with mean $n\bar p$: $\Pr[X>n\bar p+t]\le e^{-2t^2/n}$ and $\Pr[X<n\bar p-t]\le e^{-2t^2/n}$ for $t>0$.
4. (82). For $j_h\in\mathcal H$, $j_m\in\mathcal M$: $\Pr[X_{j_h}\le X_{j_m}]\le 2e^{-\delta^2n/2}$.
5. (83). $\Pr[X_{j_m}<X_{j_h}\ \forall j_h\in\mathcal H,\ j_m\in\mathcal M]\ge1-2m^2e^{-\delta^2n/2}$.

Significance

The theorem is the paper's answer to its title question. Its bound holds for every voting behaviour, including the threshold and cardinal strategies the paper studies and strategies with arbitrary correlation inside a ballot. So the security guarantee does not depend on voters coordinating or on knowing the signal model. All it needs is that signals are informative by a margin $\delta$. The bound also shows the trade-off quantitatively: the failure probability grows quadratically in the number of candidates $m$ and decays exponentially in the number of voters $n$. This is the basis of the paper's Corollaries 1 and 2 on the threshold and cardinal strategies.

The paper proves the result on paper (Appendix B.2, p. 48), using a Chernoff–Hoeffding bound it cites from Dubhashi and Panconesi. As far as the platform's index shows, no machine-checked version of the result or of its committee model exists. The mission contributes the first formal model of $k$-winner approval voting with adversarial tie-breaking on Prove2Me, a formal statement of the Poisson-binomial law of approval counts, and the one-sided Hoeffding bound for sums of independent Bernoulli variables in the $e^{-2t^2/n}$ form. The formalization also records three places where the printed text needs correcting (see Formalization scope).

Difficulty

There are two difficulties. The first is the committee predicate. Ties and under-filled committees are resolved by an adversary, so $\mathbb T=H$ is a statement about every admissible committee, not about one top-$k$ list. The reduction from honesty to the score-separation event has to handle both the case where all of $\mathcal H$ is elected and the case where some member of $\mathcal H$ is left out, so that every elected candidate outscores it.

The second is the concentration step. The vote counts of different candidates are not independent, because each voter's ballot ties the approvals together, so no argument that treats the $m$ counts as independent variables applies. The paper's own step from the gap to (82), the split (80)/(81), uses strict inequalities and is false when the two thresholds coincide at an attained integer value; the printed Hoeffding bound (Theorem 6) is strict as well, so the printed chain does not close as written at that boundary.

Formalization scope

• Voters are Fin n and candidates Fin m, both 0-based. A random ballot is a measurable map Ω → (Fin m → Bool) on a probability space (Ω, P). The ballots are mutually independent (iIndepFun), and each voter's ballot law is otherwise arbitrary. This generalises the paper's Gaussian signal model and its strategy classes, which are not formalized, and the paper's per-type probabilities $p^h_i,p^m_i$ become per-candidate $p_{ij}$. The cap $|\mathcal C_v|\le t$ of Definition 2 is not imposed. The printed statements are special cases.
• $\mathbb T=H$ is the predicate "every set $T$ with $|T|=k$ and no outsider scoring above a member has $|T\setminus\mathcal M|\ge\lceil(1-p)k\rceil$", with an integer ceiling. A formalization in which some admissible committee is honest, or in which the committee is chosen by a fixed tie-breaking rule, is a different and weaker theorem. Without the condition $|T|=k$ the predicate would be trivial. An admissible committee exists for every score vector when $k\le m$.
• Standing assumptions that are made explicit: $k\le m$ (p. 9), $0\le p\le1$ ($p$ is the tolerated fraction, which the paper never bounds; the opening claim of the proof fails for $p<0$), independence across voters (§5.1.2), and measurability of each ballot.
• The min/max gap of Theorem 3 is stated pairwise for all voters $i,i'$, all $j_h\in\mathcal H$ and all $j_m\in\mathcal M$. This is equivalent when both sets are nonempty and avoids undefined extrema otherwise.
• Corrected slips: Theorem 6 is stated for $t>0$ and $n\ge1$, since it is false for negative $t$ and divides by $n$. (80)/(81) are not posed, and (82) is stated as a bound on $\Pr[X_{j_h}\le X_{j_m}]$.
• Infrastructure needed: Mathlib's independence, Measure.real, sub-Gaussian concentration for bounded independent variables, and Finset.powersetCard. The committee definitions and the Poisson-binomial law can be reused by later missions on voting and on the companion single-voter result. Proofs of any milestone are welcome, and so are alternative routes to the goal.

Selected references

• A. Benhaim, B. H. Falk, G. Tsoukalas, Scaling Blockchains: Can Committee-Based Consensus Help?, Management Science, 2023; preprint arXiv:2110.08673v2, 2022. https://arxiv.org/abs/2110.08673v2 (DOI 10.1287/mnsc.2022.03177)
• D. P. Dubhashi, A. Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511581274
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.1080/01621459.1963.10500830

Motivation

A manufacturer that makes several products to stock for price-sensitive customers controls three levers at once: the prices it posts, which shape demand; outsourcing, which clears a large backlog at a cost; and scheduling, which decides which product the single server makes next. Ata and Barjesteh (Operations Research 71(1), 2023) study this multiclass make-to-stock queue in the heavy-traffic regime, where the queue is nearly saturated and the system is approximated by a Brownian control problem. The approximation collapses to a one-dimensional problem in the workload, the total amount of work in the system. Its solution is a two-barrier policy whose state-dependent drift translates back into a dynamic pricing rule, an outsourcing threshold and a scheduling priority (§7 of the paper).

The one-dimensional problem belongs to the family of drift-rate control problems for Brownian motion under a long-run average cost criterion (Ata, Harrison and Shepp, Ann. Appl. Probab. 2005; Rubino and Ata, Oper. Res. 2009). Problems of this kind are solved by a Bellman equation with free boundaries and a verification argument; the present paper adds two-sided singular control (outsourcing at the bottom, idling at the top) to a quadratic drift cost and a piecewise linear state cost.

Setting

There are $K\ge1$ products with mean production times $m_k>0$ and holding, backorder and outsourcing cost rates $h_k,b_k,r_k>0$. A symmetric positive definite matrix $H$ describes the curvature of the revenue rate. Write $a=m'H^{-1}m$ and

$$h^\star=\min_k\frac{h_k}{m_k},\qquad b^\star=\min_k\frac{b_k}{m_k},\qquad \kappa=\min_k\frac{r_k}{m_k}.$$

The drift cost and the effective holding cost are

$$c(x)=\min\{\zeta'H\zeta:\ m'\zeta=x\},\qquad h(w)=h^\star w\ (w\ge0),\quad h(w)=-b^\star w\ (w<0).$$

Let $B$ be a Brownian motion with drift $\mu\ge0$ and variance $\sigma^2>0$, started at $0$, with respect to a filtration $\mathbb F$. An admissible control consists of a progressively measurable drift rate $\theta$ and nondecreasing, right-continuous, adapted processes $L$ (effective outsourcing) and $U$ (idleness) with $L(0)=U(0)=0$. The workload is

$$W(t)=B(t)-\int_0^t\theta(s)\,ds-U(t)+L(t),$$

and admissibility also requires $\mathbb E|W(t)|/t\to0$. The equivalent workload formulation (EWF) is to minimize

$$\limsup_{t\to\infty}\frac1t\,\mathbb E\Big[\int_0^tc(\theta(s))\,ds+\int_0^th(W(s))\,ds+\kappa L(t)\Big]. \tag{29}$$

A barrier policy with barriers $l<u$ keeps $W$ in $[l,u]$, increases $L$ only when $W=l$ and $U$ only when $W=u$.

For $\gamma\ge0$ put $l_\gamma=-\frac1{b^\star}(\gamma+\mu\kappa+\frac a4\kappa^2)$ and $u_\gamma=\gamma/h^\star$. Let $v^-_\gamma$ solve the Riccati equation

$$v'=\frac a{2\sigma^2}(v^2-\kappa^2)-\frac{2\mu}{\sigma^2}(v+\kappa)+\frac{2(h(l_\gamma)-h(w))}{\sigma^2}\ \text{on }[l_\gamma,0],\qquad v(l_\gamma)=-\kappa,$$

and $v^+_\gamma$ solve $v'=\frac a{2\sigma^2}v^2-\frac{2\mu}{\sigma^2}v+\frac{2(h(u_\gamma)-h(w))}{\sigma^2}$ on $[0,u_\gamma]$ with $v(u_\gamma)=0$. The paper's $\gamma^\star$ is the unique $\gamma$ with $v^-_{\gamma}(0)=v^+_{\gamma}(0)$; $v$ pastes $v^-_{\gamma^\star}$ and $v^+_{\gamma^\star}$ at $0$, and the candidate drift is $\theta(w)=\frac a2v(w)$.

Formalization targets

Goal: Theorem 1

For every filtered probability space carrying such a Brownian motion,

$$\lim_{t\to\infty}\frac{J_{\text{cand}}(t)}t=\gamma^\star\quad\text{for every barrier policy at }(l_{\gamma^\star},u_{\gamma^\star})\text{ with drift }\theta(W),\qquad \limsup_{t\to\infty}\frac{J(t)}t\ge\gamma^\star\ \text{for every admissible control},$$

where $J$ is the expected cumulative cost in (29). The constant $\gamma^\star$ is the paper's construction, not a parameter.

Milestones

1. Lemma 1 and Lemma 2: the closed forms $c(x)=x^2/a$ and its conjugate $\varphi(y)=\frac a4y^2$, maximized at $\psi(y)=\frac a2y$.
2. Proposition 2: a barrier policy whose $(\gamma,f)$ solves the ODE (35)–(36) has long-run average cost $\gamma$.
3. Lemma 3: any solution of the Riccati-form Bellman equation (43)–(45) has $\gamma>0$, $l=l_\gamma<0$, $u=u_\gamma>0$.
4. Lemmas 18–20 and Corollary 6: sign and monotonicity of the Riccati solutions.
5. §6.3 well-posedness, Lemma 4(i)–(ii), Corollary 1: uniqueness of $v^\pm_\gamma$, their monotone dependence on $\gamma$, and the unique crossing $\gamma^\star$.
6. Proposition 3 and Corollary 2: $(l_{\gamma^\star},u_{\gamma^\star},\gamma^\star,v)$ is the unique solution of (43)–(45), and $f=\int v$ solves the Bellman equation (37)–(39), uniquely up to a constant.

Significance

The theorem identifies an explicit optimal policy for a two-sided singular drift-control problem: two barriers and a strictly increasing, non-positive drift, all determined by a scalar root $\gamma^\star$ of a monotone equation. In the paper it drives the proposed pricing, outsourcing and scheduling policy (§7) and its asymptotic analysis; the Riccati structure is what makes $\gamma^\star$ computable by line search.

The result is proved in the paper; none of it has been machine-checked. Formalizing it gives a checked verification theorem for an average-cost Brownian control problem with singular controls, and checked statements of the Riccati comparison lemmas on which it rests. Several printed statements of the paper are corrected here (see the scope section), so the formal versions are the first fully precise ones.

Difficulty

The optimality half of Theorem 1 is a verification argument: apply Itô's formula to $f(W(t))$ for an arbitrary admissible control with jumps in $L$ and $U$, use the Bellman inequality pointwise, and control $\mathbb E f(W(t))/t$ with the growth condition (32). Mathlib does not yet have Itô's formula for continuous semimartingales with finite-variation, possibly discontinuous parts, and the candidate's average cost (Proposition 2) needs the same tool plus the fact that a reflected diffusion spends zero time at the barriers.

The deterministic half is not routine either. The obvious reading of the paper, solving each Riccati problem for every $\gamma\ge0$ and passing $\gamma\to\infty$, fails: the solutions blow up in finite time, so $v^\pm_\gamma$ exist only for $\gamma$ in a bounded initial interval, and the crossing argument must be run on that interval. The comparison arguments of Lemmas 18–20 also need second derivatives of solutions whose right-hand side has a kink at $w=0$.

Formalization scope

Time is indexed by $\mathbb R$ and only $t\ge0$ matters. The Brownian motion is defined locally (drift, variance, start at $0$, independence of increments from the filtration). Expected costs are computed in $[0,\infty]$, so a control with infinite cost counts as $+\infty$. The integrals in (34) are Lebesgue–Stieltjes integrals against the paths of $L$ and $U$, jumps included. Derivatives at the barriers are one-sided; $C^1$ and $C^2$ up to the boundary are ContDiffOn on the closed interval. Minima and maxima (in $c$, (37), (40)) are stated as attained.

Standing assumptions added to every statement, all implicit in the paper: $K\ge1$; $m_k,h_k,b_k,r_k>0$; $H$ symmetric positive definite; $\mu\ge0$, $\sigma>0$; $B$ starts at $0$; $L,U$ right-continuous; $\theta$ progressively measurable with locally integrable paths; $l<u$ in the Bellman equations.

Corrected statements. Lemmas 18–20 are printed for solutions on $[0,\infty)$, which do not exist; they are posed on every bounded interval where a solution exists. The §6.3 claim that $v^\pm_\gamma$ exist for every $\gamma\ge0$ is replaced by uniqueness, solvability at $\gamma=0$ and order-connectedness of the solvability sets. Lemma 4's limits as $\gamma\to\infty$ become unboundedness on those sets. Theorem 1's comparison class is every admissible control, which the paper's proof treats, and which contains the stationary Markov policies to which §6 restricts attention.

Not posed. The existence of the reflected diffusion realizing the candidate policy is presupposed by the paper and not claimed: the first half of the goal quantifies over all barrier policies with the given data. The second half is a statement about every admissible control and is not vacuous.

$\gamma^\star$, $v$, $f$ and $\theta$ are built from the Riccati solutions by choice, exactly as the paper constructs them; taking them as hypotheses-constrained parameters, or defining $c$ by its closed form, would trivialize the goal and is ruled out. Contributions are welcome on the Riccati lemmas (pure real analysis, reusable for other drift-control problems), on Itô's formula for semimartingales with finite-variation parts, and on Skorokhod-type existence of reflected diffusions.

Selected references

• B. Ata and N. Barjesteh, An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime, Operations Research 71(1):341–357, 2023. https://doi.org/10.1287/opre.2022.2361 (accepted manuscript: https://ssrn.com/abstract=3464763)
• B. Ata, J. M. Harrison and L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2):1145–1160, 2005. https://doi.org/10.1214/105051604000000855
• M. Rubino and B. Ata, Dynamic control of a make-to-order, parallel-server system with cancellations, Operations Research 57(1):94–108, 2009. https://doi.org/10.1287/opre.1080.0532
• J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698

Motivation

A supplier who must build capacity before a selling season would like to know how large demand will be, and the retailer downstream often knows better. Under a simple wholesale-price contract, however, the retailer gains from overstating demand: more capacity means more sales for her, and the cost of idle capacity falls on the supplier. Since the retailer's message costs nothing and binds nobody, a rational supplier ignores it. That such cheap talk (Crawford and Sobel, 1982) cannot convey information in a one-shot wholesale-price relationship is the benchmark result of Özer, Zheng and Chen (2011), yet firms are observed to share forecasts informally.

Avinadav and Shamir propose an explanation based on partial vertical ownership (PVO): retailers often hold passive equity stakes in their suppliers. A retailer that owns a share $\beta$ of the supplier bears a fraction $\beta$ of the losses her misreport inflicts on him. Their Theorem 2 says exactly how large the stake must be for truthful reporting to be self-enforcing, and how this depends on the gap between the two possible demand levels. This mission formalizes that theorem.

Setting

A retailer sources a component from a supplier. The supplier secures capacity $K$ at unit cost $c$; after demand is realized, the retailer orders and pays the wholesale price $w$ per unit and sells at the retail price $r$, with $0<c<w<r$. Unmet demand is lost, and leftover capacity is worthless.

Demand in market state $i\in\{L,H\}$ is $D_i=\mu_i+\varepsilon$ with $0<\mu_L<\mu_H$, where $\varepsilon$ is a zero-mean random variable with a density, distribution function $F$, and lower support end $\underline{\varepsilon}<0$ satisfying $\mu_L+\underline{\varepsilon}\ge0$. The information gap is $\Delta=\mu_H-\mu_L$. Write $F^{-1}(z)=\inf\{x: F(x)\ge z\}$ and define the critical fractiles $z_s=1-c/w$ and $z_r=1-w/r$.

The retailer may commit to an advance order $q^{adv}$ which the supplier must cover. The supplier's and retailer's expected profits are

$$\pi_s(K\mid\mu_i,q^{adv})=\mathbb E\big[w\min(K,\max(\mu_i+\varepsilon,q^{adv}))-cK\big],$$ $$\pi_r(q^{adv},K\mid\mu_i)=\mathbb E\big[(r-w)\min(\mu_i+\varepsilon,K)-w\max(q^{adv}-\mu_i-\varepsilon,0)\big].$$

A retailer holding the share $\beta\in[0,1]$ of the supplier maximizes the accounting payoff $v_r(q^{adv},K\mid\mu_i)=\pi_r(q^{adv},K\mid\mu_i)+\beta\,\pi_s(K\mid\mu_i,q^{adv})$.

Only the retailer observes the state. In the cheap-talk game she places no advance order and announces a state; a supplier who believes the announcement builds the newsvendor capacity $K_L=\mu_L+F^{-1}(z_s)$ or $K_H=\mu_H+F^{-1}(z_s)$. Truthful reporting requires

$$\text{(12)}\quad v_r(0,K_H\mid\mu_H)\ge v_r(0,K_L\mid\mu_H),\qquad\text{(13)}\quad v_r(0,K_L\mid\mu_L)\ge v_r(0,K_H\mid\mu_L).$$

Formalization targets

Goal: Theorem 2

Let

$$\underline{\underline{\beta}}=\frac{\pi_r(0,K_H\mid\mu_L)-\pi_r(0,K_L\mid\mu_L)}{\pi_s(K_L\mid\mu_L,0)-\pi_s(K_H\mid\mu_L,0)},\qquad R(d)=\frac1d\int_{F^{-1}(z_s)}^{d+F^{-1}(z_s)}F(x)\,dx\quad(d>0).$$

The goal asserts: (12) holds for every $\beta\in[0,1]$; for every $\beta\in[0,1]$, (12) and (13) hold if and only if $\beta\ge\underline{\underline{\beta}}$;

$$\underline{\underline{\beta}}=\frac{z_r}{1-z_r}\left(\frac{1-z_s}{R(\Delta)-z_s}-1\right),\qquad R(\Delta)<1;$$

and for every $\beta\in(0,1]$ the equation $R(d)=z_s+\frac{1-z_s}{1+\beta(1/z_r-1)}$ has a unique root $\underline{\underline{\Delta}}>0$, and truthful cheap talk is possible only if $\Delta\ge\underline{\underline{\Delta}}$.

Milestones

In attack order: the closed forms (2) and (3) of the expected profits; condition (12) always holds; (E.1), that (13) is equivalent to $\beta\ge\underline{\underline{\beta}}$ with positive numerator and denominator; (E.2), the closed form of $\underline{\underline{\beta}}$; and the properties of $R$ (strictly increasing on $(0,\infty)$, limits $z_s$ at $0^+$ and $1$ at $\infty$, values in $(z_s,1)$). A companion item states Proposition 1: $\underline{\underline{\beta}}<1$ if and only if the integrated chain earns less with $K_H$ than with $K_L$ in the low state.

Significance

Theorem 2 identifies an ownership channel through which a one-shot wholesale-price relationship can sustain truthful information exchange, in contrast with the impossibility of cheap talk without such links. The threshold $\underline{\underline{\beta}}$ is the ratio of the low-type retailer's operational gain from lying to the supplier's loss from being misled, and part (ii) turns it into a lower bound on the information gap: a sufficiently small gap rules out cheap talk for every stake. Proposition 1 translates feasibility ($\underline{\underline{\beta}}<1$) into a comparison of the integrated chain's profits. The same comparisons underlie the paper's later analysis of signaling with advance orders, which takes cheap talk as its benchmark.

The result is proved in the source, in Appendix E of the authors' manuscript; it has no machine-checked proof. The mission produces a formal statement in which every profit is an expectation over a general noise distribution, so that the closed forms the paper derives become theorems rather than definitions, together with the supporting analysis of the averaged distribution function $R$.

Difficulty

The algebra after the closed forms is short. The work lies in two places. First, the closed forms (2) and (3) are integration-by-parts identities for expectations of truncated linear functions of $\varepsilon$, under a general law rather than a density on a compact interval, including the case of an upper support end at $+\infty$. Second, the properties of $R$: the paper differentiates $R$ and applies L'Hôpital's rule, which presumes more regularity than the standing assumptions give; positivity of the numerator and denominator of $\underline{\underline{\beta}}$, the strict bounds $z_s<R<1$, and the existence and uniqueness of $\underline{\underline{\Delta}}$ all rest on continuity and strict increase of $F$ near $F^{-1}(z_s)$. The case $\beta=0$ in part (ii) is degenerate: the argument of $R^{-1}$ is then $1$, which $R$ never attains.

Formalization scope

The source is the authors' manuscript of 2022-06-06; theorem numbers, equation numbers and pages are the manuscript's. The model is a structure with real fields $c,w,r,\mu_L,\mu_H,\underline{\varepsilon}$ and a measure $P$ on $\mathbb R$ (the law of $\varepsilon$), with $F=$ cdf P. Every theorem assumes the standing hypotheses:

• $P$ is a probability measure, absolutely continuous with respect to Lebesgue measure;
• $\varepsilon$ is integrable with mean zero (integrability is implicit in "zero-mean");
• $\underline{\varepsilon}<0$, $F(\underline{\varepsilon})=0$, and $F$ is strictly increasing on $\{x\ge\underline{\varepsilon}:F(x)<1\}$ (added: the paper uses $F^{-1}$ as an inverse);
• $0<\mu_L<\mu_H$, $\mu_L+\underline{\varepsilon}\ge0$, and $c<w<r$ together with the added $c>0$.

The profits $\pi_s,\pi_r,v_r$ are Bochner integrals against $P$, $\underline{\underline{\beta}}$ is the plain quotient of profit differences (the first expression of (14)), and conditions (12)–(13) are the payoff comparisons themselves. Defining any of these by the paper's closed forms would make the milestones definitional and is ruled out. $R$ is used only at $d>0$; $\underline{\underline{\Delta}}$ is characterized as the unique positive root rather than through a junk inverse, and part (ii) is stated for $\beta\in(0,1]$. The supply-chain profit $\pi_{sc}$ is taken at advance order $0$, as in the proof of Proposition 1. The prior over market states and the signaling and pooling equilibria (Theorems 3–4) are outside this mission.

Mathlib provides distribution functions, Bochner and interval integrals and limits. A complete development needs layer-cake identities for $\mathbb E[\min(K,\cdot)]$ and $\mathbb E[(\cdot)^+]$ in terms of $\int F$, continuity of the CDF of an absolutely continuous law, and the monotonicity and limits of interval averages of a monotone function; these are reusable well beyond this model. Proofs of any milestone, or of general lemmas they need, are welcome.

Selected references

• T. Avinadav and N. Shamir, Partial Vertical Ownership, Capacity Investment, and Information Exchange in a Supply Chain, Management Science, 2023 (authors' manuscript of 2022-06-06). https://doi.org/10.1287/mnsc.2023.4673
• V. P. Crawford and J. Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390
• Ö. Özer, Y. Zheng and K.-Y. Chen, Trust in Forecast Information Sharing, Management Science 57(6), 2011. https://doi.org/10.1287/mnsc.1110.1348