Operations Research

Motivation

A seller who changes prices while learning demand faces two costs: a price experiment may earn less revenue now, while insufficient experimentation leaves later prices poorly calibrated. Customer features make the balance harder because both willingness to buy and sensitivity to price may vary between customers. Ban and Keskin study this problem when the number of recorded features can be large relative to the selling horizon. Their known-support policy, ILSX, provides the upper bound formalized here Ban and Keskin, 2021, §§2 and 4.1.

The paper's result is a statement about learning a demand model while serving sequential customers, rather than about fitting that model after all observations are available. A price at period $t$ must use information then available, including the arriving customer's features but excluding that customer's demand shock. The seller therefore needs a policy whose expected revenue loss can be bounded uniformly over the unknown parameters in a specified model Ban and Keskin, 2021, pp. 5552–5556.

Setting

In each period $t=1,2,\ldots$, a customer arrives with a feature vector $Z_t\in\mathbb R^d$. The seller observes the augmented vector $X_t=[1;Z_t]$, posts a price $p_t\in[\ell,u]$ with $0<\ell<u$, and then observes demand. In the linear demand model, demand equals

$$D_t=\alpha\cdot X_t+(\beta\cdot X_t)p_t+\varepsilon_t.$$

The intercept and slope vectors $\alpha,\beta$ are unknown. The seller knows the sparsity structure $\mathcal S$: outside this set of coordinate indices, both parameter vectors vanish. The compressed parameter $\theta_{\mathcal S}=(\alpha_{\mathcal S},\beta_{\mathcal S})$ lies in a compact coordinate rectangle $\Theta_{\mathcal S}$, and $s=|\mathcal S|\ge1$. The compressed customer vector is $X_{\mathcal S,t}=(X_{t,i})_{i\in\mathcal S}$ Ban and Keskin, 2021, pp. 5552–5555.

At price $p$, expected single-period revenue is $r(p,\theta_{\mathcal S},x)=p[\alpha_{\mathcal S}\cdot x+(\beta_{\mathcal S}\cdot x)p]$. The clairvoyant price is $\varphi(\theta_{\mathcal S},x)=-(\alpha_{\mathcal S}\cdot x)/(2\beta_{\mathcal S}\cdot x)$ when the slope is negative. The paper assumes this price is in $(\ell,u)$ throughout its model domain. Expected regret $\Delta^{\pi}_{\theta_{\mathcal S}}(T)$ is the expected sum, through period $T$, of the clairvoyant revenue minus the revenue at the policy's price Ban and Keskin, 2021, (2)–(4), p. 5553–5554.

The ILSX policy charges one fixed experimental price $m_1$ at periods $1,4,9,\ldots$ and a distinct price $m_2$ at periods $2,5,10,\ldots$. At every other period it estimates the compressed demand parameter by least squares using experimental observations, projects the estimate onto $\Theta_{\mathcal S}$, and applies $\varphi$ to the projected estimate and the current customer vector. Both prices lie in $[\ell,u]$ Ban and Keskin, 2021, (7), (8), (12), pp. 5555–5556.

Formalization targets

The goal is Theorem 2: for the stated model and ILSX policy, a finite positive constant $C$ exists such that

$$\Delta^{\mathrm{ILSX}(m_1,m_2)}_{\theta_{\mathcal S}}(T)\le Cs\sqrt T\log T\qquad(\theta_{\mathcal S}\in\Theta_{\mathcal S},\ T\ge2).$$

The constant is chosen after the model, shock process, experimental prices, and estimator selection are fixed, but before the parameter and horizon. The theorem and Remark 5 are on pp. 5556–5557 of Ban and Keskin, 2021.

The milestones reproduce the paper's route into this claim: the experimental-period count following (7); the growth bound (15) for the price-variation statistic $J_t$; Lemma 1's minimum-eigenvalue probability bound for the experimental information matrix $\widetilde{\mathcal J}_{\mathcal S,t}$; and Lemma 2's high-probability bound for its noise-driven estimation error. The least-squares error identity (11) is included as a supporting item on invertible samples, not as a milestone. The constants and thresholds in these targets remain existential where the article leaves them existential Ban and Keskin, 2021, pp. 5555–5556.

Significance

The theorem gives a guarantee for a concrete pricing policy under feature-dependent price sensitivity. The bound grows with the horizon at order $\sqrt T\log T$ for a fixed known support, with an explicit factor $s$ in the published statement. It lets a seller compare the cost of this policy with the revenue of a seller who knew the demand coefficients before pricing. The paper presents its result as matching its lower-bound benchmark up to logarithmic factors, under the paper's respective hypotheses Ban and Keskin, 2021, Theorems 1–2, pp. 5554–5556.

The mathematical result was published in 2021. This mission seeks a machine-checked statement and proof of the known-support guarantee and its stated intermediate results. The checked Prove2Me prior-art catalog contains featureless dynamic-pricing results and separate least-squares results, but no matching formalization of ILSX. A completed development would add reusable definitions for a feature-dependent price regressor, experimental information matrix, nonanticipating estimator selection, and expected regret. The article places its proofs in an electronic companion, which is not included in the held source PDF; this mission does not reproduce those proofs as source material.

Difficulty

The policy learns from a sparse set of deliberately chosen periods, while its regret accumulates at every period. A pointwise least-squares identity alone does not control the regret: the information matrix can be singular at early periods, and the customer features and shocks are random. In particular, the printed inverse identity (11) says “for all $t\ge2$”, although at $t=2$ the matrix has rank at most two and cannot be invertible when $s\ge2$. The formal statement therefore confines the inverse identity to invertible samples. Lemma 2's event also includes invertibility so a default inverse of a singular matrix cannot make its error bound automatic Ban and Keskin, 2021, (9)–(11), Lemma 2, p. 5556.

Formalization scope

Lean uses one-based periods and a support subtype of the augmented feature coordinates. Coordinate zero is the paper's intercept coordinate one. The parameter has coordinates $(j,i)$ for demand intercept or price slope $j\in\{0,1\}$ and support index $i\in\mathcal S$. The regressor $[1;p]\otimes X_{\mathcal S,t}$ gives the information matrix in (10). Euclidean squared norms are explicit sums of squares, and the minimum-eigenvalue claim is the equivalent Rayleigh inequality. The parameter rectangle is nonempty, and its Euclidean projection is coordinatewise clamping.

The standing assumptions are $d\ge1$, $s\ge1$, $0<\ell<u$, distinct experimental prices in $[\ell,u]$, bounded i.i.d. features with mean zero and positive-definite covariance, and a fixed shock process with conditional mean zero, bounded conditional second moment, and finite conditional exponential moments near zero. The feature process is measurable and integrable. The model additionally states independence of the next customer's features from the past primitives, the reading of the paper's joint probability construction used here. The slope is negative and the clairvoyant price lies in $(\ell,u)$ for every allowed parameter and realized feature. These conditions ensure that the price formula represents a genuine revenue maximum. The phrase about continuous features having positive measure in the interior of their domains is omitted because the page does not specify the domains or a reference measure Ban and Keskin, 2021, §2, pp. 5552–5554.

The estimator is any measurable minimizer of the experimental least-squares objective for histories with at least two observations. Its type depends only on earlier observations; at nonexperimental periods the recorded pseudo-observations are ignored by the objective. The shock law is fixed while the parameter varies. Expected regret uses a nonnegative integral, and conditional second and exponential moments use nonnegative conditional expectations. The theorem binds $C$ before the parameter and horizon, while leaving support size fixed with the model. Consequently, the stronger uniformity in $s$ suggested by Remark 5 is outside this statement. These choices exclude vacuous integrals, unconstrained estimators, and accidental bounds from a singular matrix inverse. Work on the probability estimates, least-squares identity, and regret bound is welcome under these exact definitions.

Selected references

• G.-Y. Ban and N. B. Keskin, Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity, Management Science 67(9):5549–5568, 2021. DOI: 10.1287/mnsc.2020.3680.

Motivation

Online combinatorial optimization is a repeated game in which a learner selects, round after round, a structured object (a subset of fixed size, a path, a matching, a spanning tree) encoded as a 0/1 vector, and an adversary assigns a cost to every coordinate. It models routing, ranking, scheduling and many other sequential decision problems in operations research and machine learning, and it contains prediction with expert advice as the special case of one-hot vectors.

The most widely used algorithm for this game is the exponentially weighted forecaster, which keeps a weight on every action and multiplies it by $\exp(-\eta\cdot\text{loss})$ after each round. Applied to a combinatorial action set it is called EXP2 (Audibert, Bubeck and Lugosi), or Expanded Hedge in the full-information case (Koolen, Warmuth and Kivinen, COLT 2010). Its standard analysis gives regret of order $m^{3/2}\sqrt{n\log(d/m)}$, while online mirror descent with the negative entropy (Component Hedge) achieves $m\sqrt{n\log(d/m)}$, which is optimal. Koolen, Warmuth and Kivinen left open whether a better tuning or a better analysis of EXP2 could close this gap.

Timeline.

• 1997: Freund and Schapire analyse Hedge for experts.
• 2010: Koolen, Warmuth and Kivinen introduce Component Hedge, prove the $m\sqrt{n\log(d/m)}$ bound, and ask whether Expanded Hedge can match it.
• 2012–2014: Audibert, Bubeck and Lugosi (arXiv:1204.4710; Math. Oper. Res. 39(1), 2014) answer negatively: Theorem 1 exhibits an action set on which EXP2's full-information regret is at least $0.01\,d^{3/2}\sqrt n$ for every learning rate.

Setting

Fix integers $d$ (the dimension) and $n$ (the number of rounds). An action set is a nonempty finite set $\mathcal A\subseteq\{0,1\}^d$ whose elements all have the same number $m$ of ones: $\|a\|_1=m$ for every $a\in\mathcal A$. At each round $t=1,\dots,n$:

1. the player chooses a probability distribution $p_t$ on $\mathcal A$ and draws $a_t\sim p_t$;
2. simultaneously, the adversary chooses a loss vector $z_t\in[0,1]^d$;
3. the player pays $a_t^\top z_t$ and, in the full-information game, observes $z_t$.

The regret after $n$ rounds is

$$R_n=\mathbb E\sum_{t=1}^n a_t^\top z_t-\min_{a\in\mathcal A}\mathbb E\sum_{t=1}^n a^\top z_t .$$

EXP2 with learning rate $\eta$ starts from the uniform distribution $p_1$ on $\mathcal A$ and updates, for every $a\in\mathcal A$,

$$p_{t+1}(a)=\frac{\exp(-\eta\,a^\top z_t)\,p_t(a)}{\sum_{b\in\mathcal A}\exp(-\eta\,b^\top z_t)\,p_t(b)} .$$

In the Lean development IsBinaryActionSet A m is the action-set condition, exp2Weights A η z t is $p_{t+1}$, and exp2Regret A η z n is $R_n$ against a fixed loss sequence $z$. thmOneSet d, adv1 d and adv2 d ε are the action set and the two adversaries of the paper's proof.

Formalization targets

Goal: Theorem 1 (p. 6)

For $n\ge d$ with $d$ a multiple of $4$, there is an action set $\mathcal A\subseteq\{0,1\}^d$ with constant $\|a\|_1$ such that for every $\eta\ge0$ some adversary with losses in $[0,1]^d$ makes EXP2 pay

$$R_n\ \ge\ 0.01\,d^{3/2}\sqrt n .$$

The action set is chosen before the learning rate, and the adversary after it.

Milestones (App. A and App. C)

1. Lemma 3 (p. 19): for $k\ge1$ and $1\le c\le 2$,

$$\frac{\sum_{i=0}^k(1-i/k)\binom ki^2c^i}{\sum_{i=0}^k\binom ki^2c^i}\ \ge\ \frac13 .$$

2. First adversary (p. 15): on the action set of App. A, against the alternating adversary, $R_n=\frac{nd}{16}\tanh\frac{\eta d}{8}$ for $n$ even.
3. Second adversary (p. 16): against the constant adversary with $\varepsilon=\min(\log2/(\eta n),1)$, $R_n\ge\min\bigl(\frac{d\log2}{12\eta},\frac{nd}{12}\bigr)$ for $\eta>0$.
4. Optimization over $\eta$ (pp. 14–15): for every $\eta>0$,

$$\max\Bigl(\tfrac{nd}{16}\tanh\tfrac{\eta d}{8},\ \min\bigl(\tfrac{d\log2}{12\eta},\tfrac{nd}{12}\bigr)\Bigr)\ \ge\ \min\bigl(0.04\,nd,\ 0.01\,d^{3/2}\sqrt n\bigr).$$

Significance

The result. Theorem 1 shows that the gap between EXP2 and mirror descent with the negative entropy is not an artefact of the analysis: on an action set with $m=d/2$, where the optimal rate is of order $d\sqrt n$, no learning rate brings EXP2 below $0.01\,d^{3/2}\sqrt n$. Exponential weights over the actions are therefore provably suboptimal in online combinatorial optimization, which motivates working with the convex hull of $\mathcal A$ (mirror descent) rather than with the actions themselves. The construction is also a template for algorithm-specific lower bounds: two adversaries, one punishing large and one punishing small learning rates.

Formalizing it. The result is proved in the paper (App. A, with Lemma 3 in App. C); to our knowledge none of it is machine-checked. A formalization yields a checked algorithm-specific lower bound for exponential weights, an exact closed-form regret computation for EXP2 on a structured action set, and a rigorous proof of Lemma 3, whose printed proof checks $k\le10^6$ numerically before an asymptotic argument with Stirling's formula.

Difficulty

The statements are elementary, but each step hides a real computation. The first adversary requires the exact distribution of EXP2 on a set of $2\binom{d/2}{d/4}$ actions over alternating rounds, and a regret identity rather than a bound. The second requires controlling EXP2's expected loss over all $n$ rounds against a constant adversary on the same exponentially large set. Lemma 3 is the hardest piece: at $c=2$ it is tight at $k=1$, while the ratio tends to $1-\sqrt2/(1+\sqrt2)\approx0.414$ as $k\to\infty$; the printed proof verifies $k\le10^6$ numerically, so a formal proof needs an argument valid for every $k$. A naive attempt to prove the goal with a single adversary fails: one adversary only defeats either large or small learning rates.

Formalization scope

• Actions are real vectors Fin d → ℝ with entries in $\{0,1\}$, so $a^\top z$ is the dot product. Coordinates and rounds are 0-based: the paper's odd rounds are the even indices.
• EXP2 is defined by the recursion of Figure 2 with $\tilde z_t=z_t$, starting uniform on $\mathcal A$; its closed form $p_t(a)\propto\exp(-\eta\sum_{s<t}a^\top z_s)$ is a consequence, not the definition.
• The regret is defined against a deterministic, oblivious loss sequence, for which the expectation is a finite sum. Exhibiting such an adversary proves the paper's $\sup_{\text{adversary}}$, since it is a special case of the paper's adaptive adversaries.
• The minimum over $\mathcal A$ is a Finset.inf'; every statement requires $\mathcal A$ nonempty, so no junk value enters.
• Added hypotheses: $4\mid d$ in the goal (the proof's own simplifying assumption; the printed statement fails at $d=1$, where any constant-norm $\mathcal A$ is a singleton); $\eta>0$ and $n\ge1$ wherever $1/\eta$ or $1/(\eta n)$ appears. The goal does not assume $n$ even, although App. A does; the second-adversary milestone does not need it either.
• The action set of App. A is printed with "or"; it is formalized with exactly one of the two intervals filled, as the prose and the constant norm $\|a\|_1=d/2$ require.
• Ruled out: an existential over $\eta$, an adversary chosen before $\eta$, an action set depending on $\eta$, unbounded losses, and an empty action set with a junk minimum would each make the goal trivial or different; the statement quantifies as above.

Contributions welcome: proofs of the milestones, a proof of Lemma 3 by any method, and reusable lemmas on exponential weights (normalization, closed form, monotonicity of weights along a constant adversary). The paper's proofs are in its App. A and App. C.

Selected references

• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in Online Combinatorial Optimization, Math. Oper. Res. 39(1), 2014; arXiv:1204.4710v2. https://arxiv.org/abs/1204.4710
• W. M. Koolen, M. K. Warmuth, J. Kivinen, Hedging Structured Concepts, Proceedings of COLT 2010 (reference [26] of the paper above).
• Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, J. Comput. Syst. Sci. 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Found. Trends Mach. Learn. 5(1), 2012; arXiv:1204.5721. https://arxiv.org/abs/1204.5721

Motivation

A prophet inequality compares an online decision maker, who sees random values one at a time and must decide irrevocably, with a "prophet" who sees all values in advance. The classic result of Krengel, Sucheston and Garling (1977) and Samuel-Cahn (1984) says that for a single item and independent values a single threshold earns at least half of the expected maximum. In mechanism design the same inequalities describe posted-price mechanisms: a seller approaches buyers in sequence and offers each a menu of prices; each buyer takes the outcome it likes best. Such mechanisms are truthful, simple and online, so a prophet inequality for a feasibility constraint is a welfare guarantee for a practical selling procedure.

Before this paper, prophet inequalities were proved one constraint at a time (matroids, matroid intersections, polymatroids, unit-demand and combinatorial auctions), each with its own probabilistic argument. Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49(3), 2020; conference version FOCS 2017) showed that a single extension theorem reduces all of them to a deterministic question about full-information instances.

Setting

There are $n$ agents $N=\{1,\dots,n\}$. Agent $i$ has an outcome space $X_i$ containing a null outcome $\varnothing$. An outcome profile is $\mathbf x=(x_1,\dots,x_n)$; $\mathbf x_{[i-1]}$ is $\mathbf x$ with the outcomes of agents $i,\dots,n$ replaced by $\varnothing$. The feasible profiles form a downward-closed set $\mathcal F$: removing outcomes keeps a profile feasible.

Agent $i$'s valuation $v_i:X_i\to[0,1]$ is drawn independently from a known distribution $\mathcal D_i$; $\mathcal D=\prod_i\mathcal D_i$. The welfare of $\mathbf x$ is $\mathbf v(\mathbf x)=\sum_iv_i(x_i)$, and $\mathbf v(\mathrm{OPT}(\mathbf v,S))$ is the largest welfare over a set $S$ of profiles. An outcome rule $\mathrm{ALG}$ maps each valuation profile to a feasible profile.

A pricing rule assigns a price $p_i(x_i\mid\mathbf y)\in[0,\infty]$ to outcome $x_i$ offered to agent $i$ when the partial allocation is $\mathbf y$, with price $\infty$ when $x_i$ cannot be feasibly added to $\mathbf y$. In the posted-price mechanism the agents are approached in index order; agent $i$ sees the prices given the allocation so far and takes an outcome maximizing its utility $v_i(x_i)-p_i(x_i\mid\mathbf y)$.

A set $\mathcal H$ of profiles is exchange compatible with $\mathbf x$ if $(y_i,\mathbf x_{-i})\in\mathcal F$ for every $\mathbf y\in\mathcal H$ and every $i$. For a fixed valuation profile $\mathbf v$, a pricing rule $p^{\mathbf v}$ is $(\alpha,\beta)$-balanced (Definition 3.1) with respect to $\mathrm{ALG}$ and an exchange-compatible family $(\mathcal F_{\mathbf x})_{\mathbf x}$ if for every $\mathbf x\in\mathcal F$

$$\text{(a)}\quad\sum_{i}p^{\mathbf v}_i(x_i\mid\mathbf x_{[i-1]})\ \ge\ \tfrac1\alpha\bigl(\mathbf v(\mathrm{ALG}(\mathbf v))-\mathbf v(\mathrm{OPT}(\mathbf v,\mathcal F_{\mathbf x}))\bigr),$$ $$\text{(b)}\quad\sum_{i}p^{\mathbf v}_i(x'_i\mid\mathbf x_{[i-1]})\ \le\ \beta\cdot\mathbf v(\mathrm{OPT}(\mathbf v,\mathcal F_{\mathbf x}))\quad\text{for all }\mathbf x'\in\mathcal F_{\mathbf x}.$$

Property (a) says the prices paid by $\mathbf x$ cover the welfare $\mathbf x$ blocks; (b) says that what remains available is not overpriced.

Formalization targets

Goal: Theorem 3.2 (p. 549)

If every $p^{\tilde{\mathbf v}}$ is $(\alpha,\beta)$-balanced with respect to one exchange-compatible family, post $\delta p$ with $p_i(x_i\mid\mathbf y)=\mathbb E_{\tilde{\mathbf v}}[p^{\tilde{\mathbf v}}_i(x_i\mid\mathbf y)]$ and $\delta=\alpha/(1+\alpha\beta)$. Then the welfare $\mathbf x(\mathbf v)$ of the mechanism satisfies

$$\mathbb E_{\mathbf v}\bigl[\mathbf v(\mathbf x(\mathbf v))\bigr]\ \ge\ \frac1{1+\alpha\beta}\,\mathbb E_{\mathbf v}\bigl[\mathbf v(\mathrm{ALG}(\mathbf v))\bigr].$$

Milestones

The steps of the paper's proof (pp. 549–550), in order: the prefix $\mathbf x_{[i-1]}(\mathbf v)$ does not depend on $v_i$; the per-agent utility bound against a deviation drawn from an independent sample $\mathbf v'$; (3.1); the bound (3.2) from property (b); (3.3); the pointwise revenue bound from property (a); (3.4); and welfare = utilities + revenue. Two applications complete the list: Claim 3.3 (the single-item price $\max_\ell v_\ell$ is $(1,1)$-balanced, which with the goal gives the classic factor 2) and the balancedness half of Theorem 4.2 for knapsack.

Significance

The theorem turns prophet inequalities into a deterministic design problem: to obtain a $1/(1+\alpha\beta)$ guarantee against any benchmark $\mathrm{ALG}$, it suffices to exhibit balanced prices for each fixed valuation profile. The paper uses it to rederive the single-item factor 2, to obtain $O(d)$ guarantees for combinatorial auctions with bundles of size $d$, a constant for knapsack, and bounds for MPH-$k$ valuations, sparse packing problems and multidimensional matroids. Because $\mathrm{ALG}$ can be any (for example polynomial-time) algorithm, the guarantee is relative to what can be computed, not only to the optimum.

The result is proved in the paper. As far as is known, no part of it has a machine-checked proof; the platform holds no posted-price framework of this generality. A formal proof would provide a reusable model of sequential posted-price mechanisms over arbitrary outcome spaces and a checked reduction that later formalizations of the applications can invoke instead of repeating a probabilistic argument.

Difficulty

The obvious argument fixes the realized valuations and charges each agent's purchase against the welfare it blocks. That fails because the prices are averages over a hypothetical profile $\tilde{\mathbf v}$, not the prices of the realized instance, and the set of outcomes still available depends on everyone's random values. The proof needs an independent copy $\mathbf v'$ of the valuations and the fact that the allocation before agent $i$ does not depend on $v_i$, so that $v_i$ and $v'_i$ can be exchanged without changing the distribution. Formally, the run of the mechanism is a recursion over agents, the exchange is a measure-preserving swap of coordinates of a product measure, the optimal value $\mathbf v(\mathrm{OPT}(\mathbf v,\mathcal F_{\mathbf x}))$ is a supremum that need not be attained, and the family $\mathcal F_{\mathbf x}$ may be empty.

Formalization scope

Agents are Fin n, 0-based; the index order is the order of Fin n. Outcomes are (X : Fin n → Type*) with a null profile nul. Valuation types V i are countable with the discrete σ-algebra (a disclosed restriction: the paper allows any distribution); this makes every function measurable and every bounded one integrable. A type w : V i values outcomes through val i w : X i → ℝ, with values in $[0,1]$ as on p. 547. The distribution is Measure.pi μ with every μ i a probability measure.

Prices are ℝ≥0∞-valued, ⊤ standing for $\infty$; the expected price is a Lebesgue integral in $[0,\infty]$. Property (a) passes its real right side through ENNReal.ofReal, and no price sum is ever converted to a real number, so an infinite price is never read as $0$. $\mathbf v(\mathrm{OPT}(\mathbf v,S))$ is the real supremum sSup of the welfare over $S$, equal to $0$ on $S=\varnothing$ as in the proof of Claim 3.3. Exchange compatibility of the family is required at every profile, not only feasible ones. The pricing-rule condition "$\infty$ when infeasible" is imposed at feasible partial allocations, which is where the paper defines prices.

Two standing assumptions are disclosed. First, the null outcome is free: $p^{\tilde{\mathbf v}}_i(\varnothing\mid\mathbf y)=0$ for feasible $\mathbf y$. Every pricing rule of the paper satisfies it, and without it the proof's deviation does not exist when $\mathcal F_{\mathbf x(\mathbf v)}=\varnothing$. Second, the agents' behaviour is a choice rule that sees only the agent's own type and the allocation so far, assumed utility-maximizing (finite price, best utility among finitely priced outcomes) at every feasible partial allocation. The constant $\delta=\alpha/(1+\alpha\beta)$ is written into the posted prices, not passed as a parameter.

A trivializing formalization is ruled out: the goal mentions only the run of the mechanism, the expected prices scaled by $\delta$, balancedness and the two expectations. It does not assume the utility or revenue bounds, it does not let an agent's choice see other agents' types, and a supplementary check confirms that its hypotheses are jointly satisfiable. Milestones that involve the proof's deviation $\mathrm{OPT}(\mathbf v',\mathcal F_{\mathbf x(\mathbf v)})$ are stated for an arbitrary selector from $\mathcal F_{\mathbf x}$, a generalization that avoids assuming that the supremum is attained. Theorem 4.2 is stated as $(2,1)$-balanced, which is what its proof establishes; the printed "$(1,2)$" is false.

Useful infrastructure, reusable beyond this mission: measure-preserving coordinate swaps for Measure.pi and products of product measures, ε-maximizer selection for bounded suprema, and induction principles for the sequential run. Contributions of proofs of individual milestones are welcome.

Selected references

• P. Dütting, M. Feldman, T. Kesselheim, B. Lucier, Prophet inequalities made easy: Stochastic optimization by pricing nonstochastic inputs, SIAM J. Comput. 49(3):540–582, 2020. https://doi.org/10.1137/20M1323850
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bull. Amer. Math. Soc. 83(4):745–747, 1977. https://doi.org/10.1090/S0002-9904-1977-14378-4
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12(4):1213–1216, 1984. https://doi.org/10.1214/aop/1176993150
• R. Kleinberg, S. M. Weinberg, Matroid prophet inequalities and applications to multi-dimensional mechanism design, Games Econom. Behav. 113:97–115, 2019. https://doi.org/10.1016/j.geb.2014.11.002
• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, STOC 2010, 311–320. https://doi.org/10.1145/1806689.1806733

Motivation

Maximizing a homogeneous polynomial $p$ over the unit sphere, $p_{\max}=\max_{x\in S^{d-1}}p(x)$, covers the largest stable set of a graph (degree three), the $2\to4$ norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic $p$ it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces "$\gamma-p\ge0$ on the sphere" by "$\gamma-p$ is a sum of squares of polynomials of degree at most $\ell$ on the sphere", giving upper bounds $p_\ell\ge p_{\max}$ that are computable by a semidefinite program of size $d^{O(\ell)}$ and decrease to $p_{\max}$. How fast they converge decides how large $\ell$ has to be for a given accuracy. Fang–Fawzi, §1–1.1

Timeline:

• 1995. Reznick shows, for $p_{\min}=0$, that $p_\ell/p_{\max}\to1$ at rate $d/\ell$ for $\ell$ large enough. Rez95
• 2012. Doherty and Wehner study the same hierarchy on the hypersphere and obtain the same rate. DW12
• 2019. De Klerk and Laurent prove a rate $O(1/\ell^2)$ for a hierarchy of lower bounds on $p_{\max}$, and ask whether the upper bounds $p_\ell$ converge at the same rate. dKL19
• 2019. Fang and Fawzi answer this: for $\ell\ge C_nd$ the error is $O((d/\ell)^2)$, and the statement holds for symmetric matrix-valued polynomials with constants that do not depend on the matrix size. Fang–Fawzi, Theorems 1–2

Setting

Write $x=(x_1,\dots,x_d)$, $\|x\|^2=\sum_ix_i^2$, and $S^{d-1}=\{x\in\mathbb R^d:\|x\|^2=1\}$. A $k\times k$ matrix polynomial $F$ has a real polynomial in each entry, and $F(x)$ is the real matrix of values. $A\succeq0$ means that the symmetric matrix $A$ is positive semidefinite. A matrix polynomial $G$ is $\ell$-sos on $S^{d-1}$ if there are finitely many $k\times k$ matrix polynomials $U_j$, each entry of total degree at most $\ell$, with

$$G(x)=\sum_jU_j(x)U_j(x)^{\mathsf T}\qquad\text{for all }x\in S^{d-1}.$$

For a scalar polynomial $p$, $p_\ell$ is the least $\gamma$ such that $\gamma-p$ (a $1\times1$ matrix) is $\ell$-sos on $S^{d-1}$, and $p_{\min}$ is the minimum of $p$ on $S^{d-1}$. The level value is $+\infty$ when no such $\gamma$ exists.

The milestones use three further objects. A harmonic decomposition of a homogeneous $f$ of degree $2n$ is $f=\sum_{k=0}^n\|x\|^{2(n-k)}f_{2k}$ with $f_{2k}$ homogeneous of degree $2k$ and $\Delta f_{2k}=0$. $B_{2n}$ is the least constant with $\max_{S^{d-1}}|f_{2k}|\le B_{2n}\max_{S^{d-1}}|f|$ for all such $f$ in all dimensions. The Gegenbauer coefficients $\lambda_i(\phi)$ of a univariate polynomial $\phi$ are its coefficients against the orthogonal polynomials $C_i$ for the weight $(1-t^2)^{(d-3)/2}$ on $[-1,1]$, equation (9). For $q$ of degree at most $\ell$, the kernel error is

$$\rho_{2n}(d,\ell)=\min_{\deg q\le\ell,\ \lambda_0(q^2)=1}\ \sum_{k=1}^n\big|\lambda_{2k}(q^2)^{-1}-1\big|.$$

Formalization targets

Goal: Theorem 2 (p. 3)

For every $n$ there are constants $C_n,C'_n$ depending only on $n$ such that, for all $d,k,\ell$ and every $k\times k$ matrix polynomial $F$, homogeneous of degree $2n$ with $n\le d$, symmetric at every $x$, with $0\preceq F(x)\preceq I$ on $S^{d-1}$:

$$\ell\ge C_nd\ \Longrightarrow\ F+C'_n\Big(\frac d\ell\Big)^2I\ \text{is }\ell\text{-sos on }S^{d-1}.$$

The goal fixes only the shape $(d/\ell)^2$ and the regime $\ell\ge C_nd$, and leaves the constants open.

Milestones

They follow the paper's proof, in attack order:

1. Harmonic projection: Lemma 16 (Reznick's bound on $\Delta^kf$), Proposition 5 ($B_{2n}$ is independent of $d$, with $B_2\le2$, $B_4\le9$), the explicit value (34), and Proposition 17 (matrices, spectral norm).
2. Kernels: the Funk–Hecke formula (8), Remark 1, and the first part of Theorem 6: $F+\frac{B_{2n}}2\sum_k|\lambda_{2k}^{-1}-1|\,I$ is $\ell$-sos for every admissible $q$.
3. The kernel error: $C_i'(1)/C_i(1)=i(i+d-2)/(d-1)$, Proposition 18 (tangent line at $1$), Proposition 8 (spectra of Toeplitz matrices of linear functions), the value of $h'(1)$ and the eigenvalue comparison from the proof of Proposition 7, Proposition 9 ($\rho\le\tilde\rho/(1-\tilde\rho)$), and the second part of Theorem 6:

$$\rho_{2n}(d,\ell)\le C_n\Big(\frac d\ell\Big)^2\qquad(\ell\ge C'_nd).$$

4. Corollary: Theorem 1, $1\le\frac{p_\ell-p_{\min}}{p_{\max}-p_{\min}}\le1+(C_nd/\ell)^2$ for $\ell\ge C_nd$.

Significance

Theorem 2 says how the level must grow with the dimension: $\ell=\Theta(d/\sqrt\varepsilon)$ suffices for relative error $\varepsilon$, where Reznick's analysis needs $\ell=\Theta(d/\varepsilon)$. Theorem 10 of the paper shows that, for $n=1$, the kernel error of this technique really is of order $(d/\ell)^2$. Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree $(2n,2)$ on $S^{k-1}\times S^{d-1}$. The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14

The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.

Difficulty

Positive semidefiniteness of $F+\delta I$ at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel $\langle x,y\rangle^{2\ell}$ only reaches error $d/\ell$. Two estimates must be uniform at once. First, harmonic projection of a degree-$2n$ form must be bounded in sup norm independently of $d$; the $L^2$ bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error $\rho_{2n}(d,\ell)$ must be bounded throughout the regime $\ell\ge C_nd$, which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on $\lambda_{\max}$ in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.

Formalization scope

• Objects. $\mathbb R^d$ is Fin d → ℝ (0-based coordinates), and $S^{d-1}$ is the equation $\sum_ix_i^2=1$, not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.
• $\ell$-sos. A finite family of $k\times k$ factors, every entry of total degree at most $\ell$, with equality on the sphere only. Without the degree bound the level disappears; with equality on all of $\mathbb R^d$ Theorem 2 becomes false. Neither change is a faithful reading.
• Constants. In the goal the constants are chosen before $d$, $k$, $\ell$ and $F$. No assumption $d\ge2$ is added: the cases $d=0,1$ are true and elementary.
• Standing assumption $d\ge2$. Every milestone that uses the Gegenbauer objects assumes it, as §2–3 do: the weight $(1-t^2)^{(d-3)/2}$, $\omega_{d-1}/\omega_d$ and the divisions by $d-1$ need it. Gegenbauer polynomials are normalized by $C_i(1)$ and defined by their three-term recurrence. $\sigma$ is the normalized surface measure built from Mathlib's Measure.toSphere.
• $B_{2n}$. It is not defined (it would be a real infimum). Statements quantify over every constant $B$ with the defining property, and $B_{2n}$ is one of them.
• $\rho_{2n}$. It takes values in $[0,\infty]$, with $|\lambda^{-1}-1|=\infty$ at $\lambda=0$ and $\infty$ on an empty feasible set. Its sum runs over $k=1,\dots,n$, following (12), (13) and (16); (10) prints $2n$, a slip. Its minimum is over $\deg q\le\ell$, as in (13). The first part of Theorem 6 is posed per polynomial $q$, which is what (12) proves and implies the printed form.
• Other conventions. Proposition 17's spectral norm is written as $\max_{\|y\|=1}|y^{\mathsf T}Ay|$, and homogeneity of $F$ is explicit there. Theorem 1 is stated cross-multiplied, so that it is meaningful when $p$ is constant on the sphere. Its level value is extended real to record infeasibility; the theorem asserts a finite attained value and a degree-bounded SOS certificate.
• Not posed. Proposition 7 ($\lambda_{\max}(\mathcal T[h])\ge1-\frac{7n}{12}\frac{d^2}{\ell^2}$) fails, for example, at $d=2$, $n=1$, $\ell=10$. The zero bound it quotes and the explicit constants at the end of p. 9 are not posed either; the true first inequality of its proof is.

Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.

Selected references

• K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
• B. Reznick, Uniform denominators in Hilbert's seventeenth problem, Mathematische Zeitschrift 220(1), 75–97, 1995. https://doi.org/10.1007/BF02572604
• A. C. Doherty, S. Wehner, Convergence of SDP hierarchies for polynomial optimization on the hypersphere, arXiv preprint, 2012. https://arxiv.org/abs/1210.5048
• E. de Klerk, M. Laurent, Convergence analysis of a Lasserre hierarchy of upper bounds for polynomial minimization on the sphere, arXiv preprint, 2019. https://arxiv.org/abs/1904.08828
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3), 796–817, 2001. https://doi.org/10.1137/S1052623400366802

Motivation

A decision maker who must choose $x$ to minimize an expected cost $\mathbb E_F[c(x;\xi)]$ rarely knows the distribution $F$ of the uncertain parameter $\xi$; what is available is a sample $\xi^1,\dots,\xi^N$. Sample average approximation (SAA) replaces $F$ by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set $\mathcal F_N$ of distributions built from the data, which protects against the error of the empirical distribution at small $N$. Many such sets have been proposed: moment sets (Delage and Ye, 2010), $\phi$-divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).

Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as $N\to\infty$, its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.

Setting

The support $\Xi\subseteq\mathbb R^d$ of $\xi$ is closed, and $\mathcal P(\Xi)$ is the set of Borel probability distributions on $\Xi$ with the topology of weak convergence. The data $\xi^1,\xi^2,\dots$ are i.i.d. from an unknown $F\in\mathcal P(\Xi)$. A data-driven uncertainty set (DUS) map assigns to each sample $(\xi^1,\dots,\xi^N)$ a set $\mathcal F_N\subseteq\mathcal P(\Xi)$; it is the confidence region of the test that rejects a hypothesis $F_0$ exactly when $F_0\notin\mathcal F_N$. Decisions lie in a closed set $X\subseteq\mathbb R^{d_x}$, the cost is $c(x;\xi)$, and the robust objective is the worst-case expectation

$$\mathcal C(x;\mathcal F_N)=\sup_{F_0\in\mathcal F_N}\mathbb E_{F_0}[c(x;\xi)] .$$

A test is uniformly consistent (Definition 3) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ lies outside $\mathcal F_N$ for infinitely many $N$. The admissible instances are those satisfying three assumptions: (1) $c(\cdot;\xi)$ is equicontinuous in $x$ uniformly over $\xi$; (2) $X$ is bounded, or $c$ is coercive in $x$ uniformly over a set $D$ of positive $F$-probability and bounded below off $D$; (3) $\Xi$ is bounded, or there is a growth function $\phi\ge0$ with $c(x;\xi)=O(\phi(\xi))$ whose expectation the DUS tracks: $\sup_{F_0\in\mathcal F_N}|\mathbb E_{F_0}\phi-\frac1N\sum_i\phi(\xi^i)|\to0$ almost surely. The convergence conditions are (18) $\mathcal C(x;\mathcal F_N)\to\mathbb E_F[c(x;\xi)]$ uniformly on compact subsets of $X$; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.

Formalization targets

Goal: Theorem 2

For a DUS map with nonempty sets,

$$\mathcal F_N\ \text{is uniformly consistent}\iff\Big[\forall F,X,c\ \text{satisfying Assumptions 1–3}:\ (18),(19),(20)\ \text{hold a.s.}\Big].$$

The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.

Milestones

1. Proposition 8: under uniform consistency and Assumptions 1 and 3, almost surely $\mathbb E_{F_N}[c(x;\xi)]\to\mathbb E_F[c(x;\xi)]$ for every $x\in X$ and every sequence $F_N\in\mathcal F_N$.
2. Proposition 9: deterministically, convergence of $\mathcal C(x_N;\mathcal F_N)$ along every convergent $x_N\to x$ implies (18).
3. Theorem 2, "only if" side: uniform consistency implies (18)–(20) a.s. for every admissible instance.
4. Theorem 2, "if" side: if the test is not uniformly consistent, some admissible instance fails (18)–(20) with positive probability.
5. Theorem 3: if $\mathcal F_N$ always contains the empirical distribution and the test is $c$-consistent (Definition 5, consistency with respect to the expected costs only), then (18)–(20) hold a.s.
6. Proposition 4 (first sentence): a uniformly consistent test is consistent in the classical sense, $\mathbb P(F_0\notin\mathcal F_N)\to1$ for each $F_0\neq F$.

Significance

The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the $\chi^2$ and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.

Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.

Difficulty

Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, $x$-dependent cost under the members of $\mathcal F_N$. Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of $\mathbb E_{F_N}[c(x;\xi)]$ from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when $X$ is unbounded. The tempting route through a single limiting minimization problem fails: the sets $\mathcal F_N$ change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of $\mathcal C(\cdot;\mathcal F_N)$ could escape to infinity unless coercivity on $D$ transfers to every member of $\mathcal F_N$. The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.

Formalization scope

Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space $\Xi^{\mathbb N}$ with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence $F_N$. An expectation over a member of $\mathcal F_N$ is $+\infty$ when the integrand is not integrable, never Lean's default $0$. Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large $N$.

Four hypotheses are added to the page, each used by the paper's own proof: every $\mathcal F_N$ is nonempty (otherwise the worst case is $-\infty$ and uniform consistency is vacuous); $c(x;\cdot)$ is continuous on $\Xi$; the set $D$ of Assumption 2b is open; the growth function $\phi$ of Assumption 3b is continuous, with $\mathbb E_F\phi<\infty$ as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at $N=0$ would make the statements false or vacuous, and is ruled out.

A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445v3, https://doi.org/10.1007/s10107-017-1174-z
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• P. Mohajerin Esfahani, D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1

Motivation

The newsvendor problem is the basic single-period inventory decision: a retailer orders $q\ge0$ units at unit cost $c$ before a random demand $\tilde d$ is observed, sells at unit price $p>c$, and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.

Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to $1$ have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an $\alpha$-th moment for an arbitrary real $\alpha>1$. This mission formalizes their result that the zero-order phenomenon survives for every such $\alpha$.

Setting

Write the critical ratio as $\eta=1-c/p\in[0,1)$. A demand law is a probability measure $F$ on $[0,\infty)$. Fix a real $\alpha>1$ and two moments $m_1,m_\alpha$ with

$$m_\alpha>m_1^\alpha>0 .$$

The ambiguity set is

$$\mathcal F_{1,\alpha}=\Big\{F:\ \int_0^\infty w\,dF(w)=m_1,\ \int_0^\infty w^\alpha\,dF(w)=m_\alpha\Big\},$$

the laws on $[0,\infty)$ with mean $m_1$ and $\alpha$-th moment $m_\alpha$. The worst-case expected shortage is

$$\Pi_{1,\alpha}(q)=\sup_{F\in\mathcal F_{1,\alpha}}\mathbb E_F[\tilde d-q]^+ ,$$

and the robust newsvendor problem (3.2) is

$$\min_{q\ge0}\ \big((1-\eta)q+\Pi_{1,\alpha}(q)\big).$$

An optimal order quantity is a minimizer $q^*\ge0$ of this objective. Two thresholds appear:

$$\eta_0=1-\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},\qquad q_0=\frac{\alpha-1}{\alpha}\Big(\frac{m_\alpha}{m_1}\Big)^{1/(\alpha-1)} .$$

In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.

Formalization targets

Goal: Proposition 3.2 (p. 13)

$\eta_0\in(0,1)$, and

• for every $\eta\in[0,\eta_0)$ the set of optimal order quantities is exactly $\{0\}$;
• for every $\eta\in(\eta_0,1)$ an optimal order quantity exists, and every optimal order quantity $q^*$ satisfies $q^*>0$ and

$$q^*\ge q_0 ;$$

• for $\eta=\eta_0$ every $q\in[0,q_0]$ is optimal.

Milestones

1. Proposition 3.1 (p. 12): for $0\le q\le q_0$,

$$\Pi_{1,\alpha}(q)=m_1-q\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},$$

and the two-point law with mass $(m_1^\alpha/m_\alpha)^{1/(\alpha-1)}$ at $(m_\alpha/m_1)^{1/(\alpha-1)}$ and the rest at $0$ lies in $\mathcal F_{1,\alpha}$ and attains the supremum. 2. Properties of $\Pi$ (§2.1, p. 6): $\Pi_{1,\alpha}$ is non-increasing and convex, $\Pi_{1,\alpha}(q)+q=m_1$ for $q\le0$, and $\Pi_{1,\alpha}(q)\to0$ as $q\to\infty$. 3. Display (3.10) (p. 14): for $\eta\in[0,1)$ and $0\le q\le q_0$,

$$(1-\eta)q+\Pi_{1,\alpha}(q)=m_1-q(\eta-\eta_0).$$

Significance

Proposition 3.2 shows that for every finite moment order $\alpha>1$, however high, there is a nonempty interval $[0,\eta_0)$ of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold $\eta_0$ and the minimum positive order $q_0$ in closed form. For $\alpha=2$ it recovers Scarf's zero-order region. The worst-case law associated with $\Pi_{1,\alpha}$ therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).

The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on $[0,\infty)$, of the stop-loss transform $q\mapsto\mathbb E[\tilde d-q]^+$, and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.

Difficulty

The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in $\mathcal F_{1,\alpha}$, including laws with unbounded support and non-integer $\alpha$. The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on $[0,q_0]$. To conclude anything about minimizers on all of $[0,\infty)$, where no closed form is known for general $\alpha$ (the dual leads to equations $aw^\alpha+bw+c=0$, p. 11), one needs convexity of $\Pi_{1,\alpha}$ on the whole line. Inspecting the objective on $[0,q_0]$ alone does not determine the global minimizers.

Formalization scope

• Demand laws are Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.
• $\Pi_{1,\alpha}$ is a real sSup. Under the standing hypotheses $\alpha>1$, $m_1>0$, $m_\alpha>m_1^\alpha$ the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by $m_1+|q|$, so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range $\eta\in[0,1)$ in (3.10), which is the paper's standing range of the critical ratio.
• Optimality is minimization over $q\in[0,\infty)$, as in (3.2), not over $\mathbb R$. Over $\mathbb R$ the objective equals $m_1-\eta q$ for $q\le0$, and part (a) would fail at $\eta=0$.
• Trivializing readings are ruled out. Part (a) asserts that $\{0\}$ is the whole set of minimizers, not only that $0$ is a minimizer. Part (b) asserts that a minimizer exists, so its lower bound is not vacuous. Dropping the support constraint, the normalization, or the integrability clauses would change the problem or let junk integrals satisfy the moment constraints.
• The unit cost and price never appear; everything is stated in $\eta$.
• The ambiguity set, worst-case value and objective come from the shared HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.

Selected references

• B. Das, A. Dhara and K. Natarajan, On the heavy-tail behavior of the distributionally robust newsvendor, Operations Research 69(4), 2021; preprint arXiv:1806.05379v2, 2019. https://arxiv.org/abs/1806.05379
• H. Scarf, A min–max solution of an inventory problem, in K. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, pp. 201–209, Stanford University Press, 1958 (no DOI; reference [42] of https://arxiv.org/abs/1806.05379).

Motivation

Robust Sample Average Approximation (Robust SAA) is a data-driven approach to stochastic optimization proposed by Bertsimas, Gupta and Kallus (arXiv:1408.4445; Mathematical Programming (2018), doi:10.1007/s10107-017-1174-z). Instead of minimizing the empirical average of a cost, a decision maker minimizes the worst-case expected cost over a distributional uncertainty set: the set of distributions that a statistical goodness-of-fit (GoF) test does not reject at a chosen significance level, given the observed data. Each classical GoF test therefore produces its own robust optimization model.

Whether such a model behaves well as data accumulate depends on a property of the test. Theorem 2 of the paper shows that Robust SAA converges, in objective, optimal value and optimal solutions, for every admissible cost if and only if the underlying test is uniformly consistent. This mission concerns the univariate case: it asks for a proof that the five standard tests on the real line, those of Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling, are uniformly consistent (Theorem 5, p. 14). The companion missions of the series treat the characterization (Theorem 2) and the discrete χ² and G-tests (Theorem 4).

Setting

Let $F$ be a probability distribution on $\mathbb R$, and let $\xi^1,\xi^2,\dots$ be independent draws from $F$. As in §3.2 of the paper, $\xi$ is a continuous random variable: $F$ has no atoms. For a candidate distribution $F_0$ write $F_0(t)=F_0((-\infty,t])$ for its cdf, and write $\xi^{(1)}\le\dots\le\xi^{(N)}$ for the sorted sample of size $N$. With $u_i=F_0(\xi^{(i)})$, the five statistics (8) are

$$\begin{aligned} D_N&=\max_{1\le i\le N}\max\Big\{\tfrac iN-u_i,\ u_i-\tfrac{i-1}N\Big\},& V_N&=\max_i\Big(u_i-\tfrac{i-1}N\Big)+\max_i\Big(\tfrac iN-u_i\Big),\\ W_N&=\Big(\tfrac1{12N^2}+\tfrac1N\sum_{i=1}^N\Big(\tfrac{2i-1}{2N}-u_i\Big)^2\Big)^{1/2},& U_N&=\Big(W_N^2-\Big(\tfrac1N\sum_{i=1}^Nu_i-\tfrac12\Big)^2\Big)^{1/2}, \end{aligned}$$ $$A_N=\Big(-1-\sum_{i=1}^N\tfrac{2i-1}{N^2}\big(\log u_i+\log(1-u_{N+1-i})\big)\Big)^{1/2}.$$

For a statistic $S_N$ and a threshold $Q_{S_N}(\alpha)$, the confidence region (7) is $\mathcal F^\alpha_{S_N}=\{F_0: S_N(F_0;\xi^1,\dots,\xi^N)\le Q_{S_N}(\alpha)\}$: the distributions the test does not reject. A test is uniformly consistent (Definition 3, p. 13) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ is rejected infinitely often, i.e. $F_N\notin\mathcal F_N$ for infinitely many $N$. The Lévy metric between cdfs is $d_{\text{Lévy}}(G,G')=\inf\{\epsilon>0: G(\xi-\epsilon)-\epsilon\le G'(\xi)\le G(\xi+\epsilon)+\epsilon\ \forall\xi\}$, and $\hat F_N$ denotes the empirical cdf.

Formalization targets

Goal: Theorem 5

For thresholds $\tau_N$ with $\tau_N\le q/\sqrt N$ for some constant $q$ and all $N\ge1$,

$$\text{the regions }\{F_0: S_N(F_0)\le\tau_N\},\quad S_N\in\{D_N,V_N,W_N,U_N,A_N\},\ \text{are uniformly consistent.}$$

The statement fixes only the rate $O(N^{-1/2})$ of the thresholds, which is all the paper's argument uses; it holds for any sequence with that rate, in particular for the tabulated quantiles $Q_{S_N}(\alpha)$.

Milestones (§10.7, pp. 38–39)

1. $d_{\text{Lévy}}$ metrizes weak convergence on $\mathbb R$; almost surely $d_{\text{Lévy}}(\hat F_N,F)\to0$.
2. $d_{\text{Lévy}}(\hat F_N,F_0)\le D_N(F_0)$, and $D_N\le V_N$.
3. $D_N^2(F_0)\le\max\{1/\sqrt N+3/(2N),\ \sqrt N\,W_N^2(F_0)+2/\sqrt N\}$, and the same with $W_N^2$ replaced by $A_N^2$.
4. $W_N^2-U_N^2=(\tfrac1N\sum_iF_0(\xi^{(i)})-\tfrac12)^2\le\max\{\dots\}$, a bound in terms of $D'_N(F_0)=\max_i|F_0(\xi^{(i)})-\tfrac{2i-1}{2N}|$.

Significance

The result. Together with Theorem 2 of the paper, Theorem 5 guarantees that Robust SAA built on any of these five univariate tests converges for every cost that is equicontinuous in the decision and satisfies the paper's growth conditions. It also feeds Proposition 5, which extends the guarantee to multivariate problems with separable costs by testing marginals. Without it, the univariate tests would carry only the finite-sample guarantee of Proposition 1 and no asymptotic one.

The formalization. The theorem is proved in the paper, but the published argument for the Watson test has a gap. Its last step asserts that $(\tfrac1N\sum_i\min\{1,\tfrac{2i-1}{2N}+D'_N\}-\tfrac12)^2=O(1/N)$ whenever $D'_N\ge1/\sqrt N+1/N$, which fails when $D'_N$ stays bounded away from $0$ (at $D'_N=1/2$ the expression tends to $9/64$). The Watson clause is believed true, but a complete proof needs a different argument. The Anderson–Darling step relies on a cited integral representation rather than an argument on the page. A machine-checked proof would close both points. No part of the theorem is formalized elsewhere, as far as a search of the platform shows.

Difficulty

The Kolmogorov–Smirnov case reduces to deterministic inequalities once the Lévy-metric picture is in place, but each of the other statistics controls $D_N$ only indirectly. The Cramér–von Mises statistic is an $L^2$ quantity, and an $L^2$ bound does not by itself control a supremum. What closes the gap is monotonicity of $F_0$ together with the rate of the threshold, so a threshold that merely tends to $0$ is not enough. The Watson statistic is invariant under cyclic rotation of the transformed sample $u_1,\dots,u_N$ on the circle $[0,1)$, so a small $U_N$ leaves the centring term $\tfrac1N\sum_iF_0(\xi^{(i)})-\tfrac12$ uncontrolled until the boundary constraints $0\le F_0\le1$ are used. The obvious attempt, bounding the centring term by $D'_N$ alone, is the step that fails on p. 39.

Formalization scope

Distributions are MeasureTheory.ProbabilityMeasure ℝ, with weak convergence as their topology. The cdf is Mathlib's ProbabilityTheory.cdf. The data are the coordinates of the canonical product space ℕ → ℝ under Measure.infinitePi, so the sample of size $N$ is $(\omega_0,\dots,\omega_{N-1})$. Order statistics are the sorted sample s ∘ Tuple.sort s, and every formula of (8) is written with the paper's 1-based index ($i$ in Lean is the paper's $i+1$; $\xi^{(N+1-i)}$ is Fin.rev i).

Committed conventions:

• distributions range over all of $\mathbb R$; a support $[\underline\xi,\overline\xi]$ with infinite endpoints is this case;
• the data law has no atoms (§3.2's standing assumption, expressed by the predicate IsContinuousLaw), although the paper's proof does not use it;
• $A_N$ takes values in $[0,\infty]$ and is $+\infty$ when some $F_0(\xi^{(i)})\in\{0,1\}$, so Lean's $\log0=0$ never makes a distribution look close;
• the threshold hypothesis is an explicit constant, $\tau_N\le q/\sqrt N$ for $N\ge1$;
• maxima over an empty index set are $0$, and every fixed-$N$ milestone assumes $N\ge1$.

Uniform consistency is quantified over all sequences $F_N$ inside the almost-sure event, as in Definition 3. A pointwise consistency statement for a fixed $F_0$ is a different and weaker theorem and does not count.

A full development needs the Lévy metric and its metrization of weak convergence on $\mathbb R$, the Glivenko–Cantelli theorem in Lévy form, and elementary order-statistic inequalities. The first two are reusable well beyond this mission. Contributions of independent value include a corrected proof of the Watson step, and a proof of the goal without the atomless hypothesis.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3 (2016); Mathematical Programming (2018). https://arxiv.org/abs/1408.4445, https://doi.org/10.1007/s10107-017-1174-z
• R. M. Dudley, Real Analysis and Probability, Cambridge University Press, 2002, Theorem 11.4.1. https://doi.org/10.1017/CBO9780511755347
• R. B. D'Agostino, M. A. Stephens (eds.), Goodness-of-Fit Techniques, Marcel Dekker, New York, 1986 (reference [14] of the paper; the source of the formulas (8)).