Operations Research

Why effort breaks the standard coordinating contracts

A supplier selling through a retailer earns more when the retailer works harder at selling. Examples are a better shelf position, more knowledgeable sales staff, local advertising and keeping the display in order. These activities cost the retailer, raise demand, and usually cannot be observed or verified by the supplier, so no contract can be written on them directly. Chapter 6 of the Handbook of Operations Research and Management Science, Vol. 11: Supply Chain Management (G. P. Cachon, Supply Chain Coordination with Contracts, 2003) surveys contracts that align a retailer's decisions with the interest of the whole supply chain. Its §6.4 asks which of these contracts survive when the retailer also chooses such an unverifiable effort level.

The question goes back to the marketing literature on retail effort (Chu and Desai 1995, Desai and Srinivasan 1995, Desiraju and Moorthy 1997, Lal 1990, Lariviere and Padmanabhan 1997). It was taken up for newsvendor contracts by Taylor (2000), who showed that a sales rebate combined with a buy back restores coordination, and by Krishnan, Kapuscinski and Butz (2001), who let effort be chosen after demand is observed. This mission is the third in a series that formalizes the chapter's section capstones. It covers §6.4.1.

The newsvendor with effort-dependent demand

One supplier sells to one retailer for a single selling season. Before the season the retailer chooses an order quantity $q \ge 0$ and an effort level $e \ge 0$. Effort costs him $g(e)$, where $g(0) = 0$, $g' > 0$ and $g'' > 0$. Demand $D$ given effort $e$ has distribution function $F(\cdot \mid e)$ on $[0, \infty)$, with $F(0 \mid e) = 0$ and $F(\cdot \mid e)$ strictly increasing. Demand is stochastically increasing in effort: $\partial F(y \mid e)/\partial e < 0$ for $y > 0$. Units sell at the retail price $p$ and cost $c < p$ to produce. Goodwill costs, the salvage value and the retailer's own unit cost are zero. Expected sales and the integrated channel's profit are

$$S(q, e) = \mathbb E[\min(q, D)] = q - \int_0^q F(y \mid e)\,dy, \qquad \Pi(q, e) = pS(q, e) - cq - g(e).$$

Let $(q^o, e^o)$ maximize $\Pi$. A contract fixes the transfer the retailer pays the supplier, as a function of what the supplier can verify: the order and, for some contracts, sales or leftover units, but never effort. The contracts compared are the buy back $\{w_b, b\}$, quantity flexibility $\{w_q, \delta\}$, revenue sharing $\{w_r, \phi\}$, the sales rebate $\{w_s, r, t\}$ and the quantity discount $w_d(q)$. Under each, the retailer's profit $\pi_r(q, e)$ is his revenue $pS(q, e)$ less the transfer and $g(e)$.

Formalization targets

Goal

The goal combines the section's negative and positive results.

1. Buy backs distort effort (Eq. (19)). For every $b > 0$, $q > 0$ and $e > 0$,

$$\frac{\partial \pi_r(q, e, w_b, b)}{\partial e} < \frac{\partial \Pi(q, e)}{\partial e}.$$

2. The quantity discount aligns effort and splits profit. With

$$w_d(q) = (1 - \lambda)p\,\frac{S(q, e^o)}{q} + \lambda c - (1 - \lambda)\frac{g(e^o)}{q}, \qquad \lambda \in [0, 1],$$

the following hold for every $q > 0$. The retailer earns $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ and the supplier earns $(1 - \lambda)\Pi(q, e^o)$. The retailer's marginal profit of effort equals the channel's. His optimal efforts are the channel's. 3. The optimal order. If $(q^o, e^o)$ maximizes $\Pi$, both firms' profits at effort $e^o$ are maximized by $q^o$.

Milestones

The milestones follow the section's own claims: the integral form of $S$ (p. 41); the first-order condition (18) for the chain-optimal effort; (19); the analogous strict inequalities for quantity flexibility ($\delta > 0$) and revenue sharing ($\phi < 1$), and the reverse inequality for the sales rebate ($r > 0$, $q > t$); the two displays of $\pi_r$ under the quantity discount; and the fact that $S(q, e)/q$ decreases in $q$.

Significance

The result separates two jobs a contract does. To coordinate the order quantity, buy backs, quantity flexibility and revenue sharing all shield the retailer from part of the demand risk or take part of his revenue. The same shield dulls his incentive to raise demand, so each one leads him to under-invest in effort. The sales rebate pushes the other way, toward too much effort. The quantity discount works because the retailer keeps every unit of realized revenue and bears all of his own effort cost. The schedule then prices the order against expected revenue at the optimal effort, so the order is coordinated without touching the effort incentive. Because $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ with $\lambda$ free in $[0, 1]$, any split of the channel's optimal profit is attainable. The chapter extends this observation to retailers that also set price (p. 43).

The section's claims are proved on the page only in outline; several are introduced with "it can be shown". To our knowledge none has a machine-checked proof. Formalizing them requires differentiating expected sales in a parameter of the demand law. That step recurs throughout stochastic inventory and pricing models.

Difficulty

Most of the algebra is short. The substance is in the derivatives. $\partial S(q, e)/\partial e = -\int_0^q \partial F(y \mid e)/\partial e\,dy$ is a differentiation under the integral sign. The strict inequalities need this integral to be strictly negative. That in turn needs $\partial F/\partial e$ to be integrable and negative on a set of positive length, which is why $q > 0$ (and $q > t \ge 0$ for the sales rebate) matters.

The natural reading "the quantity discount makes $(q^o, e^o)$ the retailer's joint optimum" is not what the page shows, and it fails in general. The page gives two partial statements: for each fixed $q$ the retailer's effort incentive is the chain's, and at $e = e^o$ his best order is $q^o$. Since $\pi_r(q, e) = \Pi(q, e) - (1 - \lambda)\Pi(q, e^o)$, the retailer can gain by moving $q$ and $e$ together when $\lambda$ is small. The goal states exactly the two partial claims.

Formalization scope

The Lean namespace is CachonCoord.EffortNewsvendor. A structure Model collects the data: $p$ and $c$ with $0 \le c < p$; a family of demand laws indexed by effort (probability measures on $[0, \infty)$ with finite mean, no atom at $0$, strictly increasing distribution function); the effort derivative $\partial F(y \mid e)/\partial e$, negative for $y > 0$, $e > 0$; and $g$ with $g(0) = 0$ and positive first and second derivatives for $e > 0$. $S$ is defined as an expectation, and its integral form is a milestone. Derivative claims are HasDerivAt statements at interior efforts $e > 0$. The inequalities assert that both derivatives exist.

The following hypotheses are standing assumptions or disclosed additions:

• the chapter's model paragraph (p. 7) and the zeros $g_r = g_s = v = c_r = 0$ of p. 41;
• as regularity, differentiation of $e \mapsto \int_a^b F(y \mid e)\,dy$ under the integral sign, with interval-integrable $\partial F/\partial e$;
• $0 \le c$ (a production cost);
• $w_q > 0$ and $\delta \le 1$ for quantity flexibility (the contract's range, p. 24);
• $t \ge 0$ for the sales rebate threshold;
• $q > 0$ wherever $w_d$, which divides by $q$, is used.

Revenue sharing and the sales rebate use §6.2's profit functions (pp. 21, 27) with this section's zeros, less $g(e)$.

The page prints the last term of $w_d$ as $+(1 - \lambda)g(e^o)/q$. With that sign the page's own displays $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ and $\pi_r(q, e)$ fail by $2(1 - \lambda)g(e^o)$. The formalization uses $-(1 - \lambda)g(e^o)/q$, under which both hold. $w_d$ is the explicit printed schedule with this correction. It is not defined as "a schedule with $\pi_r = \lambda\Pi$", which would make the goal empty.

Not covered: the price-and-effort schedule at the bottom of p. 43, for which the page gives no argument. The cachon-2005 revenue-sharing effort results (RevShareCoord.Effort.*, deterministic revenue $R(q, e)$) are a different model and are not referenced. Proofs of any milestone, and a reusable library for differentiating newsvendor expectations in a parameter, are welcome.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. https://doi.org/10.1016/S0927-0507(03)11006-7 (read in the author's 3rd draft, January 2003).
• T. A. Taylor, Supply Chain Coordination under Channel Rebates with Sales Effort Effects, Management Science 48(8), 2002, 992–1007. https://doi.org/10.1287/mnsc.48.8.992.168
• H. Krishnan, R. Kapuscinski, D. A. Butz, Coordinating Contracts for Decentralized Supply Chains with Retailer Promotional Effort, Management Science 50(1), 2004, 48–63. https://doi.org/10.1287/mnsc.1030.0154
• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

Motivation

In airline and hotel revenue management a firm sells a fixed stock of a perishable resource (seats on a flight leg, rooms on a night) over a finite selling horizon, and in each period decides which fare classes to open. Customers do not buy a fixed fare: they choose among the fares on offer, or leave. Talluri and van Ryzin (Management Science, 2004) formulated this single-leg, choice-based problem as a dynamic program over the time remaining and the units remaining.

Practical revenue management systems rarely offer arbitrary sets of fares. They use nested controls: fares are opened from the most expensive downwards, so the open set is always "every fare above some threshold". Whether restricting to such revenue-ordered offer sets is natural depends on how the optimal threshold moves as the state changes. For mixtures of multinomial logit models, Rusmevichientong, Shmoys, Tong and Topaloglu (Production and Operations Management, 2014, Theorem 6) showed that the best revenue-ordered threshold moves monotonically in both the remaining capacity and the remaining time.

Berbeglia and Joret (arXiv:1606.01371v3, §5, Theorem 5.1) extend these two monotonicity properties to every regular discrete choice model, the class that contains essentially every model used in revenue management, including all random utility models. This mission formalizes that result.

Setting

A finite nonempty set $\mathcal C$ of products is sold. For a choice set $S\subseteq\mathcal C$ and a product $x$, $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys $x$; the no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The system $\mathcal P$ is regular when (i) all these probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$, (iii) $\sum_{x\in S}\mathcal P(x,S)\le 1$, and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$, for every $x\in S$ and for the no-purchase option $x=0$.

Each product $x$ has a revenue $r(x)>0$. Let $r_1<r_2<\cdots<r_k$ be the distinct revenues. For $\ell\in[k]=\{1,\dots,k\}$ the revenue-ordered assortment is $S_\ell=\{x\in\mathcal C:r(x)\ge r_\ell\}$; a larger index $\ell$ gives a smaller set, $S_1=\mathcal C$.

In the multi-period model one customer arrives per period. With $t$ periods remaining and $q$ units left, the firm offers some $S_\ell$. The values of the revenue-ordered dynamic program are

$$\mathcal J_t(q,\ell)=\sum_{x\in S_\ell}\mathcal P(x,S_\ell)\bigl(r(x)+\mathcal J_{t-1}(q-1)\bigr)+\mathcal P(0,S_\ell)\,\mathcal J_{t-1}(q)\qquad(t,q>0),$$

$\mathcal J_t(q,\ell)=0$ when $t=0$ or $q=0$, and $\mathcal J_t(q)=\max_{\ell\in[k]}\mathcal J_t(q,\ell)$. The optimal revenue-ordered index is the smallest maximiser,

$$\ell^*_t(q)=\min\{\ell\in[k]:\mathcal J_t(q,\ell)=\mathcal J_t(q)\},$$

and $\Delta\mathcal J_t(q)=\mathcal J_t(q)-\mathcal J_t(q-1)$ is the marginal value of capacity.

Formalization targets

Goal: Theorem 5.1

For every $t\ge 1$ and $q\ge 1$,

$$\ell^*_t(q)\le\ell^*_t(q-1)\ \text{ if } q\ge 2,\qquad \ell^*_t(q)\ge\ell^*_{t-1}(q)\ \text{ if } t\ge 2 .$$

More units left give a weakly larger optimal offer set; more periods left give a weakly smaller one. The paper states the theorem for $t\in[T]$, $q\in[Q]$; the horizon and the capacity only bound $t$ and $q$, so the goal is stated for all $t,q\ge 1$.

Milestones

1. Lemma 2.1 (p. 6): $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
2. Lemma .1 (p. 35): with $\mathcal L^*(\delta)$ the set of indices $\ell$ maximising $\sum_{x\in S_\ell}\mathcal P(x,S_\ell)(r(x)+\delta)$, if $\delta_1+r_k\ge 0$ and $\delta_1\le\delta_2$ then $\min\mathcal L^*(\delta_2)\le\min\mathcal L^*(\delta_1)$.
3. Equation (16) (p. 36): $\mathcal J_t(q)=\max_{\ell}\sum_{x\in S_\ell}\mathcal P(x,S_\ell)(r(x)-\Delta\mathcal J_{t-1}(q))+\mathcal J_{t-1}(q)$.
4. Equations (17)–(18) (p. 36): $\ell^*_t(q)=\min\mathcal L^*(-\Delta\mathcal J_{t-1}(q))$.
5. Marginal value at most $r_k$ (p. 36): $\Delta\mathcal J_t(q)\le r_k$.
6. Marginal value non-increasing in capacity (p. 36, citing Talluri–van Ryzin, Lemma 4): $\Delta\mathcal J_t(q+1)\le\Delta\mathcal J_t(q)$.
7. Marginal value non-decreasing in time (p. 37, citing Talluri–van Ryzin, Lemma 5): $\Delta\mathcal J_t(q)\le\Delta\mathcal J_{t+1}(q)$.

Milestones 5–7 are asserted or cited in the paper, not proved there; milestones 6–7 are stated for this restricted dynamic program, which is the one the paper applies them to.

Significance

The theorem says that a firm restricted to revenue-ordered offer sets can implement its policy as a nested booking control: as seats sell out, the threshold fare can only rise, and as departure approaches with seats in hand, it can only fall. This is the structure that standard revenue management systems already assume, and Rusmevichientong et al. point out that such monotonicity can be used to implement them. The paper's contribution is that the property depends only on regularity of the choice model, not on its multinomial-logit form.

Formalizing it adds a machine-checked statement of the single-leg choice-based dynamic program over a general choice model, a precise account of the tie-breaking rule (the smallest maximiser), and machine-checked versions of the two marginal-value monotonicity facts that the paper cites from Talluri and van Ryzin rather than proves. To our knowledge none of these statements has been formalized in any proof assistant; the paper's proofs are informal.

Difficulty

The paper's proof is short, but two of its steps are not proved there. The marginal-value inequalities are imported from Talluri and van Ryzin, whose dynamic program optimises over all offer sets; here only the $k$ revenue-ordered sets are available and the empty set is not, so those proofs have to be redone for this program, and the bound $\Delta\mathcal J\le r_k$ is needed to keep each stage's shifted problem well behaved. The claim $\Delta\mathcal J\le r_k$ itself is justified on the page only by an informal sentence.

The second subtlety is tie-breaking. The monotonicity is about the smallest optimal index. Several indices can be optimal at once, and the comparison of Lemma .1 transfers optimality of one index from one shift to another only through Lemma 2.1, that is, through the no-purchase case of the regularity axiom. Without that case the statement fails.

Formalization scope

• Products form a finite nonempty type C; choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: its probability is the derived quantity noPurchase P S = 1 − ∑_{x∈S} P x S.
• IsChoiceSystem P is axioms (i)–(iii); IsRegular P adds axiom (iv) for products and for the no-purchase option. Milestones 5–7 assume only axioms (i)–(iii), as the paper says suffices; Lemma .1, (16), (18) and the goal assume regularity and $r>0$.
• Revenue levels use the paper's 1-based index: level r ℓ is $r_\ell$ for $1\le\ell\le k$, topRevenue r is $r_k$, and roSet r ℓ is $S_\ell$ as a Finset. The paper's sorting of products ($S_\ell=\{1,\dots,j(\ell)\}$) is notation only and is not used.
• The dynamic program is defined by structural recursion on $t$; there is no stochastic process. Maxima over $[k]$ are Finset.sup', and the minima defining $\ell^*_t(q)$ and $\min\mathcal L^*(\delta)$ are Finset.min' over sets proved nonempty.
• $\Delta\mathcal J_t(q)$ is used only for $q\ge 1$; milestones are stated with $t+1$, $q+1$ in place of the paper's $t-1$, $q-1$ to avoid natural-number subtraction, which the goal keeps under its hypotheses $q\ge 2$, $t\ge 2$.

Formalizations that would trivialize the statement are ruled out: the dynamic program maximises over the $k$ revenue-ordered sets only, never over all subsets (that is Talluri and van Ryzin's program); $\ell^*$ is the smallest maximiser, never the largest; and $T$, $Q$, $k$ and the choice model are arbitrary, never fixed.

The definitions (regular choice model, revenue-ordered assortments, the restricted dynamic program) are reusable for other results on nested policies. Proofs of the cited Talluri–van Ryzin lemmas for this program are especially welcome, as they are the part the paper leaves to the literature.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$. Let $n=|V|$ and $m=|E|$, counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$, with $c(v,w)=-c(w,v)$. A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$. Its excess $e_f(v)$ is the sum of flow entering $v$. A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$. An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$-optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$-optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$-optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$. Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

$$R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).$$

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

$$K\leq 3n(n-1)+3nm+3n^2(m+n).$$

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$-optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$-optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$-optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$. Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$, and relabel raises $p(v)$. This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$, $3n(n-1)$, $3nm$, and $3n^2(m+n)$; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
• Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

Why contracts in a newsvendor supply chain

A supplier sells to a retailer who must order before a single selling season with random demand. Each firm maximizes its own expected profit, and with the simplest contract, a fixed wholesale price per unit, the retailer orders too little: he bears all the risk of unsold stock but earns only part of the margin on each sale. The supply chain as a whole then earns less than it could. A contract is said to coordinate the supply chain if the chain-optimal actions are an equilibrium of the two firms' game. Which contracts coordinate, and how they divide the chain's profit, is the subject of a large literature in operations management. G. P. Cachon's survey chapter in the Handbooks in Operations Research and Management Science (Cachon 2003) gives its standard account. This mission formalizes §6.2 of that chapter, Coordinating the newsvendor, read in the author's 3rd draft (January 2003).

Timeline of the contracts treated in §6.2:

• Pasternack (1985) shows that buy-back (returns) contracts coordinate the newsvendor.
• Tsay (1999) and Tsay and Lovejoy (1999) study quantity flexibility contracts, in which the supplier refunds unsold units up to a fraction δ of the order.
• Cachon and Lariviere (2005, working paper 2000) analyze revenue sharing and show it is equivalent to buy back in the newsvendor.
• Taylor (2002) studies sales rebates. Moorthy (1987) and Kolay and Shaffer (2002) treat quantity discounts.

Setting

Demand $D \ge 0$ has distribution function $F$, with $\bar F = 1 - F$ and mean $\mu = E[D]$. The retail price is $p$. The supplier's unit production cost is $c_s$ and the retailer's unit cost is $c_r$, with $c = c_s + c_r < p$. Unmet demand costs the retailer a goodwill penalty $g_r$ per unit and the supplier $g_s$, with $g = g_s + g_r$. Each unsold unit is worth $v < c$ to the retailer.

Expected sales are $S(q) = E[\min(q, D)]$, leftover inventory is $I(q) = E[(q - D)^+]$ and lost sales are $L(q) = E[(D - q)^+]$. If $T$ is the expected payment from the retailer to the supplier, the firms earn

$$\pi_r(q) = (p - v + g_r)S(q) - (c_r - v)q - g_r\mu - T, \qquad \pi_s(q) = g_sS(q) - c_sq - g_s\mu + T,$$

and the chain earns $\Pi(q) = (p - v + g)S(q) - (c - v)q - g\mu$. Let $q^o$ be a maximizer of $\Pi$, with $\Pi(q^o) > 0$.

Under the quantity flexibility contract $(w_q, \delta)$ the retailer pays $w_q$ per unit ordered and is refunded $w_q + c_r - v$ for each unsold unit, up to $\delta q$ units:

$$T_q(q, w_q, \delta) = w_qq - (w_q + c_r - v)\int_{(1-\delta)q}^q F(y)\,dy.$$

The wholesale price that makes $q^o$ satisfy the retailer's first-order condition is

$$w_q(\delta) = \frac{(p - v + g_r)\,\bar F(q^o)}{\bar F(q^o) + (1-\delta)F((1-\delta)q^o)} - c_r + v.$$

Formalization targets

Goal: the quantity flexibility contract can split the profit in any way

With $\pi_r(q, w_q(\delta), \delta)$ and $\pi_s(q, w_q(\delta), \delta)$ the firms' profits under $(w_q(\delta), \delta)$:

$$\pi_r(q^o, w_q(0), 0) = \Pi(q^o) + g_s\big(\mu - S(q^o) + \bar F(q^o)q^o\big) \ge \Pi(q^o),$$ $$\pi_s(q^o, w_q(1), 1) = \Pi(q^o) + \mu g_r \ge \Pi(q^o),$$

and for every $a \in [0, \Pi(q^o)]$ some $\delta \in [0,1]$ gives the retailer $a$ and the supplier $\Pi(q^o) - a$ (§6.2.5, p. 25).

Milestones, in attack order

1. $S(q) = q - \int_0^q F$, $I(q) = q - S(q)$, $L(q) = \mu - S(q)$ (p. 10).
2. The unique maximizer $q^o$ of $\Pi$ satisfies $\bar F(q^o) = (c - v)/(p - v + g)$ (Eq. (2), p. 11).
3. $w_q(0) = (p - v + g_r)\bar F(q^o) + v - c_r$ and $w_q(1) = p + g_r - c_r$. Also, $w_q$ is increasing on $[0,1]$, which gives $v - c_r \le w_q(\delta) \le p + g_r - c_r$ (p. 24).
4. $q^o$ maximizes the retailer's profit under $(w_q(\delta), \delta)$ (Eq. (11), p. 24).
5. The supplier's first-order condition holds at $q^o$ (p. 25).
6. The δ = 0 identity and the δ = 1 identity (p. 25).

Companion results of §6.2

• Revenue sharing $\{w_r,\phi\}$ equals the buy back $w_b = w_r + (1-\phi)p$, $b = (1-\phi)(p - v)$ for every demand realization (p. 22).
• The sales rebate contract: first-order condition (12), price (13), the retailer's profit and its monotonicity in the threshold (p. 27), and failure under voluntary compliance (p. 28).
• The quantity discount gives the retailer $\pi_r = \lambda(\Pi(q) + g\mu) - g_r\mu$, so $q^o$ is optimal for both firms (p. 29).
• Under the wholesale price contract, the retailer's profit increases in the induced quantity (p. 14).

Significance

The goal is what makes quantity flexibility a complete coordinating family. Retailer optimality (milestone 4) says $q^o$ can be implemented. The allocation statement says that bargaining power can then be expressed through the single parameter δ without losing efficiency. Together with the supplier's first-order condition, these are the facts that matter in practice: forced compliance suffices for coordination, and the choice of δ is purely distributional. The companions put §6.2's other contracts on the same footing. Revenue sharing and buy back are equivalent. Sales rebates coordinate only with forced compliance. Quantity discounts coordinate with a bounded retailer share.

All of these results are stated in the source. Related results are Proved on the platform in Snyder and Shen's chapter (SupplyChainTheory.*), including the chain-optimal fractile and retailer optimality under quantity flexibility. This mission states them locally because Snyder and Shen's contract data impose stronger restrictions on salvage value than Cachon's model. The efficiency formula $(k+1)^{-(1+1/k)}(k+2)$ for the power distribution on p. 14 is already posed as the Open item RevShareCoord.Wholesale.alpha_family_efficiency and is not posed again.

Difficulty

Each identity is elementary algebra once $S$, its derivative and the integrals of $F$ are under control. That is where the work lies. Expected sales are defined as an expectation, so $S(q) = q - \int_0^q F$ is a theorem to prove, not a definition to unfold.

Differentiating $\int_{(1-\delta)q}^q F$ needs continuity of $F$ at two points. The sales rebate transfer is piecewise and has a kink at the threshold, so derivatives must be taken on the right side of it.

The allocation clause rests on continuity of δ ↦ π_r(q^o, w_q(δ), δ). The obvious argument, "the profits are continuous in δ", hides two facts. First, the denominator of $w_q(\delta)$ stays positive on $[0,1]$. Second, $F((1-\delta)q^o)$ moves continuously, which fails for a demand law with atoms. Both must be derived from the model, not assumed.

Formalization scope

The local ContractData follows Cachon's $v<c_s+c_r$ and $c_s+c_r<p$. Its $r$ is Cachon's price $p$, and its $p_s,p_r$ are the goodwill penalties $g_s,g_r$. The penalties are nonnegative costs. Net salvage may be negative and may exceed $c_r$; both possibilities were excluded by the related published model.

A demand law is a probability measure on ℝ with no mass on $(-\infty, 0)$, finite mean and no atoms (so $F$ is continuous). $F$ is strictly increasing on $[0, \infty)$ as long as $F < 1$. Its derivative is specified on the positive interior of that active support. This reading admits the bounded-support power law the chapter itself uses on p. 14, whose cdf has a corner at the support endpoint. Derivative conclusions use HasDerivAt.

Optimality is IsMaxOn … Set.univ over real quantities; the optimum is positive under the model assumptions. $\Pi(q^o) > 0$ is a hypothesis wherever an optimum is named, following p. 11.

Cachon's sales rebate $r$ is rebate in Lean.

Three printed slips are corrected, and the milestone quotes keep the print:

• p. 24 writes $w$ for $w_q$ in $T_q$.
• p. 25 mixes $q$ and $q^o$ in the δ = 0 and δ = 1 displays.
• p. 28 has a spurious $-v$ in $w_s(r) - r$.

Two encodings are ruled out. $w_q(\delta)$ is the explicit formula, never "the solution of (11)". The supplier's profit is the model's own function, not $\Pi$ minus the retailer's profit, so no clause holds by definition.

The local definition file CachonCoord.Newsvendor.Contracts contains the model, its expected profits, the contract transfers, the sales rebate price $w_s(r)$, the quantity discount schedule, and realized profits and payments. Lemmas about $S$, $\int F$ and continuity of contract prices are reusable across the series. The sales rebate existence-of-threshold argument and the normal-distribution counterexample of p. 25 are outside this mission.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves, T. de Kok (eds.), Handbooks in OR & MS Vol. 11, North-Holland, 2003 (3rd draft, Jan. 2003). https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal pricing and return policies for perishable commodities, Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166
• A. A. Tsay, The quantity flexibility contract and supplier–customer incentives, Management Science 45(10), 1999. https://doi.org/10.1287/mnsc.45.10.1339
• G. P. Cachon, M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005. https://doi.org/10.1287/mnsc.1040.0215
• T. A. Taylor, Supply chain coordination under channel rebates with sales effort effects, Management Science 48(8), 2002. https://doi.org/10.1287/mnsc.48.8.992.168
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Ch. 14. https://doi.org/10.1002/9781119584445

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

• Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
• Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
• Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$.
• Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$, $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer buys $x$. The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if

1. $\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$.

Each product has a revenue $r(x)>0$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$.

Let $r_1<\dots<r_k$ be the distinct revenues, with $r_0:=0$, and $S_i=\{x: r(x)\ge r_i\}$. The heuristic earns

$$\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).$$

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$, $N_{k+1}=0$, and $\ell$ the largest index with $N_\ell>0$. Section 3 of the paper proves

• (A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
• (B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$, with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
• (C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$, with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$, revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$, such that

$$k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.$$

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$, for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$. Product $(i,j)$ has revenue $\varepsilon^{-j}$, and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$, and $0$ otherwise, for $0<\varepsilon\le\tfrac12$. The milestones follow the proof on pp. 10–11:

• the axiom (iii) bound;
• (7);
• (8);
• (9);
• regularity;
• the distinct revenues $r_i=\varepsilon^{-i}$;
• $\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$;
• $\mathrm{OPT}=k$, attained by $\{(i,i)\}$;
• the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$;
• $N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$.

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$, $D_r$ and $D_N$, revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

• the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
• the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
• the claim that the full set is the best threshold set;
• the evaluation of $D_N(S^*)$, which needs $\ell=k$.

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$.

Formalization scope

• Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
• IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
• $\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$. $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
• The distinct revenues are the sorted image of r, indexed by Fin k from $0$: the Lean index $i$ is the paper's $i+1$, and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
• Bounds are multiplicative ($\mathrm{OPT}\le D\cdot\mathrm{RO}$); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
• The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

• a fixed $k$, since "for every $k$" is the content;
• tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$, which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$), so only the sum forms are claimed tight;
• an instance whose regularity is assumed;
• a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$, and general lemmas on sorted distinct values of a finite function.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724

Motivation

A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).

The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).

Setting

Let $\mathcal C$ be a finite nonempty set of products. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer offered $S$ buys $x$. Buying nothing is the option $0$, with $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular when

1. $\mathcal P(x,S)\ge0$ for products and for $x=0$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4 at $x=0$ says that enlarging the offer set never makes buying nothing more likely.

Prices are a function $r:\mathcal C\to\mathbb R_{>0}$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$. Let $r_1<\dots<r_k$ be the distinct values of $r$, and let $S_i=\{x:r(x)\ge r_i\}$ for $i\in[k]$. The revenue-ordered strategy earns

$$\mathrm{RO}=\max_{1\le i\le k}\mathrm{rev}(S_i).$$

For an assortment $S^*$, the purchase profile is

$$N_i=\sum_{x\in S^*,\ r(x)\ge r_i}\mathcal P(x,S^*)\qquad(i\in[k]),\qquad N_{k+1}:=0,$$

the probability that a customer offered $S^*$ buys something priced at least $r_i$. It is non-increasing in $i$.

Formalization targets

Goal: Theorem 3.3 (p. 9)

Let $S^*$ be optimal, $\mathrm{rev}(S^*)=\mathrm{OPT}$, suppose $N_1>0$, and let $\ell\in[k]$ be maximum with $N_\ell>0$. Then

$$\mathrm{OPT}\le\Big(\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\Big)\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le1+\ln\nu,\quad\nu=\frac{N_1}{N_\ell}.$$

The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form $1/(1+\ln\nu)$.

Milestones (in proof order)

• Lemma 2.1 (p. 6): $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• First observation of the proof (p. 9): $N_i\le\sum_{x\in S_i}\mathcal P(x,S_i)$ and $N_ir_i\le\sum_{x\in S_i}\mathcal P(x,S_i)r_i$.
• Inequality (6) (p. 9): $N_ir_i\le\mathrm{RO}$ for every $i\in[k]$.
• Revenue identity (p. 9): $\mathrm{rev}(S^*)=\sum_{i=1}^{\ell}(N_i-N_{i+1})r_i=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}N_ir_i$.
• Logarithmic step (p. 9, the comparison $1/\sum\ge1/(1+\ln\nu)$ in Theorem 3.3, used in the last inequality of the proof): for $N_1\ge\dots\ge N_\ell>0$ and $N_{\ell+1}=0$, $\sum_{i=1}^{\ell}(N_i-N_{i+1})/N_i\le1+\ln(N_1/N_\ell)$. The paper states this step without proof.

Significance

Theorem 3.3 gives a guarantee that is independent of prices. The bound $1+\ln(r_k/r_1)$ of Theorem 3.2 grows when prices are spread out. The bound $1+\ln\nu$ is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the $1/(1+\ln m)$ guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.

The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.

Difficulty

Each step is elementary. The difficulty is bookkeeping. The revenue of $S^*$ has to be regrouped by distinct price levels rather than by products: several products may share a price, and $k$ counts values. The regrouping uses an Abel-type rearrangement with the boundary convention $N_{k+1}=0$. Comparing $N_i$ with the purchase probability of $S_i$ needs regularity twice. First, axiom 4 for products passes from $S^*$ to $S^*\cap S_i$. Then the no-purchase case passes from $S^*\cap S_i$ to $S_i$. A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.

Formalization scope

• Products form a finite type C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's $k\ge1$. Offer sets are Finset C, and $\mathcal P$ is P : C → Finset C → ℝ. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. $\mathrm{RO}$ is Finset.sup' over the indices $1,\dots,k$ of the threshold sets only.
• Indices are 1-based natural numbers. level r i is $r_i$ for $1\le i\le k$. purchaseProfile P r S i is $N_i$ for $1\le i\le k$ and $0$ otherwise, which builds in $N_{k+1}=0$.
• Optimality is the hypothesis $\mathrm{rev}(S^*)=\mathrm{OPT}$. The index $\ell$ is a variable with hypotheses $1\le\ell\le k$, $N_\ell>0$, and $N_i\not>0$ for $\ell<i\le k$. $N_1>0$ is kept as in the paper.
• The approximation factor is stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. Both the sum form and the logarithmic form are stated. $\ln$ is Real.log, applied to $\nu\ge1$.
• The milestones other than the goal are stated for an arbitrary $S^*$, because the proof does not use optimality there.

The following statements are trivial or false and are not this mission: a maximum over all subsets in place of $\mathrm{RO}$; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while $\mathrm{rev}(S^*)$ is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular $\mathcal P$.

A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that $N$ is non-increasing.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371v3
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Motivation

Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows which advertisers accept each kind of impression and has estimates of how frequently those kinds will arrive. The question is how much this advance distributional information helps when decisions still have to be immediate.

This mission studies the paper's first offline-guided algorithm. It computes a maximum matching for the expected traffic and follows that matching during the actual random run. The paper shows that this natural policy reaches the familiar $1-1/e$ performance level and that its own analysis cannot be improved for this policy, even if performance is averaged over runs. The result sets the baseline for the paper's later two-suggested-matchings algorithm, which improves on that level under its stated assumptions. Feldman et al., §§1 and 4.1

Setting

An instance consists of a finite advertiser set $A$, a finite impression-type set $I$, and allowed edges $E\subseteq A\times I$. For each type $i$, the nonnegative integer $e_i$ is its expected number of arrivals. There are $n=\sum_{i\in I}e_i>0$ arrivals. Each arrival independently has type $i$ with probability $e_i/n$. A type with $e_i=0$ remains in the graph but has zero arrival probability. On an arrival of type $i$, an online algorithm may assign it to an adjacent advertiser that has not been assigned before, or may leave it unassigned. The hindsight optimum, $\mathrm{OPT}(\omega)$, is the largest matching in the realization graph with one vertex for every arrival position, including separate vertices for repeated types. Feldman et al., §2, pp. 3–4

The suggested matching algorithm first selects any maximum integral flow in the expected-instance network. Each advertiser has capacity one, and each type $i$ has capacity $e_i$. Equivalently, the selected edges form a maximum degree-capped bipartite matching $M\subseteq E$. Let $A^*$ be the advertisers covered by $M$. When type $i$ arrives, the algorithm chooses each advertiser joined to $i$ by a selected edge with probability $1/e_i$; any remaining probability chooses no advertiser. It assigns the chosen advertiser if available and otherwise makes no assignment. Its number of assignments is $\mathrm{ALG}(\omega)$. This rule includes the algorithm's random choice in addition to the random arrival types. Feldman et al., §4.1, p. 5

The canonical residual cut of $M$ places each advertiser and impression type on the source side if it is reachable from the source by residual edges. Write $A_T$ for advertisers on the sink side and $I_S$ for types on the source side. These sets describe the comparison between the expected-instance matching and the optimum of a realized run. The mission also uses occupancy: after $n$ independent uniform throws into $n$ bins, count how many bins in a fixed subset receive at least one ball. Feldman et al., §§2.1 and 4.1

Formalization targets

Theorem 4's general-instance guarantee is expressed in the additive form established by its analysis. For every $\varepsilon>0$, there are $\delta>0$ and $N$, uniform across all finite instances, all maximum integral flows, and all valid ways of realizing the algorithm's random choice, such that $n\ge N$ implies

$$\Pr\!\left[\mathrm{ALG}(\omega)\ge(1-e^{-1})\mathrm{OPT}(\omega)-\varepsilon n\right] \ge 1-e^{-\delta n}.$$

The complete bipartite family gives the tightness target. When $A=I=\{0,\ldots,n-1\}$ and every $e_i=1$, every maximum expected-instance matching is perfect. For every run, $\mathrm{OPT}=n$, and

$$\mathbb E[\mathrm{ALG}] =n\left(1-\left(1-\frac1n\right)^n\right), \qquad \lim_{n\to\infty}\frac{\mathbb E[\mathrm{ALG}]}{n}=1-e^{-1}.$$

The milestone list follows the paper's Fact 1 and the named passages “Bounding ALG,” “Bounding OPT,” and “Tightness of the Analysis” in §4.1. The cut identity $|A^*|=|A_T|+\sum_{i\in I_S}e_i$ is a separate deterministic milestone. Feldman et al., Theorem 4 and §4.1, pp. 5–6

Significance

The result establishes exactly what this one-matching policy achieves under integer-frequency independent arrivals. It gives a guarantee for the actual number of assignments relative to the best assignment made with hindsight, and a family on which the limiting expected ratio equals the guarantee. That tight family explains why the paper introduces a second suggested matching rather than seeking a stronger bound for the same policy. Feldman et al., §4

The mathematical theorem is proved in the paper; the mission asks for its machine-checked formalization. The development would also provide reusable finite models of repeated-type realizations, integral degree-capped bipartite matchings, uniform occupancy, and residual reachability cuts. No machine-checked proof of these mission items is being claimed by this draft.

Difficulty

The expected-instance matching is selected before the arrivals, but the hindsight optimum can exploit the actual multiplicities of every type. Counting only the ads selected online does not compare the algorithm with that hindsight optimum. Also, a type may have several selected advertisers when $e_i>1$, so replacing the algorithm's random choice by a deterministic designated ad would change its law. The cut and concentration statements have to apply uniformly to every maximum integral flow, including flows chosen by different tie-breaking rules. Feldman et al., §4.1, pp. 5–6

Formalization scope

Advertisers and types are finite Lean types. The edge relation is a finite set, and $e_i$ and $n$ are natural numbers with $n=\sum_i e_i>0$. An integral maximum flow is represented by a maximum cardinality edge set with advertiser degree at most one and type-$i$ degree at most $e_i$. The theorem quantifies over every such set. This is the unit-advertiser, integer-type-capacity flow used in §4.1, without a separate real-valued flow object. The canonical cut is defined through residual reachability. The hindsight optimum maximizes over matchings of the realized graph, with each arrival position distinct.

The run uses $n$ independent uniform draws from $\sum_i\{0,\ldots,e_i-1\}$. A valid labelling assigns each selected advertiser at type $i$ to a distinct copy. The drawn copy determines the type and, if labelled, the ad selected by the algorithm. This gives type probability $e_i/n$, conditional ad probability $1/e_i$ on selected edges, and the remaining “no ad” probability. Counts, probabilities, and expectations use finite sums, so there is no integrability convention. Since $n>0$, the run sample space is nonempty; no value of $\mathrm{ALG}/\mathrm{OPT}$ at $\mathrm{OPT}=0$ is needed. The complete-graph family has $n\ge1$.

The paper writes $1-e^{-\Omega(n)}$ in both bounding passages. The Lean statements spell this out as $\forall\varepsilon>0,\ \exists\delta>0,\ \exists N,\ \forall$ instances with $n\ge N$, with $\delta,N$ preceding the instance. Theorem 4's ratio language is represented by the additive estimate its proof yields; a vanishing ratio error requires a separate lower bound on $\mathrm{OPT}/n$. The exact finite-$n$ expectation and its limit make “tight, even in expectation” precise. The printed Fact 1 exponent is $\varepsilon n/2$, while its Appendix A proof yields $\varepsilon^2n/2$; the formalized concentration statement uses the proved exponent and the milestone retains the printed wording. Neither a ratio with a zero denominator nor a labelling that changes the algorithm's choice law is accepted as a shortcut.

Contributions toward the occupancy bound, the residual cut identity, the realized matching bound, and the complete-graph expectation are welcome. The finite occupancy and matching interfaces are intended for reuse beyond this specific algorithm.

Selected references

• Jon Feldman, Aranyak Mehta, Vahab Mirrokni, and S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, arXiv:0905.4100v1, 2009; FOCS 2009. Preprint