Probability

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

Motivation

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of $1-1/e$ for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).

The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.

Setting

There are $n$ boys, represented by rows, and $n$ girls, represented by columns. A bipartite graph $G\subseteq[n]\times[n]$ records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of $G$ . This assumption supplies an offline benchmark of $n$ matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.

Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order $n,n-1,\ldots,1$ . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance $p(A)$ is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).

The paper's hard family begins with the complete upper-triangular graph $T_n$ , where row $i$ is adjacent to column $j$ exactly when $i\le j$ . Its columns arrive from largest to smallest. Relabeling the rows by a permutation $\pi$ gives an instance $T_\pi$ that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write $V_{T_n}(n,\varnothing)$ for RANDOM's expected number of matches on $T_n$ , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).

Formalization targets

Main theorem

For every $\varepsilon>0$ , there is one threshold $N$ such that, for every $n\ge N$ and every randomized online algorithm $A$ on $n$ rows and columns, a graph $G$ with a perfect matching satisfies

\mathbb E_A[|M(G)|]\le (1-e^{-1}+\varepsilon)n.

The threshold is uniform over algorithms. The graph may depend on $A$ . This is the quantified upper-bound reading of Theorem 2's $p(A)\le n(1-1/e)+o(n)$ (Karp, Vazirani, and Vazirani, 1990, Theorem 2).

Milestone statements

Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted $T_n$ with RANDOM's expected size on $T_n$ . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit

\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.

Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).

Significance

Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from $n$ is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.

Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.

Difficulty

For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the $o(n)$ claim in Lemma 16.

Formalization scope

Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order $n,\ldots,1$ is represented by zero-based order $n-1,\ldots,0$ ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.

RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For $n=0$ , the matching and RANDOM value are zero; the main theorem is eventual in $n$ and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's $o(n)$ in Theorem 2 is stated as $\forall\varepsilon>0,\exists N,\forall n\ge N$ with $N$ before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.

Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.

Selected references

Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, pp. 352–358, 1990. DOI: 10.1145/100216.100262.

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Supply Chain Coordination with Contracts X: Under Forced Compliance, Options Contracts with Shares λ_l and min{λ_h, λ̂_h} Separate the Two Demand Types and Coordinate CapacityTextbook

Motivation

A manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.

The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.

Setting

Demand $D_\theta$ has one of two types $\theta \in \{h, l\}$ with distribution function $F_\theta(x) = F(x\mid\theta)$ . The page assumes $F_\theta(x) = 0$ for $x < 0$ , $F_\theta(x) > 0$ for $x \ge 0$ (so demand has an atom at $0$ ), $F_\theta$ increasing and differentiable, and stochastic dominance $F_h(x) < F_l(x)$ for all $x \ge 0$ . The supplier $S$ builds capacity $k$ at cost $c_k > 0$ per unit; after demand is observed he produces $\min\{D_\theta, k\}$ at cost $c_p > 0$ per unit; the manufacturer $M$ earns $r > c_p + c_k$ per unit of demand satisfied; unused capacity is worth nothing.

Expected sales with $x$ units of capacity are $S_\theta(x) = x - E[(x - D_\theta)^+]$ , and the supply chain's expected profit is

\Omega_\theta(k) = (r - c_p)S_\theta(k) - c_k k .

An optimal capacity $k_\theta^o$ maximizes $\Omega_\theta$ over $k \ge 0$ , and $\Omega_\theta^o = \Omega_\theta(k_\theta^o)$ .

In an options contract $M$ buys $q_i$ options at $w_o$ each and pays $w_e$ for each option exercised. With $k = q_i$ her profit is $\Pi_\theta(q_i) = (r - w_e)S_\theta(q_i) - w_o q_i$ and the supplier's is $(w_e - c_p)S_\theta(q_i) + w_o q_i - c_k q_i$ . The contract with share $\lambda$ sets $r - w_e = \lambda(r - c_p)$ and $w_o = \lambda c_k$ . Under a wholesale price contract with price $w$ the supplier earns $\pi_\theta(k) = (w - c_p)S_\theta(k) - c_k k$ ; the price inducing capacity $k$ is $w_\theta(k) = c_k/\bar F_\theta(k) + c_p$ with $\bar F_\theta = 1 - F_\theta$ , and the manufacturer then earns $\Pi_\theta(k) = (r - w_\theta(k))S_\theta(k)$ .

With asymmetric information only $M$ observes $\theta$ . Let $\hat\pi$ be the supplier's minimum acceptable profit, and define the shares

\lambda_l = 1 - \frac{\hat\pi}{\Omega_l^o},\qquad \lambda_h = 1 - \frac{\hat\pi}{\Omega_h^o},\qquad \hat\lambda_h = \frac{\Omega_l^o - \hat\pi}{\Omega_l(k_h^o)},\qquad \lambda_H = \min\{\lambda_h, \hat\lambda_h\}.

Formalization targets

Goal: forced-compliance separating contracts (§6.10.3, pp. 103–104)

The low type offers the options contract with share $\lambda_l$ and initial order $k_l^o$ , the high type the one with share $\lambda_H$ and initial order $k_h^o$ . Assuming $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$ :

0 < \lambda_l < \lambda_H < 1,\qquad \lambda_l\,\Omega_h(k_l^o) < \lambda_H\,\Omega_h^o,\qquad \lambda_H\,\Omega_l(k_h^o) \le \Omega_l^o - \hat\pi,

the supplier earns $\hat\pi$ from the low type and at least $\hat\pi$ from the high type, and each initial order $k_\theta^o$ maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.

Milestones

$S_\theta(x) = x - \int_0^x F_\theta$ (p. 98).
$\Omega_\theta$ is concave, and $k > 0$ is optimal iff $\bar F_\theta(k) = c_k/(r - c_p)$ (p. 99).
$\Omega_l(k) < \Omega_h(k)$ for $k > 0$ , hence $\Omega_l^o < \Omega_h^o$ (implicit on p. 104).
The options contract with share $\lambda \in [0,1]$ gives $\Pi_\theta = \lambda\Omega_\theta$ and the supplier $(1-\lambda)\Omega_\theta$ , so it coordinates (pp. 99–100).
Under voluntary compliance, $\partial\pi(k_\theta^o, k_\theta^o, \theta)/\partial k < 0$ (p. 100).
A capacity $k > 0$ is optimal for the supplier under a wholesale price $w$ iff $w = w_\theta(k)$ (p. 101).
A stationary point $k^*$ of $\Pi_\theta$ satisfies $\bar F_\theta(k^*) = \bar F_\theta(k_\theta^o)\bigl(1 + f_\theta(k^*)S_\theta(k^*)/\bar F_\theta(k^*)^2\bigr)$ , so $k^* < k_\theta^o$ (p. 102).

Significance

The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.

The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.

Difficulty

The incentive constraints look like arithmetic on shares, but the strict inequality $\lambda_l < \hat\lambda_h$ needs $\Omega_l(k_h^o) < \Omega_l^o$ : the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume $F_\theta$ strictly increasing, so $\Omega_l$ need not be strictly concave and may have a whole interval of maximizers. Likewise $\Omega_l^o < \Omega_h^o$ needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of $w_\theta(k)$ needs the density at $k^*$ , and $k^* < k_\theta^o$ fails when that density is $0$ .

Formalization scope

Each demand law is a probability measure on $\mathbb R$ and $F_\theta$ is Mathlib's cdf. $F_\theta$ is required to be differentiable only on $(0,\infty)$ , because the page's $F_\theta(0) > 0$ makes it jump at $0$ . $S_\theta$ is defined by the expectation $x - E[(x - D_\theta)^+]$ , whose integrand is integrable because $D_\theta \ge 0$ almost surely. Optimal capacities are passed as arguments characterized as maximizers over $[0,\infty)$ , never chosen; $k_\theta^o > 0$ is footnote 46's assumption. Derivatives are HasDerivAt statements.

Hypotheses added relative to the page, all disclosed in the items: $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$ in the goal (the page divides by $\Omega_l(k_h^o)$ and needs $\lambda_l \in (0,1)$ ); $\lambda > 0$ for the voluntary-compliance derivative (at $\lambda = 0$ it vanishes); $\bar F_\theta(k^*) > 0$ and $f_\theta(k^*) > 0$ for the non-coordination result. The page's assumption $w''_\theta > 0$ is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need $F_\theta$ strictly increasing. The prior $\Pr(\theta = h) = \rho$ does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of $\hat\lambda_h$ (for example $\lambda_H \le \hat\lambda_h$ ) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.

All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom $p_\theta$ at $0$ and an exponential tail, $p_h < p_l$ ), 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. doi:10.1016/S0927-0507(03)11006-7 (formalized from the author's 3rd draft, January 2003).
G. P. Cachon and M. A. Lariviere, Contracting to assure supply: how to share demand forecasts in a supply chain, Management Science 47(5), 629–646, 2001. doi:10.1287/mnsc.47.5.629.10486
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (increasing failure rate distributions, cited on p. 102).

10 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Wait-and-Judge Scenario Optimization 1: For Convex Programs, Seeing s_N Support Constraints Gives P^N{V(x_N) > ε(s_N)} ≤ γ, the Value of the Variational Problem (10)Research Paper

Motivation

Many decision problems in control, finance and engineering must hold against an uncertain parameter $\delta$ whose distribution is unknown, while samples of $\delta$ (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the $N$ observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen $\delta$ violate it?

The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on $N$ and the dimension $d$ , and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than $d$ samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.

Timeline:

2005–2006, Calafiore and Campi: a convex scenario program in $\mathbb R^d$ has at most $d$ support constraints; first sample-size bounds.
2008, Campi and Garatti: the exact bound $\mathbb P^N\{V(x^*_N)>\epsilon\}\le\sum_{i=0}^{d-1}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ , with equality for fully-supported problems.
2018, Campi and Garatti: the wait-and-judge bound, Theorem 1 below, with the 2008 bound as a corollary.

Setting

The decision variable is $x\in\mathbb R^d$ . A problem consists of a cost vector $c\in\mathbb R^d$ , a convex domain $\mathcal X\subseteq\mathbb R^d$ , convex constraint sets $\mathcal X_\delta\subseteq\mathbb R^d$ indexed by $\delta$ in a probability space $(\Delta,\mathcal F,\mathbb P)$ , and convex tie-break functions $t_1,\dots,t_p$ . Given an i.i.d. sample $\delta^{(1)},\dots,\delta^{(N)}$ with $N>d$ , the scenario program is

\min_{x\in\mathcal X}\ c^{\mathsf T}x\quad\text{subject to}\quad x\in\bigcap_{i=1}^N\mathcal X_{\delta^{(i)}}.

Ties are broken by minimising $t_1$ among the minimisers, then $t_2$ , and so on; the resulting solution is $x^*_N$ .

The violation of a point is $V(x)=\mathbb P\{\delta\in\Delta: x\notin\mathcal X_\delta\}$ .
A constraint is a support constraint if removing it changes the solution; $s^*_N$ is their number.
Assumption 1: for every $m$ and every sample of size $m$ , the program with those $m$ constraints has a unique tie-broken solution.
Assumption 2 (non-degeneracy): for every $m$ , with probability one, keeping only the support constraints does not change the solution.

The variational problem (10) is: for a function $\epsilon:\{0,\dots,d\}\to[0,1]$ ,

\gamma^*=\inf_{\xi\in C^d[0,1]}\xi(1)\quad\text{s.t.}\quad\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}\xi(t)\ge\binom Nk t^{N-k}\,\mathbf 1_{[0,1-\epsilon(k))}(t),\ \ t\in[0,1],\ k=0,\dots,d.

Formalization targets

Goal: Theorem 1 (p. 10)

For every $[0,1]$ -valued $\epsilon(k)$ , under Assumptions 1 and 2,

\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}\ \le\ \gamma^*.

The level $\epsilon$ is evaluated at the observed number of support constraints. The goal fixes no particular $\epsilon$ , which keeps it stable under any later choice of levels.

Milestones (the proof of Theorem 1, Sect. 5.1)

$s^*_m\le d$ for every sample (quoted from [7]).
(14): $\mathbb P^N\{V(x^*_N)>\epsilon(k)\wedge s^*_N=k\}=\binom Nk\,\mathbb P^N\{A\}$ , where $A$ adds "the first $k$ constraints are of support".
$A=B$ up to a null set, where $B$ concerns the program on the first $k$ samples.
(16): $\mathbb P^N\{A\}=\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$ , with $F_k(v)=\mathbb P^k\{V(x^*_k)\le v\wedge s^*_k=k\}$ .
(17): $\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}=\sum_{k=0}^d\binom Nk\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$ .
(18): $\sum_{k=0}^{\min\{m,d\}}\binom mk\int_{[0,1]}(1-v)^{m-k}\,\mathrm dF_k(v)=1$ for every $m$ .
Weak duality between the truncated moment problem (20) and its dual (21), giving (22).
(23): $\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}t^m=\binom mk t^{m-k}$ for $m\ge k$ , and $0$ otherwise.
(24): the infimum of $p(1)$ over polynomials feasible for (10) equals $\gamma^*$ .

Companions

Theorem 2 (p. 11): for $\beta\in(0,1)$ and $\epsilon(k)=1-t(k)$ , with $t(k)$ the unique root in $(0,1)$ of $\frac{\beta}{N+1}\sum_{m=k}^N\binom mk t^{m-k}-\binom Nk t^{N-k}=0$ , the probability is at most $\beta$ .
The root lemma of Sect. 5.3, including its sign and divergence claims.
$\gamma^*\le\sum_{i<d}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ for constant $\epsilon$ (Sect. 5.2).
Corollary 1, the 2008 bound.

Significance

Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of $\epsilon(k)$ , a user who finds $k\ll d$ support constraints obtains a level $\epsilon(k)$ comparable to that of a $k$ -dimensional problem, which is far below the a-priori level for dimension $d$ . The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.

The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:

a formal account of scenario programs with lexicographic tie-break and of support constraints in the "changes the solution" sense;
the exchangeability argument (14) on product measures;
the representation (17) of a tail probability through generalized distribution functions;
a weak-duality argument for a generalized moment problem. The 2008 bound itself is posed on the platform as an open problem under other hypotheses; Corollary 1 states it under this paper's assumptions.

Difficulty

The obvious approach bounds the probability for each value of $s^*_N$ separately by a binomial tail, then sums. This fails: the event $s^*_N=k$ is not known in advance, and summing the individual bounds over $k$ loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the $(d+1)$ -tuple $(F_0,\dots,F_d)$ . It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in $d+1$ measures, and solves it by duality.

Two steps carry most of the work. One is the almost-sure identity $A=B$ , which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in $C^d[0,1]$ . The bound $s^*_N\le d$ itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.

Formalization scope

Spaces. The decision space is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from $0$ . $\mathbb P$ is a probability measure and $\mathbb P^N$ is the product measure.
Tie-break. The tie-broken solution is the lexicographic minimiser of $(c^{\mathsf T}x,t_1(x),\dots,t_p(x))$ and depends only on the feasible set, which is what makes the exchangeability step valid. A support constraint is one whose removal changes this solution; this is not the platform's earlier "removal lowers the cost" notion.
Assumptions. Assumption 1 is required for every sample, Assumption 2 almost surely.
Measurability. The paper takes measurability for granted (footnote 1). Here it is two explicit hypotheses: the relation $\{(x,\delta):x\in\mathcal X_\delta\}$ is measurable, and every solution map $\omega\mapsto x^*_m(\omega)$ is measurable. No event is assumed measurable directly.
$F_k$ . $F_k$ is the finite measure on $\mathbb R$ given by the law of $V(x^*_k)$ on the event $\{s^*_k=k\}$ ; it is not normalised.
Problem (10). $C^d[0,1]$ is ContDiffOn ℝ d on $[0,1]$ , with derivatives taken within $[0,1]$ . $\gamma^*$ is a real infimum over a set that is nonempty ( $\xi(t)=t^N$ ) and bounded below by $0$ .
Probabilities are compared with real quantities through ENNReal.ofReal.
Theorem 2 is stated for every $\epsilon$ whose values $1-\epsilon(k)$ are roots of (11) in $(0,1)$ , which by its first part is the paper's $\epsilon$ .
Added hypothesis. The constant- $\epsilon$ companion assumes $d\ge1$ : at $d=0$ , $\epsilon=0$ its inequality is false.

Ruled-out trivializations:

The solution is never a free function of the sample.
The goal does not mention $F_k$ , moments or polynomials.
Assumption 1 is not weakened to almost surely.
$N>d$ is kept on Theorems 1, 2 and Corollary 1.
The indicators keep the paper's open and closed ends: $[0,1-\epsilon(k))$ in (10), $(\epsilon(k),1]$ in (16)–(21).

Contributions welcome:

the support-constraint bound under lexicographic tie-break, which is reusable for any convex scenario result;
the exchangeability lemma on Measure.pi;
the duality and density lemmas, which are pure analysis.

Selected references

M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming 167 (2018). https://doi.org/10.1007/s10107-016-1056-9
G. C. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102 (2005). https://doi.org/10.1007/s10107-003-0499-y
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51 (2006). https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19 (2008). https://doi.org/10.1137/07069821X

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Supply Chain Coordination with Contracts VIII: In the Two-Location Base-Stock Model the Linear Transfers (39)–(41) Make the Optimal Base Stocks the Unique Nash EquilibriumTextbook

Motivation

In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter $\lambda$ that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).

Setting

Two firms, a retailer $r$ and a supplier $s$ , each use a base stock policy: firm $i$ keeps its inventory position equal to its base stock level $s_i \in \mathbb R$ . A negative supplier base stock means planned backorders. Let $D_r$ and $D_s$ be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means $\mu_r$ , $\mu_s$ , and their distribution functions $F_r$ , $F_s$ are continuous, zero at $0$ , strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$ . Holding costs are $h_r$ and $h_s$ , with $0 < h_s < h_r$ . Each backorder at the retailer costs the retailer $\beta_r > 0$ and the supplier $\beta_s > 0$ per unit time. Write $\beta = \beta_r + \beta_s$ .

At retailer inventory level $y$ the expected on-hand stock is $I_r(y) = E[(y-D_r)^+]$ and the expected backorders are $B_r(y) = E[(D_r-y)^+]$ . The retail-level cost rates are $c_r(y) = h_rI_r(y) + \beta_rB_r(y)$ , $c_s(y) = \beta_sB_r(y)$ and $c(y) = c_r(y) + c_s(y)$ . Because the supplier may stock out, the retailer's actual inventory level is $s_r - (D_s - s_s)^+$ , and every retail-level quantity is averaged accordingly:

g(s_r,s_s) = E\big[g(s_r - (D_s-s_s)^+)\big] = F_s(s_s)g(s_r) + \int_{s_s}^\infty g(s_r+s_s-x)f_s(x)\,dx .

With the supplier's inventory $I_s(y) = E[(y-D_s)^+]$ and backorders $B_s(y) = \mu_s - y + I_s(y)$ , the firms' costs and the chain's cost are

\pi_r(s_r,s_s) = c_r(s_r,s_s), \qquad \pi_s(s_r,s_s) = h_sI_s(s_s) + c_s(s_r,s_s), \qquad \Pi = \pi_r + \pi_s .

A pair $\{s_r^o, s_s^o\}$ minimizing $\Pi$ is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.

Under a linear transfer the supplier pays the retailer $t_II_r(s_r,s_s) + t_B^rB_r(s_r,s_s) + t_B^sB_s(s_s)$ (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter $\lambda \in (0,1]$ are

t_I = (1-\lambda)h_r, \qquad t_B^r = \beta_r - \lambda\beta, \qquad t_B^s = \lambda h_s\frac{F_s(s_s^o)}{1-F_s(s_s^o)} .

Formalization targets

Goal: the contracts coordinate, uniquely

If $\{s_r^o, s_s^o\}$ is optimal with $s_s^o > 0$ and $\lambda \in (0,1]$ , then under the contracts

\pi_r = \lambda c(s_r,s_s) - t_B^sB_s(s_s), \qquad \pi_s = (h_s+t_B^s)I_s(s_s) + (1-\lambda)c(s_r,s_s) + t_B^s(\mu_s - s_s),

$\{s_r^o, s_s^o\}$ is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every $\lambda$ in the range.

Milestones

In the uncontracted game, every retailer best response exceeds $\hat s_r > 0$ , where $F_r(\hat s_r) = \beta_r/(h_r+\beta_r)$ , and every supplier best response is positive (pp. 79–80).
In the uncontracted game, for every $s_s$ the retailer's optimal base stock is below the chain's; consequently the competition penalty $(\Pi(s^*) - \Pi(s^o))/\Pi(s^o)$ is positive at every equilibrium $s^*$ (pp. 80–81).
The partial derivatives (35)–(36) of $\Pi$ , and every optimum with $s_s > 0$ satisfies $c'(s_r) = h_s$ , i.e. $F_r(s_r) = (h_s+\beta)/(h_r+\beta)$ (37) (p. 83).
Optima with $s_s \le 0$ have $s_r + s_s = \bar s$ , where $\Pr(D_r + D_s \le \bar s) = \beta/(h_r+\beta)$ (38) (p. 83).
The cost identities (42)–(43) under the contracts (p. 84).
Under the contracts the retailer's best response decreases in $s_s$ , and the supplier's marginal cost along it has the closed form printed on p. 84.

Significance

The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter $\lambda$ splits the retail-level costs between the firms in any proportion up to $\lambda = 1$ . Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers $t_I$ and $t_B^r$ are those of the single-location model (§6.7), even though the retailer's target fractile changes from $\beta/(\beta+h_r)$ to $(\beta+h_s)/(\beta+h_r)$ .

The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.

Difficulty

The firms' costs are compositions: a convex single-location cost evaluated at the random level $s_r - (D_s - s_s)^+$ , which is concave in $s_s$ . The supplier's cost is therefore not obviously convex in $s_s$ ; its convexity at $s_r = s_r^o$ depends on the value of $t_B^s$ and on $c'(s_r^o) = h_s$ . Uniqueness is the hard part. Under the contracts the retailer's best response $s_r(s_s)$ decreases, but the supplier's marginal cost along that best response, $F_s(s_s)(h_s - (1-\lambda)c'(s_r(s_s)) + t_B^s) - t_B^s$ , is not monotone in general when $\lambda$ is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.

Formalization scope

Demand laws are probability measures on $\mathbb R$ with no mass below $0$ , finite means, and continuous distribution functions, zero at $0$ , strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$ . These are the section's standing assumptions, together with $0 < h_s < h_r$ and $\beta_r, \beta_s > 0$ (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: $I_r$ , $B_r$ , $I_s$ and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against $f_s(x)\,dx$ are written against the law of $D_s$ , so no density hypothesis is made. Base stocks range over all of $\mathbb R$ , and "optimal" means minimizing $\Pi$ over $\mathbb R^2$ ; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of $D_r$ and $D_s$ , implicit on the page, enters only through the convolution of their laws in (38).

The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.

Corrected slips: (42) is stated with $\lambda c(s_r,s_s)$ where the page prints $\lambda\Pi(s_r,s_s)$ (the difference $\lambda h_sI_s(s_s)$ does not depend on $s_r$ ). The retailer's single-location fractile on p. 79 is stated as $\beta_r/(h_r+\beta_r)$ , not the printed $\beta/(h_r+\beta)$ . The garbled display after (43) and the $f_s$ / $F_s$ slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case $s_s^o \le 0$ , and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of $E[g(s - (D-t)^+)]$ , are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.

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, North-Holland, 2003, §6.8. https://doi.org/10.1016/S0927-0507(03)11006-7
G. P. Cachon and P. H. Zipkin, Competitive and cooperative inventory policies in a two-stage supply chain, Management Science 45(7), 936–953, 1999. https://doi.org/10.1287/mnsc.45.7.936
F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426
A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 818–836, 1984. https://doi.org/10.1287/opre.32.4.818

10 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts III: With Effort-Dependent Demand, Buy-Backs, Quantity Flexibility and Revenue Sharing Under-Reward Effort, While a Quantity Discount Gives λΠ(q, e°)Textbook

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.

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}.

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

11 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts I: The Newsvendor Quantity-Flexibility Contract (w_q(δ), δ) Gives the Retailer at Least Π(q°) at δ = 0, the Supplier at Least Π(q°) at δ = 1Textbook

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

$S(q) = q - \int_0^q F$ , $I(q) = q - S(q)$ , $L(q) = \mu - S(q)$ (p. 10).
The unique maximizer $q^o$ of $\Pi$ satisfies $\bar F(q^o) = (c - v)/(p - v + g)$ (Eq. (2), p. 11).
$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).
$q^o$ maximizes the retailer's profit under $(w_q(\delta), \delta)$ (Eq. (11), p. 24).
The supplier's first-order condition holds at $q^o$ (p. 25).
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

9 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

The Chromatic Number of Random Graphs: For Fixed 0 < p < 1, Almost Every G(n,p) Has n/s₀ ≤ χ(G) ≤ (n/s₀)(1 + 3 log log n / log n), where s₀ ≈ 2 log_d n and d = 1/(1−p)Research Paper

Motivation

The chromatic number $\chi(G)$ of a graph is the least number of colours in a proper vertex colouring. Determining it for a typical graph was, in the words of the paper, "one of the best known and most studied unsolved problems in the theory of random graphs". For the dense random graph $G_{n,p}$ with fixed edge probability $p$ , the clique number had been known precisely since the 1970s, but the chromatic number was known only up to a factor of $2$ .

Timeline:

1975. Grimmett and McDiarmid (doi:10.1017/S0305004100051124) proved that almost every $G_{n,p}$ satisfies $\frac{n}{2\log_d n}(1+o(1))\le\chi(G_{n,p})\le\frac{n}{\log_d n}(1+o(1))$ , with $d=1/(1-p)$ . The lower bound comes from the independence number; the upper bound from the greedy algorithm.
1976. Bollobás and Erdős (doi:10.1017/S0305004100053056) determined the clique number of $G_{n,p}$ up to two consecutive values, and slightly sharpened the bounds above.
1987. Matula (Combinatorica 7) improved the upper bound to $\frac{2n}{3\log_d n}(1+o(1))$ . Shamir and Spencer (Combinatorica 7) proved that $\chi(G_{n,p})$ is concentrated on an interval of length $\omega(n)\sqrt n$ , without locating that interval.
1988. Bollobás (this paper, doi:10.1007/BF02122551) showed that the lower bound is the truth: $\chi(G_{n,p})=(1+o(1))\,n/(2\log_d n)$ for almost every $G_{n,p}$ .

Setting

Let $n\ge 1$ , let $V=[n]$ , and let $N=\binom n2$ . For a fixed real $0<p<1$ , the random graph $G_p=G_{n,p}$ includes each of the $N$ pairs of vertices as an edge independently with probability $p$ . A graph $G$ on $V$ with $e(G)$ edges thus occurs with probability $p^{e(G)}(1-p)^{N-e(G)}$ . A property of graphs holds for almost every $G_p$ if its probability tends to $1$ as $n\to\infty$ .

Put $q=1-p$ and $d=1/q$ . Write $\log$ for the natural logarithm and $[x]$ for the integer part of $x$ , and set

s_0=\bigl[\,2\log_d n-\log_d\log_d n+2\log_d(e/2)+1\,\bigr].

$s_0$ is slightly larger than the independence number of $G_p$ , which is about $2\log_d n-2\log_d\log_d n$ .

Supporting objects: $E(n,r)=\binom nr p^{\binom r2}$ is the expected number of $r$ -cliques of $G_{n,p}$ , and $E_q(n,r)$ is the same with $q$ for $p$ . $X$ is the maximal number of pairwise edge-disjoint $K^r$ subgraphs, and $X'$ is the number of $K^r$ subgraphs that share no edge with any other $K^r$ . Finally $s_1=s_0-\lfloor 5\log_d\log n\rfloor$ .

Formalization targets

Goal: Theorem 4

\mathbb P\Bigl(\frac n{s_0}\le\chi(G_p)\le\frac n{s_0}\Bigl(1+\frac{3\log\log n}{\log n}\Bigr)\Bigr)\longrightarrow 1\qquad(n\to\infty).

Both bounds are part of the goal. The companion statement $\chi(G_p)=(n/s_0)(1+o(1))$ for almost every $G_p$ is a separate item.

Milestones

Lemma 1 (a martingale inequality the paper attributes to Freedman). If $|X_{k+1}-X_k|\le c$ , $b=mc^2$ and $a>0$ , then $\mathbb P(X_m\le\mathbb E X_m-a)\le\bigl(\tfrac b{a+b}\bigr)^{a+b}e^a\le\exp\{-a^2/2(a+b)\}$ .
Adding one edge changes $X$ by at most one. Hence (5): $\mathbb P(X\le\mathbb EX-a)\le\exp\{-a^2/2(a+N)\}$ .
(6), (8), (9): $\mathbb E(X')\ge(1+o(1))E(n,r)$ when $E(n,r)=n^\alpha$ , $\alpha\ge\tfrac12$ , $n^\alpha=o(n^2/(\log n)^4)$ .
Theorem 2: under those hypotheses, $\mathbb P(Y_r\le(1-c)n^\alpha)\le\exp\{-(c^2+o(1))n^{2\alpha-2}\}$ for $0<c\le1$ , where $Y_r$ is the number of $r$ -cliques.
Corollary 3: under explicit growth conditions on $n'$ and $r'$ , almost every $G_p$ has a $K^{r'}$ in every $n'$ -subset of vertices.
The complement of $G_p$ is $G_q$ , and almost no $G_q$ contains $K^{s_0+1}$ . This gives the lower bound.
The choice of $n_1$ with $2n_1^{5/3}\le E_q(n_1,s_1)\le3n_1^{5/3}$ and $n_1=O(n/(\log n)^2)$ ; the greedy colouring bound $\chi\le n/s_1+n_1$ ; and the final inequality $n/s_1+n_1<(n/s_0)(1+3\log\log n/\log n)$ .

Significance

Theorem 4 settles the first-order asymptotics of $\chi(G_{n,p})$ for constant $p$ : $\chi(G_{n,p})\sim n/(2\log_d n)$ . It shows that the trivial lower bound $n/\alpha(G)$ is asymptotically tight. It also shows that greedy colouring, which uses about twice as many colours, is far from optimal. The method also became standard: concentration of a cleverly chosen packing variable, combined with the edge-exposure martingale. It reappears in Łuczak's extension to sparse random graphs and in the later literature on the concentration of $\chi(G_{n,p})$ .

The theorem has been proved since 1988 and is textbook material (Bollobás, Random Graphs; Alon–Spencer, The Probabilistic Method). As of this mission it has no machine-checked proof in Mathlib. A formal proof would add:

a reusable finite model of $G(n,p)$ on SimpleGraph (Fin n);
a lower-tail martingale inequality of Freedman type;
the first formal treatment of the edge-exposure martingale;
a careful audit of the paper's constants, several of which are misprinted (see Formalization scope).

Difficulty

The natural first attempt is to colour greedily and to control the independence number of every large vertex set by a union bound. It fails. The probability that a fixed set of $n'$ vertices has no independent set of size about $2\log_d n'$ is not small enough to beat the $\binom n{n'}$ sets. The second moment method gives only a polynomially small failure probability, and that is what limits earlier results to a constant factor.

The paper needs a failure probability of order $\exp(-n'^{1+\delta})$ for the absence of a large independent set. Two difficulties block this:

The number $Y_r$ of $r$ -cliques is not a Lipschitz function of the edges: one edge can lie in many cliques.
Its concentration is therefore not available from a bounded-differences inequality.

Replacing $Y_r$ by the edge-disjoint packing number $X$ restores the Lipschitz property. The price is a lower bound on $\mathbb E X$ , which requires the count $X'$ of "isolated" cliques and a delicate estimate of the overlap sums $\sum_l F_l$ . These estimates depend on $r$ being within $O(1)$ of the clique number, so the asymptotics of $r_1(n)$ and of the binomial coefficients must be controlled uniformly in $n$ .

Formalization scope

Model. Vertices are Fin n, graphs are SimpleGraph (Fin n), and $G(n,p)$ is given by explicit finite sums: the weight $p^{e(G)}(1-p)^{N-e(G)}$ , probabilities and expectations. No measure is built for the random graph. "Almost every" is Tendsto (fun n => P_n) atTop (𝓝 1). Lemma 1 alone is stated on an arbitrary probability space with a Mathlib Filtration and Martingale.
Fixed $p$ . $p$ is a real constant with $0<p<1$ , the standing assumption of §1, and never depends on $n$ .
Asymptotic notation. $o(1)$ is an explicit sequence $\varepsilon_n\to0$ , quantified after every parameter the page fixes. $f=o(g)$ is Asymptotics.IsLittleO. Hypotheses on $n$ -indexed sequences hold for all large $n$ , because $E(n,r)=n^\alpha$ cannot hold for small $n$ .
Conventions. $\chi$ is Mathlib's chromaticNumber, which is finite on Fin n and converted to ℕ. $s_0,s_1$ are integers built with Int.floor and Real.logb d. For small $n$ they take junk values that no asymptotic statement depends on.
Corrected misprints, each disclosed in the item's Formalization Note:
- Theorem 2's exponent is stated as in the last display of its proof, $\exp\{-(c^2+o(1))n^{2\alpha-2}\}$ .
- (6) omits a factor $\mathbb P(A)$ ; the inequality is stated without conditioning.
- The "maximal" $n_1$ should be minimal; only its existence is stated.
- The printed $n_1\le n/(\log n)^2$ is false with constant $1$ and is replaced by $n_1\le Cn/(\log n)^2$ for some $C>0$ .
- The last display has $n/s_1$ on its right-hand side; it is stated with $n/s_0$ , which is what Theorem 4 requires.
Added hypotheses. Lemma 1 assumes $X_0$ almost surely constant, without which it is false at $m=0$ ; this matches the paper's application. The greedy colouring assumes $s\ge1$ .
Not trivializable. The goal mentions only $\chi$ , $s_0$ and the random graph. It contains no martingale, packing number, $s_1$ or $n_1$ . It keeps both bounds, so neither the well-known lower bound alone nor the asymptotic companion suffices.
Infrastructure needed and reusable:
- the identity $\sum_G p^{e(G)}(1-p)^{N-e(G)}=1$ , and the marginalization over a fixed edge set;
- the edge-exposure martingale on SimpleGraph (Fin n);
- a one-sided Freedman/Bennett inequality, for which Mathlib's conditional sub-Gaussian MGF bounds are a natural starting point;
- Stirling-type estimates for $\binom nr p^{\binom r2}$ near the clique number.

Contributions to any of these are welcome, as are independent proofs of the deterministic milestones (greedy colouring, the final inequality, the complement identity).

Selected references

B. Bollobás, The chromatic number of random graphs, Combinatorica 8 (1988) 49–55. https://doi.org/10.1007/BF02122551
G. R. Grimmett and C. J. H. McDiarmid, On colouring random graphs, Math. Proc. Cambridge Philos. Soc. 77 (1975) 313–324. https://doi.org/10.1017/S0305004100051124
B. Bollobás and P. Erdős, Cliques in random graphs, Math. Proc. Cambridge Philos. Soc. 80 (1976) 419–427. https://doi.org/10.1017/S0305004100053056
D. W. Matula, Expose-and-merge exploration and the chromatic number of a random graph, Combinatorica 7 (1987).
E. Shamir and J. Spencer, Sharp concentration of the chromatic number on random graphs $G_{n,p}$ , Combinatorica 7 (1987).
D. A. Freedman, On tail probabilities for martingales, Ann. Probab. 3 (1975) 100–118. https://doi.org/10.1214/aop/1176996452
K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Math. J. 19 (1967) 357–367. https://doi.org/10.2748/tmj/1178243286
B. Bollobás, Random Graphs, Academic Press, 1985.

15 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 2: The Suggested Matching Algorithm Achieves 1 − 1/e with High Probability, and This Is Tight Even in ExpectationResearch Paper

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

10 thms2 active usersReviewed

Completed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 3: A Worst-Case Transport Plan Exists in a Locally Compact Normed Space under Growth Conditions on c and fResearch Paper

Motivation

In distributionally robust modelling, a baseline probability model $\mu$ on a space $S$ is distrusted, and the analyst reports the largest expected loss over every model within a budget of $\mu$ . Blanchet and Murthy (arXiv:1604.01446; Math. Oper. Res. 44(2), 2019, doi:10.1287/moor.2018.0936) measure the budget with an optimal transport cost and prove strong duality for the resulting worst-case expectation on an arbitrary Polish space, with a lower semicontinuous cost and an upper semicontinuous performance function. Duality computes the worst-case value. A risk manager also wants the worst-case model: a distribution that attains the value, whose structure explains which perturbation of $\mu$ is most harmful.

Such a model need not exist. Unlike the Kantorovich problem, where the set of couplings with two fixed marginals is weakly compact, the feasible set here fixes only one marginal and is not compact in general. Section 5 of the paper gives an example on $\mathbb R$ where the supremum is not attained, then gives abstract conditions under which it is (Proposition 9), and growth conditions on a locally compact normed space that imply them (Corollary 1). Related existence results in $\mathbb R^d$ were obtained by Gao and Kleywegt (arXiv:1604.02199, 2016) and, for empirical baselines and norm costs, by Mohajerin Esfahani and Kuhn (arXiv:1505.05116, 2018).

Setting

Let $S$ be a Polish space with its Borel $\sigma$ -algebra, $\mu$ a probability measure on $S$ , $\delta>0$ a budget, $c:S\times S\to[0,\infty)$ a cost and $f:S\to\mathbb R$ a performance function. The standing assumptions are:

(A1) $c$ is lower semicontinuous and $c(x,y)=0$ iff $x=y$ ;
(A2) $f$ is upper semicontinuous and $\mu$ -integrable.

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ with first marginal $\mu$ and $\int c\,d\pi\le\delta$ (transport plans out of $\mu$ of cost at most $\delta$ ). The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ and the primal value is $I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}$ . The dual feasible set $\Lambda_{c,f}$ consists of pairs $(\lambda,\varphi)$ with $\lambda\ge0$ , $\varphi:S\to[-\infty,\infty]$ universally measurable and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$ . The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ and the dual value is $J=\inf J(\lambda,\varphi)$ . For $\lambda\ge0$ put $\varphi_\lambda(x)=\sup_y\{f(y)-\lambda c(x,y)\}$ .

Section 5 assumes throughout that $(\lambda^*,\varphi_{\lambda^*})\in\Lambda_{c,f}$ is a dual optimal pair with $I=J=J(\lambda^*,\varphi_{\lambda^*})<\infty$ . Write $\Phi'_{\mu,\delta}$ for the plans in $\Phi_{\mu,\delta}$ concentrated on $\{f(x)\le f(y)\}$ .

(P-Compactness): for every $\varepsilon>0$ there are a compact $K_\varepsilon$ with $\mu(K_\varepsilon)>1-\varepsilon$ and $\gamma>0$ such that $\{(x,y)\in K_\varepsilon\times S: f(y)-\lambda^*c(x,y)\ge\varphi_{\lambda^*}(x)-\gamma\}$ has compact closure. (P-USC): $\limsup_n I(\pi_n)\le I(\pi^*)$ whenever $\pi_n\in\Phi'_{\mu,\delta}$ converge weakly to $\pi^*\in\Phi_{\mu,\delta}$ .

On a normed space $E$ : (A3) $c(x,y)\ge g(\|x-y\|)$ for $\|x-y\|>C$ , with $g$ nondecreasing and $g(t)\uparrow\infty$ . (A4) $(f(y)-f(x))/(1+h(\|x-y\|))\le K$ for an increasing $h$ with $h(t)\uparrow\infty$ ; and for every $\varepsilon>0$ , $f(y)-f(x)\le\varepsilon(1+c(x,y))$ once $\|x-y\|>C_\varepsilon$ .

Formalization targets

Goal: Corollary 1 (p. 27)

Let $E$ be a real normed space that is locally compact, and let $c,f$ satisfy (A1)–(A4). Under the standing assumption, if $\lambda^*>0$ there is $\pi^*\in\Phi_{\mu,\delta}$ with

I(\pi^*)=I=J=J(\lambda^*,\varphi_{\lambda^*}).

Milestones

Remark 4, (10)–(11) (p. 8): for $\pi\in\Phi_{\mu,\delta}$ , $I-I(\pi)$ is the sum of two nonnegative gaps, $\int(\varphi_{\lambda^*}(x)-f(y)+\lambda^*c(x,y))\,d\pi$ and $\lambda^*(\delta-\int c\,d\pi)$ ; so an $\varepsilon$ -optimal plan has both gaps at most $\varepsilon$ .
Lemma 17 (p. 43): every plan in $\Phi_{\mu,\delta}$ can be replaced by one in $\Phi'_{\mu,\delta}$ with at least the same value.
§5 display (p. 26): $I=\sup\{I(\pi):\pi\in\Phi'_{\mu,\delta}\}$ .
Proposition 9 (p. 26): on a Polish space, (P-Compactness) and (P-USC) give a primal optimizer.
Corollary 1, Step 1 (p. 28): (A1)–(A4) and $\lambda^*>0$ give (P-Compactness).
Corollary 1, Step 2 (pp. 28–29): (A1), (A2), (A4) and $I<\infty$ give (P-USC):

\limsup_n\int f(y)\,d\pi_n\le\int f(y)\,d\pi^*.

Significance

The result. An attained worst case turns duality into a structural statement. By Theorem 1(b) of the paper, an optimizer moves mass from $x$ only to maximizers of $f(y)-\lambda^*c(x,y)$ and, when $\lambda^*>0$ , uses the full budget. When those maximizers are unique (Remark 8: $c$ convex in $y$ , $f$ concave) the worst-case model is unique and is the image of $\mu$ under a transport map. That map is what stress tests and robust estimators are built from. Without existence, these statements describe an object that may not be there.

Formalizing it. The paper's proofs are complete; nothing here is open. No machine-checked version of this result is known: the worst-case optimal transport literature, including the strong duality of this paper, is unformalized. The mission produces the transport objects of §2 in a form that keeps the paper's generality (Polish space, lower semicontinuous real cost, universally measurable dual variables, the $\infty-\infty$ convention), a tightness argument for nearly optimal one-marginal plans, and an upper semicontinuity argument for unbounded upper semicontinuous integrands under uniform integrability.

Difficulty

The obvious argument takes a maximizing sequence and extracts a weak limit. Both steps fail without more structure. First, $\Phi_{\mu,\delta}$ is not tight: only the first marginal is fixed, and a sequence may push mass to infinity at bounded cost. That is exactly what happens in Example 2 (p. 26), where $\lambda^*=0$ and the value $1$ is approached but never reached. Tightness has to come from the dual: nearly optimal plans concentrate near maximizers of $f(y)-\lambda^*c(x,y)$ , and (A3)–(A4) with $\lambda^*>0$ confine those maximizers. Second, $f$ is only upper semicontinuous and unbounded, so weak convergence alone does not give $\limsup\int f\,d\pi_n\le\int f\,d\pi^*$ . A uniform integrability bound is needed, and it uses the restriction to $\Phi'_{\mu,\delta}$ in an essential way. A third, Lean-specific difficulty is measure-theoretic: $\varphi_{\lambda^*}$ is only universally measurable, and the gaps of Remark 4 are integrals against completions.

Formalization scope

All declarations sit in the namespace ModelRiskOT.PrimalOpt. Values of $I(\pi)$ , $I$ , $J(\lambda,\varphi)$ , $J$ and $\varphi_\lambda$ are in EReal. $I(\pi)$ is $\int f^+(y)\,d\pi-\int f^-(y)\,d\pi$ with lower integrals, and Mathlib's $\top-\top=\bot$ realises the paper's reading of the supremum (footnote 2, p. 5). Integrals of nonnegative or extended-real functions are lower integrals (lintegral), never Bochner integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. Weak convergence is the topology of ProbabilityMeasure (S × S). Measures on $S\times S$ use the product $\sigma$ -algebra.

The following readings are fixed:

The standing assumption of §5 ( $(\lambda^*,\varphi_{\lambda^*})\in\Lambda_{c,f}$ , $I=J$ , $J=J(\lambda^*,\varphi_{\lambda^*})$ , finiteness) consists of hypotheses of Proposition 9 and Corollary 1. $I=J$ is Theorem 1(a), the goal of the companion mission on strong duality, and is not assumed proved here.
In (P-Compactness) the constant $\gamma$ may depend on $\varepsilon$ .
"Increasing" in (A4) is strict.
Remark 4's second conclusion in (11) is also stated as $\lambda^*(\delta-\int c\,d\pi)\le\varepsilon$ , which covers $\lambda^*=0$ .
Lemma 17's last inequality is stated for every plan, which is equivalent under the EReal convention.
Corollary 1's space is a real normed space with LocallyCompactSpace. It also carries PolishSpace, which is redundant, since a locally compact real normed space is finite-dimensional.

The goal cannot be satisfied by a junk value: $I$ and $J$ are EReal suprema and infima, not real sSup, and the hypothesis $\lambda^*>0$ is kept because Example 2 shows the conclusion fails without it. A sorry-free check that $c(x,y)=(x-y)^2$ , $f(y)=y$ on $\mathbb R$ satisfy (A1), (A3) and (A4) accompanies the drafts.

A complete development needs Prokhorov's theorem (in Mathlib), a Fatou lemma for weakly converging measures with a lower semicontinuous integrand, an upper semicontinuity theorem for uniformly integrable upper semicontinuous integrands, and the change of variables $\int\varphi(x)\,d\pi=\int\varphi\,d\mu$ for universally measurable $\varphi$ . The last three are reusable well beyond this mission. Proofs of any milestone, and these general lemmas as separate contributions, are welcome.

Selected references

J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
A. M. Zapała, Unbounded mappings and weak convergence of measures, Statist. Probab. Lett. 78(6):698–706, 2008. doi:10.1016/j.spl.2007.09.033
C. Villani, Optimal Transport: Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

18 thms2 active usersReviewed

Completed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 2: The Worst-Case Probability of a Closed Set A Equals the Baseline Probability of Its Inflation {x : c(x, A) ≤ 1/λ*}Research Paper

Motivation

A probability model $\mu$ for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to $\mu$ . When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where $\mu$ puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.

Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of $A$ is the baseline probability of an inflated version of $A$ . This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.

Setting

Let $S$ be a Polish space with its Borel $\sigma$ -algebra, $P(S)$ its probability measures, and $\mu \in P(S)$ the baseline. A cost $c : S \times S \to \mathbb R_+$ satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and $c(x,y) = 0$ if and only if $x = y$ .

For $\mu_1, \mu_2 \in P(S)$ , a coupling of $\mu_1$ and $\mu_2$ is a probability measure $\pi$ on $S \times S$ with marginals $\mu_1$ and $\mu_2$ ; $\Pi(\mu_1,\mu_2)$ is the set of couplings, and the optimal transport cost is

d_c(\mu_1,\mu_2) = \inf\Big\{\int c\,d\pi : \pi \in \Pi(\mu_1,\mu_2)\Big\}.

For a budget $\delta > 0$ , the primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S \times S$ with first marginal $\mu$ and $\int c\,d\pi \le \delta$ .

Fix a nonempty closed set $A \subseteq S$ and let $c(x,A) = \inf\{c(x,y) : y \in A\}$ be the cheapest cost of moving unit mass from $x$ into $A$ . The worst-case probability is

I = \sup\{P(A) : d_c(\mu,P) \le \delta\}. \tag{12}

Its dual is the univariate problem

\inf_{\lambda \ge 0}\Big\{\lambda\delta + E_\mu\big[(1 - \lambda c(X,A))^+\big]\Big\}, \tag{13}

and for a minimizer $\lambda^* \in [0,\infty)$ of (13) the paper defines

\underline c = \int_{\{c(x,A) < 1/\lambda^*\}} c(x,A)\,d\mu(x), \qquad \overline c = \int_{\{c(x,A) \le 1/\lambda^*\}} c(x,A)\,d\mu(x). \tag{14}

Formalization targets

Goal: Theorem 3 (p. 10)

If $\lambda^* \in [0,\infty)$ attains the infimum in (13) and $\underline c = \overline c$ , then

\sup\{P(A) : d_c(\mu,P) \le \delta\} = \mu\{x : c(x,A) \le 1/\lambda^*\}. \tag{15}

Milestones, in the order the proof uses them

Coupling form (§2.2, p. 5, for $f = 1_A$ ): $I = \sup\{\pi(S \times A) : \pi \in \Phi_{\mu,\delta}\}$ .
Indicator supremum (pp. 8–9): $\sup_{y}\{1_A(y) - \lambda c(x,y)\} = (1 - \lambda c(x,A))^+$ for $\lambda \ge 0$ .
(13) (p. 9): $I$ equals the infimum in (13).
Remark 4, (11) for $f = 1_A$ (p. 8): an $\varepsilon$ -optimal plan $\pi_\varepsilon$ satisfies $\int(\varphi_{\lambda^*}(x) - (1_A(y) - \lambda^* c(x,y)))\,d\pi_\varepsilon \le \varepsilon$ and, for $\lambda^* > 0$ , $(\delta - \varepsilon/\lambda^*)^+ \le \int c\,d\pi_\varepsilon \le \delta$ .
Lemma 4 (p. 11): plans $\pi_n \in \Phi_{\mu,\delta}$ , $n > 1$ , with $\pi_n(C_n) \ge 1 - 1/n$ , no cost outside the set $C_n$ of §2.4.1, and $\pi_n(S \times A) \ge I - 2/n$ .
Lemma 2 (p. 10): $\underline c \le \delta \le \overline c$ if $\lambda^* > 0$ attains (13); $\delta \ge \overline c = \underline c$ if $\lambda^* = 0$ does.

Significance

Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: $\mu$ of the set of points that can reach $A$ at cost at most $1/\lambda^*$ , where $1/\lambda^*$ is determined by $\delta$ through the one-dimensional function $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$ . For the cost $c = d$ of a metric this is the baseline probability of the $1/\lambda^*$ -neighbourhood of $A$ . The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where $S$ is a path space; the result applies there because nothing in it uses local compactness of $S$ .

The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an $\varepsilon$ -optimal-plan argument that avoids assuming a primal optimizer exists.

Difficulty

The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each $x$ with $c(x,A) \le 1/\lambda^*$ to a nearest point of $A$ and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed $A$ in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level $c(x,A) = 1/\lambda^*$ : when $\mu$ charges it, as for atomic baselines, the identity (15) can fail (for $\mu$ a point mass at distance $1$ from $A$ and $\delta < 1$ , the worst case is $\delta$ , not $1$ ), and the hypothesis $\underline c = \overline c$ is exactly what excludes this. Measurability is a second obstacle: $x \mapsto c(x,A)$ is an infimum of a lower semicontinuous function over $A$ and in general only universally measurable, so integrals of it are taken against the completion of $\mu$ .

Formalization scope

All objects live in the namespace ModelRiskOT.WorstProb. $S$ carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; $\mu$ is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on $S \times S$ , and $c(x,y) = 0 \iff x = y$ ). Committed conventions:

Values in $[0,\infty]$ . $d_c$ , $I$ , the objective of (13), $\underline c$ and $\overline c$ are ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part $(\cdot)^+$ is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of $\mu$ , which is the paper's reading (p. 4). No Bochner integral is used.
The threshold $1/\lambda^*$ is written in multiplied form: $c(x,A) \le 1/\lambda^*$ is $\lambda^* c(x,A) \le 1$ , and likewise for the strict inequality and for the sets $C_n$ . For $\lambda^* > 0$ this is the printed condition; at $\lambda^* = 0$ it is the whole space, the paper's convention $1/0 = \infty$ .
$d_c$ fixes both marginals; $\Phi_{\mu,\delta}$ fixes only the first.
$c(x,A)$ is a real infimum over the subtype $A$ ; every statement assumes $A$ nonempty.
" $\lambda^*$ attains the infimum in (13)" is $\lambda^* \ge 0$ and $g(\lambda^*) \le g(\lambda)$ for all $\lambda \ge 0$ .
Inequalities $X \ge I - t$ are written $I \le X + t$ in $[0,\infty]$ ; sequences " $n > 1$ " are indexed by $n \in \mathbb N$ with $1 < n$ .

A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give $I = 1$ for every nonempty $A$ ; the definitions here fix both marginals of the couplings in $d_c$ , and the hypothesis $\underline c = \overline c$ is kept as stated rather than replaced by continuity of $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$ .

A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of $c(\cdot,A)$ through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.

Selected references

J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, arXiv:1604.01446v2, 2017; Mathematics of Operations Research 44(2):565–600, 2019. https://arxiv.org/abs/1604.01446, https://doi.org/10.1287/moor.2018.0936
C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171:115–166, 2018. https://doi.org/10.1007/s10107-017-1172-1
D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (universal measurability, Ch. 7).

11 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Scheduling Deteriorating Jobs on a Single Processor I: Under Linear Deterioration, Sequencing by Increasing E(X_i)/α_i Minimizes the Expected MakespanResearch Paper

Motivation

In classical single-machine stochastic scheduling, $N$ jobs with independent random processing requirements $X_i$ are processed one after another, and the makespan (the completion time of the last job) is the same for every schedule that never idles: it is $X_1+\dots+X_N$ . Research therefore concentrated on weighted flow times and rewards. Browne and Yechiali (Operations Research 38(3), 1990, 495–498) studied jobs that deteriorate while they wait: the longer a job is delayed, the more processing it needs. Such models arose in the control of queueing and communication systems (Browne 1988; Browne and Yechiali 1989) and in inventory issuing, where stored items lose quality at item-specific rates. Under deterioration the actual processing times depend on the order, so the makespan, and its expectation, become functions of the schedule, and the basic question is which order minimizes the expected makespan.

Setting

There are $N$ jobs, all available at time $0$ , and a single processor. Job $i$ has an initial processing requirement $X_i$ , a random variable on a probability space $(\Omega,\mathcal F,P)$ : the time needed to complete job $i$ if it is processed first. Under linear deterioration, a job whose processing is delayed until time $t$ needs

Y_i(t) = X_i + \alpha_i t,

where $\alpha_i>0$ is its deterministic growth rate. A job stops deteriorating once it is put on the processor.

Only nonpreemptive strategies without idling are allowed, so a policy is a permutation $\pi$ of $\{1,\dots,N\}$ , with $\pi(i)=j$ meaning that job $j$ is the $i$ -th processed. The completion times follow the model: $S_0(\pi)=0$ , and the job in position $k$ starts at $S_{k-1}(\pi)$ and takes $Y_{\pi(k)}(S_{k-1}(\pi))$ , so

S_k(\pi) = S_{k-1}(\pi) + X_{\pi(k)} + \alpha_{\pi(k)} S_{k-1}(\pi), \qquad k = 1,\dots,N.

The makespan is $S_N(\pi)$ and the expected makespan is $\mathrm E\,S_N(\pi)$ . In Lean these are completionTime X α π k ω, makespan X α π ω and expectedMakespan P X α π in the namespace DeterioratingJobs.Makespan.

The paper's Lemma 1 concerns, for real numbers $\mu_i$ and $\gamma_i$ , the sum (1)

F_{\mu,\gamma}(\pi) = \sum_{i=1}^{N} \mu_{\pi(i)} \prod_{r=i+1}^{N} \gamma_{\pi(r)},

the Lean lemma1Sum μ γ π (empty product $=1$ ).

Formalization targets

Goal: the expected-makespan index rule (§1, p. 496)

If the $X_i$ are integrable, $\alpha_i>0$ , and $\pi$ schedules the jobs by increasing values of $\mathrm E(X_i)/\alpha_i$ , then

\mathrm E\,S_N(\pi) \le \mathrm E\,S_N(\sigma) \qquad\text{for every permutation } \sigma .

Milestones

Lemma 1 (p. 495). If $\gamma_i>1$ for all $i$ , the sum (1) is minimized over all permutations by any permutation ordered by increasing $\mu_i/[\gamma_i-1]$ , and maximized by any permutation ordered by decreasing values.
Eq. (2) (p. 496). For every $\pi$ and $j\le N$ ,

S_j(\pi) = \sum_{i=1}^{j} X_{\pi(i)} \prod_{r=i+1}^{j} \bigl(1+\alpha_{\pi(r)}\bigr).

The expected makespan in the form (1) (p. 496, after (2)).

\mathrm E\,S_N(\pi) = \sum_{i=1}^{N} \mathrm E(X_{\pi(i)}) \prod_{r=i+1}^{N}\bigl(1+\alpha_{\pi(r)}\bigr) = F_{\mathrm E X,\,1+\alpha}(\pi).

Significance

The result is an index rule: each job receives a number computed from its own data, $\mathrm E(X_i)/\alpha_i$ , and sorting by that number is optimal. It needs only the means of the initial requirements, not their distributions, and it holds without independence. The same reduction to Lemma 1 gives the paper's other index rules: the variance of the makespan under independent requirements, the Poisson-shock model (5), Lévy-type growth (6) and setup/detach times (7). In inventory issuing, it says which stored item to issue first when items lose value at item-specific linear rates. Lemma 1 itself, which the paper attributes to Rau (1971) and relates to optimal search, is a general statement about ordering products of factors along a sequence.

The result is proved in the paper by an appeal to Lemma 1, whose proof is given there as one sentence ("direct upon an interchange argument"). None of these statements has a machine-checked proof on Prove2Me or in Mathlib. This mission produces a formal model of linear deterioration on a single machine, a formal proof of the interchange lemma with ties handled, and the formal index rule.

Difficulty

The algebra of one adjacent interchange is short. The work is in passing from that local comparison to optimality over all $N!$ permutations, with ties allowed: the paper speaks of "the permutation ordered by increasing values", but with equal indices several permutations qualify, and each of them must be shown optimal. The natural route, "an optimal permutation exists and must be sorted", needs care, because a sorted permutation is not unique and the swap that improves an unsorted permutation may only weakly improve it. On the probabilistic side, the expectation of the makespan must be reduced to the expectations of the $X_i$ ; the makespan is a polynomial in the $X_i$ with deterministic coefficients, so this is linearity of the integral, but integrability has to be carried through the recursion.

Formalization scope

Jobs are Fin N (0-based: Lean job i is the paper's job $i+1$ ); a policy is π : Equiv.Perm (Fin N) with π k the job in position k, as in the paper's $\pi(i)=j$ . $N=0$ is allowed.
The probability space is (Ω, P) with [IsProbabilityMeasure P]; $X_i$ is Ω → ℝ; expectations are Bochner integrals, and every theorem about them assumes each $X_i$ integrable. The growth rates are deterministic reals.
Completion times are defined by the model recursion $S_{k}=S_{k-1}+Y_{\pi(k)}(S_{k-1})$ , never by the closed form (2), so that (2) is a theorem about the model.
Explicit readings of loose phrases: "the permutation ordered by increasing values of $v_i$ " means any permutation with $k\mapsto v_{\pi(k)}$ non-strictly increasing (Monotone), and "decreasing" means Antitone; "is minimized" means $\le$ against every permutation; "expected" means the integral of an integrable random variable.
Added hypotheses: $\alpha_i>0$ in the goal (the paper divides by $\alpha_i$ without stating it) and $\gamma_i>1$ in Lemma 1 (the paper applies it only with $\gamma_i = 1+\alpha_i$ or $(1+\alpha_i)^2$ ; for $\gamma_i<1$ the ordering reverses).
Omitted assumptions: positivity of the $X_i$ and their independence. The goal holds without them, so the formal statement is slightly more general than the paper's.
Trivializing formalizations are excluded: defining $S$ by formula (2) would make milestone 2 a definition unfolding; a strictly increasing ordering would make the goal vacuous whenever two indices tie; ordering $\pi^{-1}$ instead of $\pi$ states a different theorem; dropping integrability makes all expectations $0$ ; allowing $\alpha_i=0$ makes $\mathrm E(X_i)/\alpha_i=0$ a meaningless index.
Not formalized here: the variance result (3), the Poisson model (5), the Lévy model (6), Proposition 1, setup times (7), exponential growth (9), and the NP-hardness conjecture. Proposition 2 (weighted expected completion time) is the companion mission Scheduling Deteriorating Jobs on a Single Processor II.
Related platform items, none of which states these results: PalmQueueing.Ordering.interchange_permutations (interchange permutations of a GI/GI/1 queue) and the additive, non-deteriorating completion-time models MooreLateJobs.Shared.completionTime and NumStochOpt.ListScheduling.Makespan.

Contributions welcome: proofs of the milestones, a reusable "sorted permutation minimizes a sum of products" lemma, and the variance index (3) as an extension.

Selected references

S. Browne, U. Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 1990, 495–498. https://doi.org/10.1287/opre.38.3.495
J. G. Rau, Minimizing a Function of Permutations of n Integers, Operations Research 19(1), 1971, 237–240. https://doi.org/10.1287/opre.19.1.237
F. P. Kelly, A Remark on Search and Sequencing Problems, Mathematics of Operations Research 7(1), 1982, 154–157. https://doi.org/10.1287/moor.7.1.154
R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

6 thms2 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 1: When OPT = Ω(n), the Two Suggested Matchings Algorithm Achieves ALG/OPT ≥ (1 − 2/e²)/(4/3 − 2/(3e)) − ε ≈ 0.670 with Probability 1 − e^(−Ω(n))Research Paper

Motivation

Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.

When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is $1 - 1/e \approx 0.632$ , achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat $1 - 1/e$ , and answers yes.

Timeline.

1990: Karp, Vazirani and Vazirani give RANKING, with ratio $1 - 1/e$ for adversarial arrivals, and show this is optimal in that model.
2005: Mehta, Saberi, Vazirani and Vazirani obtain $1 - 1/e$ for the budgeted AdWords generalization.
2009: Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) show that in the i.i.d. model the two suggested matchings algorithm achieves about $0.670$ with high probability when OPT is linear in $n$ , the first ratio above $1 - 1/e$ for this model, and that no online algorithm reaches $26/27$ in expectation.

Setting

An instance is a bipartite graph $G = (A, I, E)$ with a finite set $A$ of advertisers, a finite set $I$ of impression types, and edges $E \subseteq A \times I$ recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected ( $e_i = 1$ ). So $n = |I|$ impressions arrive one at a time, with types $\omega(0), \dots, \omega(n-1)$ drawn independently and uniformly from $I$ . On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. $\mathrm{ALG}(\omega)$ is the number of impressions an algorithm assigns. $\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 $a$ with $(a, \omega(t)) \in E$ .

The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph $G_f$ has a source arc of capacity $2$ into every advertiser, a unit-capacity arc along every edge of $E$ , and an arc of capacity $2$ from every type to a sink. The algorithm takes the edge set $E_f$ of an integral maximum flow. Every vertex then has at most two edges of $E_f$ , so $E_f$ splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:

on cycles, the colours alternate;
on odd paths, the colours alternate, with more blue than red;
on even paths between advertisers, the colours alternate;
on even paths between types, the first two edges are blue, then the colours alternate, ending in blue.

Online, the first arrival of type $i$ tries the advertiser along $i$ 's blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: $A_{BR}$ (one blue, one red), $A_{BB}$ (two blue), $A_B$ (one blue only) and $A_R$ (one red only).

Formalization targets

Goal: Theorem 5, first sentence, $e_i = 1$

Let

\alpha = \frac{1 - 2/e^2}{4/3 - 2/(3e)} \approx 0.67029 .

The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every $\varepsilon > 0$ and $c > 0$ there are $\delta > 0$ and $N$ such that, for every instance with $n \ge N$ , every maximum flow edge set and every rule-following colouring,

\Pr_\omega\big[\ \mathrm{OPT} \ge c\,n \implies \mathrm{ALG} \ge (\alpha - \varepsilon)\,\mathrm{OPT}\ \big] \;\ge\; 1 - e^{-\delta n}.

Third, $\alpha > 1 - 1/e$ .

Milestones

Facts 1 and 2: concentration for two balls-in-bins statistics.
The note of §4.2.1: each type has no coloured edge, one blue edge, or one blue and one red edge.
Equation (1): $|E_f| = 2|A_{BR}| + 2|A_{BB}| + |A_B| + |A_R|$ .
Equation (2): with high probability, $\mathrm{ALG} \ge (1 - 1/e^2)|A_{BB}| + (1 - 2/e^2)|A_{BR}| + (1 - 3/(2e))(|A_B| + |A_R|) - 4\varepsilon n$ .
Equation (3): $|E_f| = 2(|A_T| + |I_S|) + |E_\delta|$ for the surgered residual cut $(S,T)$ of $G_f$ .
Equation (4): with high probability, $\mathrm{OPT} \le |A_{BR}| + |A_{BB}| + \tfrac12(|A_B| + |A_R|) + (\tfrac12 - \tfrac1e)|E_\delta| + \varepsilon n$ .
Lemma 1: $|E_\delta| \le \tfrac23|A_{BR}| + \tfrac43|A_{BB}| + |A_B| + \tfrac13|A_R|$ .

Significance

The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above $1 - 1/e$ . The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly $1 - 1/e$ , so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.

The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.

Difficulty

The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of $E_f$ ). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality $|A_B| \ge |A_R|$ behind (2). On the probabilistic side, the advertisers of $A_{BR}$ share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to $d$ sequences.

Formalization scope

All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and $E$ is a Finset (A × I). Probabilities are counting ratios $\#\{\omega : \mathrm{Fin}\ n \to I \mid P\,\omega\}/|I|^n$ , so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of $G_f$ is its set of saturated middle edges, i.e. a subset of $E$ with at most two edges per vertex; $E_f$ is such a set of maximum cardinality. A colouring is given by a listing of the components of $E_f$ as vertex sequences. Every theorem quantifies over every maximum $E_f$ and every colouring the rules allow, since the paper fixes neither.

The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:

"with probability $1 - e^{-\Omega(n)}$ " and "with high probability" (Theorem 5, (2), (4)) become: $\exists\, \delta > 0,\ \exists\, N$ , chosen before the instance, with probability at least $1 - e^{-\delta n}$ for all $n \ge N$ ;
"as long as OPT $= \Omega(n)$ " becomes the event $\mathrm{OPT} \ge c\,n$ for an arbitrary $c > 0$ fixed before $\delta$ and $N$ ;
the $O(1)$ term in the bound on $|A^*_\delta|$ (p. 8) is absorbed into $\varepsilon n$ for $n \ge N$ .

Corrections to the printed statements:

Theorem 5 prints $\mathrm{ALG}/\mathrm{OPT} - \epsilon \ge \alpha$ ; the proof concludes $\mathrm{ALG}/\mathrm{OPT} + \epsilon \ge \alpha$ , so the goal states $\mathrm{ALG} \ge (\alpha - \varepsilon)\mathrm{OPT}$ ;
Fact 1 prints the failure probability $2e^{-\epsilon n/2}$ ; its proof gives $2e^{-\epsilon^2 n/2}$ , which is used;
Fact 2 states two hypotheses its proof uses: the bins of a sequence are distinct, and $c^2 < n$ .

The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer $e_i$ (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.

Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.

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
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, FOCS 2005; J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321

13 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems 2: Worst-Case Distribution with Largest Covariance for Piecewise-Linear PortfoliosResearch Paper

Motivation

A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.

The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.

Setting

Let $n$ assets have a random return vector $\xi\in\mathbb R^n$ , and let $x\in\mathbb R^n$ be a portfolio, so the return is $\xi^{\mathsf T}x$ . A distribution of $\xi$ is a Borel probability measure on $\mathbb R^n$ with finite second moments. For symmetric matrices, $A\preceq B$ (the Loewner order) means $B-A$ is positive semidefinite.

Given a support set $S$ , a centre $\mu_0$ , a positive definite matrix $\Sigma_0\succ0$ and $\gamma_1\ge0$ , $\gamma_2>0$ , the distributional set of Assumption 3 is

\mathcal D_1(S,\mu_0,\Sigma_0,\gamma_1,\gamma_2)=\Big\{P\ :\ P(\xi\in S)=1,\ (\mathbb E[\xi]-\mu_0)^{\mathsf T}\Sigma_0^{-1}(\mathbb E[\xi]-\mu_0)\le\gamma_1,\ \mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]\preceq\gamma_2\Sigma_0\Big\}.

The second constraint, (1b), is the covariance constraint.

The utility is piecewise linear concave, $u(y)=\min_{k\in\{1,\dots,K\}}a_ky+b_k$ with $K\ge1$ pieces, and the cost of a return is $-u$ :

h(x,\xi)=\max_{k}\ \big(-a_k\,\xi^{\mathsf T}x-b_k\big).

With estimates $\hat\mu$ , $\hat\Sigma\succ0$ of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean ( $\gamma_1=0$ ) is

\max_{P\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,0,\gamma_2)}\ \mathbb E_P\big[h(x,\xi)\big].\tag{18}

The proof relates (18) to a semidefinite program in variables $\Lambda_k\in\mathbb R^{n\times n}$ , $\lambda_k\in\mathbb R^n$ , $\nu_k\in\mathbb R$ :

\max\ \sum_k\big(-a_k\,x^{\mathsf T}\lambda_k-b_k\nu_k\big)\quad\text{s.t.}\quad \sum_k\Lambda_k\preceq\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T},\ \ \sum_k\lambda_k=\hat\mu,\ \ \sum_k\nu_k=1,\ \ \begin{bmatrix}\Lambda_k&\lambda_k\\\lambda_k^{\mathsf T}&\nu_k\end{bmatrix}\succeq0.\tag{19}

Formalization targets

Goal: Proposition 3

For every $\gamma_1\ge0$ (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case $\gamma_1=0$ ),

\exists\,P^*\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2):\quad \mathbb E_{P^*}\big[(\xi-\hat\mu)(\xi-\hat\mu)^{\mathsf T}\big]=\gamma_2\hat\Sigma\quad\text{and}\quad \mathbb E_Q[h(x,\xi)]\le\mathbb E_{P^*}[h(x,\xi)]\ \ \forall\,Q\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2).

The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio $x$ , every $K\ge1$ , every $a,b$ , every $\hat\mu$ , every $\hat\Sigma\succ0$ , every $\gamma_1\ge0$ and every $\gamma_2>0$ .

Milestones

Every value of (18) is dominated by the value of a feasible point of (19).
(19) has an optimal solution at which $\sum_k\Lambda_k=\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T}$ .
If $\begin{bmatrix}\Lambda&\lambda\\\lambda^{\mathsf T}&\nu\end{bmatrix}\succeq0$ and $\nu>0$ , a random vector with mean $\lambda/\nu$ and second moment $\Lambda/\nu$ exists.
The mixture $\sum_k\nu_kP_k$ of such vectors, built from a tight feasible point with all $\nu_k>0$ , lies in $\mathcal D_1$ and has second moment $\gamma_2\hat\Sigma$ about $\hat\mu$ .
The expected cost under that mixture is at least the objective value of (19) at the point.
(18) and (19) have the same attained optimal value.

Significance

The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound $\gamma_3\Sigma_0\preceq\mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]$ (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with $\gamma_2=1$ , the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).

The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with $\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2)$ ; the paper's proof writes out only $\gamma_1=0$ "for simplicity of our derivations". The goal states the proposition for every $\gamma_1\ge0$ ; the milestones follow the written proof and are stated for $\gamma_1=0$ .

Difficulty

The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in $\mathcal D_1$ must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in $\xi$ . Second, an optimal point of (19) must be turned back into a distribution in $\mathcal D_1$ ; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where $\nu_k=0$ , which the paper sets aside "without loss of generality" although such a block can carry a nonzero $\Lambda_k$ that the mixture would lose.

Formalization scope

Vectors are Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; $A\preceq B$ is (B - A).PosSemidef; $\Sigma_0^{-1}$ is Mathlib's matrix inverse, used only with $\Sigma_0\succ0$ .
A distribution is a Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in $L^2$ (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to $0$ .
$P(\xi\in S)=1$ is an almost-everywhere statement; the goal uses $S=\mathbb R^n$ ("infinite support constraint"). The convexity of $S$ , $\mu_0\in\operatorname{int}S$ and the separation oracle of Assumption 3 concern the paper's algorithms and are not part of the set.
The maximum of (18) is never a real supremum: the goal asserts a maximizer that dominates every member of the set. The cost uses a finite maximum over $K\ge1$ pieces ([NeZero K]).
Standing hypotheses: $\hat\Sigma\succ0$ (Assumption 3's $\Sigma_0\succ0$ , and endnote 1), $\gamma_2>0$ (§3), $\gamma_1\ge0$ (Assumption 3) in the goal; the milestones fix $\gamma_1=0$ as the proof does. The portfolio $x$ ranges over all of $\mathbb R^n$ ; the simplex constraint (16b) plays no role in the inner problem, so dropping it only strengthens the statements.
The objective of (19) has the sign of the proof's final computation (p. 21), $\sum_k(-a_kx^{\mathsf T}\lambda_k-b_k\nu_k)$ ; display (19a) on p. 19 prints the opposite signs, a misprint.
Ruling out trivial readings: the goal requires both membership in $\mathcal D_1$ with tight covariance and domination of every member of $\mathcal D_1$ . A distribution with covariance $\gamma_2\hat\Sigma$ alone, or a maximizer alone, would not suffice. The goal does not claim that every maximizer is tight; for $K=1$ the cost is linear and every member of $\mathcal D_1$ is a maximizer.
Infrastructure needed: existence of distributions with prescribed mean and covariance (for instance multivariate Gaussians, or degenerate laws on a subspace), finite mixtures of measures and their moments, Schur complements of positive semidefinite block matrices, and compactness of the feasible set of (19). Proofs of the milestones in any order are welcome.

The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.

Selected references

E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010 (authors' draft of 20 February 2008 used here). https://doi.org/10.1287/opre.1090.0741
I. Popescu, Robust mean-covariance solutions for stochastic optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
Y. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

9 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Optimality and Duality Theory for Stochastic Optimization Problems with Nonlinear Dominance Constraints 2: With Finite Scenarios and Slater's Condition, Piecewise-Linear Utilities Are MultipliersResearch Paper

Motivation

Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.

In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.

Setting

There are $n$ scenarios $\omega_1,\dots,\omega_n$ with probabilities $p_j \ge 0$ , $\sum_j p_j = 1$ , and $m$ benchmark constraints, indexed by $i \in I = \{1,\dots,m\}$ ; $J = \{1,\dots,n\}$ . A decision $z$ ranges over a convex set $Z \subseteq \mathbb R^N$ . For each scenario $j$ , $h_j:\mathbb R^N\to\mathbb R$ is the objective contribution and $g_{ij}:\mathbb R^N\to\mathbb R$ the $i$ th outcome, all concave. The benchmark $Y_i$ has realizations $y_{ij}$ . Write $(t)_+=\max(t,0)$ .

The second-order dominance of a finitely distributed $X_i$ (realizations $x_{ij}$ ) over $Y_i$ on an interval $[a_i,b_i]$ reads

\sum_{j} p_j(\eta - x_{ij})_+ \le \sum_j p_j(\eta-y_{ij})_+ \quad\text{for all } \eta\in[a_i,b_i]. \tag{36}

The split-variable problem (38)–(41) is

\max \sum_{j=1}^n p_j h_j(z)\quad\text{s.t.}\quad \sum_{j} p_j(y_{ik}-x_{ij})_+ \le \sum_j p_j(y_{ik}-y_{ij})_+,\quad x_{ik}\le g_{ik}(z),\quad z\in Z,

for all $i\in I$ , $k\in J$ , over $z$ and $X=(x_{ij})\in\mathbb R^{mn}$ . The Slater condition asks for $\tilde z \in \operatorname{relint} Z$ and $\tilde X$ satisfying the dominance constraints (39) with $\tilde x_{ik} < g_{ik}(\tilde z)$ for all $i,k$ .

The utility set $V_i$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave, nondecreasing, piecewise linear with break points only at the $y_{ik}$ , and zero on $[\max_k y_{ik},\infty)$ . With $\theta_{ij}\ge 0$ multipliers for the splitting constraints $x_{ij}\le g_{ij}(z)$ , the Lagrangian is

L(z,X,u,\theta) = \sum_{j=1}^n p_j\Big[h_j(z)+\sum_{i=1}^m\theta_{ij}g_{ij}(z)\Big]+\sum_{i=1}^m\sum_{j=1}^n p_j\big[u_i(x_{ij})-u_i(y_{ij})-\theta_{ij}x_{ij}\big]. \tag{42}

Multipliers $\mu_{ik}$ of the inequalities (39) generate the utility $u_i(t)=-\sum_k\mu_{ik}(y_{ik}-t)_+$ (46). The dual functional is $D(u,\theta)=\sup_{z\in Z,\,X}L(z,X,u,\theta)$ (47).

Formalization targets

Goal: Theorem 6

Under the Slater condition, $(\hat z,\hat X)$ optimal for (38)–(41) implies that there are $\hat u_i\in V_i$ and $\hat\theta\ge 0$ with

L(\hat z,\hat X,\hat u,\hat\theta)=\max_{(z,X)\in Z\times\mathbb R^{mn}}L(z,X,\hat u,\hat\theta),\qquad \sum_j p_j[\hat u_i(\hat x_{ij})-\hat u_i(y_{ij})]=0,\qquad \hat\theta_{ij}(\hat x_{ij}-g_{ij}(\hat z))=0;

conversely, these conditions together with feasibility imply optimality.

Milestones

Lemma 2 (p. 15): if $a_i\le y_{ij}\le b_i$ , then (36) is equivalent to the $mn$ inequalities (37) at the realizations $\eta=y_{ik}$ , and also to (36) on the whole line.
Eq. (46) (p. 17): for any $\mu$ , the standard Lagrangian $\Lambda(z,X,\mu,\theta)$ equals $L(z,X,u,\theta)$ with $u$ given by (46).
p. 18: for $\mu_i\ge0$ , the utility (46) lies in $V_i$ .
pp. 16–17: under Slater, an optimal solution admits Kuhn–Tucker multipliers $\mu\ge0$ , $\theta\ge0$ for (38)–(41) with complementarity.
p. 18: every $v\in V_i$ is of the form (46) with $\mu_i\ge0$ .
Theorem 7 (p. 18), after the goal: the dual problem $\min\{D(u,\theta): u\in V_1\times\dots\times V_m,\ \theta\ge0\}$ has a solution and no duality gap.

Significance

Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, $V_i$ is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.

The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set $V_i$ and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.

Difficulty

The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of $\mathbb R^N$ . Neither fits: the dominance constraint at the smallest realization $y_{i,[1]}$ has right-hand side $0$ and a nonnegative left-hand side, so it can never hold strictly, and $Z$ may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in $V_i$ must be written as a nonnegative combination of the kinks $(y_{ik}-t)_+$ , which requires handling repeated realizations and the one-sided slopes at each break point.

Formalization scope

$\mathbb R^N$ is Fin N → ℝ; $X$ , $\theta$ , $\mu$ are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.
Probabilities satisfy $p_j\ge0$ , $\sum_jp_j=1$ ; $p_j=0$ is allowed, as on the page.
Standing assumptions of p. 2 are explicit hypotheses: $Z$ convex and $h_j$ , $g_{ij}$ concave on $\mathbb R^N$ . Continuity is not stated, since finite concave functions on $\mathbb R^N$ are continuous.
The relative interior is intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.
$V_i$ is defined by concavity, monotonicity, affinity on every interval whose interior contains no $y_{ik}$ , and $u=0$ on $[\max_ky_{ik},\infty)$ . This last clause is the page's $u(y_{i,[n]})=0$ combined with $V_i\subset\mathcal U_1([a_i,b_i])$ . No positive slope is required, because the printed " $c>0$ " in $\mathcal U_1$ is a misprint for $c\ge0$ .
"max" in (43) is an attained maximum over all of $Z\times\mathbb R^{mn}$ , with no constraints on $X$ . The dual functional (47) is an EReal supremum.
Theorem 6 keeps the Slater condition as a hypothesis of the whole statement, as printed, although its converse part does not use it.
A trivializing formalization is ruled out. $V_i$ is not defined as the set of functions of the form (46), which would make milestones 3 and 5 true by definition. Slater does not require strict dominance constraints, which would make it unsatisfiable. A sorry-free check confirms that the goal's hypotheses hold on an instance ( $n=2$ , $Z=[0,1]$ ).
Reusable beyond this mission: the Kuhn–Tucker theorem with polyhedral constraints and relative-interior Slater point (milestone 4), and Lemma 2. Proofs of any item, and alternative proofs of the goal that avoid milestone 4, are welcome.
The pure-dominance case is the earlier paper of Dentcheva–Ruszczyński (2003). The function $F_2$ and its expected-shortfall form are due to Ogryczak–Ruszczyński. The general Lagrange duality on the platform (ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.

Selected references

D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program., 2004 (cited here from the authors' revised manuscript, April 2003). https://doi.org/10.1007/s10107-003-0453-z
D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003) 548–566. https://doi.org/10.1137/S1052623402420528
W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13 (2002) 60–78. https://doi.org/10.1137/S1052623400375075
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §28. https://doi.org/10.1515/9781400873173

8 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Maximum Pressure Policies in Stochastic Processing Networks I: Under the EAA Assumption, Maximum Pressure Is Pathwise Stable Whenever the Static Planning LP Has a Feasible Solution with ρ ≤ 1Research Paper

Why throughput matters

A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)

Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4

Network and allocations

There are $I$ internal buffers, $J$ activities, and $K$ processors. Buffer $0$ represents the outside world. The $K\times J$ matrix $A$ records resource use: $A_{kj}=1$ when activity $j$ requires processor $k$ . The $J\times(I+1)$ matrix $B$ records which buffers an activity processes. An input activity processes Buffer $0$ ; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.

For activity $j$ , the processing requirements have mean $m_j$ and the routing counts have long-run matrix $P^j$ . Write $\mu_j=1/m_j$ . The input-output matrix is

R_{ij}=\mu_j\left(B_{ji}-\sum_{i'=0}^{I}B_{ji'}P^j_{i'i}\right),\qquad i=1,\ldots,I.

Positive $R_{ij}$ means activity $j$ consumes net material from internal buffer $i$ ; negative means it produces net material there. An allocation $a\in\mathcal A$ assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set $\mathcal E$ consists of the extreme points of this allocation set. At buffer vector $z$ , allocation $a$ has network pressure $p(a,z)=z\cdot Ra$ . The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of $\mathcal E$ . Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3

The extreme-allocation-available assumption (EAA) says that for every nonnegative $z$ , a pressure maximizer in $\mathcal E$ can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions $x\ge0$ and a service-processor load $\rho$ such that $Rx=0$ , every input processor has load one, and every service processor has load at most $\rho$ . Dai and Lin (2005), p. 202

Formalization targets

The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with $\rho\le1$ implies

\mathbb P\!\left(\forall i\in\{1,\ldots,I\},\ \lim_{t\to\infty}\frac{Z_i(t)}{t}=0\right)=1.

The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of $(Z(rt),T(rt))/r$ along positive scales $r\to\infty$ . The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214

What the result gives

Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2

The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.

Why the proof is difficult

Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214

Formalization scope

The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in $\mathbb N\cup\{\infty\}$ and uniform-on-compact distance using the $\ell^1$ norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)

The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and $m_j>0$ , so $\mu_j=1/m_j$ is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of $P^j$ sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200

The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold $J$ at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact $\rho\le1$ bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.

Selected references

J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. DOI.
S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Annals of Applied Probability 11(3):608–649, 2001. DOI.

10 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Kullback–Leibler Upper Confidence Bounds for Optimal Sequential Allocation II: Empirical KL-UCB Draws a Suboptimal Arm log(T)/K_inf(ν_a, μ*) + O((log T)^{4/5} log log T) TimesResearch Paper

Motivation

In a stochastic multi-armed bandit a player repeatedly chooses one of $K$ arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm $a$ at least $(1+o(1))\log T/\mathcal K_{\inf}(\nu_a,\mu^\star)$ times in $T$ rounds, where $\mathcal K_{\inf}$ is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.

For rewards in $[0,1]$ , classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve $O(\log T)$ pulls but with a constant governed by the gap of the means, not by $\mathcal K_{\inf}$ . Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on $[0,1]$ . A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).

Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.

Setting

A bandit has $K\ge2$ arms with reward distributions $\nu_1,\dots,\nu_K$ in a known model $\mathcal F$ : the set of probability distributions over $[0,1]$ with finite support. Write $\mathrm E(\nu)=\int x\,d\nu(x)$ , $\mu_a=\mathrm E(\nu_a)$ and $\mu^\star=\max_a\mu_a$ ; arm $a$ is suboptimal if $\mu_a<\mu^\star$ . At each round $t\ge1$ the player picks an arm $A_t$ based on past observations and observes a reward drawn from $\nu_{A_t}$ . $N_a(T)=\sum_{t=1}^T\mathbb I\{A_t=a\}$ is the number of pulls of arm $a$ up to round $T$ .

Equivalently, each arm has a reward stack $X_{a,1},X_{a,2},\dots$ of i.i.d. draws from $\nu_a$ , all stacks independent, and the $n$ -th pull of arm $a$ returns $X_{a,n}$ . The empirical distribution of the first $n$ rewards is $\hat\nu_{a,n}=\frac1n\sum_{k=1}^n\delta_{X_{a,k}}$ , and $\hat\nu_a(t)=\hat\nu_{a,N_a(t)}$ .

The minimal divergence is

\mathcal K_{\inf}(\nu,\mu)=\inf\bigl\{\mathrm{KL}(\nu,\nu'):\nu'\in\mathcal F,\ \mathrm E(\nu')>\mu\bigr\}\in[0,+\infty],

the smallest Kullback–Leibler divergence from $\nu$ to a distribution of the model whose mean exceeds $\mu$ .

Empirical KL-UCB (Algorithm 3) pulls each arm once, then for $t=K,K+1,\dots$ pulls an arm maximizing

U_a(t)=\sup\Bigl\{\mathrm E(\nu):\nu\in\mathfrak M_1\bigl(\mathrm{Supp}(\hat\nu_a(t))\cup\{1\}\bigr),\ \mathrm{KL}(\hat\nu_a(t),\nu)\le\frac{f(t)}{N_a(t)}\Bigr\},

where $\mathfrak M_1(A)$ is the set of probability distributions carried by $A$ and $f(t)=\log t+\log\log t$ . The added point $1$ is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is $0$ .

Formalization targets

Goal: Theorem 2 (pp. 15–16)

Assume $\mu_a>0$ for all arms and $\mu^\star<1$ . There is a constant $M(\nu_a,\mu^\star)>0$ depending only on $\nu_a$ and $\mu^\star$ such that, for every suboptimal arm $a$ and all $T\ge3$ ,

\begin{aligned}\mathbb E[N_a(T)]\le{}&\frac{\log T}{\mathcal K_{\inf}(\nu_a,\mu^\star)}+\frac{36}{(\mu^\star)^4}(\log T)^{4/5}\log\log T+\Bigl(\frac{72}{(\mu^\star)^4}+\frac{2\mu^\star}{(1-\mu^\star)\mathcal K_{\inf}(\nu_a,\mu^\star)^2}\Bigr)(\log T)^{4/5}\\&+\frac{(1-\mu^\star)^2M(\nu_a,\mu^\star)}{2(\mu^\star)^2}(\log T)^{2/5}+\frac{\log\log T}{\mathcal K_{\inf}(\nu_a,\mu^\star)}+\frac{2\mu^\star}{(1-\mu^\star)\mathcal K_{\inf}(\nu_a,\mu^\star)^2}+4.\end{aligned}

The constants are the paper's. $M$ is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but $(\nu_a,\mu^\star)$ .

Milestones

(7), p. 9: the sets $\mathcal C_{\mu,\gamma}=\{\nu:\exists\nu'\in\mathcal F,\ \mathrm E(\nu')>\mu,\ \mathrm{KL}(\nu,\nu')\le\gamma\}$ satisfy $\mathcal C_{\mu,\gamma}\subseteq\{\nu:\mathcal K_{\inf}(\nu,\mu)\le\gamma\}$ .
(5), p. 9: the decomposition $\{A_{t+1}=a\}\subseteq\{\mu^\dagger\ge U_{a^\star}(t)\}\cup\{\mu^\dagger<U_a(t),\ A_{t+1}=a\}$ .
The display after (7), p. 9: $\mathbb E[N_a(T)]\le1+\sum_{t=K}^{T-1}\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}+\sum_{t=K}^{T-1}\mathbb P\{\hat\nu_{a,N_a(t)}\in\mathcal C_{\mu^\dagger,f(t)/N_a(t)},\ A_{t+1}=a\}$ .
(8), p. 10: the second sum is at most $\sum_{n=1}^{T-K}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$ .
(9)–(10), p. 10: $\mathbb E[N_a(T)]\le f(T)/\mathcal K_{\inf}(\nu_a,\mu^\star)+\sum_{n>n_0}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}+\sum_t\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}+2$ with $n_0=\lceil f(T)/\mathcal K_{\inf}(\nu_a,\mu^\star)\rceil$ .
p. 15: the supremum defining $U_a(t)$ over $\mathcal F$ equals the supremum over $\mathfrak M_1(\mathrm{Supp}(\hat\nu_a(t))\cup\{1\})$ .
Implicit in Theorem 2: $0<\mathcal K_{\inf}(\nu,\mu)<\infty$ for $\nu\in\mathcal F$ and $\mathrm E(\nu)<\mu<1$ .
Proposition 1, p. 20: for $n$ i.i.d. observations from any $\nu_0$ on $[0,1]$ with $\mathrm E(\nu_0)\in(0,1)$ and every $\varepsilon>0$ ,

\mathbb P\{U(\hat\nu_n,\varepsilon)\le\mathrm E(\nu_0)\}\le\mathbb P\{\mathcal K_{\inf}(\hat\nu_n,\mathrm E(\nu_0))\ge\varepsilon\}\le e(n+2)\exp(-n\varepsilon).

Significance

Theorem 2 gives a finite-time bound whose leading term, $\log T/\mathcal K_{\inf}(\nu_a,\mu^\star)$ , equals the Burnetas–Katehakis lower bound for the model $\mathcal F$ . Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in $[0,1]$ , and the regret $\sum_a(\mu^\star-\mu_a)\mathbb E[N_a(T)]$ inherits the optimal constant. Since $\mathcal K_{\inf}(\nu_a,\mu^\star)$ is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point $1$ added, valid for every law on $[0,1]$ , not only finitely supported ones.

The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about $\mathcal K_{\inf}$ that the bound needs. A formal proof would supply an explicit $M(\nu_a,\mu^\star)$ , which the paper defines only inside the supplement.

Difficulty

The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be $o(\log T)$ with explicit constants. The second, $\sum_n\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$ , needs a deviation estimate for the empirical $\mathcal K_{\inf}$ of a suboptimal arm that is precise enough to keep the leading constant $1/\mathcal K_{\inf}(\nu_a,\mu^\star)$ : a bound that only controls the deviation of the empirical mean loses it, since $\mathcal K_{\inf}$ depends on the whole distribution. The first, $\sum_t\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}$ , concerns the optimal arm after a random number of pulls $N_{a^\star}(t)$ , which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of $\mathcal K_{\inf}$ as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.

Formalization scope

Arms are Fin K, and arm $a$ of the paper is index $a-1$ . The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: $X_{a,k}$ (indexed from $0$ ) are independent, identically distributed within each arm, with mean $\mu_a$ . Pull counts and $\mu^\star$ are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in $[0,1]$ pathwise (a representation of " $\nu_a$ is carried by $[0,1]$ "), every arm choice is measurable, and in the goal the strategy is non-anticipating ( $A_{t+1}$ is measurable with respect to the arms and rewards of rounds $1,\dots,t$ ). A run of Algorithm 3 is a pathwise predicate: rounds $1,\dots,K$ pull distinct arms, and every later round pulls a maximizer of $U_\cdot(t)$ , with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in $[0,+\infty]$ , with the empirical distribution as first argument. $\mathcal K_{\inf}$ is kept in $[0,+\infty]$ and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's $\sum_{n\ge n_0+1}$ in (10) is stated as the finite sum over $n_0<n\le T-K$ that (8) produces. The probability space of Theorem 2 lies in Type.

Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains $\mathrm E(\hat\nu_a(t))$ ) and bounded above, so it is never Lean's junk value. $\mathcal K_{\inf}$ and $\mathcal C_{\mu,\gamma}$ range over $\mathcal F$ , not over all measures. The run predicate has both the initialization and the argmax clause. $M$ is quantified before the bandit and the horizon.

Reusable beyond this mission: $\mathcal K_{\inf}$ for $\mathcal F$ , the empirical-likelihood bound $U$ of (15), and Proposition 1, a concentration inequality for empirical $\mathcal K_{\inf}$ that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.

Selected references

O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3):1516–1541, 2013. arXiv:1210.1136v4, doi:10.1214/13-AOS1119; supplement doi:10.1214/13-AOS1119SUPP.
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6(1):4–22, 1985. doi:10.1016/0196-8858(85)90002-8
A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Adv. Appl. Math. 17(2):122–142, 1996. doi:10.1006/aama.1996.0007
J. Honda, A. Takemura, An asymptotically optimal bandit algorithm for bounded support models, COLT 2010, 67–79.
P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Mach. Learn. 47:235–256, 2002. doi:10.1023/A:1013689704352

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Revenue Management with Forward-Looking Buyers: Under Weakly Decreasing Demand the Deterministic Optimal Cutoffs Fall over Time and Satisfy One-Period Look-AheadResearch Paper

Motivation

Retailers of seasonal goods (fashion, electronics, airline seats) sell a fixed stock over a finite season to customers who arrive over time, and those customers know that prices may fall. A customer who expects a markdown waits, and a seller who ignores this loses revenue. The classical revenue-management literature (Gallego and van Ryzin 1994; Talluri and van Ryzin 2004) models myopic customers who buy on arrival or leave; the literature on forward-looking (strategic) buyers, for instance Aviv and Pazgal (2008), studies particular price paths.

Board and Skrzypacz ask the mechanism-design question: among all selling schemes, which maximizes the seller's expected discounted revenue when buyers arrive over time, have private values and time their purchases strategically? Their answer, published in the Journal of Political Economy in 2016, is that the optimal mechanism has a simple structure: in every period the seller sells to the highest remaining buyer if and only if his value exceeds a cutoff that depends only on the period and the number of units left. When demand is weakly decreasing over time, the cutoffs are characterized by one-period indifference conditions, which in the continuous-time limit can be implemented by posted prices. The source used here is the authors' accepted manuscript of February 6, 2015; all page numbers refer to that manuscript.

Setting

A seller has units of a good and sells them over periods $t\in\{1,\dots,T\}$ ; unsold units are worth zero after period $T$ . Payoffs are discounted by $\delta\in(0,1)$ . At the start of period $t$ a random number $N_t$ of buyers arrives, independently across periods, with a law that may depend on $t$ . Each buyer wants one unit; his value is drawn independently from a distribution with continuous density $f$ , distribution function $F$ and support $[\underline v,\bar v]$ . The marginal revenue of a buyer with value $v$ is

m(v)=v-\frac{1-F(v)}{f(v)},

assumed strictly increasing and continuously differentiable, with $m(\underline v)<0$ .

By the standard mechanism-design reduction (§2.1, eq. (2.5)), the seller's problem is to choose when to serve each buyer so as to maximize the expected discounted sum of the served buyers' marginal revenues. The state in period $t$ , after the period- $t$ entrants have arrived, is the number $k$ of units left and the values $y^1\ge y^2\ge\cdots$ of the buyers present. The value $\Pi^k_t$ and the pre-entry value $\tilde\Pi^k_{t}$ satisfy the Bellman equation (4.3):

\Pi^k_t(\mathbf y)=\max_{0\le j\le k}\Big[\sum_{i=1}^j m(y^i)+\delta\,\tilde\Pi^{k-j}_{t+1}(\mathbf y^{-j})\Big],\qquad \tilde\Pi^k_{t+1}(\mathbf y)=E_{t+1}\big[\Pi^k_{t+1}(\mathbf y\cup\mathbf v_{t+1})\big],

where $\mathbf y^{-j}$ is the set of buyers left after the $j$ highest are served and $\mathbf v_{t+1}$ the next period's entrants. Selling one unit to $y^1$ today rather than none gives the difference function

\Delta\Pi^k_t(y^1,\mathbf y^{-1})=m(y^1)+\delta\tilde\Pi^{k-1}_{t+1}(\mathbf y^{-1})-\delta\tilde\Pi^k_{t+1}(y^1,\mathbf y^{-1}),

and the cutoff $x^k_t$ is the smallest $y\in[\underline v,\bar v]$ with $\Delta\Pi^k_t(y,\varnothing)\ge 0$ . Comparing selling to $y^1$ today with waiting and selling at least one unit tomorrow (to the best of $y^1$ and the entrants) gives $D\Pi^k_t(y^1)$ (p. 17). Demand is weakly decreasing in the usual stochastic order if $P(N_{t+1}>x)\le P(N_t>x)$ for all $x$ and $t$ .

Formalization targets

Goal: Theorem 2 (p. 17)

If $N_t$ is weakly decreasing in the usual stochastic order then, for every $k\ge 1$ ,

x^k_{t+1}\le x^k_t\quad(1\le t\le T-1),\qquad D\Pi^k_t(x^k_t)=0,

and $x^k_t$ is the unique root of $D\Pi^k_t$ in $[\underline v,\bar v]$ for $t\le T-1$ : the seller is indifferent between selling to the cutoff type today and waiting one period to sell that unit tomorrow (the one-period-look-ahead property).

Central milestone: Theorem 1 (p. 15)

For every $t$ and $k\ge 1$ , the optimal rule sells to the highest buyer iff $y^1\ge x^k_t$ , whatever the values of the lower buyers; $x^{k+1}_t\le x^k_t$ ; and $x^k_t$ is the unique root of $\Delta\Pi^k_t$ .

Milestones

In attack order:

Lemma 1: allocations are monotone in values.
Lemma 2: with cutoffs decreasing in the unit index, units can be treated one at a time.
Equation (A.1): increasing differences of $\Pi$ .
Lemma 3: $\Delta\Pi$ is independent of lower buyers, continuous and strictly increasing in $y^1$ , and increasing in $k$ .
Footnote 12: the boundary values of $\Delta\Pi$ .
Theorem 1.
Strict monotonicity of $D\Pi$ in $y^1$ (p. 18).
Lemma 4: $D\Pi^k_{t+1}\ge D\Pi^k_t$ .

After the goal, (4.7) gives the period- $(T-1)$ cutoff equation $m(x^k_{T-1})=\delta E_T[\max\{m(x^k_{T-1}),m(v^k_T)\}]$ .

Significance

Theorem 1 says that the optimal allocation does not depend on how many buyers are present or what their values are, only on time and inventory. This is what makes the optimal mechanism implementable without eliciting values from buyers as they arrive. Theorem 2 turns the global dynamic program into local indifference conditions. In the continuous-time limit (§5 of the paper) these become differential equations, and the optimum is implemented by posted prices with an auction at the end of the season. Under weakly decreasing demand, therefore, the classical revenue-management practice of posting prices loses nothing against the best possible mechanism.

The paper's results are proved, in prose, with envelope-theorem and coupling arguments. They have not been machine-checked. A formal development would produce a verified backward-induction model of multi-unit dynamic allocation with random arrivals, with the structural results (monotonicity, deterministic cutoffs, monotone comparative statics in inventory and time) that recur across dynamic pricing and optimal stopping. Two printed gaps are recorded below: the positivity of $m(\bar v)$ , and the restriction of footnote 12 to $t\le T-1$ .

Difficulty

The obvious argument fails at "deterministic". A priori the cutoff for the highest buyer depends on the values of the lower buyers, because selling a unit today changes which of them will be served later and when. Lemma 3(a) holds only under the induction hypothesis that all future cutoffs are already deterministic and decreasing in inventory, so Lemma 3, Theorem 1 and (A.1) form a single backward induction over periods and units, and none of them can be proved in isolation. The value function is an expectation, over a random number of i.i.d. entrants, of a maximum over sorted values, so continuity and strict monotonicity in $y^1$ (Lemma 3(b), and the same for $D\Pi$ ) are not available from general facts. The tempting argument for Theorem 2, that cutoffs fall over time simply because fewer buyers arrive later, is incomplete: Lemma 4 has to compare two periods with different arrival laws and different future cutoffs at once.

Formalization scope

Periods are natural numbers $1,\dots,T$ with $T\ge1$ , and units are natural numbers. Values, marginal revenues and profits are real numbers. The buyers present form a finite multiset of reals, and an absent buyer is absent, never a value $0$ . The value law is the measure with density $f$ ; the density is positive and continuous on $[\underline v,\bar v]$ and zero outside, and $m$ is defined from $f$ and $F$ . Expectations over a cohort are lower Lebesgue integrals against $\sum_n P(N_t=n)\,\mu^{\otimes n}$ of nonnegative bounded quantities, so no non-measurable or non-integrable integrand can silently become $0$ . The value function is defined by the Bellman equation (4.3), with $\Pi_{T+1}\equiv0$ . The sequence problem (4.1) over purchase times is not formalized; the paper says either may be used (footnote 16).

Standing assumptions and handled gaps:

$\delta\in(0,1)$ ;
$N_t$ independent across periods (only the marginal laws enter);
$m$ strictly increasing and $C^1$ on $[\underline v,\bar v]$ with $m(\underline v)<0$ ;
added: $m(\bar v)>0$ , which footnote 12 uses without stating; without it no unit is ever sold and no cutoff exists;
added: $f>0$ on the closed support, needed for $m$ to be defined there;
footnote 12's equality $\Delta\Pi^k_t(\bar v)=(1-\delta)m(\bar v)$ is stated for $t\le T-1$ only, since $\Delta\Pi^k_T=m$ ;
$D\Pi^k_t$ is used only for $t\le T-1$ , and Lemma 4 needs $t+1\le T-1$ ;
"decreasing" and "increasing" are weak except in Lemma 3(b) and for $D\Pi$ ;
at $y^1=x^k_t$ both selling and waiting are optimal.

The cutoff is defined from $\Delta\Pi$ , never as the threshold of an optimal policy, and "optimal" always means maximal in (4.3) over every number of units sold. A formalization that postulates a threshold policy, replaces the random cohort by its mean, or sets absent buyers to value $0$ would trivialize or change the statements and is ruled out. The mechanism-design reduction (IC/IR to (2.5)) and the continuous-time results of §5 are out of scope.

The usual stochastic order is the published platform definition StochasticOrders.Usual.UsualOrder. A complete development needs finite-horizon dynamic programming over multisets, expectations of functions of sorted i.i.d. samples, envelope arguments, and monotone coupling for the usual stochastic order on $\mathbb N$ ; these parts are reusable beyond this mission. Proofs of any milestone are welcome, as is a proof that (4.3) agrees with the sequence problem (4.1).

Selected references

S. Board and A. Skrzypacz, Revenue Management with Forward-Looking Buyers, Journal of Political Economy 124(4), 2016. https://doi.org/10.1086/686713
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3), 2008. https://doi.org/10.1287/msom.1070.0183
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

14 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems 1: For Symmetric Right-Hand-Side Uncertainty, the Robust Optimum Is at Most Twice the Stochastic OptimumResearch Paper

Motivation

Many planning problems are made in two stages: a first decision $x$ (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision $y$ (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy $\omega\mapsto y(\omega)$ , and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair $(x,y)$ that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).

The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.

Setting

Fix $A\in\mathbb R^{m\times n_1}$ , $B\in\mathbb R^{m\times n_2}$ and nonnegative costs $c\in\mathbb R^{n_1}_+$ , $d\in\mathbb R^{n_2}_+$ . A set $\Omega$ of scenarios carries a probability measure $\mu$ , and each scenario $\omega$ has a right-hand side $b(\omega)\in\mathbb R^m_+$ . The uncertainty set is $\mathcal I_b(\Omega)=\{b(\omega):\omega\in\Omega\}$ . First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ( $p_2=0$ ).

The stochastic problem $\Pi_{\mathrm{Stoch}}(b)$ , (1.1), chooses $x$ and a policy $y(\cdot)$ :

z_{\mathrm{Stoch}}(b)=\inf\ c^Tx+\mathbb E_\mu[d^Ty(\omega)]\quad\text{s.t.}\quad Ax+By(\omega)\ge b(\omega)\ \ \forall\omega\in\Omega .

The robust problem $\Pi_{\mathrm{Rob}}(b)$ , (1.2), chooses one $y$ for all scenarios:

z_{\mathrm{Rob}}(b)=\inf\ c^Tx+d^Ty\quad\text{s.t.}\quad Ax+By\ge b(\omega)\ \ \forall\omega\in\Omega .

A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for all $z$ ; $u^0$ is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection $\{2u^0-x\}$ the same mass.

Formalization targets

Goal: Theorem 2.1 (p. 10)

If $\mathcal I_b(\Omega)$ is symmetric with point of symmetry $b(\omega^0)$ , $p_2=0$ , and $\mu$ satisfies

\mathbb E_\mu[b(\omega)]\ \ge\ b(\omega^0)\qquad(2.1)

then

z_{\mathrm{Rob}}(b)\ \le\ 2\cdot z_{\mathrm{Stoch}}(b).

Milestones on the way

Lemma 2.2 (p. 12): the coordinatewise bounding box $H$ of a symmetric set $S$ is the smallest hypercube containing $S$ .
Lemma 2.3 (p. 12): the centre $x^0$ of $H$ is the point of symmetry of $S$ , and $x\le 2x^0$ on $S$ when $S\subseteq\mathbb R^n_+$ .
Eqs. (2.9)–(2.10) (p. 13): if $(x,y)$ covers $b(\omega^0)$ then $(2x,2y)$ covers every $b(\omega)$ , so it is robust feasible.
p. 14 display: under (2.1), the mean second-stage decision $\mathbb E_\mu[y(\omega)]$ covers $b(\omega^0)$ .
Lemma 2.1 (p. 11): a symmetric probability measure has mean $u^0$ , so it satisfies (2.1).
Theorem 2.7 (p. 21): the same bound $z_{\mathrm{Rob}}(b)\le 2\,z_{\mathrm{Stoch}}(b)$ when $\mathcal I_b(\Omega)$ is convex and positive (contained in a symmetric subset of $\mathbb R^m_+$ whose centre lies in $\mathcal I_b(\Omega)$ ).

Significance

The result. The robust problem is one mixed-integer program, independent of $\mu$ ; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution $(x,y)$ used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least $n+1$ ) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).

Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).

Difficulty

Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of $\Pi_{\mathrm{Stoch}}(b)$ ; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from " $Ax+By(\omega)\ge b(\omega)$ for all $\omega$ " to " $Ax+B\,\mathbb E_\mu[y]\ge\mathbb E_\mu[b]$ " needs integrability of the policy and of $b$ and linearity of the Bochner integral through a matrix. The bound $b(\omega)\le 2b(\omega^0)$ uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since $\mathbb E_\mu[y(\omega)]$ need not be integral.

Formalization scope

Vectors are Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set $I$ of coordinates", which is the paper's $\mathbb R^{n-p}_+\times\mathbb Z^p_+$ up to relabelling.
$\Omega$ is an arbitrary measurable space with a probability measure; $\mathcal I_b(\Omega)$ is Set.range b. Constraints hold for every scenario, not almost surely.
Second-stage policies are $\mu$ -integrable, and $b$ is $\mu$ -integrable in every statement that uses (2.1). Without these, Lean's integral of a non-integrable function is $0$ and (2.1) would degenerate.
$z_{\mathrm{Stoch}}$ and $z_{\mathrm{Rob}}$ are infima in EReal, equal to $+\infty$ when infeasible; no attainment is assumed. A real-valued infimum would return $0$ on an infeasible robust problem and make the goal trivial; that formalization is ruled out.
The bounding box of (2.5)–(2.7) uses suprema and infima, with boundedness assumed where needed.
Corrections to the page: Lemma 2.3's inequality $x\le 2x^0$ is stated under $S\subseteq\mathbb R^n_+$ , which its proof uses and which holds in every application; Lemma 2.1 assumes the measure has a mean; Theorem 2.7 carries the standing assumption $p_2=0$ of §2.

Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.

Selected references

D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace)
A. Ben-Tal, A. Nemirovski, Robust optimization — methodology and applications, Mathematical Programming 92, 2002. https://doi.org/10.1007/s101070100286
D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106, 2006. https://doi.org/10.1007/s10107-005-0578-0
D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134, 2012. https://doi.org/10.1007/s10107-011-0444-4

10 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Airline Seat Allocation with Multiple Nested Fare Classes 1: Protection Levels Solving f₁Pr[X₁ > p₁ ∩ … ∩ X₁ + … + X_k > p_k] = f_{k+1} Maximize Expected RevenueResearch Paper

Motivation

An airline sells the seats of one flight leg at several fares. Cheaper fares are booked earlier, so the airline must decide, while low-fare requests arrive, how many seats to hold back for later and more valuable passengers. In nested booking control a seat that could be sold at a low fare is always available to a higher fare. The airline therefore chooses protection levels: $p_k$ seats are reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain.

For two classes the optimal protection level was found by Littlewood (1972): protect $p_1$ seats, where $f_1 \Pr[X_1 > p_1] = f_2$ . For more classes the industry used the EMSRa heuristic of Belobaba (1987, 1989), which applies Littlewood's rule to each pair of classes separately and adds the results. Brumelle and McGill (1993) gave the exact optimality conditions for any number of nested classes and showed that EMSRa is in general not optimal. Their conditions are part of the standard theory of single-leg revenue management, as presented in Talluri and van Ryzin (2004).

Setting

There are fare classes $k = 1, 2, \dots$ , numbered from the highest fare. Class $k$ has fare $f_k$ and random demand $X_k \ge 0$ . The standing assumptions (pp. 128–129) are: the demands are mutually independent random variables on a probability space $(\Omega, \mathcal F, P)$ , and the fares are strictly decreasing, $f_1 > f_2 > \cdots$ . Demands arrive in order of increasing fare: all of class $k+1$ before any of class $k$ . There are no cancellations or no-shows, and the decision to close a class depends only on the number of current bookings.

A protection-level policy is a vector $p = (p_1, p_2, \dots)$ with $p_k \ge 0$ ; the dummy $p_0 = 0$ . The revenue $R_k[s; p; x]$ of the $k$ highest classes with $s$ seats available and demand vector $x$ is defined recursively by (8)–(9), p. 130:

R_1[s; p; x] = f_1 \min(s, x_1),

R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k, \\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1}, \\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s. \end{cases}

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$ . A policy $p$ is optimal if $ER_k[s; q; X] \le ER_k[s; p; X]$ for every policy $q$ , every $k \ge 1$ and every $s \ge 0$ .

For $g : \mathbb R \to \mathbb R$ , $\delta_+ g[s]$ and $\delta_- g[s]$ denote the right and left derivatives, and the subdifferential $\delta g[s]$ is the interval $[\delta_+ g[s], \delta_- g[s]]$ , with $\delta_- g[0] = +\infty$ (p. 131).

Formalization targets

Goal: Theorem 3 (p. 134)

If the protection levels satisfy

f_1 \Pr[X_1 > p_1 \cap X_1 + X_2 > p_2 \cap \dots \cap X_1 + \dots + X_k > p_k] = f_{k+1} \quad \text{for all } k \ge 1, \tag{31}

then $p$ is optimal.

Milestones

(27), p. 132: $ER_1$ is concave, and $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$ .
Lemma 1, p. 131: if $ER_k[\,\cdot\,; p; X]$ is concave on $s \ge 0$ and $f_{k+1} \in \delta ER_k[p_k; p; X]$ , then $E\{R_{k+1}[s; p; X] \mid X_{k+1}\}$ is concave in $s$ .
Corollary 1, p. 131: under the same conditions $ER_{k+1}[\,\cdot\,; p; X]$ is concave on $s \ge 0$ .
Theorem 1, p. 131: if $f_{k+1} \in \delta ER_k[p_k; p; X]$ for every $k$ (condition (20)), then $p$ is optimal.
Lemma 2, p. 134: under (31), for $s \ge p_k$ ,

\delta_+ E\{R_{k+1}[s; p; X] \mid X_{k+1}\} = f_1 \Pr[X_1 > p_1 \cap \dots \cap X_1 + \dots + X_k > p_k \cap X_1 + \dots + X_{k+1} > s \mid X_{k+1}].

Corollary 2, p. 134: the unconditional version (37) of Lemma 2 for $\delta_+ ER_{k+1}[s; p; X]$ .

Significance

Theorem 3 turns the optimal nested protection levels into a sequence of equations in the joint distribution of the cumulative demands $X_1 + \dots + X_j$ . For $k = 1$ it is Littlewood's rule. For $k \ge 2$ it identifies exactly what EMSRa approximates: EMSRa replaces the joint event in (31) by separate pairwise comparisons, and the paper shows (§4) that EMSRa can both over- and underestimate the optimal protection levels. The conditions are also the input of numerical methods: given demand forecasts, the levels $p_1, p_2, \dots$ are found one after another by solving (31), and §3.3 notes that a continuous joint demand distribution guarantees a solution exists.

The results are proved in the paper. As far as is known they have no machine-checked proof. Related platform items cover the two-class, integer-seat case from Belobaba (1987) (SeatInventory.Nested.emsr_protection_level_optimal) and the integer marginal-seat-revenue analogue of (27). They use a different model: two classes, natural-number seats and first differences. This mission formalizes the multi-class statement with real-valued seats and one-sided derivatives. A sister mission of the series proves the existence of optimal integer policies for integer-valued demand (Theorem 2).

Difficulty

The expected revenue is not differentiable: for discrete demand it is piecewise linear, so first-order conditions must be stated with one-sided derivatives and subdifferentials. The natural approach, to optimize each protection level separately with the others fixed, fails without concavity, and concavity of $ER_{k+1}$ in $s$ is not automatic. It holds only when the lower protection levels already satisfy the first-order conditions. Concavity and optimality must therefore be carried through one joint induction over the classes. Passing from (31) to (20) requires computing the right derivative of the expected revenue in closed form for every $s \ge p_k$ . This involves exchanging differentiation with expectation and conditioning on one class's demand at a time.

Formalization scope

Classes are indexed by $\mathbb N$ from $1$ ; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$ , with no bound on the number of classes. Seats and protection levels are real numbers.
Expectation is the Bochner integral on a probability space. The standing assumptions are a single predicate: probability measure, measurable nonnegative demands, mutual independence (iIndepFun), strictly decreasing fares.
$E\{\cdot \mid X_k\}$ evaluated at $X_k = y$ is the integral with the $k$ -th demand frozen at $y$ . Because the demands are independent this is a version of the conditional expectation, and "with probability 1" becomes "for every $y \ge 0$ ", which is stronger.
One-sided derivatives are HasDerivWithinAt on half-lines and must exist; derivWithin, which returns $0$ where no derivative exists, is not used. $\delta_- g[0] = +\infty$ is encoded as a disjunct.
Optimality is global: $p$ beats every policy $q$ at every level $k$ and every $s \ge 0$ . The page's proof of Theorem 1 shows coordinatewise optimality of $p_k$ , and the global form follows by induction on $k$ .
Fares are not assumed positive in the model: under (20) or (31) with strictly decreasing fares, $f_1 > 0$ follows. The milestone (27), stated with only the hypotheses on $X_1$ that it needs, assumes $X_1 \ge 0$ and $f_1 \ge 0$ , without which $ER_1$ is not concave.
No continuity of the demand distribution is assumed. Theorem 3 is conditional on a solution of (31).
The page's hypothesis of Lemma 1 has the misprint " $(p_0, \dots, p_{k+1})$ " for $(p_0, \dots, p_{k-1})$ . The formal statement uses the latter.

The goal assumes only the standing assumptions, $p \ge 0$ , and (31). It does not assume concavity, condition (20) or any derivative formula: those are milestones. A formalization that quantified optimality over one level, one value of $s$ , or policies differing from $p$ in one coordinate would be weaker than the paper and is excluded.

A complete development needs one-sided derivatives of integrals of piecewise-linear functions (dominated convergence for difference quotients), concavity of piecewise functions glued at points where the slopes decrease, and the independence calculus that turns $E[E\{\cdot \mid X_{k+1}\}]$ into an iterated integral. These pieces are reusable for other newsvendor-type and revenue-management models. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1), 127–137, 1993. https://doi.org/10.1287/opre.41.1.127
K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12, 95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

8 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms III: With One Unknown Parameter, Staged Re-estimation Has Regret O((log log n)(log n)^{1/2}/n^{1/2})Research Paper

Motivation

A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.

Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret $O\big((\log\log n)(\log n)^{1/2}/n^{1/2}\big)$ . The paper's lower bound for parametric families (Proposition 4) is of order $n^{-1/2}$ , so the rate is optimal up to logarithmic factors.

Setting

Market. Prices lie in $[\underline p,\overline p]\cup\{p_\infty\}$ with $0<\underline p<\overline p<p_\infty$ . Posting the off price $p_\infty$ stops demand. The seller starts with inventory $x>0$ and sells over the horizon $[0,T]$ , $T>0$ .

Demand. A demand function $\lambda$ maps a price to a demand rate. The class $\mathcal L(M,\underline K,\overline K,m)$ consists of the functions that are non-increasing with an inverse $\gamma$ on $[\underline p,\overline p]$ , have a concave revenue rate $r(l)=l\gamma(l)$ , are bounded by $M$ , are $\overline K$ -Lipschitz with a $\underline K^{-1}$ -Lipschitz inverse, and attain a revenue rate $\max_p p\lambda(p)\ge m$ . The parametric family is $\lambda(p;\theta)$ , $\theta\in\Theta=[\theta_{\mathrm{lo}},\theta_{\mathrm{hi}}]$ , with every member in the class (Assumption 1). Assumption 2 adds a test price $p_1$ , differentiability of $\sqrt{\lambda(p_1;\cdot)}$ and the Lipschitz bound $|\lambda(p;\theta)-\lambda(p;\theta')|\le\overline K_2|\theta-\theta'|$ . Assumption 3 requires $\inf_{p,\theta}\lambda(p;\theta)>l_0>0$ and an $\alpha$ -Lipschitz solution map $d\mapsto g(p,d)$ of the equation $\lambda(p;\cdot)=d$ .

Demand process. Let $N$ be a unit-rate Poisson process. Under a price path $p(\cdot)$ and parameter $\theta^*$ , the cumulative demand up to time $t$ is $N\big(\int_0^t\lambda(p(s);\theta^*)\,ds\big)$ . Sales stop when the inventory runs out.

Benchmark and regret. The deterministic relaxation $J^D(x,T\mid\theta)$ is the supremum of $\int_0^T p(s)\lambda(p(s);\theta)\,ds$ over price paths with $\int_0^T\lambda(p(s);\theta)\,ds\le x$ . In the market of size $n$ the inventory is $nx$ and the demand $n\lambda$ . If $J^\pi_n(x,T;\theta)$ is the expected revenue of a policy $\pi$ , its regret is $\mathcal R^\pi_n=1-J^\pi_n/J^D_n$ .

Algorithm 3. Start from $\hat p_1=p_1$ and use stages of lengths $\Delta^{(1)}_n,\dots,\Delta^{(\ell_n)}_n$ summing to $T$ . Stage $i$ applies $\hat p_i$ , estimates the demand rate $\hat d_i$ from the stage's demand, solves for $\hat\theta_i=g(\hat p_i,\hat d_i)$ , and sets $\hat p_{i+1}=\max\{p^u(\hat\theta_i),p^c(\hat\theta_i)\}$ . Here $p^u(\theta)$ maximizes $p\lambda(p;\theta)$ and $p^c(\theta)$ minimizes $|\lambda(p;\theta)-x/T|$ . The tuning (19)–(20) is $\ell_n=(\log2)^{-1}\log\log n$ stages with $\Delta^{(m)}_n=\beta_n n^{(a_{\ell_n}/a_m)-1}$ and $a_m=2^{m-1}/(2^m-1)$ .

Formalization targets

Goal: Proposition 5

\exists\,C>0,\ \exists\,n_0,\quad \forall n\ge n_0,\ \forall\theta\in\Theta:\qquad \mathcal R^{\pi_n}_n(x,T;\theta)\le C\,\frac{(\log\log n)(\log n)^{1/2}}{n^{1/2}} .

The constants are uniform in $\theta$ and $n$ . This is the paper's (21): $\sup_\theta\mathcal R^{\pi}_n=O(\cdot)$ .

Milestones, in proof order

Fact 1: $J^D_n=nJ^D$ and $J^D\ge m\min\{T,x/M\}$ on the class.
Lemma 1: the deterministic relaxation is solved by the fixed price $p^D=\max\{p^u,p^c\}$ .
Lemma 2: Poisson deviation bounds at scale $(\log n/r_n)^{1/2}$ .
(A-27): a revenue lower bound that splits the loss into stage-wise terms and an overflow term.
The per-stage revenue gap $r(p^D)-\mathbb E\,r(\hat p_i)\le C_2(n\Delta^{(i-1)}_n)^{-1/2}$ .
(A-30): the stage- $i$ demand rate rarely exceeds the run-out rate.
The overflow bound $\mathbb E[(Y_n-nx)^+]\le nC_8(\log n)^{1/2}n^{a_{\ell_n}-1}$ .
(A-31): the revenue ratio before the exponents are evaluated.
The rate estimate $n^{a_{\ell_n}-1}\le e\,n^{-1/2}$ .

Milestones 6–8 hold in the case $\lambda(\overline p;\theta^*)\le x/T$ , the only case the paper's proof treats in detail.

Significance

Proposition 5 shows that with one unknown parameter, learning while earning reaches the $n^{-1/2}$ rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only $n^{-1/4}$ and $n^{-1/3}$ . The paper leaves open whether the multi-parameter case attains the lower bound.

The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.

The result is proved in the paper, but parts of the proof are only sketched. The case $\lambda(\overline p;\theta^*)>x/T$ is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.

Difficulty

The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries $\Lambda_i=\sum_{j\le i}n\lambda(\hat p_j;\theta^*)\Delta^{(j)}_n$ depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses $\Delta^{(i)}_n/(n\Delta^{(i-1)}_n)^{1/2}$ are all of the same order. That balance has to be checked exactly, including the rounding of $\ell_n$ to an integer.

Formalization scope

Poisson process. A structure on an arbitrary probability space: $N(0)=0$ , monotone right-continuous paths, measurable marginals, Poisson increments, and independent increments over finite partitions. No process is published on the platform.
Class and family. Conditions on $\lambda$ are imposed on $[\underline p,\overline p]\cup\{p_\infty\}$ , the only prices a path uses. The inverse $\gamma$ is Function.invFunOn. $\Theta$ is a nonempty closed interval of $\mathbb R$ .
Assumption 3. As printed it cannot hold for $d>\sup_\theta\lambda(p;\theta)$ . It is read as an $\alpha$ -Lipschitz map $g(p,\cdot):[0,\infty)\to\Theta$ that inverts $\lambda(p;\cdot)$ on $\Theta$ . $g$ is jointly measurable, so that estimates at random prices are random variables.
Selections. $p^u,p^c$ are any measurable selections of the maximizer and minimizer; the statements hold for each.
Inventory. The inventory is $\lfloor nx\rfloor$ units, and sales are capped cumulative counts.
Time change. Eq. (1) is applied stage by stage with random stage boundaries.
Typos. In Algorithm 3, " $\lambda(p_i,\theta)$ " is read as $\lambda(\hat p_i;\theta)$ and " $x/t$ " as $x/T$ .
Stages. $\ell_n=\lceil\log_2\log n\rceil$ .
Integrals. Expectations are lower Lebesgue integrals of nonnegative quantities, converted to reals. The relaxation is a real supremum over measurable paths.
Asymptotics. The $O(\cdot)$ is rendered with an explicit $n_0$ . The clause "asymptotically optimal" is omitted, since it needs the second half of Lemma 1.
Ruled out. Each of the following would trivialize the statement: removing the inventory cap, replacing the random stage boundaries by deterministic ones, fixing $\theta$ , letting $C$ depend on $\theta$ , or using a non-measurable selection (whose expectation would be a junk value).

Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.

Selected references

O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

15 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms II: The Parametric Learn-then-Price Policy Has Regret at Most C(log n)^{1/2}/n^{1/3}Research Paper

Why learn demand while pricing?

A seller with a fixed inventory must choose prices before knowing how customers respond to them. A price that earns a high margin can sell too slowly; a price that sells quickly can exhaust stock before the selling season ends. Learning demand uses time and inventory, so the seller must account for the cost of its own experiments. This mission formalizes the parametric policy and regret bound of Besbes and Zeevi (2009), Proposition 3. Their setting differs from a finite-arm bandit: the permitted ordinary prices form an interval, customer arrivals are random, and the available stock caps total sales.

The paper first analyzes a nonparametric class with a slower upper bound in Proposition 1, then imposes a known finite-dimensional form on the unknown demand curve in Section 5. Proposition 3 shows how that additional information improves the regret rate for its Algorithm 2. The authors also prove a lower bound for a suitable parametric family in Proposition 4; that result is outside this mission's capstone, which concerns the performance guarantee of the concrete policy.

Market, demand, and policy

The selling horizon has length $T>0$ , and the initial stock is $x>0$ . An ordinary price $p$ lies in $[\underline p,\overline p]$ , with $0<\underline p<\overline p$ . The special price $p_\infty>0$ stops demand. At parameter $\theta\in\Theta\subseteq\mathbb R^k$ , the demand rate is $\lambda(p;\theta)\ge0$ . The parameter set $\Theta$ is nonempty, compact, and convex; $k$ is positive. The seller knows the family $\lambda(\cdot;\theta)$ but does not know the true parameter $\theta^*$ .

For each parameter, demand is nonincreasing in the price and has an inverse $\gamma(\cdot;\theta)$ on the attainable rate interval. The rate revenue is $r(\ell;\theta)=\ell\gamma(\ell;\theta)$ , a concave function of the rate. Every member of the family satisfies Assumption 1 with the same positive constants $M,\underline K,\overline K,m$ : demand is at most $M$ , its price variation is at most $\overline K$ times the price difference, its inverse is $\underline K^{-1}$ -Lipschitz, and some ordinary price earns revenue rate at least $m$ . These conditions define the class in which the bound is uniform. See §§3–4.2 of the source.

Customer requests follow a unit-rate Poisson process $N$ run on a demand-dependent clock. Under price $p(t)$ , cumulative requests at time $t$ equal $N(\int_0^t\lambda(p(s);\theta^*)\,ds)$ . The market of size $n$ has stock $nx$ and rate $n\lambda$ . Sales stop when stock runs out. The deterministic relaxation $J_n^D$ is the best integrated rate revenue over measurable price paths satisfying the expected-demand stock constraint, with the same scaling. The policy revenue $J_n^\pi$ is its expected sales revenue, and its relative regret is $R_n^\pi=1-J_n^\pi/J_n^D$ . Fact 1 states $J_n^D=nJ^D$ and gives a positive uniform lower bound on $J^D$ .

Assumption 2 selects $k$ distinct ordinary test prices. Their mean rates identify the parameter through a Lipschitz inverse map $g$ , and demand changes at most $\overline K_2\|\theta-\theta'\|_\infty$ as the parameter varies. The square root of each test-price rate is differentiable on $\Theta$ . Algorithm 2 spends $\tau_n$ time units testing these prices in equal subintervals, estimates each rate from its Poisson count increment, and sets $\widehat\theta=g(\widehat d)$ . It then posts $\widehat p=\max\{p^u(\widehat\theta),p^c(\widehat\theta)\}$ , where $p^u$ maximizes revenue rate and $p^c$ minimizes the distance of demand to $x/T$ . It keeps that price until time $T$ or stock-out. See §5.1–5.2.

Formalization targets

The capstone is the uniform bound in Proposition 3, equation (17). With $\tau_n\asymp n^{-1/3}$ , the mission asks for one constant $C>0$ , independent of $n$ , $\theta^*$ , the optimizer choices, and the probability space, such that

\forall\theta^*\in\Theta,\qquad R_n^\pi(x,T;\theta^*)\le C\frac{\sqrt{\log n}}{n^{1/3}}\quad(n\ge2).

The intermediate quantitative target is equation (A-25), which retains the learning time:

R_n^\pi\le\frac{C_3}{m^D}\left(\tau_n+\frac{\sqrt{\log n}}{\sqrt{n\tau_n}}\right),\qquad m^D=m\min\{T,x/M\}.

The milestone list also carries Fact 1, the optimal deterministic price path and value from the first assertion of Lemma 1, both Poisson tails of Lemma 2, the pricing-phase revenue bound (A-17), the deterministic stability bounds (A-19), (A-22), and (A-23), and the parameter-estimation bound of Lemma 6. The paper's assertion that the policy is “asymptotically optimal” follows from the displayed regret estimate together with nonnegative regret; the displayed numerical estimate is the formal goal.

What the result provides

A finite-dimensional demand model lets the seller learn from a fixed set of $k$ prices rather than probing an increasingly fine price grid. Proposition 3 quantifies the resulting revenue loss at $O(\sqrt{\log n}\,n^{-1/3})$ , compared with the paper's $O(\sqrt{\log n}\,n^{-1/4})$ upper bound for its nonparametric learn-then-price policy. Both guarantees compare actual expected revenue with the full-information deterministic benchmark, including stock-out. These rates are proved in the article; the mission seeks machine-checked Lean proofs of the stated model, auxiliary bounds, and capstone. No such proof is claimed here.

The formalization would also provide reusable interfaces for a unit-rate Poisson counting process, deterministic inventory-constrained revenue optimization, measurable price selectors, and a random price chosen from normalized count observations. The later single-parameter policy in the paper uses related ideas but is a separate mission with different stages and a different rate.

Main difficulty

A rate estimate can be close to the true rate while the selected price changes between two different optimizers: the unconstrained revenue maximizer and the price that matches inventory to expected demand. A bound for only one optimizer does not control the maximum of the two. The learning price is random, and the number of requests in the pricing phase is evaluated at a random Poisson clock. Stock-out further couples the learning phase to the amount available for later sales. These features prevent a direct substitution of an ordinary parameter-estimation bound into the final revenue formula.

Formalization scope

Lean uses $\mathrm{Fin}(k)\to\mathbb R$ with its sup norm for parameter vectors, a finite positive off price, and a Poisson process on an arbitrary probability space. Each demand curve is defined on all real prices but is constrained on $[\underline p,\overline p]$ and at $p_\infty$ ; the inverse and concavity conditions apply on the attainable rate interval. The deterministic benchmark is a real supremum over measurable, integrable admissible price paths. The class assumptions make its value nonempty and bounded. Policy revenue uses a nonnegative integral of pathwise revenue, avoiding a default zero from a nonintegrable signed expectation.

Inventory is measured in whole units, so the cap is $\lfloor nx\rfloor$ , equal to the paper's $nx$ when that quantity is integral. Test-price observations remain uncapped in the formula for $\widehat d$ ; if stock runs out during learning, capped later sales are already zero. The continuous optimizer choices are measurable selections satisfying the actual max/min properties for every member of $\Theta$ . The bound is uniform over these choices and over all unit-rate Poisson processes.

The printed Assumption 2(i)b asks for a solution to the test-rate equations for every vector in $\mathbb R^k$ . Such a solution cannot always lie in compact $\Theta$ , although the proof applies Assumption 2(ii) to $\widehat\theta$ . Here $g$ is a Lipschitz map into $\Theta$ that recovers each true parameter from its test-rate vector; it can be viewed as the unconstrained inverse followed by a nonexpansive projection in the paper's box example. This explicit convention is required to make the estimate and subsequent use of Assumption 2(ii) coherent. It is an interpretive repair of the printed condition.

The paper prints the regret bound for $n\ge1$ , where $\sqrt{\log1}=0$ . The exploration policy can lose revenue at $n=1$ , so the formal theorem starts at $n\ge2$ . The comparison $\tau_n\asymp n^{-1/3}$ is encoded by positive lower and upper multipliers after a fixed threshold, with $0<\tau_n\le T$ for all relevant market sizes. This admits the usual finite initial adjustments and leaves the bound uniform over the sequence. No fixed demand curve, known parameter, finite price grid, or uncapped sales model can satisfy this target by substitution.

Selected references

Omar Besbes and Assaf Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009, authors' final manuscript revised December 16, 2007. DOI: 10.1287/opre.1080.0640.

13 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons 3: With a Discrete Price Set the Two-Price Stopping-Time Heuristic Is Asymptotically OptimalResearch Paper

Motivation

Airlines, hotels and cruise lines rarely change prices continuously. They sell a fixed product (seats on one flight, rooms on one night) over a finite selling season, and they sell it at a small set of fares, opening and closing fare classes as the season unfolds. Gallego and van Ryzin, in Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), model this as the sale of $n$ items over a horizon of length $t$ , with Poisson demand whose rate depends on the current price. Section 4 of the paper restricts the price to a finite menu and asks how much is lost by using a simple rule that charges only two adjacent prices and switches once. The answer, Theorem 5, gives one explanation of fixed-fare-class yield management: with two fares and one well-timed switch, a seller earns asymptotically the best revenue any policy over the menu can earn. The source of this mission is the published 1994 article.

The paper is the starting point of a long line of work on fluid (deterministic) approximations in revenue management, including Feng and Gallego (1995) on optimal switching times between two prices and later re-solving and bid-price analyses, all of which compare stochastic policies to the value of a deterministic problem in the same way.

Setting

A menu consists of $K\ge2$ prices $p_1<p_2<\dots<p_K$ and Poisson demand rates $\lambda_1>\lambda_2>\dots>\lambda_K>0$ ; the firm may also charge the null price $p_\infty$ , at which demand is $0$ . The revenue rates $r_k=p_k\lambda_k$ satisfy $r_1>r_2>\dots>r_K$ , and the points $(\lambda_k,r_k)$ lie on a concave function on $[0,\infty)$ vanishing at $0$ .

The deterministic problem replaces random demand by its rate. If $t_k\ge0$ is the time spent at price $p_k$ , the problem is the linear program

J^D(n,t)=\sup\Big\{\sum_k r_k t_k:\ \sum_k t_k\le t,\ \sum_k\lambda_k t_k\le n,\ t_k\ge0\Big\}.

Given $n\in\mathbb N$ and $t>0$ , let $k=k^*$ be the index with $\lambda_k t\ge n>\lambda_{k+1}t$ , and put

t_k=\frac{n-\lambda_{k+1}t}{\lambda_k-\lambda_{k+1}},\qquad m=\lceil\lambda_k t_k\rceil,\qquad t_m=\frac{m}{\lambda_k}.

The stopping-time (ST) heuristic starts at price $p_k$ and switches to $p_{k+1}$ at the random time $\tau=\min(T_m,t_m)$ , where $T_m$ is the time of the $m$ -th demand. Sales stop when the $n$ items are gone or at time $t$ . $J^{ST}(n,t)$ is its expected revenue.

Formalization targets

Goal: Theorem 5

For a fixed index $k$ with $1\le k\le K-1$ and any sequences $n_j\in\mathbb N$ , $t_j\to\infty$ with $\lambda_k t_j\ge n_j>\lambda_{k+1}t_j$ ,

\lim_{j\to\infty}\frac{J^{ST}(n_j,t_j)}{J^D(n_j,t_j)}=1.

No rate of convergence is fixed in the goal, and the ratio $n_j/t_j$ may vary along the sequence.

Milestones

Proposition 4. The LP is solved by pricing at $p_{k^*}$ for time $t_{k^*}$ and at $p_{k^*+1}$ for time $t_{k^*+1}=(\lambda_{k^*}t-n)/(\lambda_{k^*}-\lambda_{k^*+1})$ , together with the edge cases $k^*=0$ and $k^*=K$ .
The wasteful heuristic is a lower bound: $J^W(n,t)\le J^{ST}(n,t)$ , where the wasteful heuristic offers $m$ units at $p_k$ during $[0,t_m]$ and $n-m$ units at $p_{k+1}$ afterwards.
Equation (28): the shrunk horizon $t'=t_m+(n-m)/\lambda_{k+1}$ satisfies $t-(\lambda_k-\lambda_{k+1})/(\lambda_k\lambda_{k+1})<t'\le t$ .
The closed form of $J^D$ and $J^D(n,t)<J^D(n,t')+(p_{k+1}-p_k)$ .
Equation (29): $J^{ST}(n,t)/J^D(n,t)\ge J^W(n,t)/J^D(n,t)\ge J^W(n,t')/(J^D(n,t')+(p_{k+1}-p_k))$ .
The wasteful bound: $J^W(n,t')\ge p_k[m-\tfrac12\sqrt m]+p_{k+1}[(n-m)-\tfrac12\sqrt{n-m}]$ and $J^W(n,t')/J^D(n,t')\ge1-\tfrac12(1/\sqrt m+1/\sqrt{n-m})$ .

Significance

Theorem 5 says that a policy with one price change, chosen from the deterministic solution, loses a vanishing fraction of the deterministic revenue. Since $J^D$ bounds the optimal expected revenue over all non-anticipating policies with prices in the menu (§4.0.1 of the paper), the ST heuristic is asymptotically optimal, and the optimal policy, which solves a Hamilton–Jacobi–Bellman system with no closed form, can be replaced by a rule that is computed by hand. The result also shows that a finite menu, together with dynamic allocation of capacity between two neighbouring prices, can realize the effective price of a continuous demand curve.

The theorem is proved in the paper. As far as the platform's index shows, neither this result nor the controlled Poisson sales process it needs has been formalized; Mathlib has the exponential and Poisson distributions but no counting process with a policy-dependent intensity. The mission produces a machine-checked version of the paper's proof chain: the LP solution, the coupling inequality between two heuristics, the deterministic horizon estimate (28), and the Poisson overflow estimate built on Gallego's bound (inequality (18) of the paper, already proved on the platform as PricingRM.DetHeuristic.gallego_bound).

Difficulty

The deterministic parts (Proposition 4, (28), the closed form of $J^D$ ) are finite-dimensional linear algebra. The difficulty sits in the stochastic comparison $J^W\le J^{ST}$ . The ST heuristic's switching time depends on the sales process, and after the switch the remaining stock and the remaining time are both random. The obvious attempt, writing $J^{ST}$ as a sum of two independent Poisson terms, is wrong: the two phases are dependent through $\tau$ . Any comparison has to handle a second phase whose starting stock and starting time are both random, which brings in the behaviour of the sales process after a random time determined by the process itself. The limit step then needs the overflow bound uniformly along sequences whose ratio $n/t$ is not fixed.

Formalization scope

All declarations live in the namespace GVRPricing.StoppingTime. The committed conventions are:

Indices are 0-based (Fin K): Lean index $k$ is the paper's price number $k+1$ , and lamN, pN, rN extend the sequences by $0$ beyond $K$ , matching the paper's $\lambda_{K+1}=r_{K+1}=0$ .
The menu carries the printed conditions plus an added concavity condition: the points $(\lambda_k,r_k)$ lie on a concave function vanishing at $0$ . This is the reading of §4's "corresponding to price $p_k$ , we have a known demand rate $\lambda_k$ " for a regular demand function with concave revenue rate. Without it Proposition 4 and Theorem 5 are false: the menu $\lambda=(3,2,1)$ , $p=(1,1.01,1.5)$ meets every printed condition, but at $t=1$ , $n=1.5$ Proposition 4's allocation earns $1.76$ while a feasible mix of $p_1$ and $p_3$ earns $1.875$ , and the ST ratio tends to about $0.939$ .
$J^D$ is defined directly as the LP value; the reduction from the rate-path problem (11) is the paper's assertion and is not formalized.
The sales process is built from $n$ i.i.d. standard exponential clocks by the time change of the ST policy's cumulative intensity, so at most $n$ items are sold. Time is elapsed time from $0$ . $J^{ST}$ is the expectation of the sum of prices charged at sales in $[0,t]$ , a lower Lebesgue integral of a bounded nonnegative function.
$J^W$ is the paper's two-Poisson formula of p. 1018.
$J^*$ is not defined, so the left ratio of (29) uses $J^D$ in place of $J^*$ (a stronger inequality, since $J^*\le J^D$ ), and the §4.0.1 upper bound $J^*\le J^D$ is not a milestone.
Corrected slips: the page prints $t_{n-m}\doteq n-m/\lambda_{k+1}$ for $(n-m)/\lambda_{k+1}$ ; the wasteful bound is stated at the shrunk horizon $t'$ , where its integrality assumptions hold exactly, instead of along the paper's subsequence; the ratio bound assumes $m<n$ , since $1/\sqrt{n-m}$ is undefined otherwise. Proposition 4 is stated as optimality, without the uniqueness that fails when three menu points are collinear.
Excluded: the edge cases $k^*=0$ and $k^*=K$ of Theorem 5, treated on the page only in an unproved remark.

A trivializing formalization would define $J^{ST}$ through the wasteful formula, or by a closed-form expression, which makes the goal the wasteful bound; here $J^{ST}$ is the expected revenue of the switching rule $\tau=\min(T_m,t_m)$ on the sales process. Likewise the limit is taken along sequences with $t_j\to\infty$ , not at a single $(n,t)$ .

Useful infrastructure, reusable beyond this mission: the exponential-clock construction of a Poisson process with piecewise-constant intensity, the strong Markov property at a stopping time of the clocks, and the expected Poisson overflow $\mathbb E(N_\mu-\mu)^+$ . Contributions to any milestone, and alternative proofs of $J^W\le J^{ST}$ , are welcome.

Selected references

G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. doi:10.1287/mnsc.40.8.999
G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11, 55–60, 1992 (the source of inequality (18)).
Y. Feng, G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995.
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the source).

11 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Constructing Uncertainty Sets for Robust Linear Optimization 1: A Distortion Risk Constraint Equals a Robust Constraint over a Permutohull and an Explicit Linear SystemResearch Paper

Motivation

Robust linear optimization replaces an uncertain constraint $\tilde a'x \ge b$ by the requirement that $a'x \ge b$ hold for every $a$ in an uncertainty set $\mathcal U$ (Ben-Tal and Nemirovski 1999). The method leaves open where $\mathcal U$ should come from. Risk theory answers a related question from the other side: a decision maker's attitude to an uncertain reward is described by a risk measure $\mu$ , and the constraint is imposed as $\mu(\tilde a'x - b) \le 0$ .

Bertsimas and Brown (2009) connect the two. When $\mu$ is coherent and $\tilde a$ is supported on finitely many observed data points $a_1, \dots, a_N$ , the risk constraint is exactly a robust constraint whose uncertainty set is built from the data and the family of probability vectors generating $\mu$ . For the class of distortion risk measures, the uncertainty set has an explicit polyhedral form, the $q$ -permutohull of the data, and the robust constraint has a reformulation of polynomial size. This mission formalizes that chain of results, Sections 2–4.3 of the paper.

Setting

The sample space is finite, $\Omega = \{\omega_1, \dots, \omega_N\}$ , and a random variable is a vector $X \in \mathbb R^N$ , read as a reward; $X \ge Y$ means $X_i \ge Y_i$ for every $i$ . The probability simplex is $\Delta^N = \{p \in \mathbb R^N_+ : e'p = 1\}$ , and $\mathbb E_q[X] = \sum_i q_i X_i$ .

A risk measure is a function $\mu : \mathbb R^N \to \mathbb R$ with $X \ge Y \Rightarrow \mu(X) \le \mu(Y)$ and $\mu(X + c) = \mu(X) - c$ . It is coherent if it is moreover convex and positively homogeneous. A set $\mathcal Q \subseteq \Delta^N$ generates $\mu$ if $\mu(X) = \sup_{q \in \mathcal Q} \mathbb E_q[-X]$ for all $X$ . The conditional value-at-risk under a probability vector $p$ is $\mathrm{CVaR}_\alpha(X) = \inf_{\nu \in \mathbb R}\{\nu + \frac1\alpha \mathbb E_p[(-\nu - X)^+]\}$ for $\alpha \in (0,1]$ .

Two random variables are comonotone if $(X(\omega) - X(\omega'))(Y(\omega) - Y(\omega')) \ge 0$ for all $\omega, \omega'$ ; $\mu$ is comonotonic if it is additive on comonotone pairs, and law invariant if it takes equal values on random variables with the same distribution. A distortion risk measure is a coherent, comonotonic, law-invariant risk measure. From Section 4.2 on, $\Omega$ carries the uniform distribution $\mathbb P\{\omega_i\} = 1/N$ .

The restricted simplex is $\hat\Delta^N = \{q \in \Delta^N : q_1 \ge \cdots \ge q_N\}$ . For $q \in \hat\Delta^N$ put

\mu_q(X) = -\sum_{i=1}^N q_i x_{(i)},

where $x_{(1)} \le \cdots \le x_{(N)}$ are the increasing order statistics of $X$ . The data are $\mathcal A = \{a_1, \dots, a_N\} \subseteq \mathbb R^n$ , the uncertain vector $\tilde a$ takes the value $a_i$ at $\omega_i$ , and the $q$ -permutohull of $\mathcal A$ is

\Pi_q(\mathcal A) = \operatorname{conv}\Big\{\sum_{i=1}^N q_{\sigma(i)} a_i : \sigma \in S_N\Big\}.

Formalization targets

Goal: Theorem 4.3

Under the uniform distribution, for every distortion risk measure $\mu$ there is $q \in \hat\Delta^N$ with $\mu = \mu_q$ , and for this $q$ , all data and every $b$ ,

\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \Pi_q(\mathcal A)\} = \{x : \exists y_1, y_2 \in \mathbb R^N,\ e'y_1 + e'y_2 \ge b,\ y_{1,i} + y_{2,j} \le q_i\, a_j'x\ \forall i, j\}.

The vector $q$ depends on $\mu$ only; the data are quantified after it.

Milestones

Theorem 2.1. $\mu$ is coherent if and only if some family $\mathcal Q \subseteq \Delta^N$ generates it.
Theorem 3.1. For coherent $\mu$ generated by $\mathcal Q$ , $\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \operatorname{conv}\{Aq : q \in \mathcal Q\}\}$ ; conversely every nonempty $\mathcal U \subseteq \operatorname{conv}(\mathcal A)$ arises from the coherent measure generated by $\{q \in \Delta^N : Aq \in \mathcal U\}$ .
Generation of (4). $\mu_q$ is generated by the permuted vectors $q \circ \sigma$ , $\sigma \in S_N$ .
Theorem 4.1 (Schmeidler). A coherent $\mu$ is comonotonic if and only if $\mu(X) = \int (-X)\,dg$ (Choquet integral) for a monotone, normalized, submodular $g : 2^\Omega \to [0,1]$ .
Second differences (proof of Lemma 4.1). A submodular $g$ depending only on $|A|$ has nonincreasing increments along $\emptyset \subset \{\omega_1\} \subset \{\omega_1, \omega_2\} \subset \cdots$ .
Lemma 4.1. A risk measure is a distortion risk measure if and only if $\mu(X) = \int_{(0,1]} \mathrm{CVaR}_\alpha(X)\,\nu(d\alpha)$ for a probability measure $\nu$ .
The CVaR display (proof of Theorem 4.2). $\mathrm{CVaR}_\alpha(X) = \sup\{\mathbb E_q[-X] : q \in \Delta^N,\ q_i \le 1/(N\alpha)\} = \mu_{q^\alpha}(X)$ with $q^\alpha \in \hat\Delta^N$ .
Theorem 4.2. A risk measure is a distortion risk measure if and only if $\mu = \mu_q$ for some $q \in \hat\Delta^N$ ; every such $q$ is a convex combination of the generators $\hat q^j$ of $\mathrm{CVaR}_{j/N}$ .
Assignment duality (proof of Theorem 4.3). $a'x \ge b$ on $\Pi_q(\mathcal A)$ if and only if the linear system in $(y_1, y_2)$ above is feasible.

A companion item states Corollary 4.3: $\Pi_{\sum_j \lambda_j \hat q^j}(\mathcal A) = \operatorname{conv}\{\sum_j \lambda_j \frac1j \sum_{i \le j} a_{\sigma_j(i)} : \sigma_j \in S_N\}$ , and the class equality it yields: the uncertainty sets $\Pi_q(\mathcal A)$ of all distortion risk measures $\mu = \mu_q$ are exactly the polytopes $\mathcal U_\lambda(\mathcal A)$ , $\lambda \ge 0$ , $\sum_j \lambda_j = 1$ .

Significance

The goal theorem identifies the uncertainty set implied by any distortion risk measure: it is a permutohull of the data, a polytope with up to $N!$ vertices that is nevertheless representable with $2N$ extra variables and $N^2$ linear constraints. Combined with Theorem 4.2, the uncertainty sets of distortion measures are exactly the mixtures of the sets of $j$ -point averages of the data (Corollary 4.3), with $\mathrm{CVaR}_{j/N}$ as the generators. The later sections of the paper build on this: centrally symmetric permutohulls (Section 4.4) and the construction of a distortion risk measure from a given polyhedral uncertainty set (Section 4.5) are the subjects of the two companion missions.

The results are proved in the paper; no machine-checked version is known. The formalization adds checked statements of the finite-space representation theory of coherent and distortion risk measures, which the paper obtains partly by citing general results, and records the corrections the printed statements need.

Difficulty

The two equalities of the goal have unequal weight. The second is a statement about one polytope with up to $N!$ vertices and a linear system of size $O(N^2)$ ; it is finite-dimensional linear programming. The first requires the complete characterization of distortion risk measures on a finite uniform space, and that is where the obvious approach fails. The known representation of law-invariant comonotonic coherent measures as mixtures of CVaR (Kusuoka 2001) is proved for atomless spaces and does not transfer to a discrete $\Omega$ . The uniform distribution is essential, not a convenience: Remark 4.2 of the paper gives a two-point space with probabilities $1/3, 2/3$ and a monotone, normalized, submodular set function depending only on probability whose induced distortion is not concave, so the conclusion of Theorem 4.2 fails there.

Formalization scope

$\Omega$ is Fin N with $N \ge 1$ ; random variables are Fin N → ℝ; indices are 0-based throughout, so qhat j is the paper's $\hat q^{j+1}$ and $q_1 \ge \cdots \ge q_N$ is Antitone q. Order statistics are X ∘ Tuple.sort X.
Probability measures on $\Omega$ are probability vectors in stdSimplex ℝ (Fin N). Generation (1) is an IsLUB over an arbitrary set of probability vectors, not a maximum over a finite family (that version is false).
Sign of the risk constraint. Display (2) and Theorem 4.3 print $\mu(\tilde a'x - b) \ge 0$ . The paper introduces the constraint as $\mu(\tilde a'x - b) \le 0$ (p. 1486) and the proof of Theorem 3.1 computes $\mu(\tilde a'x - b) = -\inf_{a \in \mathcal U} a'x + b$ ; all statements use $\le 0$ .
Standing assumptions. Theorems 2.1 and 3.1 assume a probability vector $p$ with $p_i > 0$ (full support makes $\mathbb Q \ll \mathbb P$ vacuous; with a null atom Theorem 2.1 fails for functions on $\Omega$ ). From Lemma 4.1 on the distribution is uniform (Assumption 4.1). Theorem 3.1's converse adds $\mathcal U \neq \emptyset$ .
CVaR is a real infimum, used only for $\alpha \in (0,1]$ , where the objective is bounded below by $\mathbb E[-X]$ . In Lemma 4.1 the mixing measure $\nu$ is a probability measure on $(0,1]$ ; the page's $\int_0^1$ is read over $(0,1]$ . The CVaR display uses the corrected coefficient $(N\alpha - \lfloor N\alpha \rfloor)/(N\alpha)$ in place of the printed $/\lfloor N\alpha \rfloor$ . The assignment-duality milestone is stated for every $q \in \mathbb R^N$ .
The goal must assert the representation $\mu = \mu_q$ together with the set equalities: a statement "there is some $q$ for which the sets coincide" would let $q$ depend on the data and is not Theorem 4.3. The goal does not assume $\mu = \mu_q$ , which is Theorem 4.2's conclusion.
Needed infrastructure: Birkhoff's theorem (in Mathlib), LP duality, the rearrangement inequality, Choquet integrals of step functions. Lemmas about $\mu_q$ and order statistics are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

D. Bertsimas, D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
D. Schmeidler, Integral representation without additivity, Proceedings of the AMS 97(2):255–261, 1986. https://doi.org/10.1090/S0002-9939-1986-0835875-8
R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
S. Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3:83–95, 2001. https://doi.org/10.1007/978-4-431-67891-5_4
H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075

11 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons 1: A Fixed Price Earns at Least 1 − 1/(2√min{n, λ*t}) of the Optimal Expected RevenueResearch Paper

Motivation

A firm holds a fixed stock of a perishable or seasonal product: airline seats, hotel rooms, fashion goods, tickets. It must sell the stock over a finite season, and whatever is left at the end is worth nothing. The firm can change its price at any time, and demand responds to the price at random. Should it adjust its price continually as sales occur and time runs out, or is one well-chosen price nearly as good?

Gallego and van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), set up this question as a continuous-time stochastic control problem and answered it. The source for this mission is the published 1994 article. Its answer is quantitative: the expected revenue of a single fixed price is within a factor $1-1/(2\sqrt{\min\{n,\lambda^*t\}})$ of the best possible dynamic policy. The paper is one of the founding results of dynamic pricing in revenue management. The deterministic (fluid) upper bound it introduced became the standard benchmark of the field, and later work on re-solving heuristics, network revenue management and learning-while-pricing builds on it.

Setting

Demand. The firm chooses a demand intensity $\lambda$ from an interval $\Lambda\ni 0$ of allowable rates, and the market charges the inverse-demand price $p(\lambda)$ . On nonzero rates, $p$ is strictly decreasing and nonnegative; rate $0$ corresponds to the null price $p_\infty$ , at which nothing sells. The revenue rate is $r(\lambda)=\lambda p(\lambda)$ . It has $r(0)=0$ , and it is continuous, concave and bounded on $\Lambda$ . $\lambda^*$ denotes its least maximizer, and $p^*=p(\lambda^*)$ , $r^*=r(\lambda^*)$ . Such data form a regular demand function (§2.1).

The stochastic problem. At time $0$ the firm holds $n$ items and has a horizon $[0,t]$ . A non-anticipating pricing policy $u$ chooses the intensity $\lambda_s\in\Lambda$ at each elapsed time $s$ as a function of the sales history so far. Sales follow a Poisson process with this controlled intensity, and at most $n$ items can be sold. A sale at time $s$ earns the current price $p_s$ . The expected revenue is $J_u(n,t)=E_u[\int_0^t p_s\,dN_s]$ , where $N_s$ counts the sales, and the optimal expected revenue is $J^*(n,t)=\sup_u J_u(n,t)$ .

The deterministic problem. Replacing random sales by their rates gives

J^D(x,t)=\sup\Big\{\int_0^t r(\lambda(s))\,ds:\ \lambda(s)\in\Lambda,\ \int_0^t\lambda(s)\,ds\le x\Big\}.

It is solved by the constant rate $\lambda^D=\min\{\lambda^*,x/t\}$ (Proposition 2).

Fixed-price heuristics. $J^{FP}(n,t)$ is the expected revenue of charging $p^D=p(\lambda^D)$ for the whole horizon. $J^{OFP}(n,t)$ is the expected revenue of the best constant price.

Formalization targets

Goal: Theorem 3

For $\lambda^*>0$ , $n\ge1$ and $t>0$ , $J^*(n,t)$ is finite and positive, and

\frac{J^{OFP}(n,t)}{J^*(n,t)}\ \ge\ \frac{J^{FP}(n,t)}{J^*(n,t)}\ \ge\ 1-\frac{1}{2\sqrt{\min\{n,\lambda^*t\}}}.

Milestones

Proposition 2: $\lambda^D$ solves (11), and $J^D(x,t)=t\,r(\lambda^D)$ .
Eqs. (13)–(14): $E_u[N_t]=E_u[\int_0^t\lambda_s ds]\le n$ and $J_u(n,t)=E_u[\int_0^t r(\lambda_s)ds]$ for every policy.
Eq. (15) and Lemma 1: $J_u(n,t)\le J_u(n,t,\mu)\le J^D(n,t,\mu)$ for all $\mu\ge0$ .
The zero duality gap: $J^D(n,t)=\min_{\mu\ge0}J^D(n,t,\mu)$ .
Theorem 2: $J^*(n,t)\le J^D(n,t)$ for all $n\ge 0$ , $t\ge0$ .
Eq. (17): a fixed price $p$ earns $p\,E[\min\{n,N_{\lambda(p)t}\}]$ , with $N$ Poisson.
Inequality (18), Gallego's bound $E[(N-n)^+]\le(\sqrt{\sigma^2+(n-\mu)^2}-(n-\mu))/2$ , already on the platform.
The two case bounds of the proof of Theorem 3, including (19), and the exact fixed-price revenue of the Remark.

Significance

The result. Theorem 2 says that uncertainty can only cost revenue. The deterministic value is a computable upper bound for every policy, so any heuristic can be judged against it. Theorem 3 turns this into a guarantee: with 400 items and scarce stock, a single price earns at least 97.5% of the optimum. The loss vanishes as the expected sales volume grows. This is the justification for the stable, rarely changed prices seen in practice, and the template for the asymptotic-optimality analyses that followed: fluid bounds, re-solving, bid prices.

Formalizing it. The results are proved on paper, and none is formalized. The platform has a discrete-time Bernoulli analogue of Theorem 2 (Talluri–van Ryzin, RevenueManagement.deterministic_upper_bound) and Bitran–Caldentey's periodic-review version as open items. Neither is this continuous-time model. A formalization would add a controlled Poisson sales process with a policy-dependent intensity, the compensator identities (13)–(14) for it, and a Lagrangian-duality argument over measurable rate paths. These are reusable for every continuous-time revenue-management model on the platform. Gallego's moment bound (18) is already proved there.

Difficulty

The deterministic side (Proposition 2, the duality gap) is convex analysis on one concave function. The fixed-price bounds reduce to a Poisson computation and (18). The obstacle is Theorem 2's stochastic step. The revenue is collected at random jump times chosen by an adaptive policy, and comparing it with a deterministic integral requires the compensator identity $E_u[\int p_s\,dN_s]=E_u[\int r(\lambda_s)\,ds]$ for an arbitrary non-anticipating intensity. The paper cites Brémaud's martingale theory for this, which Mathlib does not have. A first idea is to apply Jensen's inequality to $J_u$ directly. It fails because the stock constraint holds only pathwise, through $N_t\le n$ , and not in expectation for a rate path. Restricting to Markovian policies does not remove the need for the identity.

Formalization scope

Model. Rates are real numbers, and $\Lambda\subseteq[0,\infty)$ is an interval containing $0$ . $p$ is a real function, strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$ . $r(\lambda)=\lambda p(\lambda)$ is continuous, concave and bounded above on $\Lambda$ , and $\lambda^*$ is its least maximizer. $p(0)$ is never used, since the null price may be $+\infty$ .
Policies depend on elapsed time and the past sale times (the internal history); randomized policies are not included. Intensities are jointly measurable and locally integrable.
The sales process is built from i.i.d. $\mathrm{Exp}(1)$ clocks, one per item. A sale occurs when the intensity integrated since the last sale reaches the next clock, so at most $n$ items are sold. Constraint (2) is part of the construction, not a hypothesis.
Values. Expected revenues and $J^*$ are in $[0,\infty]$ , as lower Lebesgue integrals and suprema. $J^D$ is a real supremum over measurable, integrable rate paths, nonempty and bounded for $x,t\ge0$ . $J^{FP}$ and $J^{OFP}$ are expected revenues of constant-price policies of this process, and the goal also asserts $0<J^*<\infty$ . Defining $J_u$ by the right side of (14), $J^*$ by the HJB equation, or $J^{FP}$ by formula (17) would trivialize the mission, and is ruled out.
Added hypotheses. Theorem 3 assumes $n\ge1$ , $t>0$ and $\lambda^*>0$ , which the page leaves implicit: the ratios divide by $J^*$ , which vanishes otherwise. Eqs. (13)–(14) are stated for every policy, without Proposition 1's bound $\lambda_s\le\lambda^*$ , and without the reduction to Markovian policies.
Corrected slips. (12) prints $J^D(x,t)=t\min\{r^*,r^0\}$ , which is false for $x>\lambda^*t$ (exponential demand with $x=at$ gives $r^0=0$ ). The statement uses $t\,r(\lambda^D)$ , and the printed form where $x\le\lambda^*t$ . The Remark's " $E(N_n-n)^+=n(1-P\{N_n=n\})$ " should read $E[\min\{N_n,n\}]$ ; its displayed $J^{FP}$ formula is right. Proposition 2's "the optimal solution" is stated as optimality, since uniqueness fails without strict concavity.
Welcome contributions. Infrastructure for counting processes with stochastic intensity (the clock construction, the compensator identity), Jensen and Lagrangian duality for concave integral functionals on rate paths, and Poisson truncated-mean computations.

Selected references

G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11:55–60, 1992 (cited in the paper's references, p. 1019).
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the paper).
K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004 (Chapter 5; on the platform as RevenueManagement.*).
G. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003 (on the platform as PricingRM.DetHeuristic.*).

15 thms2 active usersReviewed

Completed

Machine Learning Optimization Statistics·Captain: mikedeng1

Non-Strongly-Convex Smooth Stochastic Approximation with Convergence Rate O(1/n): Averaged Constant-Step-Size LMS Has Expected Excess Risk at Most (1/2n)[σ√d/(1−√(γR²)) + R‖θ₀−θ*‖/√(γR²)]²Research Paper

Motivation

Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate $O(1/\sqrt n)$ for non-strongly-convex objectives, and $O(1/(\mu n))$ when the objective is $\mu$ -strongly convex. For least squares, $\mu$ is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.

F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate $O(1/n)$ with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.

Setting

Let $\mathcal H=\mathbb R^d$ with $d\ge1$ , inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . For $a\in\mathcal H$ , $a\otimes a$ is the operator $b\mapsto\langle a,b\rangle a$ . For self-adjoint operators, $A\preccurlyeq B$ means that $B-A$ is positive semi-definite.

The data are independent and identically distributed pairs $(x_n,z_n)\in\mathcal H\times\mathcal H$ , $n\ge1$ , with finite second moments. The covariance operator is $H=\mathbb E[x_n\otimes x_n]$ , assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective

f(\theta)=\tfrac12\,\mathbb E\big[\langle\theta,x_n\rangle^2-2\langle\theta,z_n\rangle\big]

attains its global minimum at $\theta^*$ , and $\xi_n=z_n-\langle\theta^*,x_n\rangle x_n$ is the residual. The model need not be well specified: $\mathbb E[\xi_n\mid x_n]$ need not vanish. Two constants $R,\sigma>0$ satisfy

\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq\sigma^2H,\qquad \mathbb E\big[\|x_n\|^2x_n\otimes x_n\big]\preccurlyeq R^2H .

These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size $\gamma$ , started at $\theta_0\in\mathcal H$ , is

\theta_n=\theta_{n-1}-\gamma\big(\langle\theta_{n-1},x_n\rangle x_n-z_n\big)=(I-\gamma x_n\otimes x_n)\theta_{n-1}+\gamma z_n ,

and its average is $\bar\theta_{n-1}=n^{-1}\sum_{k=0}^{n-1}\theta_k$ .

Formalization targets

Goal: Theorem 1, Eq. (2)

For every step size $0<\gamma<1/R^2$ and every $n\ge1$ ,

\mathbb E\big[f(\bar\theta_{n-1})-f(\theta^*)\big]\le\frac{1}{2n}\left[\frac{\sigma\sqrt d}{1-\sqrt{\gamma R^2}}+R\|\theta_0-\theta^*\|\frac{1}{\sqrt{\gamma R^2}}\right]^2 .

The constants are the paper's. A companion item states the case $\gamma=1/(4R^2)$ , where the bound reads $\frac2n\big[\sigma\sqrt d+R\|\theta_0-\theta^*\|\big]^2$ .

Milestones (Appendix A)

The excess risk is a quadratic form: $f(\theta)-f(\theta^*)=\tfrac12\langle\theta-\theta^*,H(\theta-\theta^*)\rangle$ .
Consequences of (A6): $\mathbb E\|x_n\|^2\le R^2$ , $\operatorname{tr}H\le R^2$ , $H\preccurlyeq R^2I$ , and $\gamma H\preccurlyeq I$ for $\gamma\le1/R^2$ .
Lemma 1: for a recursion $\alpha_n=(I-\gamma x_n\otimes x_n)\alpha_{n-1}+\gamma\xi_n$ with martingale-difference noise and $\gamma R^2\le1$ ,

(1-\gamma R^2)\,\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle+\tfrac{1}{2n\gamma}\mathbb E\|\alpha_n\|^2\le\tfrac{1}{2n\gamma}\|\alpha_0\|^2+\tfrac{\gamma}{n}\textstyle\sum_{k=1}^{n}\mathbb E\|\xi_k\|^2 .

Lemma 3: $(1-(1-u)^n)^2\le nu$ for $u\in[0,1]$ and $n>0$ .
Lemma 2: for $\alpha_n=(I-\gamma H)\alpha_{n-1}+\gamma\xi_n$ with $\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq C$ , the second-moment bound (13) and

\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle\le\tfrac{1}{n\gamma}\|\alpha_0\|^2+\tfrac1n\operatorname{tr}(CH^{-1}).

The pathwise decomposition $\theta_n-\theta^*=M^n_1(\theta_0-\theta^*)+\gamma\sum_{k=1}^nM^n_{k+1}\xi_k$ (A.2).
The initial-condition bound $\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\le\|\eta_0\|^2/(n\gamma)$ for the noise-free process (A.3).
The expansion of the noise process (A.4): the remainder recursion (16), the covariance bound (17) $\mathbb E[\eta^r_{n-1}\otimes\eta^r_{n-1}]\preccurlyeq\gamma^{r+1}R^{2r}\sigma^2I$ , the order- $r$ bound $\frac1n\gamma^rR^{2r}d\sigma^2$ , the remainder bound $\frac{\gamma^{r+2}\sigma^2R^{2r+4}}{1-\gamma R^2}$ , and the noise bound

\big(\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\big)^{1/2}\le\frac{\sigma\sqrt d}{\sqrt n}\cdot\frac{1}{1-\sqrt{\gamma R^2}}\quad(\eta_0=0,\ \gamma R^2<1).

Significance

The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term $\sigma^2d/n$ , which matches the minimax rate for least-squares regression, and a bias term $R^2\|\theta_0-\theta^*\|^2/(\gamma n)$ . Neither involves the smallest eigenvalue of $H$ , so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in $\mathbb R^d$ , second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator $H$ , so they apply beyond this model. The mission also records the corrections the appendix needs (an " $=$ " that should be " $\preccurlyeq$ " in (13), an index in (16), and the exponent of $\|\eta_0\|$ in A.5).

Difficulty

Two steps resist the naive approach. First, the obvious one-step analysis — expand $\|\theta_n-\theta^*\|^2$ and take expectations — yields the bias part and Lemma 1, but on the noise it gives only $\gamma\sum_k\mathbb E\|\xi_k\|^2/n$ , which does not decrease with $n$ . The $\sigma^2d/n$ rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with $x_n\otimes x_n$ replaced by its mean $H$ . The random recursion is therefore expanded in powers of $\gamma$ around the mean recursion, and each term $\eta^r$ needs its own covariance bound, by induction on $r$ , using the independence of $x_n$ from $\eta^{r}_{n-1}$ . Second, the induction relies on Loewner-order bookkeeping: sums of $(I-\gamma H)^{2k}H$ must be bounded uniformly in $n$ without dividing by small eigenvalues.

Formalization scope

The space $\mathcal H$ is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and $H^{-1}$ is an explicit two-sided inverse. Observations are indexed from $1$ . Averages are $\bar p_{n-1}=n^{-1}\sum_{k=0}^{n-1}p_k$ , with $n\ge1$ in every statement that uses them. The covariance operator is defined by its bilinear form, $\langle v,Hw\rangle=\mathbb E[\langle x_1,v\rangle\langle x_1,w\rangle]$ . Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example $\mathbb E\langle\xi_1,v\rangle^2\le\sigma^2\langle v,Hv\rangle$ for all $v$ ), which is the same order for self-adjoint operators.

Lean's Bochner integral is $0$ on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed $x_n$ would satisfy (A6) vacuously and a conclusion could hold through the value $0$ ; neither formalization is acceptable. Independence is of the pairs $(x_n,z_n)$ , not of $x_n$ and $z_n$ separately. (A4) is attainment of the minimum, not a gradient condition.

The following hypotheses are added to the page and disclosed in each item:

$\gamma>0$ (a step size, and $\sqrt{\gamma R^2}$ is a denominator);
$n\ge1$ ;
the positivity and self-adjointness of $H$ in Lemma 2;
$\gamma R^2<1$ instead of $\le1$ in the remainder bound, which divides by $1-\gamma R^2$ .

A complete development needs:

conditional expectations of $\mathbb R^d$ -valued martingale differences, and the orthogonality of their sums;
independence of a fresh observation from the past iterates;
spectral calculus for $(I-\gamma H)^k$ ;
Minkowski's inequality in $L^2$ .

All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.

Selected references

F. Bach and E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), Advances in Neural Information Processing Systems 26, 2013. https://arxiv.org/abs/1306.2119
B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046
R. Aguech, E. Moulines and P. Priouret, On a perturbation approach for the analysis of stochastic tracking algorithms, SIAM Journal on Control and Optimization 39(3), 2000. https://doi.org/10.1137/S0363012997331639
F. Bach and E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, Advances in Neural Information Processing Systems 24, 2011. https://hal.science/hal-00608041

15 thms2 active usersReviewed

Missions

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

Motivation

Setting

Formalization targets

Main theorem

Milestone statements

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts X: Under Forced Compliance, Options Contracts with Shares λ_l and min{λ_h, λ̂_h} Separate the Two Demand Types and Coordinate CapacityTextbook

Motivation

Setting

Formalization targets

Goal: forced-compliance separating contracts (§6.10.3, pp. 103–104)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Wait-and-Judge Scenario Optimization 1: For Convex Programs, Seeing s_N Support Constraints Gives P^N{V(x_N) > ε(s_N)} ≤ γ, the Value of the Variational Problem (10)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 10)

Milestones (the proof of Theorem 1, Sect. 5.1)

Companions

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts VIII: In the Two-Location Base-Stock Model the Linear Transfers (39)–(41) Make the Optimal Base Stocks the Unique Nash EquilibriumTextbook

Motivation

Setting

Formalization targets

Goal: the contracts coordinate, uniquely

Milestones

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts III: With Effort-Dependent Demand, Buy-Backs, Quantity Flexibility and Revenue Sharing Under-Reward Effort, While a Quantity Discount Gives λΠ(q, e°)Textbook

Why effort breaks the standard coordinating contracts

The newsvendor with effort-dependent demand

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts I: The Newsvendor Quantity-Flexibility Contract (w_q(δ), δ) Gives the Retailer at Least Π(q°) at δ = 0, the Supplier at Least Π(q°) at δ = 1Textbook

Why contracts in a newsvendor supply chain

Setting

Formalization targets

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

Milestones, in attack order

Companion results of §6.2

Significance

Difficulty

Formalization scope

Selected references

The Chromatic Number of Random Graphs: For Fixed 0 < p < 1, Almost Every G(n,p) Has n/s₀ ≤ χ(G) ≤ (n/s₀)(1 + 3 log log n / log n), where s₀ ≈ 2 log_d n and d = 1/(1−p)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Online Stochastic Matching: Beating 1-1/e 2: The Suggested Matching Algorithm Achieves 1 − 1/e with High Probability, and This Is Tight Even in ExpectationResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Goal: Theorem 5, first sentence, $e_i = 1$