Probability

Motivation

A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.

This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.

Setting

A demand signal $\xi \ge 0$ with density $g$ and distribution function $G$ is observed once before the selling season. Given $\xi$, demand $D$ has distribution function $F(\cdot\,|\,\xi)$, continuous and strictly increasing on $[0,\infty)$. Demand is stochastically increasing in the signal: $F(x\,|\,\xi_h) < F(x\,|\,\xi_l)$ for $\xi_h > \xi_l$. Expected sales are $S(q\,|\,\xi) = E[\min(q,D)\,|\,\xi]$. Period 1 is before the signal and period 2 is after it. The retailer's total order is $q_1$ after period 1 and $q_2 \ge q_1$ after period 2. The supplier's unit production cost is $c_i$ in period $i$, with $c_1 < c_2 < p$, where $p$ is the retail price. Salvage values and goodwill costs are zero.

The supply chain's period-2 objective is

$$\Omega_2(q_2\,|\,q_1,\xi) = pS(q_2\,|\,\xi) - c_2 q_2 + c_2 q_1 ,$$

and $q_2(q_1,\xi)$ maximizes it over $q_2 \ge q_1$. The supply chain's expected profit is $\Omega_1(q_1) = -c_1 q_1 + E[\Omega_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$.

Under the buy back contract $\{w_1, w_2, b\}$ the retailer pays $w_i$ per unit ordered in period $i$, and the supplier refunds $b$ per unsold unit. The retailer's period-2 profit is $\pi_2(q_2\,|\,q_1,\xi) = (p-b)S(q_2\,|\,\xi) - (w_2-b)q_2 + w_2 q_1$, and his period-1 profit is $\pi_1(q_1) = -w_1 q_1 + E[\pi_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$. The supplier's period-2 profit $\Pi_2$ and her period-1 profit $\Pi_1(x\,|\,q_1)$, as functions of the stock $x$ she holds, are given in the mission's Profits definition.

Formalization targets

Goal: the buy back contract coordinates

For $\lambda \in [0,1]$ with

$$p - b = \lambda p,\qquad w_2 - b = \lambda c_2,\qquad w_1 - w_2 + \lambda c_2 = \lambda c_1,$$

the identities

$$\pi_2(q_2\,|\,q_1,\xi) = \lambda\big(\Omega_2(q_2\,|\,q_1,\xi) - c_2 q_1\big) + w_2 q_1,\qquad \pi_1(q_1) = \lambda\,\Omega_1(q_1)$$

hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for $\lambda > 0$). In addition,

$$w_2 - c_2 = w_1 - \big(\lambda c_1 + (1-\lambda)c_2\big) < w_1 - c_1 \quad (\lambda < 1).$$

Milestones

1. The structure of the period-2 problem, Eqs. (25)–(26): $q_2(\xi)$ solves $F(q_2(\xi)\,|\,\xi) = (p-c_2)/p$ and increases in $\xi$, and the threshold $\xi(q_1)$ splits the signals into those that trigger a period-2 order and those that do not.
2. The retailer's period-2 identity (p. 65).
3. The supplier fills any period-2 order up to $q_2(q_1,\xi)$, and for $\lambda < 1$ she does not fill a larger one (p. 65).
4. The retailer's period-1 identity (p. 66).
5. The first-order condition (27) for $q_1^o$.
6. The supplier's period-2 profit increases in her stock below $q_1$, so she produces at least the period-1 order (p. 66).
7. The supplier produces exactly the period-1 order (p. 67).
8. The margin comparison (p. 67).

Significance

The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through $\lambda$. Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.

These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold $\xi(x)$.

Difficulty

The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and $\partial \Pi_1(x\,|\,q_1)/\partial x = -c_1 + c_2(1 - G(\xi(x)))$. The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum $\max(q_1, q_2(\xi))$ has a kink at $\xi = \xi(q_1)$. The integrand switches between two regimes, and the switch point moves with $q_1$. The supplier's period-1 profit is not differentiable at $x = q_1$; only its right derivative is negative at $q_1^o$. Turning the page's derivative statements into the global claim that $x = q_1^o$ is her unique optimum needs a monotonicity argument on both sides of $q_1^o$.

Formalization scope

The conditional law is a measurable family $\xi \mapsto D_\xi$ of probability measures on $\mathbb R$ supported on $[0,\infty)$, each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on $[0,\infty)$. The signal has a measurable density $g \ge 0$ with $\int_0^\infty g = 1$, and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. $0 < c_2 < p$ makes the critical ratio lie in $(0,1)$. Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).

The optimum $q_2(q_1,\xi)$ is a hypothesis-carried selection maximizing $\Omega_2$ over $q_2 \ge q_1$. It is never an arbitrary function: a formalization that let $q_2(q_1,\xi)$ be unconstrained would make $\pi_1 = \lambda\Omega_1$ a statement about meaningless orders. The thresholds $\xi(q_1)$ enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over $q_1 \ge 0$ and $q_2 \ge q_1$. Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).

Three corrections of the print are disclosed in the item notes:

• the strict margin inequality fails at $\lambda = 1$;
• the p. 66 identity for $\Pi_2(x, q_1, q_2, \xi)$ is off by the constant $(1-\lambda)c_2q_1$;
• "retailer optimal equals chain optimal" needs $\lambda > 0$ in the converse direction.

Contributions are welcome on all milestones. A lemma that differentiates $q \mapsto E[\max_{q_2 \ge q} \Omega_2]$ with a density-driven threshold would be reusable beyond this mission.

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
• K. L. Donohue, Efficient Supply Contracts for Fashion Goods with Forecast Updating and Two Production Modes, Management Science 46(11), 1397–1411, 2000. https://doi.org/10.1287/mnsc.46.11.1397.12088
• M. Fisher and A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 87–99, 1996. https://doi.org/10.1287/opre.44.1.87

Motivation

A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.

The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).

Setting

Let $D_r$ denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean $\mu_r=\mathbb E[D_r]$, distribution function $F_r$, and density $f_r$. At inventory level $s\in\mathbb R$, expected inventory is $I_r(s)=\mathbb E[(s-D_r)^+]$ and expected backorders are $B_r(s)=\mathbb E[(D_r-s)^+]$, where $x^+=\max(x,0)$. The section assumes $F_r(0)=0$ and a strictly increasing differentiable $F_r$ on nonnegative levels. These assumptions place the optimum above zero.

The retailer pays holding cost $h_r I_r(s)$ and its own backorder cost $\beta_r B_r(s)$. The supplier pays a further backorder cost $\beta_s B_r(s)$. All three cost rates are positive. Thus $c_r(s)=h_r I_r(s)+\beta_r B_r(s)$ and $c_s(s)=\beta_s B_r(s)$ are the firms' costs, while $c(s)=c_r(s)+c_s(s)$ is the channel cost. Write $\beta=\beta_r+\beta_s$. Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.

The proposed contract pays the retailer $t_I I_r(s)+t_B B_r(s)$ from the supplier, where $t_I$ and $t_B$ are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter $\lambda\in(0,1]$, the contract sets $t_I=(1-\lambda)h_r$ and $t_B=\beta_r-\lambda\beta$. The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter $\lambda$ describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.

Formalization targets

The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum $s_r^\circ$ is unique and satisfies

$$F_r(s_r^\circ)=\frac{\beta}{h_r+\beta};$$

the uncontracted retailer has its own unique optimum $s_r^*$ with $s_r^*<s_r^\circ$. Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family ($t_I\ge0$, with $t_I>0$ exactly for $\lambda<1$, and $\{t_B:0<\lambda\le1\}=[-\beta_s,\beta_r)$); the decomposition

$$t_I I_r(y)+t_B B_r(y)=(t_I+t_B)I_r(y)+t_B(\mu_r-y);$$

and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price $p=h_r+\beta_r$ and wholesale price $w=h_r$, the newsvendor retailer's profit $pS(q)-wq$, with expected sales $S(q)=\mathbb E[\min(q,D_r)]$, equals $-c_r(q)+\beta_r\mu_r$. The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:

$$c_r^\lambda(s)=\lambda c(s),\qquad c_s^\lambda(s)=(1-\lambda)c(s) \quad\text{for all }s\in\mathbb R\text{ and }0<\lambda\le1.$$

Consequently, the retailer's contracted cost has the same unique minimizer $s_r^\circ$ as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in $\lambda$, which is the page's statement that the retailer's share of the cost increases with $\lambda$. The result does not prescribe one fixed allocation of cost: each $\lambda$ in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.

Significance

The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to $\beta_r$, while the channel's stock decision uses $\beta_r+\beta_s$. Under the contract, the retailer bears the fraction $\lambda$ of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.

The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).

Difficulty

The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as $\lambda c$ would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.

Formalization scope

Lean represents $D_r$ by a probability measure on $\mathbb R$ supported on $[0,\infty)$, with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on $[0,\infty)$, equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates $h_r,\beta_r,\beta_s$ are fields of one model, and $I_r,B_r$ are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.

Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that $t_I>0$ for all $\lambda\in(0,1]$ fails at $\lambda=1$, where $t_I=0$; the formal statement asserts $t_I\ge0$ with strict positivity exactly for $\lambda<1$. The contract range is exactly $0<\lambda\le1$; $\lambda=0$ would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.

Selected references

• Gérard P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; source used here: author's third draft, January 2003, §6.7. DOI.

Motivation

A retailer who controls both inventory and price can respond to a supply contract in two ways. A contract that induces the right order quantity at a fixed price may change the retailer's incentive to raise or lower that price. For a one-season supply chain, Cachon's chapter compares familiar contracts under price-dependent demand and identifies a price-contingent buy-back, also called a price-discount contract, that aligns both decisions. The mission concerns §6.3 of the author's January 2003 third draft, on printed pages 33–38. Those page and equation numbers belong to the draft and may differ from the typeset chapter.

Setting

One risk-neutral supplier and one risk-neutral retailer have full information before a single selling season. The retailer chooses a nonnegative stocking quantity $q$ and a retail price $p$ from an admissible price set $P$; the price stays fixed during the season. Demand has a probability law $D_p$ that depends on $p$. Write $F(y\mid p)$ for its distribution function, $S(q,p)=\mathbb E_p[\min(q,D)]$ for expected sales, and $\mu(p)=\mathbb E_p[D]$ for mean demand. Demand is nonnegative, has a finite mean and, in the chapter's regular setting, its distribution function increases with demand level and has a positive price derivative at positive demand levels. Higher prices thus lower demand in the stochastic order used by the chapter. The price set is nonempty and open so an admissible price optimum has an interior first-order condition.

The supplier's unit cost is $c_s$, the retailer's unit procurement cost is $c_r$, and $c=c_s+c_r$ is total unit cost. Their goodwill penalties for unmet demand are $g_s$ and $g_r$, with $g=g_s+g_r$. An unsold unit has salvage value $v$ at the retailer. The integrated channel's expected profit is

$$\Pi(q,p)=(p-v+g)S(q,p)-(c-v)q-g\mu(p).$$

A buy-back contract charges a wholesale price $w_b$ for each ordered unit and pays the retailer $b$ for each unsold unit. A revenue-sharing contract charges a wholesale price $w_r$ and gives the retailer a fraction $\phi$ of sales and salvage revenue. In this section the supplier offers the terms and the retailer chooses $(q,p)$. The profit formulas use the chapter's convention that a positive transfer goes from retailer to supplier.

Formalization targets

The goal is the price-contingent buy-back on p. 35, with $\lambda\in[0,1]$:

$$b(p)=(1-\lambda)(p-v+g)-g_s,\qquad w_b(p)=\lambda c_s+(1-\lambda)(p+g-c_r)-g_s.$$

In the chapter's zero-goodwill case, $g_r=g_s=0$, every feasible $(q,p)$ then gives the retailer $\lambda\Pi(q,p)$ and the supplier $(1-\lambda)\Pi(q,p)$. The same retailer profit is obtained from revenue sharing with $\phi=\lambda$ and $w_r=\lambda(c-v)-c_r+\lambda v$. Thus every existing maximizer $(q^\circ,p^\circ)$ of the integrated profit maximizes each firm's profit under the contingent buy-back. At $\lambda=0$ the retailer is indifferent; at $\lambda=1$ the supplier is indifferent.

The milestones follow the chapter's printed claims in attack order:

1. the integrated price condition (14), p. 34;
2. the quantity-flexibility condition (15), p. 34: price coordination forces $w_q=v-c_r$ or $\delta=0$;
3. the fixed buy-back condition (16), p. 35: price coordination forces $b=-g_s$ and then $w_b=c_s-g_s$;
4. the linear price-contingent terms derived from (5)–(6), p. 35;
5. the p. 36 profit split $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$, $\pi_s=(1-\lambda)\Pi-(\lambda g-g_r)\mu$, valid for all goodwill penalties as an identity;
6. the zero-goodwill revenue-sharing price claim following (17), p. 36 (the milestone quotes its restatement in §6.3.2, p. 38);
7. the price-contingent revenue-sharing parameters, p. 37;
8. the quantity discount $w_d(q)$, pp. 37–38: with $g_s=0$ it does not distort the price, and given $p^\circ$ it makes $q^\circ$ optimal for both firms.

Significance

The result identifies a contract schedule under which the same quantity-price pair is best for the integrated channel and for the two firms' reported profit functions. It also explains the relation between a buy-back whose terms vary with the chosen price and a revenue-sharing arrangement. In the zero-goodwill setting, both allocate every realized choice's expected channel profit in fixed shares. The general-goodwill identity shows the additional mean-demand terms that matter when the retailer controls price.

The source presents these results analytically; this mission asks for Lean proofs of the stated price and profit relationships. A published Prove2Me definition already supplies expected sales and mean demand for a single demand law, and the model here applies those functions to each price's law. The earlier open theorem RevShareCoord.Single.price_quantity_coordination (from Cachon and Lariviere's revenue-sharing paper) treats deterministic revenue and a simpler cost convention. It is an overlap in theme, but its statement does not include price-indexed demand, salvage value, retailer cost or the contingent buy-back terms, so it is not posed again here. The new model can support further price-dependent contract comparisons in the chapter.

Difficulty

The obstacle is that matching the retailer's quantity incentive at a fixed price can change the retailer's price incentive. The buy-back rate required by the fixed-price coordination equations depends on $p$; a fixed buy-back contract therefore does not generally align both choices. Revenue sharing with goodwill penalties has a similar price dependence. The integrated profit need not be concave or unimodal in $(q,p)$, so a price first-order condition by itself does not establish coordination. The chapter assumes a finite integrated optimum exists and treats the price condition as necessary, not sufficient.

Formalization scope

Lean represents price-dependent demand as a family of probability measures on $\mathbb R$, one for each price in $P$. Each admissible law is supported on nonnegative demand, has no atom at zero and has an integrable identity function, so $\mu(p)$ is a genuine finite expectation. Sales are defined by $\mathbb E_p[\min(q,D)]$, using the published SupplyChainTheory_contracts definition; they are not defined by the equivalent CDF integral. The admissible decisions are exactly $q\ge0$ and $p\in P$. Unit costs and goodwill penalties are nonnegative, each admissible price exceeds $c=c_s+c_r$, and $v<c$, as in the model of §6.2. The chapter's standing risk-neutrality and full-information conventions appear in the use of expected profit with the same demand laws available to both firms.

There is a material qualification. With price-dependent demand, $\mu(p)$ may change with $p$. The printed first-order condition (14) and the p. 36 inference from $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$ to a joint optimum omit that effect when goodwill penalties are positive. Price first-order and optimality statements here therefore use $g_r=g_s=0$, a case explicitly discussed in the chapter; general-goodwill claims are limited to algebraic identities. The printed p. 36 equality of price derivatives under revenue sharing also misses its factor $\phi$, which the formal statement restores. The contingent buy-back terms are defined by the chapter's linear formulas, not by a property that hard-codes coordination. The algebraic statement permits parameter values that may violate economic buy-back bounds such as $0\le b\le w_b$; those bounds need separate checks when selecting a contract.

Two first-order statements, (15) and (16), compare price derivatives; they take the derivative of expected sales in price as a hypothesis, and (15) also takes differentiation under the integral sign of $\int_{(1-\delta)q}^{q}F(y\mid p)\,dy$ as a disclosed regularity hypothesis. For the quantity discount, the statement claims what the page shows, undistorted prices for each $q$ and optimality of $q^\circ$ given $p^\circ$, not joint optimality of $(q^\circ,p^\circ)$ for the retailer. The page's claim that revenue sharing with goodwill coordinates only with $\phi=g_r/g$ is not stated, for the mean-demand reason above.

A trivializing formalization is ruled out: no contract term is defined by the profit identity it should satisfy, the demand family cannot be replaced by a single law, and the optimal pair is a hypothesis about the integrated profit, not a chosen witness.

Reusable contributions include the price-indexed demand family, the expected-profit model with five contract types, and the price-maximizer statements. Proofs of the first-order milestones need Fermat's interior-extremum theorem on the open price set and, for (15), positivity of an interval integral; the identities need the expectation algebra of $S$ and $\mu$, including $S(0,p)=0$.

Selected references

• Gérard P. Cachon, “Supply Chain Coordination with Contracts,” in Handbooks in Operations Research and Management Science, vol. 11, Supply Chain Management, North-Holland, 2003. DOI 10.1016/S0927-0507(03)11006-7. Formalization source: author's third draft, January 2003, §6.3, pp. 33–38.
• Fernando Bernstein and Awi Federgruen, “Decentralized supply chains with competing retailers under demand uncertainty,” Management Science 51(1), 2005 (the price-discount sharing contract; cited in the draft as a 2000 working paper). DOI 10.1287/mnsc.1040.0230
• Nicholas C. Petruzzi and Maqbool Dada, “Pricing and the newsvendor problem: a review with extensions,” Operations Research 47(2), 1999, 183–194. DOI 10.1287/opre.47.2.183

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$, already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$, and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$. Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$. When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$, $D$ and $n$, but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser adjacent to $\omega(t)$: the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

$$\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],$$

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$, $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$, with the uniform distribution and $n = 3$. The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},$$

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$,

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .$$

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

1. The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$.
2. Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$, even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ($1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$, $2$, $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$. A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$, not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations "$\simeq 3/e^3$, $9/(2e^3)$, $27/(6e^3)$" of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$, the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

• "no algorithm can achieve an expected approximation of $1 - o(1)$" becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$, with $n = 3k$ tied to $k$, and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
• The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$. A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$" would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$, are welcome.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$-concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$. At the start of period $t$, the firm has inventory $x$, which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$. If $y>x$, it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$. After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$. The corresponding price is $P_t(d)$, the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$.

Actual demand is $\alpha_t d+\beta_t$. The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$, with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$. No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$, incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$. For a post-order inventory $y$ and expected demand $d$, write

$$g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].$$

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$. This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$-convex real function $f$ satisfies

$$f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k$$

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$. A function is symmetrically $k$-concave when its negative is symmetrically $k$-convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$, then for every period

$$G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.$$

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$. An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$, and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$.

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$-convexity to symmetric $k$-convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$-convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$, that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$-concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$. The statement must assert Bellman optimality at every $x$, including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$, matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$, with $T>0$ and terminal value $v_{T+1}=0$. Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$. The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$.

The formal assumptions include $k\ge0$ and $c_t\ge0$, and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$.

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

• Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

Motivation

Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter $\delta$: a solution must satisfy $x\in\mathcal X_\delta$ for every $\delta$ in a possibly infinite set $\Delta$. Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws $N$ independent samples of $\delta$, solves the convex program with those $N$ constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.

Timeline.

• Calafiore and Campi (Math. Program. 2005; IEEE TAC 2006) introduced the method and bounded the probability that the violation exceeds $\varepsilon$ by a quantity of order $\binom Nd(1-\varepsilon)^{N-d}$. The bound is valid but loose.
• Campi and Garatti (SIAM J. Optim. 2008, this mission's source) proved the bound $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for every convex problem satisfying existence and uniqueness of solutions. They showed it is attained with equality by every fully-supported problem, so it cannot be improved without further assumptions.
• Later work extended the result to non-unique solutions, constraint removal, and non-convex decisions (Campi and Garatti, Introduction to the Scenario Approach, SIAM 2018).

Setting

Let $(\Delta,\mathcal D,\mathbb P)$ be a probability space, $c\in\mathbb R^d$ with $d\ge1$, and let $\mathcal X\subseteq\mathbb R^d$ and $\mathcal X_\delta\subseteq\mathbb R^d$ ($\delta\in\Delta$) be convex closed sets. The violation probability of a point $x$ is

$$V(x)=\mathbb P\{\delta\in\Delta:\ x\notin\mathcal X_\delta\}.$$

For a multi-extraction $(\delta^{(1)},\dots,\delta^{(m)})\in\Delta^m$, the program $P_m$ minimises $c^\top x$ over $x\in\mathcal X\cap\bigcap_{i=1}^m\mathcal X_{\delta^{(i)}}$. It is assumed that every $P_m$ has a unique solution $x^*_m$. A constraint $\delta^{(r)}$ is a support constraint of $P_m$ if its removal changes the solution. A convex $P_m$ has at most $d$ support constraints (Proposition 2.2). The problem is fully-supported if, for every $m\ge d$, the program $P_m$ built from $m$ independent samples has exactly $d$ support constraints with $\mathbb P^m$-probability one.

Two further objects carry the argument. For $\mathcal I\subseteq\{1,\dots,m\}$ of cardinality $d$, $S_{\mathcal I}$ is the set of multi-extractions whose support constraints have exactly the indexes in $\mathcal I$. The violation law is

$$F(\alpha)=\mathbb P^d\{V(x^*_d)\le\alpha\},$$

the distribution of the violation of the solution built from $d$ samples.

Formalization targets

Goal: Theorem 2.4, equation (2.3)

For a fully-supported problem, every $N\ge d$ and every $\varepsilon\in[0,1]$,

$$\mathbb P^N\{V(x^*_N)>\varepsilon\}=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

Milestones (PART 1 of §3)

• Proposition 2.2: at most $d$ support constraints.
• $S_{\bar{\mathcal I}}\subseteq\widetilde S_{\bar{\mathcal I}}$ for $\bar{\mathcal I}=\{1,\dots,d\}$, where $\widetilde S_{\bar{\mathcal I}}$ is the set where $\delta^{(d+1)},\dots,\delta^{(m)}$ are not violated by the solution generated by $\delta^{(1)},\dots,\delta^{(d)}$; and $\widetilde S_{\bar{\mathcal I}}\subseteq S_{\bar{\mathcal I}}$ up to a probability-zero set.
• (3.3): $\mathbb P^m\{S_{\mathcal I}\}=\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)$ for every $\mathcal I$ of cardinality $d$.
• (3.4): $\binom md\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)=1$ for all $m\ge d$.
• Moment uniqueness: $F(\alpha)=\alpha^d$ is the only distribution on $[0,1]$ satisfying (3.4).
• (3.2): $F(\alpha)=\alpha^d$.
• Partition chain: $\mathbb P^N\{V(x^*_N)>\varepsilon\}=\binom Nd\int_{(\varepsilon,1]}(1-\alpha)^{N-d}F(\mathrm d\alpha)$.
• Integration by parts: $\binom Nd\int_\varepsilon^1(1-\alpha)^{N-d}\,d\,\alpha^{d-1}\,\mathrm d\alpha=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$.

Significance

The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on $N$, $d$ and $\varepsilon$ can be smaller, because a fully-supported problem attains it. The distribution of $V(x^*_N)$ is then a Beta law, $\mathbb P^N\{V(x^*_N)\le\varepsilon\}$ being the probability that a $\mathrm{Binomial}(N,\varepsilon)$ variable is at least $d$, the same for every fully-supported problem. This is what fixes the sample sizes used in practice: $N$ is chosen so that the binomial tail is below a confidence level $\beta$. Fact (3.2), that $V(x^*_d)$ has distribution function $\alpha^d$ whatever the problem, is a distribution-free statement of independent interest.

Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on $[0,1]$ given the moments $\int(1-\alpha)^k\,\mathrm dF=1/\binom{d+k}d$, and the incomplete-beta identity for binomial tails.

Difficulty

The obvious route would compute the law of $V(x^*_N)$ directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of $V(x^*_d)$ only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than $d$ support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first $d$ constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by $d$.

Formalization scope

Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.

Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so $\bar{\mathcal I}$ is $\{i : i<d\}$ and "$\delta^{(d+1)},\dots,\delta^{(m)}$" are the indexes $j\ge d$. $\mathbb P^m$ is Measure.pi (fun _ : Fin m => P). $V$, the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.

Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve $P_k$ and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of $\{(x,\delta):x\in\mathcal X_\delta\}$ and measurability of the solution maps, the same two hypotheses as the goal. No set $S_{\mathcal I}$ is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.

Conventions. $F$ is the push-forward measure violationLaw on $\mathbb R$, with $F(\alpha)$ = violationLaw … (Set.Iic α). Integrals against $F$ are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over $[0,1]$ for $\int_0^1$, and over $(\varepsilon,1]$ for $\int_\varepsilon^1$ in the partition chain, since that integral comes from the event $V>\varepsilon$. The integration-by-parts identity is a real interval integral. Ranges are $1\le d$, $d\le m$, $d\le N$ and $0\le\varepsilon\le1$.

Ruled out. A pointwise "exactly $d$ support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event $\{V(x^*_N)>\varepsilon\}$ or of $S_{\mathcal I}$, or the identity $\mathbb P^m\{S_{\mathcal I}\}=\mathbb P^m\{\widetilde S_{\mathcal I}\}$, as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.

Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on $[0,1]$, and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.

Selected references

• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19(3) (2008) 1211–1230. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Math. Program. 102 (2005) 25–46. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Trans. Automat. Control 51(5) (2006) 742–753. https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, SIAM, 2018. https://doi.org/10.1137/1.9781611975444
• A. N. Shiryaev, Probability, 2nd ed., Springer, 1996, Chapter II, §12. https://doi.org/10.1007/978-1-4757-2539-1

Motivation

MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor $1/2$ was essentially the best known.

Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least $0.878$ times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant $2/\pi$.

This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.

Setting

Let $n\ge 0$ and let $A\in\mathbb R^{n\times n}$ be a symmetric matrix with non-negative entries; $A_{i,j}$ is the weight between points $i$ and $j$. The graph Laplacian is $L=D-A$, where $D$ is the diagonal matrix with entries $\sum_{j=1}^n A_{i,j}$. For $x\in\{-1,1\}^n$ the vector $x$ encodes a partition, and MAXCUT is (6.7)

$$\max_{x\in\{-1,1\}^n} x^\top L x .$$

Write $\langle M,X\rangle=\operatorname{Tr}(M^\top X)$ for the Frobenius inner product and $\mathbb S^n_+$ for the symmetric positive semidefinite matrices. Since $x^\top Lx=\langle L,xx^\top\rangle$ and $xx^\top\in\mathbb S^n_+$ has unit diagonal, MAXCUT is bounded above by the SDP relaxation

$$\max\bigl\{\langle L,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1,\ i\in[n]\bigr\}.$$

A solution $\Sigma$ of the relaxation is any feasible matrix attaining this maximum. The rounding draws $\xi\sim\mathcal N(0,\Sigma)$, a centered Gaussian vector with covariance $\Sigma$, and outputs $\zeta=\operatorname{sign}(\xi)\in\{-1,1\}^n$ coordinatewise.

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

For $A$ symmetric with non-negative entries, $L=D-A$, $\Sigma$ any solution of the relaxation, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$:

$$\mathbb E\,\zeta^\top L\zeta\ \ge\ 0.878\max_{x\in\{-1,1\}^n}x^\top Lx.$$

Milestones

1. Bounded entries. If $\Sigma\in\mathbb S^n_+$ and $\Sigma_{i,i}=1$, then $|\Sigma_{i,j}|\le 1$ (remark in the proof of Lemma 6.12).
2. Lemma 6.12 (Sheppard's formula). If $\xi\sim\mathcal N(0,\Sigma)$ with $\Sigma_{i,i}=1$ and $\zeta=\operatorname{sign}(\xi)$, then $\mathbb E\,\zeta_i\zeta_j=\frac{2}{\pi}\arcsin(\Sigma_{i,j})$.
3. Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$.
4. Relaxation inequality. $\max_{x}x^\top Lx=\max_x\langle L,xx^\top\rangle\le\langle L,\Sigma\rangle$ for every solution $\Sigma$.

The separately stated Laplacian identity on p. 346 is also included as a theorem item: if $X_{i,i}=1$ for all $i$, then $\langle L,X\rangle=\sum_{i,j}A_{i,j}(1-X_{i,j})$; for $x\in\{-1,1\}^n$, $x^\top Lx=\sum_{i,j}A_{i,j}(1-x_ix_j)$.

Companion: Theorem 6.13 (Nesterov)

For $B\in\mathbb S^n_+$, $\Sigma$ a solution of $\max\{\langle B,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1\}$, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$:

$$\mathbb E\,\zeta^\top B\zeta\ \ge\ \frac{2}{\pi}\max_{x\in\{-1,1\}^n}x^\top Bx.$$

Significance

The result. Theorem 6.11 is a polynomial-time randomized $0.878$-approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to $0.878$ times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.

Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of $\Sigma$. All three are reusable.

Difficulty

The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair $(\xi_i,\xi_j)$ has the law of $(\langle V_i,\varepsilon\rangle,\langle V_j,\varepsilon\rangle)$ for a standard Gaussian $\varepsilon$, and then computing an angular measure in the plane, including the degenerate cases $\Sigma_{i,j}=\pm1$, where the pair is supported on a line. A density-based argument fails there, because $\mathcal N(0,\Sigma)$ has no density when $\Sigma$ is singular, and singular solutions of the relaxation occur (for instance $\Sigma=xx^\top$). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ($0.878$ against the true minimum $\approx0.87856$), so crude estimates do not suffice near the minimizer $t\approx-0.689$.

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. $\mathbb S^n_+$ is Matrix.PosSemidef, which includes symmetry, and $\langle M,X\rangle$ is trace (Mᵀ * X).
• $\mathcal N(0,\Sigma)$ is Mathlib's ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite $\Sigma$, singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.
• The sign is $\{-1,1\}$-valued: $\operatorname{sign}(r)=1$ for $r\ge0$ and $-1$ for $r<0$. Mathlib's Real.sign would give $\operatorname{sign}(0)=0$, which takes $\zeta$ out of $\{-1,1\}^n$; the two agree almost surely because $\Sigma_{i,i}=1$.
• The maximum over the hypercube is a finite maximum (Finset.sup') over the $2^n$ Boolean vectors read as $\pm1$ vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.
• Standing hypotheses: in Theorem 6.11, $A$ symmetric with non-negative entries (the book's MAXCUT setting); in Lemma 6.12, $\Sigma$ positive semidefinite (implicit in "$\xi\sim\mathcal N(0,\Sigma)$"); in Theorem 6.13, $B$ positive semidefinite. The identities of milestones 4 and 5 hold for every real matrix $A$ and are stated without hypotheses on $A$.
• Ruled out: tying $\xi$'s law to anything other than $\Sigma$, or dropping optimality of $\Sigma$, would make the goal false or vacuous; here the law is exactly $\mathcal N(0,\Sigma)$ and $\Sigma$ is a maximizer.
• Welcome contributions: Sheppard's formula in Mathlib's multivariate Gaussian language, a proof of (6.8), and the Schur product theorem ($A,B\succeq0\Rightarrow A\circ B\succeq0$) used in Theorem 6.13.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6):1115–1145, 1995. doi:10.1145/227683.227684
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optim. Methods Softw. 9(1–3):141–160, 1998. doi:10.1080/10556789808805690
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37(1):319–357, 2007. doi:10.1137/S0097539705447372
• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192:101–167, 1899. doi:10.1098/rsta.1899.0003