All missions

Motivation

Many planning problems ask for a decision that varies over a time horizon and must satisfy a constraint at every instant, possibly with cumulative effects of past decisions. The applications in the source paper are a maximum-flow problem with time-varying pipeline capacities, a wireless coverage problem for a moving target region, and the approximation of Pareto curves of bi-objective semidefinite programs. Ahmadi and El Khadir (arXiv:1808.03994, Mathematics of Operations Research, 2021) model these as time-varying semidefinite programs (TV-SDPs), a common generalization of semidefinite programming and of the continuous linear programs of Bellman (1953), Tyndall (1965) and Levinson (1966), which are the case of diagonal matrices.

A TV-SDP is an infinite-dimensional problem: its variable is a function. The paper's main message is that, under a strict feasibility assumption, nothing is lost by searching only over polynomial solutions, and that the best polynomial solution of a fixed degree can be computed by an ordinary SDP through sum-of-squares certificates. The first statement, Theorem 4, is what justifies the second as a convergent approximation scheme, and it is the goal of this mission.

Setting

Fix integers $n, m \ge 0$. Let $\mathbf L^n$ be the set of measurable functions $x:[0,1]\to\mathbb R^n$ that are bounded, $\sup_{t\in[0,1]}\|x(t)\|_\infty<\infty$. The data are polynomial: an objective $c=(c_1,\dots,c_n)$ of univariate polynomials, symmetric $m\times m$ matrices $A_0(t),\dots,A_n(t)$ with polynomial entries, and symmetric $m\times m$ kernels $D_1(t,s),\dots,D_n(t,s)$ with entries polynomial in $(t,s)$. For $x\in\mathbf L^n$ define the matrix function

$$\mathcal Fx(t)=A_0(t)+\sum_{i=1}^n x_i(t)A_i(t)+\sum_{i=1}^n\int_0^t x_i(s)\,D_i(t,s)\,ds .$$

A function $x$ is feasible if $x\in\mathbf L^n$ and $\mathcal Fx(t)\succeq0$ for almost every $t\in[0,1]$. The TV-SDP is

$$\mathrm{opt}=\sup\Bigl\{\langle c,x\rangle_{\mathbf L^n}=\int_0^1\langle c(t),x(t)\rangle\,dt \;:\; x \text{ feasible}\Bigr\}\in[-\infty,+\infty].$$

It is strictly feasible if some $x^s\in\mathbf L^n$ and $\varepsilon>0$ satisfy $\mathcal Fx^s(t)\succeq\varepsilon I$ for almost every $t\in[0,1]$. A polynomial solution is $x(t)=(p_1(t),\dots,p_n(t))$ for polynomials $p_i$.

The proof uses the mollifying operators $\mathcal M_v$, $v\in\mathbb N$: with the bump $J(t)=c\,e^{-1/(1-t^2)}$ for $|t|<1$, $J(t)=0$ otherwise, normalized so that $\int_{\mathbb R}J=1$,

$$\mathcal M_vf(t)=\int_0^1 v\,J(v(t-s))\,f(s)\,ds ,$$

applied entrywise to vector- and matrix-valued functions. In Lean these are Ln, Sm, Data, F, Feasible, StrictlyFeasible, obj, opt, polySol, J, cJ, Mv, MvVec and MvMat in the namespace TVSDP.PolyOpt.

Formalization targets

Goal: Theorem 4 (p. 11)

If the TV-SDP is strictly feasible, there are polynomial vectors $p^k$ such that every $x^k=p^k$ is feasible and

$$\langle c,x^k\rangle_{\mathbf L^n}\longrightarrow\mathrm{opt}\qquad(k\to\infty),$$

the limit taken in the extended reals, so $\mathrm{opt}=+\infty$ is included.

Milestones

1. Proof of Theorem 4, p. 13. For feasible $x$ and strictly feasible $x^s$ with margin $\varepsilon$, the combination $(1-\lambda)x+\lambda x^s$ satisfies $\mathcal F(\cdot)\succeq\lambda\varepsilon I$ a.e., and its objective tends to $\langle c,x\rangle$ as $\lambda\to0^+$.
2. Proposition 1, p. 11 (first two sentences). $\mathcal M_vf$ is continuous and $\int_0^1|\mathcal M_vf-f|\to0$ for bounded measurable $f$.
3. Lemma 3(a), p. 12. $M(t)\succeq0$ a.e. implies $\mathcal M_vM(t)\succeq0$ for all $t\in[0,1]$.
4. Lemma 3(b), p. 12, and the explicit rate of its proof: $\sup_{t\in[0,1]}|a(t)\mathcal M_vx(t)-\mathcal M_v(a\cdot x)(t)|\le L\gamma/v\to0$ for polynomial $a$.
5. Proof of Theorem 4, p. 13 (minimum-eigenvalue step). If $G(t)\succeq\beta I$ on $[0,1]$ and $\sup_t\|G(t)-H_v(t)\|\to0$, then $H_v(t)\succeq\frac\beta2 I$ on $[0,1]$ for large $v$.
6. Proof of Theorem 4, pp. 13–14. $\sup_t\|\mathcal Fx(t)-\mathcal Fy(t)\|\le C\sup_t\|x(t)-y(t)\|_\infty$ with $C=\sup_{t,s\in[0,1]}\sum_i(\|A_i(t)\|+\|D_i(t,s)\|)$.

Significance

The result. Theorem 4 says that the supremum of a strictly feasible TV-SDP over polynomial solutions equals its supremum over all bounded measurable solutions. Combined with the paper's Theorem 6, which computes the best degree-$d$ polynomial solution by an SDP, it shows that these SDP values form a nondecreasing sequence of lower bounds converging to $\mathrm{opt}$. Without it, the polynomial restriction could have a strictly smaller value; Example 1 of the paper shows that this happens when strict feasibility fails, where the unique feasible solution is a step function.

Formalizing it. The result is proved in the paper, not formalized anywhere. A machine-checked proof also has to repair the printed argument: the operator $\mathcal M_v$ integrates over $[0,1]$ only and is not normalized near the endpoints ($\mathcal M_v1(0)=\tfrac12$ for $v\ge1$), so three auxiliary statements of §3.1 are false as printed (see Formalization scope), although Theorem 4 itself is true. Any complete proof therefore needs an argument that handles the endpoints, which the formal development would record.

Difficulty

The natural route is "perturb into the strict interior, smooth, approximate by polynomials", and each step preserves feasibility only up to a uniform error, so the margin $\varepsilon$ must survive all three. The difficulty is uniformity on the closed interval: smoothing commutes with $\mathcal F$ only approximately, the Volterra term $\int_0^t x_i(s)D_i(t,s)\,ds$ couples times, and at $t=0$ and $t=1$ the mollifier of Definition 3 loses half its mass. Applying the printed Corollary 1 directly fails at the endpoints. In Lean, a further cost is the bookkeeping between "almost every $t\in[0,1]$" for feasibility and "every $t\in[0,1]$" for the smoothed and polynomial solutions.

Formalization scope

Conventions committed to:

• Functions are total maps on $\mathbb R$; only their values on $[0,1]$ matter. "Almost every $t\in[0,1]$" is with respect to Lebesgue measure restricted to $[0,1]$ (volume.restrict (Set.Icc 0 1)), never Lebesgue measure on $\mathbb R$.
• $\mathbf L^n$ is bounded and measurable, with the sup norm on $\mathbb R^n$; the bold $\mathbf L^1$ of the paper is $\mathbf L^n$ with $n=1$, not Lebesgue $L^1$.
• The data are polynomial (the paper's standing assumption, p. 3), with symmetric polynomial matrices. Theorem 4 is false for general bounded measurable data.
• $\mathcal F$ is defined entrywise; the kernel term is an interval integral, with variable $0$ of $D_i$ the outer time $t$ and variable $1$ the integration variable $s$.
• $\mathrm{opt}$ is an EReal supremum; the matrix inequality $X\succeq\beta I$ is positive semidefiniteness of $X-\beta I$.
• $J(\pm1)=0$ (the page's formula is undefined there); $\mathcal M_v$ is defined for $v\in\mathbb N$ exactly as in Definition 3, without normalization.
• Matrix norms are the entrywise maximum; the page allows any matrix norm.

Trivializations ruled out: feasibility is a.e. on $[0,1]$ only, solutions in $\mathbf L^n$ are bounded, $\mathrm{opt}$ is not a real sSup (which would be $0$ on an unbounded set), and polynomial solutions are genuine polynomials evaluated everywhere, not functions that agree with a polynomial almost everywhere.

Deliberately absent: the third sentence of Proposition 1 (uniform convergence $\mathcal M_vf\to f$ for continuous $f$), Lemma 3(c) and Corollary 1. All three are false for the operator of Definition 3 because of the endpoint effect; for example, Corollary 1 fails for $x=0$, $A_0=I$ at $t=0$. The printed constant $C$ on p. 14 has $D_i(s,t)$ in place of $D_i(t,s)$, and with it the Lipschitz display fails; milestone 6 uses the corrected constant. Measurability of $M$ is added in Lemma 3(a), where the paper uses it implicitly.

Infrastructure needed: interval mollification of bounded measurable functions, uniform convergence on $[0,1]$, the Weierstrass approximation theorem for $\mathbb R^n$-valued functions (in Mathlib), and Loewner-order perturbation bounds. The mollifier and the Loewner perturbation lemma are reusable beyond this mission. Contributions of proofs for any milestone, of the missing endpoint-robust smoothing step, and of the paper's Example 1 are welcome.

Selected references

• A. A. Ahmadi and B. El Khadir, Time-varying semidefinite programs, Mathematics of Operations Research, 2021; arXiv:1808.03994v2. https://arxiv.org/abs/1808.03994
• R. Bellman, Bottleneck problems and dynamic programming, Proceedings of the National Academy of Sciences 39(9), 1953. https://doi.org/10.1073/pnas.39.9.947
• W. F. Tyndall, A duality theorem for a class of continuous linear programming problems, Journal of the SIAM 13(3), 1965. https://doi.org/10.1137/0113044
• N. Levinson, A class of continuous linear programming problems, Journal of Mathematical Analysis and Applications 16(1), 1966. https://doi.org/10.1016/0022-247X(66)90184-3
• R. A. Adams and J. J. F. Fournier, Sobolev Spaces, 2nd ed., Academic Press, 2003 (Theorem 2.29, cited for Proposition 1).

Why process flexibility matters

A factory can respond to uncertain demand by allowing a plant to make more than one product. Those extra capabilities cost money, so the design question is where to place a limited number of plant–product links. The usual measure of a flexible production system is the number of units sold. When products have different contribution margins, however, two designs with the same sales may earn different profits: capacity used for a low-margin product cannot then serve a high-margin one. Wang, Wang and Zhang study this distinction through worst-case demand and show that a particular arrangement of two product classes is optimal within the family of long chains (Wang, Wang and Zhang 2020, §§1 and 4).

The result addresses a concrete design choice. A long chain gives every plant two product capabilities and connects the system in a cycle. If half the products have high margins and half low margins, should the two classes be grouped on that cycle or spread out? The paper's answer is that alternating high- and low-margin products gives at least as good a worst-case score as every other long-chain arrangement, for a broad class of scores.

Production and uncertain demand

A flexibility design $A$ is a set of arcs $(j,i)$ from plant $j$ to product $i$. Plant $j$ has capacity $C_j$, product $i$ has demand $d_i$ and margin $p_i$, and $x_{ij}$ units of product $i$ are made by plant $j$. The maximum profit $g(A,d)$ is the optimum of the finite linear program

$$g(A,d)=\max_{x\ge0}\sum_{(j,i)\in A}p_i x_{ij},\qquad \sum_jx_{ij}\le d_i,\quad \sum_i x_{ij}\le C_j.$$

Products fall into $T$ categories with margins $P_1<\cdots<P_T$. Write $S_t$ for the products with margin $P_t$ and $D_t(d)=\sum_{i\in S_t}d_i$ for their total demand. A deterministic score in the paper's class has the form $f(A,d)=h(g(A,d),(D_t(d))_t)$, with $h$ strictly increasing in its profit argument when category totals are fixed. Its robust score is $R^f(A,U)=\min_{d\in U}f(A,d)$ for an uncertainty set $U$ of nonnegative demand vectors. This includes maximum profit and scores that subtract a demand-based benchmark from profit (Wang, Wang and Zhang 2020, §2.2).

A set is part-wise independently symmetric when it is a Cartesian product of its category projections and remains unchanged if products are permuted within any category. The perturbation version applies that property to $E=\{d-\mu:d\in U\}$ for a fixed centre $\mu$. Such sets preserve the high/low distinction while treating products within each class interchangeably (Wang, Wang and Zhang 2020, Definitions 2.1–2.2).

Formalization targets

Alternate-chain optimality

In the target system there are $2k$ plants and $2k$ products, $k\ge1$, with unit plant capacities and exactly $k$ products in each of two margin classes $0<P_L<P_H$. A long chain places the fixed products in any cyclic order and connects each plant to two consecutive products. An alternate long chain places high- and low-margin products alternately. The goal, Theorem 3, says that for every such pair of chains, every part-wise independently symmetric $U$, and every robust score in the class above,

$$R^f(\mathrm{AL},U)\ge R^f(L_{HL},U).$$

This is the paper's worst-case comparison, rather than a claim about a single demand instance or a single performance measure (Wang, Wang and Zhang 2020, Theorem 3, p. 21).

Margin-group comparisons

The paper defines a dual margin group index $\delta^K_\mu(A)$ by an integer program that assigns product dual values from the finite menu $\beta_{tr}=P_t-P_r$, where $P_0=0$. The parameter $K$ counts how many products in each category receive each nonzero menu value. Its feasible set is $Q$. Theorem 1 expresses every robust score in terms of these indices and residual demand vectors; Theorem 2(a) says that index dominance for every $K\in Q$ implies robust-score dominance. Lemma 2 evaluates the index of an alternate chain in three cases, and Proposition 1 compares it with every long chain (Wang, Wang and Zhang 2020, pp. 17–22). These are the mission's milestones, alongside the profit LP's duality and two cyclic-window statements used in the comparison.

What the result provides

Within balanced, unit-capacity, two-margin long chains, the theorem resolves placement of the high-margin products without choosing one demand distribution or one profit-based robustness score. The dominance holds across the paper's whole class of category-symmetric uncertainty sets and scores. It gives a design rule within that family; it does not claim that an alternate chain beats every possible two-capability graph. The paper separately studies limits of that broader comparison (Wang, Wang and Zhang 2020, §4.3).

The paper proves these results on paper. This mission asks for machine-checked proofs of the stated Lean targets. Its reusable output includes the finite bipartite profit LP, its dual, category-wise demand symmetry, and the DMGI representation. None of the mission's theorems is presented here as already machine-checked.

Where the formal proof is difficult

The LP optimum must be related to a dual optimum whose product variables belong to a small, margin-dependent set. That is stronger than merely invoking an objective-value duality statement. The robust representation then has to account for both a discrete assignment of dual values and the permissible permutations of demand residuals within each product class. The last comparison is combinatorial: a general long chain can have runs of high-margin products, and its relevant cyclic windows must be compared with the alternating chain across every feasible count vector $K$ (Wang, Wang and Zhang 2020, Appendix A).

Formalization scope

The Lean development represents plants and products by finite index types, real capacities, demands and margins, and a design by a finite set of plant–product pairs. A separate general profit-LP definition is instantiated by the paper's margin-category system. Lean indices start at zero: category $t$ is the paper's category $t+1$, and the added margin level $P_0$ is zero. The production variable is written x j i in Lean for the paper's $x_{ij}$. Category residuals are enumerated by increasing product index; part-wise symmetry makes that choice immaterial. A long chain uses a permutation of fixed products around a cycle, so the uncertainty set stays attached to the same high- and low-margin categories.

The system requires positive numbers of plants, products and occupied margin categories, nonnegative capacities, and positive strictly increasing margins. The paper treats margins as positive profits but does not state that inequality explicitly. The model also supplies $z_j\ge0$ to the DMGI program, matching the dual program and the use of dual feasibility in the paper's proof; equations (4) and (5) omit this line. For the robust minimum, $U$ is nonempty, compact and contained in nonnegative demand, and the deterministic score is continuous there. Nonemptiness and compactness are explicit mathematical additions needed for the paper's minimum and minimizer. Every DMGI theorem restricts $K$ to $Q$. These conditions prevent empty or unbounded real infima from supplying Lean's default zero. The $k=1$ case is included.

Contributions may establish the LP duality, dual extreme-point structure, robust representations, exact alternate-chain index, or cyclic-window comparison. The definitions use finite sums and real suprema and infima; establishing attainment is part of the theorem work.

Selected references

• S. Wang, X. Wang and J. Zhang, Robust Optimization Approach to Process Flexibility Designs with Contribution Margin Differentials, Manufacturing & Service Operations Management, 2020. SSRN author version 3233721, 22 May 2020; DOI.

Why queue position has a price

A customer who is short of time may pay for a better place in a service queue. Unlike resale of a fixed ticket, this transaction changes the waits faced by later customers, and those customers' choices then change the value of the position being sold. Yang, Wang, and Cui study this feedback in an unobservable queue with a firm that repeatedly sells its place to arriving customers. Their single-scalper analysis identifies demand levels at which such a firm enters, rather than assuming that more customer traffic always makes entry more attractive (Yang, Wang, and Cui 2021, §§3–4).

The mission targets a precise claim about that entry decision. Low demand leaves few sales; very high demand forces more customers to balk and limits what a buyer will pay. The result is a possibly empty interval of demand volumes in which the scalper enters. The associated price and revenue results are useful milestones because they describe the economics of that interval using the same customer equilibrium as the entry theorem (Yang, Wang, and Cui 2021, Propositions 2–4).

Service system and customer equilibrium

The service system is an M/M/1 queue: potential customers arrive as a Poisson process at rate $\Lambda$, and a single server completes service at exponential rate $\mu>0$. Customers cannot observe the queue length or their positions. Every customer values completed service at $V$ and has a private delay cost $c$ per unit time. In this mission, $c$ is uniform on $[0,1]$ and $V>1/\mu$. A queue-scalping firm may place one scalper in line. Under the head-queueing rule, the scalper can hold the first position without blocking service while waiting to sell it to a customer. After a sale, the scalper returns to the tail. The firm pays cost $k$ per unit time for the scalper and charges a nonnegative price $P$ per sale (Yang, Wang, and Cui 2021, pp. 5–9, Lemma 1).

Customers use two cutoffs. Customers below $\tilde c$ join without buying, customers from $\tilde c$ through $c^S$ join and buy, and customers above $c^S$ balk. The actual throughput is $\lambda=\Lambda c^S$; the share of joining customers who buy is $q=(c^S-\tilde c)/c^S$. A customer with delay cost $\tilde c$ is indifferent between buying and not buying. A customer at $c^S$ can join and buy, while the corresponding utility is zero if any customers balk. These are the customer-equilibrium equations (1b)–(1d) of the paper, with $0< c^S\le1$, $0\le\tilde c\le c^S$, and stable throughput $\lambda<\mu$ (Yang, Wang, and Cui 2021, pp. 7–9).

Let $W^I_1(\lambda,q)$ be a buyer's expected delay and $W^I_2(\lambda,q)$ a nonbuyer's expected delay under the head-queueing rule. Their difference $D^I(q)=W^I_2-W^I_1$ is the buyer's delay saving. Optimal revenue $\Pi(\Lambda)$ is the attained maximum of $P\lambda q$ over nonnegative prices and compatible customer equilibria. If the firm stays out, its profit is zero. If it enters, its best profit is $\Pi(\Lambda)-k$. At equality the model takes the no-entry decision, as in the proof's entry criterion $\Pi>k$ (Yang, Wang, and Cui 2021, equation (1a), Proposition 4 and its Online Appendix proof).

Formalization targets

Entry at intermediate demand

For fixed $\mu$, $V$, and $k>0$, Proposition 4 asserts that thresholds $\underline\Lambda\le\overline\Lambda$ exist such that every positive demand volume has an optimal customer-equilibrium revenue and

$$N^*(\Lambda)=\begin{cases} 1,&\underline\Lambda<\Lambda<\overline\Lambda,\\ 0,&\text{otherwise}. \end{cases}$$

The interval can be empty. The thresholds depend on the system parameters, rather than on the demand volume being tested (Yang, Wang, and Cui 2021, Proposition 4, p. 12).

Price and revenue structure

Proposition 2 gives the optimal price in the all-join regime $\Lambda\le\mu-1/V$ and the balking regime $\Lambda>\mu-1/V$, and says that this price is unimodal. Proposition 3 says that optimal revenue is also unimodal, with a unique peak $\Lambda^*\ge\mu-1/V$. The Online Appendix identifies the cutoff $c^S$, reduces the pricing problem to the buying cutoff $\tilde c$, gives the revenue expression in each regime, and shows that revenue less cost approaches $-k$ at both extreme demand levels (Yang, Wang, and Cui 2021, Propositions 2–3, Online Appendix pp. 1–3).

What the result provides

The entry theorem classifies queue demand by the scalper's decision while allowing the equilibrium buying and balking rates to change with price. It explains why a queue with more arrivals can become less attractive to a scalper even though it offers more potential buyers. The price and revenue milestones also distinguish two operational regimes: one in which everyone joins, and one in which joining itself contracts as demand rises (Yang, Wang, and Cui 2021, §§4.1 and 9).

The paper proves these results mathematically; this mission asks for machine-checked proofs of the statements under an explicit model interface. The reusable output includes formulas for the two customer delay classes, a predicate for cutoff-based customer equilibrium, and an attained joint optimization predicate. A formal proof of entry must connect the closed-form revenue analysis to that optimization predicate. At the draft stage, the proposed theorem statements compile with sorry; they are not yet machine-checked proofs.

Where the difficulty lies

More arrivals directly create more opportunities to sell a place, but customer behavior also changes the number who join, the fraction who buy, and the price they will pay. Holding any one of these responses fixed gives the wrong entry question. The challenging point is to establish a single rise and fall of optimal revenue across the boundary between the all-join and balking regimes, while keeping the customer equilibrium and the price optimization tied together. The endpoint behavior matters as well: an interval theorem needs no entry at sufficiently low and sufficiently high demand, including the possibility that the entry interval is empty (Yang, Wang, and Cui 2021, Propositions 2–4 and Online Appendix A).

Formalization scope

Lean represents $\mu,V,k,\Lambda,\lambda,P,q,c^S,\tilde c$ as real numbers and the entry decision $N^*$ as either zero or one. Params.Standing records $\mu>0$, $V>1/\mu$, and $k\ge0$. Proposition 4 additionally assumes $k>0$; the Online Appendix uses the negative limit $-k<0$, and at zero cost the high-demand nonentry threshold need not be finite. Statements concerning demand use $\Lambda>0$. The positive cutoff $c^S$ makes the purchase-rate quotient meaningful, and stable throughput keeps the queue-delay denominators positive.

The delay formulas of Lemma 1 are taken as the model's delays; their underlying stationary queueing-process derivation is outside this mission. The uniform CDF is the identity on $[0,1]$. The paper's optimization is represented by an attained maximum over prices and customer equilibria, rather than by a supremum of arbitrary real values. The entry goal includes existence of an optimizer at every positive demand, so missing feasible equilibria cannot make the result vacuous. Contributions that establish equilibrium cutoff uniqueness, exact reduction of the pricing problem, price and revenue optimality, and the resulting demand shape are all within scope. The definitions of the equilibrium and optimum can be reused in further analysis of queue position sales under the same rule.

Selected references

• Luyi Yang, Zhongbin Wang, and Shiliang Cui, A Model of Queue-Scalping, Management Science, 2021, authors' manuscript and Online Appendix. DOI: 10.1287/mnsc.2020.3865.

Why the disparity is uncertain

An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).

The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.

Observed information and compatible joints

Let decision $\hat Y\in\{0,1\}$ and true outcome $Y\in\{0,1\}$. The protected class $A\in\{a,b\}$ has two groups, with $a$ conventionally advantaged and $b$ disadvantaged. The proxy $Z$ takes values in a measurable space $\mathcal Z$; it may be categorical, continuous, or mixed. The primary marginal is $P(\hat Y,Y,Z)$, and the auxiliary marginal is $P(A,Z)$. Both share one proxy distribution $P(Z)$, as required when they arise from a common population joint law.

For each proxy value $z$, write $\eta_{\mathrm{aux}}(\alpha,z)=P(A=\alpha\mid Z=z)$ and $\eta_{\mathrm{priT}}(\hat y,y,z)=P(\hat Y=\hat y,Y=y\mid Z=z)$. Their decision marginal is $\eta_{\mathrm{pri}}(\hat y,z)=\sum_y\eta_{\mathrm{priT}}(\hat y,y,z)$. A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set $\mathcal P_D$ contains all measurable conditional joint arrays $\pi(\alpha,\hat y,y\mid z)$ that couple $\eta_{\mathrm{priT}}(\cdot,\cdot,z)$ and $\eta_{\mathrm{aux}}(\cdot,z)$ at each $z$, together with the fixed $P(Z)$. It imposes no additional assumptions on the unknown association of class and outcomes.

The demographic disparity of a compatible joint $P'$ is $\delta_{DD}(a,b;P')=P'(\hat Y=1\mid A=a)-P'(\hat Y=1\mid A=b)$. Its partial identification set is

$$\Delta_{DD}(\mathcal P_D)=\{\delta_{DD}(a,b;P'):P'\in\mathcal P_D\}.$$

This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.

Formalization targets

For a group $\alpha$, decision $\hat y$, and proxy value $z$, define the Fréchet–Hoeffding weight endpoints

$$w^L_\alpha(\hat y,z)=\max\left\{0,1+\frac{P(A=\alpha\mid Z=z)-1}{P(\hat Y=\hat y\mid Z=z)}\right\},\qquad w^U_\alpha(\hat y,z)=\min\left\{1,\frac{P(A=\alpha\mid Z=z)}{P(\hat Y=\hat y\mid Z=z)}\right\}.$$

For a class weight function $w$, let $\mu(\alpha;w)=E[w_\alpha(\hat Y,Z)\hat Y]/P(A=\alpha)$. The goal, Proposition 7, is the equality

$$\Delta_{DD}(\mathcal P_D)= \left[\mu(a;w^L)-\mu(b;w^U),\;\mu(a;w^U)-\mu(b;w^L)\right].$$

Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).

What the result gives

The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.

Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.

Central difficulty

The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome $Y$ remains in the compatible-joint model even though demographic disparity uses only $\hat Y$. When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.

Formalization scope

The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on $Z$ and measurable, normalized, nonnegative conditional vectors $\eta_{\mathrm{aux}}$ and $\eta_{\mathrm{priT}}$. The set $\mathcal P_D$ consists of measurable conditional couplings for every $z$. Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of $\delta_{DD}(a,b;P')$ is computed from $P'$, not inserted from the auxiliary marginal.

The theorem explicitly assumes $P(A=a)>0$ and $P(A=b)>0$, since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every $z$ selects a version and does not change the attainable disparities. On a cell with $P(\hat Y=\hat y\mid Z=z)=0$, weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.

The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.

Selected references

• Nathan Kallus, Xiaojie Mao, and Angela Zhou, Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination, Management Science 68(3), 2022; preprint arXiv:1906.00285v2, 2020. Pinned preprint.

Motivation

Prices of staple vegetables in India, onions above all, rise sharply at irregular intervals. When they do, governments respond with cash transfers, subsidized sales and import programmes. A recurring explanation for these price spikes is artificial shortage: traders who control a large share of the stock withhold supply early in a season, and consumers who observe the scarcity raise the amount they are willing to spend on the commodity, so the traders sell more later at a higher price. Levi, Singhvi and Zheng (SSRN 3332493; Manufacturing & Service Operations Management) give a stylized model of this mechanism. It shows that a monopolist trader facing budget-adjusting consumers creates an artificial shortage. It then asks how three common government interventions change the shortage. This mission formalizes the paper's answer for the first intervention, a cash subsidy (CS) to the poorest consumers. The question matters for policy: the paper argues that a well-intended transfer can make the hoarding worse.

Setting

A unit mass of consumers have Period-1 budgets $b_c$ distributed uniformly on $[0,1]$. A monopolist trader sells over two periods.

• Period 1. The trader releases $q_1\in[0,1]$, which clears at price $p_1=1-q_1$. Consumers interpret $q_1<1$ as a shortage and scale their budgets by the updated-budget multiplier

$$B(q_1)=1+g(1-q_1),$$

where $g>0$ is the budget adjustment factor.

• Period 2, no intervention. A consumer buys at price $p_2$ iff $b_cB(q_1)\ge p_2$. The trader's total revenue is $q_1(1-q_1)+B(q_1)q_2(1-q_2)$.
• Artificial shortage (Definition 1): $q_1<q_2$ and $p_1<p_2$, i.e. less is sold early and the later price is still higher.

Under a cash subsidy $(c,f)$, the government gives cash $c\ge0$ to the fraction $f\in[0,1]$ of consumers with the lowest budgets, within a budget $cf\le b$. At price $p$:

• a non-subsidized consumer ($b_c\ge f$) buys iff $b_c\ge p/B(q_1)$;
• a subsidized consumer ($b_c<f$) buys iff $b_c\ge(p-c)/B(q_1)$.

The game is solved by backward induction:

1. the trader sets the Period-2 price, maximizing revenue;
2. the government, after observing $q_1$, chooses $(c,f)$ to maximize Period-2 consumer welfare $CW_2$ (eq. (5)) at the trader's response. $CW_2$ measures the buyers' original budgets against the price they pay, adds the cash they receive, and counts a utility $\lambda$ per buyer and $-\lambda$ per non-buyer, with $1+g<\lambda$;
3. the trader chooses $q_1$, anticipating both.

The set of equilibrium Period-1 quantities is $\mathrm{EqQ1}(b)$. An element is written $q^1_{CS}$, and $q^1_\phi$ is the no-intervention quantity.

Formalization targets

Goal: Proposition 3 (p. 22)

With $\bar b=(8+4g+g^2)/32$, there is a threshold $t_1\in(0,\bar b)$ such that

$$q^1_{CS}=q^1_\phi\ (b<t_1),\qquad q^1_{CS}\ge q^1_\phi\ (t_1<b\le\bar b),\qquad q^1_{CS}<q^1_\phi\ (b>\bar b),$$

and $q^1_{CS}$ is non-increasing in $b$ for $b>t_1$. The equilibrium set is also nonempty for every $b\ge0$.

Milestones

• Proposition 1 (p. 10): without intervention the unique optimum is $(q_1^*,q_2^*)=(1/2-g/8,\,1/2)$, with $p_1^*=1/2+g/8$ and $p_2^*=1/2+g/4+g^2/16$.
• Remark after Proposition 1 (p. 10): for $g>0$ this optimum is an artificial shortage.
• Theorem 1 (p. 16): the government's optimal subsidy is $f^*=\min(1,b/c^*)$, with $c^*$ given by four closed forms on four budget ranges.
• Theorem 2(i)–(iii) (p. 17): $q_1^*=1/2-g/8$ for $b<t_1$, and the roots of two explicit first-order conditions on $[t_1,\bar b)$ and $[\bar b,(4+2g+g^2)/4)$.
• Theorem 2(iv), corrected (p. 17): for $b>(4+2g+g^2)/4$,

$$q_1^*=\max\{0,(1-g)/2,1-(b-1)/g\}.$$

Significance

Proposition 3 is the paper's verdict on cash subsidies. A small budget is absorbed without effect on the trader's behaviour, because the trader's Period-2 revenue equals its no-intervention value. A moderate budget induces a larger Period-1 release and so mitigates the shortage. A budget above $\bar b$ makes the trader withhold more than without intervention, because subsidized consumers can pay more in Period 2. The non-monotone dependence on $b$ is the basis of the paper's policy advice against "oversubsidizing" and of its comparison with supply-allocation schemes (Proposition 4, not in this mission).

The paper prints no proofs; they are "available from the authors upon request" (p. 10). The threshold $t_1$ and the online appendix (Lemma O.1) are not in the published text. A machine-checked development would therefore be the first complete public proof of these statements. It would also settle Theorem 2(iv), whose printed form is false on a band of budgets and is posed here in corrected form. None of these results has a formal proof anywhere.

Difficulty

Every stage of the backward induction is a non-smooth optimization.

• Period 2. The demand is piecewise linear with up to three pieces, so the trader's revenue is bimodal. One mode sells only to non-subsidized consumers, the other also reaches subsidized ones.
• Government. It optimizes over a two-dimensional policy against this discontinuous best response. The optimum sits at the trader's point of indifference between the two modes (Theorem 1(i)), which is attained only through the trader's tie-break toward the larger quantity.
• Period 1. The trader's objective inherits the bimodality and a kink at $b=B(q_1)$. The equilibrium therefore jumps at $t_1$, and the printed closed form fails near the kink.

The tempting route is to differentiate the Period-1 objective and solve the first-order condition. It fails twice. It misses the jump at $t_1$, where the global maximizer switches modes, and it misses the kink above $(4+2g+g^2)/4$, where the maximizer is not a stationary point.

Formalization scope

All quantities are real numbers. The trader's Period-2 decision is a price $p\ge0$ with quantity equal to the explicit demand, which is equivalent to the paper's quantity form. Purchases at equality count as purchases, as in the text. The commitments are:

• Standing assumptions: $0<g$ and $1+g<\lambda$ (pp. 10, 13), and the added $g<4$, which keeps $1/2-g/8$ in $[0,1]$.
• Tie-breaks: the trader picks the larger quantity among revenue maximizers (footnote 10). The government picks the least outlay $cf$ among welfare maximizers. Without the second rule, Theorem 1(iv) and Proposition 3(i)(c) are false, because for $b>B(q_1)$ every $c\in[B(q_1),b]$ ties.
• Equilibrium: $\mathrm{EqQ1}(b)$ is the set of $q_1\in[0,1]$ that maximize total revenue against some selection of government choices and Period-2 best responses. Every claim about $q^1_{CS}$ is made for every element.
• Existential constants: $t_1$, $b^{CS}_1$ and $b^{CS}_2$, whose formulas are not in the paper. Each is pinned by the clauses around it.

The goal is stated about $\mathrm{EqQ1}$ itself. A version that substituted Theorem 2's closed forms or first-order roots for $q^1_{CS}$ would assume the content of the theorem, and is ruled out.

The development needs the Period-2 best response of a piecewise-linear demand, the government's two-variable welfare problem (eq. (5) is a polynomial in the breakpoints), and a comparison of the two modes of the Period-1 objective. Lemmas on maximizers of piecewise-quadratic functions are reusable beyond this mission. Proofs of any milestone, and sanity lemmas on the tie-breaks, are welcome.

Selected references

• R. Levi, S. Singhvi, Y. Zheng, Artificial Shortage in Agricultural Supply Chains, Manufacturing & Service Operations Management (forthcoming; SSRN version of 2021-04-14), 2021. https://ssrn.com/abstract=3332493 — DOI of the journal version: https://doi.org/10.1287/msom.2021.1010

Motivation

A seller whose customers influence one another faces a choice between two pricing policies. It can collect information about the social network and charge each customer a personalised price that reflects their position in it, or it can ignore the network and charge everyone one uniform price. Personalised pricing is never worse for the seller, but collecting network data is costly and raises privacy concerns. The question is how much profit the network information is worth.

For a fixed network the answer depends on its fine structure. Candogan, Bimpikis and Ozdaglar (Operations Research 2012) showed that with linear-quadratic utilities the optimal personalised prices are expressed through Bonacich centralities, so the gain from discrimination is a difference of discounted walk counts. Huang, Mani and Wang (SSRN 3368458; published in Management Science, 2021) study this gain, the value of price discrimination, in large random networks. Their main result for random networks, Theorem 5.1, says that in directed Erdős–Rényi networks the seller who prices uniformly loses only a vanishing fraction of the optimal profit, whatever the density of the network. This mission formalizes that theorem and the results its proof rests on.

Setting

There are $n$ consumers. The network is an $n\times n$ matrix $G$ with non-negative entries, where $G_{ij}$ is the influence of consumer $j$ on consumer $i$. For a square matrix $A$, $\|A\|$ is its spectral norm (the $\ell^2$ operator norm); $\mathbf 1$ is the all-ones vector, and $\mathbf 1^{\mathsf T}A^k\mathbf 1$ is the total weight of walks of length $k$ in $A$.

Consumer $i$ facing price $p_i$ chooses a consumption level $x_i$ to maximise

$$u_i=ax_i-x_i^2+4\rho x_i\sum_{j\ne i}\frac{G_{ij}}{\|G+G^{\mathsf T}\|}x_j-p_ix_i,$$

with a stand-alone utility $a>0$ and a network coefficient $\rho\in(0,1)$. The resulting consumption equilibrium is (eq. (1))

$$x^*(p)=\tfrac12\Big(I-\tfrac{2\rho}{\|G+G^{\mathsf T}\|}G\Big)^{-1}(a\mathbf 1-p).$$

The seller has marginal cost $c<a$ and profit $\pi(p)=(p-c\mathbf 1)^{\mathsf T}x^*(p)$. The optimal profit is $\pi^*=\max_{p\in\mathbb R^n}\pi(p)$; the optimal uniform price is $p_0=\frac{a+c}{2}\mathbf 1$. The regret and fractional regret of uniform pricing are

$$R(p_0)=\pi^*-\pi(p_0),\qquad R_F(p_0)=1-\frac{\pi(p_0)}{\pi^*}.$$

A directed Erdős–Rényi network $G(n,p)$ is the random $0/1$ matrix whose off-diagonal entries are independent with $\Pr[G_{ij}=1]=p$, and whose diagonal is zero. $\mathbb E_G$ denotes expectation over it. The constants $a,c,\rho$ are the same for every $n$.

Formalization targets

Goal: Theorem 5.1

For every sequence of densities $(p(n))_{n\in\mathbb N}$ with values in $[0,1]$,

$$\mathbb E_{G(n,p(n))}[R(p_0)]=o(n)\qquad\text{and}\qquad\mathbb E_{G(n,p(n))}[R_F(p_0)]=o(1).$$

Both parts are stated. The goal fixes no rate and no density regime; the paper's Theorems 5.2–5.4 give exact rates in three regimes and are not part of this mission.

Milestones

1. Eq. (3): $\pi^*$ is attained and equals $\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{\rho}{\|G+G^{\mathsf T}\|}(G+G^{\mathsf T}))^{-1}\mathbf 1$, with its walk series.
2. Eq. (4): $p_0$ is the optimal uniform price, and $\pi(p_0)=\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{2\rho}{\|G+G^{\mathsf T}\|}G)^{-1}\mathbf 1$.
3. Lemma 5.3 (for even $t$): $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1\le\|G+G^{\mathsf T}\|^{k-t}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^t\mathbf 1$ for $k\ge t$.
4. Eq. (29): $\mathbb E_G[R(p_0)]\le\frac12(\frac{a-c}{2})^2\,\mathbb E_G[\frac{\rho^2}{1-\rho}\|G+G^{\mathsf T}\|^{-2}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]$.
5. Appendix D.1, Case 1, and footnote 6: a non-empty binary network has $\|G+G^{\mathsf T}\|\ge1$. In the footnote's words, "Therefore a non-empty network (with at lease one link) has spectral norm greater than or equal to 1."
6. Lemma 5.2: $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]=2n(n-1)p(1-3p+2np)$.
7. Lemma 5.5 (i): $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1]\ge2^k\mathbb E_G[\mathbf 1^{\mathsf T}G^k\mathbf 1]$ for all $k\ge0$.
8. Lemma 5.5 (ii): for $1\le k<n$ and $\frac1{n-k+1}\le p<1$, the gap in (i) is at most $(k-1)2^{k-1}P(n,k)p^{k-1}+(k-1)^k2^kP(n,k-1)p^{k-2}$, with $P(n,k)=n!/(n-k)!$.
9. Eq. (12), Rayleigh step: $\|G+G^{\mathsf T}\|\ge\mathbf 1^{\mathsf T}(G+G^{\mathsf T})\mathbf 1/\mathbf 1^{\mathsf T}\mathbf 1$.
10. Eq. (9): for non-empty $G$ and $k>0$, $0<\mathbf 1^{\mathsf T}\big((G+G^{\mathsf T})/\|G+G^{\mathsf T}\|\big)^k\mathbf 1\le n$.
11. Eq. (14): $\frac n2(\frac{a-c}2)^2\le\pi^*\le\frac12(\frac{a-c}2)^2\frac n{1-\rho}$.

The paper calls the optimal uniform price $p_0$ "under the assumption that $c<a$, according to [12]" (p. 7); milestone 2 states that optimality as part of eq. (4).

Significance

Theorem 5.1 says that in large random networks the network information has asymptotically no value to a monopolist: the uniform price $p_0$ does not depend on the network, yet earns a fraction of the optimal profit tending to one, for sparse, critical and dense networks alike. This separates the deterministic picture, where some networks have a large value of discrimination (Theorem 4.1 of the paper characterises those with none), from the typical random one. It supplies a benchmark against which network-based pricing, and the cost of collecting network data, can be judged.

The paper proves the theorem by hand. No part of it, and no part of the model, has been machine-checked; the platform has no network pricing model and no walk-count results for directed random graphs. A complete development would make the closed forms (3) and (4), the spectral inequalities and the Erdős–Rényi walk moments reusable. The printed proof of Theorem 5.1 bounds expectations of ratios by almost-sure statements and splits the density sequence into "maximal subsequences"; a formal proof must replace these steps by quantitative ones. The printed proof of Lemma 5.5 (i) relies on a per-walk claim that fails (a closed walk $0\to1\to2\to0\to1$ in $G+G^{\mathsf T}$ can use four arcs of $G$ while it visits three ordered pairs), although the statement itself was checked by exhaustive enumeration for small $n$; that lemma needs a new argument.

Difficulty

The regret is a difference of two discounted walk series. Bound (29) controls it by walks of length two and the spectral norm, which suffices when the network is very sparse, but in dense networks, where $\|G+G^{\mathsf T}\|\approx2np$ and $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1\approx4n^3p^2$, it only gives $O(n)$. The dense case needs the cancellation between $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1$ and $2^k\mathbf 1^{\mathsf T}G^k\mathbf 1$ for each $k$ up to a slowly growing cutoff (Lemma 5.5), together with a lower bound on the spectral norm that holds with high probability. In the critical regime $np=\Theta(1)$, neither bound applies directly, and one needs that $\|G+G^{\mathsf T}\|$ grows with $n$ in probability. The goal quantifies over all density sequences, so the argument must be uniform across these regimes; a proof for one regime does not suffice.

Formalization scope

All objects live in the namespace NetPriceDisc.Random and are defined in one file. Networks are Matrix (Fin n) (Fin n) ℝ; the spectral norm is Mathlib's $\ell^2$ operator norm (Matrix.Norms.L2Operator). The consumption equilibrium is formula (1) for every price vector, with no non-negativity constraint on consumption, as in the paper's definition of $\pi(p)$. $\pi^*$ is defined as the supremum of $\pi$ over $\mathbb R^n$, and $R$, $R_F$ from $\pi^*$ and $\pi(p_0)$; the closed forms (3) and (4) are theorems, not definitions, so the goal cannot be discharged by unfolding formulas. Lean's convention $x/0=0$ gives the empty network no externality, hence zero regret, which is the paper's own reading of the empty network (p. 12); the empty network keeps its probability $(1-p)^{n(n-1)}$. The Erdős–Rényi expectation is the finite sum over arc sets $S$ of off-diagonal pairs with weight $p^{|S|}(1-p)^{n(n-1)-|S|}$; no measure theory is used. The fractional regret's expectation is the expectation of the ratio. "Any sequence of densities" is a function $\mathbb N\to[0,1]$, with no further restriction.

Two printed statements are corrected and disclosed: Lemma 5.3 is stated for even $t$ (as printed it fails for odd $t$; for the star $K_{1,3}$ with $t=1$, $k=2$ one gets $12>6\sqrt3$), and Lemma 5.5 (ii) for $k\ge1$ (at $k=0$ it involves the undefined $P(n,-1)$). Only the deterministic Rayleigh-quotient part of eq. (12) is stated.

Useful infrastructure includes Neumann series and Rayleigh-quotient bounds for symmetric non-negative matrices, walk moments of directed Erdős–Rényi graphs, and maximum-degree or spectral lower bounds in probability. Proofs of any milestone, and alternative routes to the goal that avoid Lemma 5.5, are welcome.

Selected references

• J. Huang, A. Mani, Z. Wang, The Value of Price Discrimination in Large Random Networks, SSRN 3368458 (EC '19 submission version); published as The Value of Price Discrimination in Large Social Networks, Management Science, 2021. https://ssrn.com/abstract=3368458, https://doi.org/10.1287/mnsc.2021.4108
• O. Candogan, K. Bimpikis, A. Ozdaglar, Optimal Pricing in Networks with Externalities, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1066
• P. Bonacich, Power and Centrality: A Family of Measures, American Journal of Sociology 92(5), 1987. https://doi.org/10.1086/228631
• M. Krivelevich, B. Sudakov, The Largest Eigenvalue of Sparse Random Graphs, Combinatorics, Probability and Computing 12(1), 2003. https://doi.org/10.1017/S0963548302005424

Motivation

Probabilistic selling, also called opaque selling, offers a customer a product whose exact version is revealed only after purchase: a "mystery box", an unnamed hotel on a travel site, a flight whose carrier is announced after booking. The firm controls the price and the probability with which each version is delivered. The classical analyses (Fay and Xie 2008; Jerath, Netessine and Veeraraghavan 2010) assume customers know these probabilities and form rational expectations.

Huang and Yin (SSRN 3627927; Manufacturing & Service Operations Management, 2020) drop that assumption. Customers do not observe the offering probability; they infer it from a few anecdotes, which are reports of what earlier buyers received, in the spirit of the literature on the belief in small samples (Tversky and Kahneman 1971), here as a model of boundedly rational expectations. Because today's deliveries become tomorrow's anecdotes, the firm's offering decision in one period shapes demand in the next, and probabilistic selling becomes a dynamic problem. The paper's first main result, Proposition 1, solves the two-period problem when every customer draws a single anecdote.

Setting

A firm sells two versions of a product, $H$ and $L$, over two periods $t=1,2$. Each period has a fresh unit mass of customers. Every customer values $H$ at $v_H$ and $L$ at $v_L$, with $v_H>v_L$; unit costs are $c_H>c_L$; and $c_L\le v_L$.

In period $t$ the firm posts one price $p_t$ for the opaque product and delivers $H$ with probability $\xi_t\in[0,1]$. A customer draws one anecdote and estimates the $H$-probability as $\tilde\xi=(\xi_0+\mathbf 1\{\text{anecdote}=H\})/2$ with prior $\xi_0=0$, so $\tilde\xi\in\{0,\tfrac12\}$. She buys if and only if

$$\tilde\xi\,v_H+(1-\tilde\xi)\,v_L\ \ge\ p_t .$$

A period-1 anecdote is $H$ with probability $\xi_1$. A period-2 anecdote comes from period 1 with probability $\alpha\in[0,1]$ and from period 2 otherwise, so it is $H$ with probability $\alpha\xi_1+(1-\alpha)\xi_2$. Writing $\gamma_t$ for the purchasing fraction, the firm's profit is

$$\Pi(\xi_1,\xi_2\mid p_1,p_2)=\sum_{t=1,2}\gamma_t\,[p_t-\xi_tc_H-(1-\xi_t)c_L].$$

The price $v_{HL}=\frac{v_H-v_L}{2}+v_L$ is what a customer with an $H$ anecdote is willing to pay; $v_L$ is what everyone pays. The alternative is transparent selling: one version $m$ at prices $q_1,q_2$, bought in period $t$ iff $q_t\le v_m$.

Formalization targets

Goal: Proposition 1

Let $\bar\alpha=\frac{\sqrt{17}-3}{2}$, $r=\frac{v_{HL}-c_L}{c_H-c_L}$ and $M=\max\{v_H-c_H,v_L-c_L\}$. Over all feasible opaque and transparent policies:

• (i) if $0\le\alpha<\bar\alpha$, $r<\frac{4-4\alpha-\alpha^2}{2-\alpha-\alpha^2}$ and $\frac{(1-\alpha)(v_{HL}-c_L)^2}{(4-4\alpha-\alpha^2)(c_H-c_L)}>M$, the optimal policy is

$$p_1^*=p_2^*=v_{HL},\quad \xi_1^*=\frac{(2-\alpha-\alpha^2)(v_{HL}-c_L)}{(4-4\alpha-\alpha^2)(c_H-c_L)},\quad \xi_2^*=\frac{(2-3\alpha-\alpha^2)(v_{HL}-c_L)}{(4-4\alpha-\alpha^2)(c_H-c_L)},$$

with profit $\Pi^*=\frac{2(1-\alpha)(v_{HL}-c_L)^2}{(4-4\alpha-\alpha^2)(c_H-c_L)}$;

• (ii) if $\bar\alpha\le\alpha\le1$, $r<\frac{2}{1+\alpha}$ and $\frac{(1+\alpha)^2(v_{HL}-c_L)^2}{8(c_H-c_L)}>M$, the optimal policy is

$$p_1^*=p_2^*=v_{HL},\quad \xi_1^*=\frac{(1+\alpha)(v_{HL}-c_L)}{2(c_H-c_L)},\quad \xi_2^*=0,\qquad \Pi^*=\frac{(1+\alpha)^2(v_{HL}-c_L)^2}{4(c_H-c_L)};$$

• (iii) otherwise, transparent selling of the version with the larger margin, at its valuation in both periods, is optimal, with $\Pi^*=2M$.

Milestones

In the order the paper's argument uses them:

1. Lemma 1 for one anecdote: the demands at $v_L$ and $v_{HL}$, and the reduction of every price pair to these two candidates;
2. displays (3)–(6): the profit at each of the four candidate price pairs;
3. the §3.3 benchmark: transparent selling earns at most $2M$;
4. Lemma 2 (i) and (ii): maximizers of (3) on $[0,1]^2$ in seven regimes;
5. Lemma 3: maximizers of (4);
6. Lemma 4, in corrected form: (5) is dominated by (3) or (4);
7. the claim after (6): $\xi_1=\xi_2=0$ is optimal at $p_1=p_2=v_L$;
8. from the proof of Proposition 1: the price pair $(v_{HL},v_L)$ is never strictly better than the best of (3) and transparent selling;
9. from the same proof: in the corner regimes of Lemma 2, the policy $(v_{HL},v_{HL})$ earns at most $2M$.

Significance

The result says when, and how, a firm should randomize its product delivery when customers learn from anecdotes. The optimal offering probability is decreasing over time, $\xi_1^*>\xi_2^*$: the firm delivers the high version generously early, so that period-1 deliveries become favourable anecdotes for period-2 customers, and then saves cost. Probabilistic selling is optimal only when both transparent margins are low, which makes it a complement to transparent selling rather than a substitute. Corollary 2 of the paper builds on Proposition 1 to show that the dynamic policy can earn up to twice the profit of the best static one.

Proposition 1 is proved in the paper's appendix (pp. 30–31), with Lemmas 1–4 proved in an online appendix. No part of it has been machine-checked. A formalization supplies the missing lemma proofs in checked form, pins down the conventions the printed statements leave implicit (tie-breaking, the price domain, the sign of $v_L-c_L$), and corrects a false part of Lemma 4 as printed. The model layer, an anecdote-based demand computed from a purchase rule, is a reusable template for other sampling-based expectation models.

Difficulty

The goal is a global optimality claim over a continuum of prices and offering probabilities and a second family of transparent policies. Lemma 1 reduces prices to two candidates, but each of the four resulting objectives is a non-separable quadratic in $(\xi_1,\xi_2)$, maximized over a box. Objective (3) has seven regimes whose boundaries depend on $\alpha$ and on the margin ratio $r$; the threshold $\bar\alpha$ is where the interior optimum's $\xi_2$ reaches zero. Comparing the regimes with each other and with transparent selling requires signed polynomial inequalities in $\alpha$ and $r$ across regime boundaries. Checking first-order conditions is not enough: in part (iii) the claim is that no opaque policy at any price beats transparent selling, which requires bounding the box maximum of every objective, including the corner regimes.

Formalization scope

Everything is real-valued and lives in the namespace DynOpaque.TwoPeriod. The definitions file states the model from its primitives: the anecdote estimate with $K=1$ and $\xi_0=0$, the purchase rule (1) with equality buying, the purchasing fraction derived from them, profit (2), transparent profit from a version and two prices, the policy type with its feasibility predicate, and global optimality. The objectives (3)–(6) are separate literal definitions, so their agreement with (2) is a theorem, not a definition.

Committed conventions, each disclosed in the statements:

• $c_L\le v_L$ is added to the paper's standing assumptions $v_H>v_L$, $c_H>c_L$, $0\le\alpha\le1$. The paper's proof uses it (p. 30), and without it $\xi_1^*$ in (i) can be negative.
• Opaque prices satisfy $p_t\le v_{HL}$. Lemma 1 places every optimal price in $\{v_L,v_{HL}\}$; above $v_{HL}$ nobody buys, there are no anecdotes, and the paper's period-2 dynamics are undefined. Transparent prices are unrestricted.
• "Otherwise" in (iii) is the negation of the full hypothesis lists of (i) and (ii).
• Lemma 4 (i) as printed ("$\xi_1=1$ or $\xi_2=0$ is optimal") is false; the mission states the corrected claim that some optimum has $\xi_1\in\{0,1\}$.
• Lemma 2's "optimal" is a maximizer over $[0,1]^2$, not a unique one.

A formalization that optimizes only over the candidate prices $\{v_L,v_{HL}\}$, defines demand by the closed forms $\xi_1$ and $\alpha\xi_1+(1-\alpha)\xi_2$, or defines the transparent value as $2M$ would make Lemma 1 or part (iii) circular; the goal quantifies over every feasible price and derives demand from the purchase rule.

The general-$K$ model (Lemma 1 with binomial sums, Proposition 3), the extensions of §5, and Corollaries 1–2 are out of scope. Proofs of any milestone are welcome, and so are reusable lemmas on maximizing quadratics over a box.

Selected references

• T. Huang and Z. Yin, Dynamic Probabilistic Selling When Customers Have Boundedly Rational Expectations, Manufacturing & Service Operations Management, 2020; SSRN manuscript 3627927. https://ssrn.com/abstract=3627927 (doi:10.1287/msom.2020.0894)
• S. Fay and J. Xie, Probabilistic Goods: A Creative Way of Selling Products and Services, Marketing Science 27(4), 674–690, 2008. https://doi.org/10.1287/mksc.1070.0318
• K. Jerath, S. Netessine and S. K. Veeraraghavan, Revenue Management with Strategic Customers: Last-Minute Selling and Opaque Selling, Management Science 56(3), 430–448, 2010. https://doi.org/10.1287/mnsc.1090.1125
• A. Tversky and D. Kahneman, Belief in the Law of Small Numbers, Psychological Bulletin 76(2), 105–110, 1971. https://doi.org/10.1037/h0031322