Probability

Motivation

Local Rademacher averages measure the complexity of a learning problem only near the functions that matter, such as those with small empirical error, rather than over the whole function class. Bartlett, Bousquet and Mendelson (Local Rademacher complexities, Ann. Statist. 33 (2005)) show that error bounds for empirical risk minimization are governed by the fixed point of a sub-root upper bound on such local averages, and that these bounds give fast rates ($1/n$ rather than $1/\sqrt n$) under variance conditions. A bound is only useful in practice if it can be computed from the data. For classification with the discrete loss, the paper's Corollary 6.2 states the bound in terms of a localized empirical Rademacher average $\hat\psi_n(r)$. That average is a supremum over a constrained subclass, and it is not obvious how to evaluate it.

Theorem 6.3 of the paper answers this. An upper bound on $\hat\psi_n(r)$ can be computed by any algorithm that minimizes a weighted empirical classification error. A similar reduction was known for the global Rademacher average of a classification class: Bartlett, Boucheron and Lugosi (Model selection and error estimation, Machine Learning 48 (2002)) observed that the empirical Rademacher average equals one half minus an expected empirical risk minimum with random labels, and Lemma 6.4 of the paper is adapted from their argument. Theorem 6.3 shows that localization and the use of star-hulls keep this reduction intact.

Setting

Fix inputs $X_1,\dots,X_n$ in a set $\mathcal X$ ($n\ge1$) and labels $Y_1,\dots,Y_n\in\{-1,1\}$. Everything below is deterministic given this sample. A classifier is a function $f:\mathcal X\to\{-1,1\}$, and $\mathcal F$ is a class of classifiers. The discrete loss is $\ell(y,y')=\mathbf 1[y\ne y']$. For a vector $z\in\mathbb R^n$ write

$$P_n\ell(f(X),z)=\frac1n\sum_{i=1}^n\ell(f(X_i),z_i),\qquad P_n\ell_f=P_n\ell(f(X),Y),$$

so $P_n\ell_f$ is the empirical risk of $f$.

A sign vector $\sigma\in\{-1,1\}^n$ plays the role of Rademacher signs, and $\mathbb E_\sigma$ is the average over all $2^n$ sign vectors. The empirical Rademacher average of the loss functions of the classifiers with empirical risk at most $b$ is

$$\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le b\}=\frac1n\,\mathbb E_\sigma\sup_{f\in\mathcal F,\ P_n\ell_f\le b}\ \sum_{i=1}^n\sigma_i\,\ell(f(X_i),Y_i).$$

For $c\ge0$, $x>0$ and $0<r\le1/2$, the empirical local Rademacher complexity of the classification loss class is

$$\hat\psi_n(r)=c\sup_{\alpha\in[\sqrt{2r},1]}\alpha\,\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le 2r/\alpha^2\}+\frac{26x}{n}.$$

In Corollary 6.2, $c=20$. The parameter $\alpha$ comes from the star-hull of the loss class: rescaling a loss function by $\alpha$ turns the constraint $P_n(\alpha\ell_f)^2\le 2r$ into $P_n\ell_f\le 2r/\alpha^2$.

For a sign vector $\sigma$ and a multiplier $\mu\ge0$, the weighted empirical risk minimum is

$$J(\mu)=\min_{f\in\mathcal F}\frac1n\sum_{i=1}^n|\sigma_i+\mu Y_i|\,\ell\big(f(X_i),\operatorname{sign}(\sigma_i+\mu Y_i)\big).$$

It is the smallest weighted training error when the labels are corrupted to $\operatorname{sign}(\sigma_i+\mu Y_i)$ and example $i$ has weight $|\sigma_i+\mu Y_i|$.

Formalization targets

Goal: Theorem 6.3

If some $f\in\mathcal F$ has $P_n\ell_f\le 2r$, then

$$\hat\psi_n(r)\le c\sup_{\alpha\in[\sqrt{2r},1]}\alpha\,\mathbb E_\sigma\min_{\mu\ge0}\Big(\Big(\frac{2r}{\alpha^2}-\frac12\Big)\mu+\frac1{2n}\sum_{i=1}^n|\sigma_i+\mu Y_i|-J(\mu)\Big)+\frac{26x}{n}.$$

The multiplier $c$ is kept general, and the term $26x/n$ appears on both sides as printed.

Milestones

1. Lemma 6.4. For every $b\in[0,1]$ with a feasible classifier,

$$\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le b\}=\frac12-\mathbb E_\sigma\min\{P_n\ell(f(X),\sigma) : f\in\mathcal F,\ P_n\ell(f(X),Y)\le b\}.$$

2. Weak duality (proof of Theorem 6.3). With $L(f,\mu)=P_n\ell(f(X),\sigma)+\mu(P_n\ell(f(X),Y)-2r/\alpha^2)$ and $g(\mu)=\min_{f\in\mathcal F}L(f,\mu)$, for every $\mu\ge0$,

$$\min\{P_n\ell(f(X),\sigma) : f\in\mathcal F,\ P_n\ell(f(X),Y)\le 2r/\alpha^2\}\ge g(\mu).$$

3. The identity for $g(\mu)$ (proof of Theorem 6.3, corrected).

$$g(\mu)=J(\mu)-\frac1{2n}\sum_{i=1}^n|\sigma_i+\mu Y_i|+\frac{1+\mu}2-\mu\frac{2r}{\alpha^2}.$$

Significance

The theorem turns a quantity defined by a supremum over a data-dependent subclass into one computable by a standard learning primitive. For each sign vector and each multiplier $\mu$, $J(\mu)$ is the value of a weighted classification problem, which any weighted empirical risk minimizer solves. The expectation over signs can be estimated by repeated sampling. The paper notes that $J$ is Lipschitz in $\mu$, so a finite grid of $\mu$ values suffices, and that a sub-root upper bound on $\hat\psi_n$ can then be read off. Combined with Corollary 6.2, this yields error bounds for empirical risk minimization in classification that are computable from the training data and that localize: they depend only on the classifiers with small empirical error.

The result is proved in the paper. It has not been formalized; as far as a search of the Prove2Me catalog shows, neither the classification loss class nor $J(\mu)$ exists as a formal object. This mission produces machine-checked statements of the theorem and of its three proof steps. These cover the exact identity between Rademacher averages of the discrete loss class and random-label empirical risk minimization, and a Lagrangian duality bound for constrained empirical risk minimization.

Difficulty

The obvious route is to apply Lemma 6.4 and then exchange the constrained minimum for a Lagrangian. Each step has a point where a careless argument fails.

• Lemma 6.4 needs a change of variables on sign vectors ($\sigma_i\mapsto-Y_i\sigma_i$) that preserves the uniform average. It also needs the identity $\ell(y,y')=|y-y'|/2$ on $\{\pm1\}$, which fails off $\{\pm1\}$.
• The Lagrangian step gives only weak duality. The bound is an inequality, and attempts to prove equality in Theorem 6.3 fail in general.
• The identity for $g(\mu)$ rests on $\ell(y,\hat y)=(1-y\hat y)/2$. This holds only for $\pm1$ arguments, while $\operatorname{sign}(\sigma_i+\mu Y_i)$ is $0$ when $\mu=1$ and $\sigma_i=-Y_i$. Those terms carry weight zero, and the bookkeeping has to show this.
• Passing the per-$\alpha$, per-$\sigma$ inequalities through the outer supremum and the average requires every supremum and minimum to be over a nonempty, bounded set. This is where the feasibility hypothesis is used.

Formalization scope

• Representation. Inputs are xs : Fin n → X for an arbitrary type X. Labels and signs are real vectors Fin n → ℝ. Classifiers are functions X → ℝ with values in $\{\pm1\}$, a class is a Set (X → ℝ), and the discrete loss is defined on all real pairs. Sign vectors are indexed by Fin n → Bool through the published UnderstandingML.signVec. Every $\mathbb E_\sigma$, on both sides of every statement, is the finite average over these $2^n$ vectors; no probability measure is used. The empirical Rademacher average is the published UnderstandingML.rademacher applied to the set of loss vectors.
• Suprema and minima. Every supremum and minimum is Lean's real ⨆/⨅ over a subtype. The hypotheses make each index set nonempty and each family bounded, so these are true suprema and minima. The convention Real.sign 0 = 0 is used where the paper's sign is undefined; it affects only weight-zero terms.
• Added hypotheses. Each of these is implicit on the page:
  • $n\ge1$;
  • $c\ge0$ (for $c<0$ the inequality reverses);
  • $0<r\le1/2$ (otherwise the range of $\alpha$ is empty);
  • $x>0$ (Corollary 6.2's "fix $x>0$");
  • a classifier with $P_n\ell_f\le 2r$ in the goal, and a feasible classifier in Lemma 6.4 and in the weak duality step (the page's minima presuppose one);
  • a nonempty $\mathcal F$ in the $g(\mu)$ identity.
• Corrections of the print. The last display of the proof on p. 30 ends each line with $-2r/\alpha^2$. From the page's own definition $g(\mu)=\min_f L(f,\mu)$, the constant is $-\mu\,2r/\alpha^2$, which is the form Theorem 6.3's term $(2r/\alpha^2-1/2)\mu$ requires. The milestone states the corrected identity.
• No trivialization. Without the feasibility hypothesis, Lean would evaluate the empty-class Rademacher average and the unbounded $\mu$-minimum to the junk value $0$, and the goal would compare junk values. The feasibility hypothesis rules this out. The goal is the inequality between the two expressions for $\hat\psi_n$ as printed; it is not restated through $g(\mu)$, $L(f,\mu)$ or Lemma 6.4.
• Contributions welcome. A reusable lemma that the uniform average over $\{\pm1\}^n$ is invariant under coordinatewise sign flips would serve beyond this mission, as would general facts about real infima over finite-valued families. Proofs of the three milestones, and of the goal from them, are the main targets.

Selected references

• P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 1497–1537, 2005. arXiv:math/0508275v1 (cited version): https://arxiv.org/abs/math/0508275, DOI https://doi.org/10.1214/009053605000000282 — §6.2, Corollary 6.2 and Theorem 6.3 (pp. 28–29), Lemma 6.4 (p. 29), proof of Theorem 6.3 (p. 30).
• P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48, 85–113, 2002. https://doi.org/10.1023/A:1013999503812
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26 (the Rademacher complexity reused here). https://doi.org/10.1017/CBO9781107298019

Motivation

Multiechelon inventory theory studies supply systems in which stock is held at several levels: here, a depot that orders from an outside supplier and a retail outlet that is replenished from the depot and faces random customer demand. The question is how much to order and ship in each period so as to minimize expected holding, shortage and ordering costs over an infinite horizon. Clark and Scarf (Management Science, 1960) showed that the finite-horizon problem of a serial system decomposes into single-location problems linked by an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) extended the decomposition to the infinite horizon under discounted and average costs, and then asked what it costs to compute an optimal policy.

In the reduced single-location problem the only nonlinear part of the one-period cost is the expected induced penalty $P^L$. Any algorithm for the reduced problem (Veinott–Wagner type policy computations, for instance) evaluates $P^L$ many times. In general each evaluation is a numerical integral. Section 4 of the paper shows that when demand is normal, $P^L$ has a closed form in the univariate and bivariate standard normal distribution functions. This mission formalizes that closed form, eq. (13) on p. 830.

Setting

Time is discrete. One-period demand is $u\sim N(\mu,\sigma^2)$ with $\sigma>0$, independent across periods. For $i\ge1$, $u^{(i)}$ is the total demand over $i$ periods. It is normal with mean $\mu^{(i)}=i\mu$ and standard deviation $\sigma^{(i)}=i^{1/2}\sigma$, density $f^{(i)}$ and cdf $F^{(i)}$. The shipment lead time from depot to outlet is $l\ge0$ and the order lead time from the supplier is $L\ge1$. The cost factors are a system-wide holding cost $h^d>0$, a retailer holding cost $h^r>0$ and a retailer shortage penalty $p^r>0$. Write $p^s=h^d+p^r$. Costs are average costs, so the discount factor is $\alpha=1$ throughout.

The retailer's one-period cost (p. 822) is

$$R(x)=-h^d(x-\mu^{(l)})+p^rE[u^{(l+1)}-x]^++(h^d+h^r)E[x-u^{(l+1)}]^+ .$$

The critical number $x^{r*}$ is a global minimizer of $R$ (property (b), p. 824). The induced penalty cost is $P(x)=0$ for $x\ge x^{r*}$ and $P(x)=R(x)-R(x^{r*})$ for $x<x^{r*}$. Its expectation over the order lead time is

$$P^L(x)=E\,P[x-u^{(L)}]\qquad\text{(eq. (10))}.$$

Let $\Phi$ and $\phi$ be the standard normal cdf and density, $\Theta(z)=z\Phi(z)+\phi(z)$, and $\Phi(\xi_1,\xi_2;\rho)$ the cdf of a bivariate normal pair with standard normal marginals and correlation $\rho$. The paper defines (p. 830)

$$\tau_1(x)=-\frac{x-(x^{r*}+\mu^{(L)})}{\sigma^{(L)}},\quad \tau_2(x)=\frac{x-\mu^{(L+l+1)}}{\sigma^{(L+l+1)}},\quad \nu^{r*}=\frac{x^{r*}-\mu^{(l+1)}}{\sigma^{(l+1)}},$$ $$\tau_3(x)=-\frac{x-(x^{r*}+\mu^{(L)})-[\sigma^{(L)}/\sigma^{(l+1)}]^2[x^{r*}-\mu^{(l+1)}]}{\sigma^{(L)}\sigma^{(L+l+1)}/\sigma^{(l+1)}},$$ $$\epsilon_1(x)=\frac{\Phi[\tau_3(x)]\phi[\tau_2(x)]}{\sigma^{(L+l+1)}},\qquad \epsilon_2(x)=\frac{\Phi(\nu^{r*})\phi[\tau_1(x)]}{\sigma^{(L)}},\qquad \iota(x)=\sigma^{(L)}\Theta[\tau_1(x)],$$ $$\kappa(x)=\sigma^{(l+1)}\Theta(\nu^{r*})\Phi[\tau_1(x)]-\{[\sigma^{(L+l+1)}]^2\epsilon_1(x)-[\sigma^{(L)}]^2\epsilon_2(x)\}-[x-\mu^{(L+l+1)}]\,\Phi[\tau_1(x),\tau_2(x);\rho],$$

with $\rho=-\sigma^{(L)}/\sigma^{(L+l+1)}$.

Formalization targets

Goal: eq. (13)

For every real $x$,

$$P^L(x)=p^s\,\iota(x)-(p^s+h^r)\,\kappa(x).$$

This is an exact identity for every admissible parameter value. It holds with no constants left free.

Milestones

The milestones follow the paper's outline of the derivation on pp. 829–831:

1. eq. (11), $R(x)=p^s[\mu^{(l+1)}-x]+(p^s+h^r)\int_{-\infty}^xF^{(l+1)}(t)\,dt-h^d\mu$;
2. eq. (12), $P^L(x)=\int_{x-x^{r*}}^\infty[R(x-t)-R(x^{r*})]f^{(L)}(t)\,dt$;
3. eq. (14), $P^{L\prime}(x)=-p^s\Phi[\tau_1(x)]+(p^s+h^r)\int_{x-x^{r*}}^\infty F^{(l+1)}(x-t)f^{(L)}(t)\,dt$;
4. eq. (15), the same derivative with the integral replaced by $\Phi[\tau_1(x),\tau_2(x);\rho]$;
5. $P^L(x)\to0$ as $x\to\infty$, hence $P^L(x)=-\int_x^\infty P^{L\prime}(t)\,dt$;
6. $\iota'(x)=-\Phi[\tau_1(x)]$ and $\iota(x)\to0$;
7. the two conditional-normal identities, which give $\Phi[\tau_3(x)]$ and $\Phi(\nu^{r*})$;
8. $\frac{d}{dx}\Phi[\tau_1(x),\tau_2(x);\rho]=\epsilon_1(x)-\epsilon_2(x)$;
9. and 10. the formulas for $\epsilon_1'$ and $\epsilon_2'$;
10. $\kappa'(x)=-\Phi[\tau_1(x),\tau_2(x);\rho]$ and $\kappa(x)\to0$.

Two side remarks of p. 830 are also included: $\Theta'=\Phi$, and the simplified form of $\tau_3$.

Significance

The result. Under normal demand, (13) replaces the numerical integral (12) with a few evaluations of $\Phi$, $\phi$ and the bivariate normal cdf, all available in standard numerical libraries. Together with the decomposition results of Sections 1–3 of the paper, it makes the policy computation for the two-echelon system with normal demand no harder than a single-location computation with an explicit cost function. The same functions reappear in the paper's Section 5 for several retail outlets, after a reinterpretation of $\sigma^{(l+1)}$.

Formalizing it. The paper proves (13) only in outline: it calls the derivation "an elementary integration problem, but … sufficiently involved to warrant an outline" and leaves "tedious algebra" and "more algebra" to the reader. A machine-checked proof turns that outline into a complete argument, including the analytic steps the outline passes over: differentiation under the integral sign, the limits at $+\infty$, and the identification of an integral of normal densities with a bivariate normal probability. To our knowledge no formal proof of (13) exists, and no bivariate normal distribution function is on the platform yet.

Difficulty

The obvious approach is to substitute (11) into (12) and integrate. The result is a double integral of normal densities over a region bounded by a line, and it does not reduce to univariate functions. The paper's route is to differentiate first, identify the derivative (14) as a probability for the correlated pair $(u^{(L)},u^{(L)}+u^{(l+1)})$, and then recover $P^L$ by integrating from $+\infty$. That route needs three things: justification for differentiating under the integral in (12), whose integrand has a kink at $t=x-x^{r*}$; control of the limits at $+\infty$; and the conditional-normal identities, which involve conditioning on a null event and so must be handled through densities. The verification of $\kappa'$ is a long computation with $\Theta$, $\epsilon_1$ and $\epsilon_2$, in which every constant matters.

Formalization scope

Everything lives in the namespace FZEchelon.NormalDemand. The model data form the structure Data (fields $\mu,\sigma,h^d,h^r,p^r,l,L,x^{r*}$). The law of $u^{(i)}$ is the platform's normal demand law InventoryControl.newsboyDemand with mean $i\mu$ and standard deviation $\sqrt i\,\sigma$. Expectations are Bochner integrals, and improper integrals are set integrals over Set.Ioi/Set.Iic. $\Phi$ is cdf (gaussianReal 0 1). The bivariate cdf is the iterated integral of the explicit bivariate density over a lower-left quadrant (meaningful for $|\rho|<1$; here $\rho\in(-1,0)$). Derivatives are HasDerivAt and limits are Tendsto … atTop (𝓝 0).

Standing hypotheses of every theorem: $\sigma>0$; $h^d,h^r,p^r>0$ (p. 821); $L\ge1$; and $x^{r*}$ minimizes $R$. Two of these are added to the page and disclosed. $\sigma>0$ is needed because every $\tau$ divides by some $\sigma^{(i)}$. $L\ge1$ is needed because $\sigma^{(0)}=0$, and the paper treats zero order lead time separately (p. 819). Demand is exactly normal, as in §4, which acknowledges that this violates $u\ge0$ and ignores the objection. No nonnegativity, truncation or approximation enters. The goal fixes $\alpha=1$, the average-cost case the section restricts to. The discounted analogue is not part of this mission.

A trivializing formalization is ruled out: every Bochner integral in the statements has an integrable integrand, since integrands grow at most linearly and the normal law has all moments. No division by a zero standard deviation can occur under the hypotheses. A sorry-free check in the workspace shows that all hypotheses hold together, with a minimizer $x^{r*}$ of $R$ proved to exist.

Needed infrastructure: properties of gaussianReal (moments, convolution of independent normals), differentiation of parametric integrals, and a bivariate normal distribution function with its partial derivatives. A reusable treatment of the bivariate normal cdf, linking the density form used here to Mathlib's multivariateGaussian, would be a contribution of independent value. Proofs of individual milestones are welcome in any order.

Selected references

• 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
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525

Motivation

Periodic-review inventory systems face a simple choice each period: how much to order before the next demand is known. When unmet demand is lost, the order can affect the stock available several periods later without preserving a backlog that records earlier shortages. This makes the optimal policy difficult to describe when replenishment takes time. An order-up-to policy offers a practical rule: order enough to bring the inventory position to a fixed level. Huh, Janakiraman, Muckstadt and Rusmevichientong ask when that simple rule performs as well as the best admissible lost-sales policy as the penalty for a lost unit grows. Their working paper, pp. 3–4 and 17–18, proves asymptotic optimality for a particular level obtained from a related backorder system.

The motivating costs are concrete. A lost sale may represent an expedited service part or a missed sale whose cost is much larger than one period of holding inventory. The paper's central comparison concerns the high-penalty regime while holding the demand law, lead time and holding rate fixed. The fixed-level policy can be computed from the distribution of demand over the lead time plus the order period; it does not require solving the full lost-sales control problem. The paper also supplies a finite-penalty bound, which this mission retains as a milestone. Huh et al., pp. 3–4, 17–18.

Setting

Let $D_1,D_2,\ldots$ be independent, identically distributed nonnegative demands with finite positive mean. An order takes a fixed integer lead time $\tau\ge1$ to arrive. At the start of period $t$, the order placed $\tau$ periods earlier arrives; then a new order is placed, and demand $D_t$ is observed. Unmet demand is lost. At period end, each unit remaining on hand incurs holding cost $h>0$, and each lost unit incurs penalty $b>0$. The inventory position counts on-hand units and outstanding orders. An order-up-to-$S$ policy raises this position to $S\ge0$ whenever possible.

Write $C^{\mathcal L,S}(h,b)$ for the long-run average cost of that policy and $C^{\mathcal L*}(h,b)$ for the infimum over admissible policies. The corresponding backorder system retains unmet demand as negative net inventory and charges $b$ per backordered unit per period. For an order-up-to level $S$, its stationary average cost is

$$C^{\mathcal B,S}(h,b)=h\mathbb E[(S-\mathbf D)^+]+b\mathbb E[(\mathbf D-S)^+],\qquad \mathbf D=\sum_{i=1}^{\tau+1}D_i.$$

The newsvendor level $S^{\mathcal B*}(h,b)$ is the smallest nonnegative $S$ with $\Pr(\mathbf D\le S)\ge b/(b+h)$; it attains the best backorder order-up-to cost $C^{\mathcal B*}(h,b)$. The paper's Assumption 1 concerns this lead-time demand $\mathbf D$: if $m_{\mathbf D}(t)=\mathbb E[\mathbf D-t\mid\mathbf D>t]$ when the conditioning event has positive probability and zero otherwise, then $m_{\mathbf D}(t)/t\to0$ as $t\to\infty$. Huh et al., pp. 3–4, 9, 11–12.

Formalization targets

Asymptotically optimal order-up-to level

Fix $h$, $\tau$ and the demand law satisfying Assumption 1. Set $S_{b+\tau h}=S^{\mathcal B*}(h,b+\tau h)$. The goal is the equivalent multiplicative form of Theorem 15(b): for every $\varepsilon>0$, all sufficiently large $b$ satisfy

$$\inf_{S\ge0}C^{\mathcal L,S}(h,b)\le C^{\mathcal L,S_{b+\tau h}}(h,b)\le(1+\varepsilon)C^{\mathcal L*}(h,b).$$

The infimum over order-up-to levels captures the paper's best such policy. The right-hand comparator remains the infimum over all admissible lost-sales policies. The multiplicative form also covers an almost-surely constant demand law, where both costs can be zero and a literal ratio would be undefined. Huh et al., Theorem 15(b), p. 17.

Explicit finite-penalty bound

Theorem 15(a) is a milestone. With $S'=S^{\mathcal B*}(h,b/(\tau+1))$ and $\psi(S';h,q)=q\mathbb E[(\mathbf D-S')^+]/(h\mathbb E[(S'-\mathbf D)^+])$, its factor is

$$\frac{1+\nu_b\psi(S';h,b/(\tau+1))}{1+\psi(S';h,b/(\tau+1))},\qquad \nu_b=\frac{(b+\tau h)(\tau+1)}{b}.$$

The milestone states the bound where the expected holding quantity in $\psi$ is positive. Earlier milestones state the pathwise comparison of the systems, the two-sided average-cost comparison with penalties $b/(\tau+1)$ and $b+\tau h$, the lower bound on unrestricted lost-sales optimal cost, the newsvendor formula, and the backorder sensitivity results used by the theorem. Huh et al., Lemmas 5, 9, 13 and Theorems 6, 15, pp. 11–18.

Significance

The theorem gives a specific computable stock level whose relative cost loss vanishes in the high-penalty regime. It addresses the gap between a tractable backorder benchmark and the more difficult lost-sales control problem. The finite-penalty factor states how the comparison depends on lead time, holding cost, penalty and the shortage-to-holding ratio; the asymptotic statement alone would not quantify that dependence. The paper establishes these mathematical results; the mission asks for machine-checked proofs of the stated Lean targets. Huh et al., pp. 17–18.

Formalizing the result would also supply reusable infrastructure for coupled inventory systems: measurable demand-path laws, pathwise recursions with delayed delivery, extended nonnegative long-run costs, and a clean comparison between an explicit policy and the infimum over unrestricted policies. The backorder newsvendor and mean-residual-life components can be reused beyond this particular lost-sales model.

Difficulty

The backorder system has a closed stationary cost formula, while a lost-sales order-up-to process generally cannot be replaced directly by that formula. The paper notes that its on-hand inventory distribution need not converge from every starting state, even under a fixed order-up-to policy. One must therefore justify the long-run comparison without assuming stationarity from an arbitrary start. A second difficulty is the benchmark: comparing only against other order-up-to policies is too weak to establish Theorem 15, because the goal uses the optimal cost over all admissible lost-sales policies. Huh et al., pp. 14–16, 18.

Formalization scope

Lean reuses the published CappedBaseStock lost-sales model. Its demands are nonnegative and i.i.d. with finite positive mean; $\tau\ge1$ and $h,b>0$. Period zero in Lean is period one in the paper. Both coupled processes start with zero on-hand stock and an empty pipeline. Inventory $X_t$ is read immediately after delivery, before current demand. Lost-sales costs lie in $[0,\infty]$ and use the limsup of expected Cesàro averages; the backorder closed form uses real Bochner expectations under finite-mean demand. The paper's stationary lost-sales cost and this Cesàro cost are identified using its long-run results, but those convergence results are outside this proposal. Huh et al., pp. 14–16.

The paper prints nonnegative rates in Theorem 15, while its displayed newsvendor fraction and shortage-to-holding ratios require positive denominators. Theorem 6(a) therefore states the ratio limit for nonconstant demand laws. The main theorem uses a multiplicative limit bound that also covers constant demand, where the printed ratio is undefined.

The quantity $C^{\mathcal L*}$ is an infimum over measurable, history-dependent policies with private randomization; no attaining policy is assumed. The backorder optimum is an infimum over nonnegative order-up-to levels. Assumption 1 is imposed on the sum of $\tau+1$ demands, and the limit $b\to\infty$ is expressed by a positive threshold uniform over all parameter records with the fixed lead time and holding rate. The mission excludes a restricted policy comparator, a fixed penalty, a one-period lead-time specialization, and Assumption 1 on single-period demand. Solvers may contribute proofs of any milestone, along with finite-mean and measurability lemmas needed to connect the model to the backorder benchmarks.

Selected references

• W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems, working paper, December 4, 2006; published in Management Science 55(3), 2009. DOI: 10.1287/mnsc.1080.0945.
• G. Janakiraman, S. Seshadri and G. Shanthikumar, A Comparison of the Optimal Costs of Two Canonical Inventory Systems, working paper, Stern School of Business, New York University, 2005; bound quoted in Huh et al., §5, p. 13. Quoted source.

Motivation

Data-dependent risk bounds in statistical learning replace combinatorial quantities such as the VC dimension with averages of how well a function class can fit random noise on the observed sample. Bartlett and Mendelson's article (JMLR 3, 2002) established these averages, the Rademacher and Gaussian complexities, as a general tool: a risk bound (their Theorem 8) holds with a complexity penalty, and the complexity of a complicated class can be bounded through structural results that relate it to the complexities of simpler classes.

This mission formalizes two of those structural results, both stated for Gaussian complexities. The first (Theorem 14) controls a Lipschitz function of several real-valued classes at once, the vector-valued analogue of the classical contraction principle. The second (Theorem 16) controls an arbitrary fixed boolean combination of classes of classifiers, such as intersections, unions or majority votes of a fixed number of base classifiers, by the sum of the complexities of the components. Such combinations arise whenever a classifier is assembled from simpler ones, for instance in decision lists, small decision trees over a base class, or voting schemes.

Setting

Let $\mathcal X$ be a set, $\mu$ a probability measure on it, and $n \ge 1$ a sample size. For a class $F$ of functions $\mathcal X \to \mathbb R$ and a sample $x = (x_1, \dots, x_n)$, the empirical Gaussian complexity is

$$\hat G_n(F)(x) = \mathbb E\left[\sup_{f\in F}\left|\frac2n\sum_{i=1}^n g_i f(x_i)\right|\right],$$

with $g_1, \dots, g_n$ independent standard Gaussian $N(0,1)$ variables, and the Gaussian complexity is $G_n(F) = \mathbb E\, \hat G_n(F)(X_1, \dots, X_n)$ for $X_1, \dots, X_n$ i.i.d. with law $\mu$ (Definition 2, p. 464). In Lean these are empiricalGaussian n F x and gaussianComplexity μ n F.

Three constructions of classes appear.

• Direct sum. With $\mathcal A = \mathbb R^m$ carrying the Euclidean distance, a class $F$ of maps $\mathcal X \to \mathcal A$ is a subset of the direct sum of real classes $F_1, \dots, F_m$ when each $f \in F$ is $x \mapsto (f_1(x), \dots, f_m(x))$ with $f_i \in F_i$ (SubsetDirectSum F Fi).
• Composition. For $\phi : \mathcal Y \times \mathcal A \to \mathbb R$, $\phi \circ f$ is $(x, y) \mapsto \phi(y, f(x))$ and $\phi\circ F$ collects these (compClass φ F).
• Boolean combination. For $g : \{\pm1\}^k \to \{\pm1\}$ and classes $F_1, \dots, F_k$ of $\{\pm1\}$-valued functions, $g(F_1, \dots, F_k) = \{x \mapsto g(f_1(x), \dots, f_k(x)) : f_j \in F_j\}$ (boolComb g F).

A centred Gaussian process indexed by a finite set $I$ is a family $(X_i)_{i \in I}$ of real random variables whose finite-dimensional laws are jointly Gaussian with mean zero; $\|X_i - X_j\|_2 = (\mathbb E(X_i - X_j)^2)^{1/2}$.

Formalization targets

Goal: Theorem 16 (p. 472)

For a fixed boolean function $g : \{\pm1\}^k \to \{\pm1\}$ with $k \ge 1$ and classes $F_1, \dots, F_k$ of $\{\pm1\}$-valued functions,

$$G_n\bigl(g(F_1, \dots, F_k)\bigr) \le 2 \sum_{j=1}^k G_n(F_j).$$

Milestones

1. Lemma 13 (p. 471), the comparison of Gaussian processes as printed: if $\|X_i - X_j\|_2 \le \|Y_i - Y_j\|_2$ for all $i, j$, then $\mathbb E\sup_i X_i \le 2\,\mathbb E\sup_i Y_i$.
2. Theorem 14 (p. 471): if each $\phi(y, \cdot)$ is $L$-Lipschitz for the Euclidean distance, passes through the origin, and $\phi$ is uniformly bounded, then for every sample $(x_k, y_k)_{k \le n}$,

$$\hat G_n(\phi \circ F) \le 2L \sum_{i=1}^m \hat G_n(F_i).$$

3. The extension of $g$ (proof of Theorem 16, p. 472): $g(x) = (1 - \|x - a\|)g(a)$ when $\|x - a\| < 1$ for a cube vertex $a$, and $0$ otherwise, is well defined, extends $g$, maps into $[-1,1]$, vanishes at $0$ and is $1$-Lipschitz.

Significance

Theorem 16 turns any bound on the Gaussian complexity of base classes into a bound for a fixed boolean combination of them, at the cost of a factor $2$ on the sum of their complexities, whatever $g$ and $k$ are. Together with the comparison between Gaussian and Rademacher complexities (Lemma 4 of the paper) and the risk bound of Theorem 8, it yields generalization bounds for classifiers built as combinations of base classifiers. Theorem 14 is the general tool: it handles any Lipschitz loss of a vector-valued predictor, such as multiclass margins, through the complexities of its coordinate classes.

All three results are proved in the paper (Lemma 13 is classical and cited from Pisier). None of them is formalized on Prove2Me; the finite-dimensional Sudakov–Fernique inequality, with constant $1$, is (HighDimProb.RandomProcesses.sudakov_fernique_finite_dim). This mission produces machine-checked versions of the vector contraction for Gaussian averages and of the boolean-combination bound, and records the corrections the printed statements need.

Difficulty

The obvious approach to Theorem 14 compares two Gaussian processes indexed by the class, but Definition 2 takes the supremum of an absolute value scaled by $2/n$, while Gaussian comparison inequalities bound the expected supremum of the process itself. The printed proof equates the two; done carefully, the comparison with the printed constant $2$ of Lemma 13 gives only $4L$. Reaching the printed $2L$ requires a comparison with constant $1$ and an argument that handles the absolute value. A second difficulty is that the classes may be infinite and unbounded, so expected suprema must be handled as extended-valued quantities, and the reduction to finite classes ("without loss of generality") must be justified. For Theorem 16 the extension of $g$ must be checked to be Lipschitz across the boundaries of the tents in the Euclidean, not the sup, norm.

Formalization scope

The source is the published JMLR article (vol. 3, 2002, pp. 463–482), not the COLT 2001 version, whose numbering differs.

• Complexities in $[0, \infty]$. $\hat G_n$ and $G_n$ are lower Lebesgue integrals of an ENNReal supremum against $N(0,1)^{\otimes n}$ and $\mu^{\otimes n}$. An unbounded class has complexity $+\infty$; a real-valued supremum or Bochner integral would silently return $0$ there and make the upper bounds false, so that encoding is ruled out. No finiteness or boundedness of any class is assumed.
• $\mathcal A = \mathbb R^m$ is EuclideanSpace ℝ (Fin m), so "Lipschitz" refers to the Euclidean distance as printed. Using Fin m → ℝ (the sup distance) would change the theorem.
• $\{\pm1\}$ is encoded as $\mathbb Z^\times$ coerced to $\mathbb R$.
• Lemma 13: centred processes added. As printed the lemma is false: $X_i \equiv 5$, $Y_i \equiv 0$ satisfy the hypothesis. Both processes are assumed mean zero, as in Slepian's lemma. The two processes may live on different probability spaces; the index set is any finite nonempty type. The constant $2$ is kept as printed.
• Theorem 14: printed proof loose, statement kept. The constant $2L$ is kept as printed; the statement is true via the constant-$1$ comparison. The uniform-boundedness hypothesis on $\phi$ is kept as printed although the extended-valued formulation does not need it.
• Theorem 16 and the extension: $k \ge 1$ added. For $k = 0$ the boolean function is a constant $\pm1$, the right side is $0$, and the left side is $\mathbb E\frac2n|\sum_i g_i| > 0$; also the extension would have $g(0) = \pm1$.
• Theorem 16: measurability guard. Each $\hat G_n(F_j)$ is assumed almost-everywhere measurable as a function of the sample, so that the expectation of $\sum_j \hat G_n(F_j)$ is the sum of the expectations. The paper does not discuss measurability.

A complete development needs Gaussian comparison for finite index sets (available on the platform), the reduction from infinite to finite classes for extended-valued suprema, and elementary Euclidean geometry of the cube. The first two are reusable for every Gaussian-average argument in learning theory. Proofs of any milestone, and of the constant-$1$ variant of Lemma 13 transported between probability spaces, are welcome.

Selected references

• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• G. Pisier, The Volume of Convex Bodies and Banach Space Geometry, Cambridge University Press, 1989. https://doi.org/10.1017/CBO9780511662454
• M. Ledoux, M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

A decision maker choosing a random outcome $X$ (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome $Y$, the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: $X$ is preferred to $Y$ by every decision maker with a concave nondecreasing utility function $u$ exactly when $X$ dominates $Y$ in the second order, $X\succeq_{(2)}Y$. Requiring $X\succeq_{(2)}Y$ as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.

Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal L^1=\mathcal L^1(\Omega,\mathcal F,P)$ the space of integrable random variables with its norm topology. For $X\in\mathcal L^1$ the distribution function is $F(X;\eta)=P[X\le\eta]$ and the second-order shortfall function is

$$F_2(X;\eta)=\int_{-\infty}^{\eta}F(X;\alpha)\,d\alpha,\qquad \eta\in\mathbb R. \tag{2.1}$$

Changing the order of integration gives $F_2(X;\eta)=\mathbb E[(\eta-X)_+]$ (2.6), where $(\cdot)_+=\max(0,\cdot)$. The relation $X\succeq_{(2)}Y$ means $F_2(X;\eta)\le F_2(Y;\eta)$ for all $\eta$, and $A_2(Y)=\{X\in\mathcal L^1:X\succeq_{(2)}Y\}$.

The problem data are a reference outcome $Y\in\mathcal L^1$, a convex closed set $C\subseteq\mathcal L^1$, a functional $f$ that is concave and continuous on $C$, and an interval $[a,b]$. The paper studies the relaxation in which dominance is enforced on $[a,b]$:

$$\max f(X)\quad\text{subject to}\quad\mathbb E[(\eta-X)_+]\le\mathbb E[(\eta-Y)_+]\ \ \text{for all }\eta\in[a,b],\qquad X\in C. \tag{3.1–3.3}$$

The uniform dominance condition (Definition 4.1) asks for some $\tilde X\in C$ with $\inf_{\eta\in[a,b]}\{F_2(Y;\eta)-F_2(\tilde X;\eta)\}>0$.

The multiplier class $\mathcal U_1$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge0$. The Lagrangian is

$$L(X,u)=f(X)+\mathbb E[u(X)]-\mathbb E[u(Y)]. \tag{4.1}$$

Formalization targets

Goal: Theorem 4.2

Assume the uniform dominance condition. If $\hat X$ is an optimal solution of (3.1)–(3.3), there is $\hat u\in\mathcal U_1$ with

$$L(\hat X,\hat u)=\max_{X\in C}L(X,\hat u)\quad(4.2)\qquad\text{and}\qquad\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)].\quad(4.3)$$

Conversely, if for some $\hat u\in\mathcal U_1$ a maximizer $\hat X\in C$ of $L(\cdot,\hat u)$ satisfies (3.2) and (4.3), then $\hat X$ is optimal for (3.1)–(3.3).

Milestones

The milestones follow the paper's proof. They are: finiteness of $\mathbb E[u(X)]$ for $u\in\mathcal U_1$; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of $A_2(Y)$, and its recession cone); the concavity of the constraint operator $G(X)(\eta)=F_2(Y;\eta)-F_2(X;\eta)$ with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier $\hat\mu$ on $[a,b]$ satisfying (4.5)–(4.6); the facts that the function $u_\mu(t)=-\int_t^b\mu([\tau,b])\,d\tau$ ($t<b$), $u_\mu(t)=0$ ($t\ge b$) of a nonnegative measure lies in $\mathcal U_1$ and that every $u\in\mathcal U_1$ is $u_\mu$ for exactly one $\mu$; the key identity

$$\int_a^b F_2(X;\eta)\,d\mu(\eta)=-\mathbb E[u_\mu(X)]; \tag{4.9}$$

and the weak-duality step: (3.2) implies $\mathbb E[u(X)]\ge\mathbb E[u(Y)]$ for every $u\in\mathcal U_1$.

Further: Theorem 5.1

With $D(u)=\sup_{X\in C}L(X,u)$, the dual problem $\min_{u\in\mathcal U_1}D(u)$ has a solution, its value equals the primal optimal value, and its solutions are exactly the $\hat u\in\mathcal U_1$ satisfying (4.2)–(4.3).

Significance

Theorem 4.2 turns an infinite family of constraints, one for each $\eta\in[a,b]$, into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility $\hat u$, and the dominance constraint is active exactly in the sense $\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)]$. Theorem 5.1 makes $\mathcal U_1$ the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).

All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant $c$). The definitions of $F_2$ and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).

Difficulty

The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space $\mathcal C([a,b])$; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on $[a,b]$, an element of the dual of $\mathcal C([a,b])$. A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of $\mathbb R$, is relaxed to a bounded interval $[a,b]$: for a reference outcome with a smallest value $y_1$, $F_2(Y;y_1)=0$, so no $\tilde X$ can dominate $Y$ strictly near $y_1$.

The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over $\mathbb R\times[a,b]$ and an integration by parts against the distribution function of an arbitrary integrable $X$, followed by a limit in which the integrability of $X$ controls the linear growth of $u$ at $-\infty$. The converse direction needs every $u\in\mathcal U_1$ to be represented by a unique measure, through the left derivative of a concave function.

Formalization scope

Outcomes are elements of Mathlib's $L^1$ space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in $\omega$. $F_2$ is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of $P[X\le\alpha]$ over $(-\infty,\eta]$. The problem data form a structure whose fields include every standing assumption of the paper: $C$ convex and closed, $f$ concave and continuous on $C$. The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use $F_2$, as printed; their equality is (2.6).

Committed conventions:

• $\mathcal U_1$ uses $c\ge0$. The paper prints $c>0$. With $c>0$ the necessity half of Theorem 4.2 is false: take $Y\equiv0$, $[a,b]=[1,2]$, $f(X)=\mathbb EX$ and $C$ the constant random variables with values in $[0,1]$. Then $\tilde X\equiv1$ satisfies Definition 4.1, $\hat X\equiv1$ is optimal, and (4.3) forces $c=0$. The proof itself produces $c=\mu([a,b])$, which vanishes for the zero multiplier of a slack constraint, and the paper calls $\mathcal U_1$ a convex cone, which must contain $0$.
• Definition 4.1's infimum is encoded as a positive lower bound $\varepsilon$ on $[a,b]$. "$=\max_{X\in C}$" is encoded as membership in $C$ plus an upper bound over $C$.
• A nonnegative measure in $\mathbf{rca}([a,b])$ is a finite Borel measure on $\mathbb R$ giving zero mass to the complement of $[a,b]$, which is the paper's own extension by zero. Integrals $\int_a^b\cdot\,d\mu$ are over the closed interval, so atoms at $a$ and $b$ count.
• No relation between $a$ and $b$ is assumed. For $a>b$ every statement remains meaningful: the constraint is vacuous and $\mathcal U_1=\{0\}$.
• Theorem 5.1's dual function takes values in the extended reals.

A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to $0$) cannot occur for $u\in\mathcal U_1$, and its integrability is a milestone. Dropping the concavity of $f$ or the convexity of $C$ would make the necessity half false, so these assumptions are fields of the problem data.

Infrastructure a complete development needs: convex duality for cone constraints in $\mathcal C([a,b])$ (or a direct separation argument in $\mathbb R\times\mathcal C([a,b])$), the Riesz representation of nonnegative functionals on $\mathcal C([a,b])$, Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.

Selected references

• D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, preprint dated December 27, 2002 (Stochastic Programming E-Print Series); published in SIAM Journal on Optimization 14(2):548–566, 2003. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• J. F. Bonnans and A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.

Motivation

The multi-secretary problem is the simplest model of capacity allocation under uncertainty: a decision maker sees $n$ candidates one at a time and may hire at most $k$ of them, with every decision final. The same structure underlies single-resource revenue management (accepting or rejecting booking requests against a fixed inventory; see Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004), online knapsack and packing problems, and dynamic assortment of limited stock.

The performance of an online policy is measured against the offline benchmark, the value of the best $k$ candidates chosen with full hindsight. The gap between the two is the regret.

• In the version where the values arrive as a uniform random permutation, Kleinberg (2005) proved that the minimal regret is of order $\sqrt k$ and gave an algorithm attaining it (as summarized in Remark 1 of the paper below).
• Arlotto and Gurvich (arXiv:1710.07719, 2017; Stochastic Systems 2019) showed that when the values have a finite support, the optimal online policy, and an explicit simple policy, have regret bounded by a constant that does not depend on $n$ or $k$. The constant depends only on the smallest probability mass.

This mission formalizes that upper bound.

Setting

Abilities take values in a finite set $\mathcal A=\{a_m<a_{m-1}<\dots<a_1\}$ of distinct positive reals, with probabilities $f_j=\mathbb P(X=a_j)>0$, $\sum_j f_j=1$. Write $\bar F(a_j)=f_1+\dots+f_{j-1}$ for the mass strictly above $a_j$, and

$$\epsilon=\tfrac12\min\{f_m,\dots,f_1\}.$$

The abilities $X_1,\dots,X_n$ are independent with this distribution. Budget pairs range over the triangle $\mathcal T=\{(n,k):0\le k\le n\}$.

• Offline value. $V^*_{\mathrm{off}}(n,k)=\mathbb E\big[\max\{\sum_t X_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\}\big]$.
• Online policies. A policy decides $\sigma_t\in\{0,1\}$ using only $X_1,\dots,X_t$ and must select at most $k$ candidates on every realization. $\Pi(n,k)$ is the set of such policies, $V^\pi_{\mathrm{on}}(n,k)=\mathbb E[\sum_t X_t\sigma^\pi_t]$, and $V^*_{\mathrm{on}}(n,k)=\max_{\pi\in\Pi(n,k)}V^\pi_{\mathrm{on}}(n,k)$.
• Counts. $Z^r_j$ is the number of $a_j$-candidates among the first $r$. The offline sort selects $\mathfrak S^r_j=\min\{Z^r_j,(k-\sum_{i<j}Z^r_i)_+\}$ of them. $S^{\pi,r}_j$ counts those selected by $\pi$.
• Action index. $j_0(n,k)$ is the largest $j$ with $\bar F(a_j)+\tfrac12f_j\le k/n$, or $1$ if there is none.
• Thresholds. $T_1=0$, $T_j=\bar F(a_j)+\tfrac12 f_j$ for $2\le j\le m$, and $T_{m+1}=+\infty$.
• Budget-Ratio (BR) policy. With remaining budget $K_t$ ($K_0=k$), at time $t+1$ the policy finds $j$ with $T_j\le K_t/(n-t)<T_{j+1}$. It selects $X_{t+1}$ if and only if $K_t>0$ and $X_{t+1}\ge a_j$.
• Stopping times. For $0<\delta<\epsilon$, $\tau_0$ is the first time the budget ratio comes within $\delta/2$ of a threshold, or the cut-off $n-2\delta^{-1}-1$. The time $\tau$ of (20) is the first later time the ratio leaves the $\delta$-band around that threshold, or the cut-off.

Formalization targets

Goal: Theorem 1 (first display)

For every $\epsilon>0$ there is a constant $M$ such that for every instance with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)\in\mathcal T$, $\mathrm{br}\in\Pi(n,k)$ and

$$V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{on}}(n,k)\le V^*_{\mathrm{off}}(n,k)-V^{\mathrm{br}}_{\mathrm{on}}(n,k)\le a_1M.$$

No constant is fixed. Only the shape is asserted: a bound uniform in $n$, $k$, the support size and the distribution, given $\epsilon$.

Milestones, in the order the proof uses them

• The benchmark inequality $V^\pi_{\mathrm{on}}\le V^*_{\mathrm{off}}$ (p. 5).
• The sort identity $V^*_{\mathrm{off}}=\sum_ja_j\mathbb E[\mathfrak S^n_j]$ (4).
• The binomial overshoot bound $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ (Lemma 2).
• The offline decomposition $V^*_{\mathrm{off}}=\sum_{i<j}a_i\mathbb E[Z^n_i]+a_j\mathbb E[\mathfrak S^n_j]+a_{j+1}\mathbb E[\mathfrak S^n_{j+1}]\pm a_1/(4\epsilon)$ (Proposition 1).
• The sufficient condition: four properties (i)–(iv) of a policy up to a stopping time imply regret at most $3a_1M+a_1/(4\epsilon)$ (Proposition 2).
• The identification $j_0(n,k)=j$ on $k/n\in[T_j,T_{j+1})$ (p. 17).
• The BR selection probability and the jump bound $|K_t/(n-t)-K_{t+1}/(n-t-1)|\le\delta/2$ (p. 13).
• $\mathbb E[\tau]\ge n-M$ (Theorem 2).
• BR and $\tau$ satisfy (i)–(iv) (Corollary 1).
• The state-space reduction $v_\ell(w,\kappa)=w+g_\ell(\kappa)$ of the Bellman recursion (Proposition 5).

Significance

The result. Bounded regret means that the loss from not knowing the future is a fixed number of candidates' worth of value, however long the horizon and however large the budget. The bound holds uniformly over all distributions with the same $\epsilon$. It is attained by an explicit, adaptive, non-randomized rule that compares one ratio with $m$ fixed thresholds. The companion result of the same paper shows that every non-adaptive policy suffers regret of order $\sqrt n$ in the interior regime. Together they quantify the value of adapting to the remaining budget. Lemma 1 of the paper shows the dependence on $\epsilon$ cannot be removed.

Formalizing it. The result is proved in the paper, but no part of it is machine-checked; there is no multi-secretary or bounded-regret development on the platform. The mission produces several pieces of machinery: a reusable finite model of sequential selection with online policies and the offline benchmark; an explicit online policy with its stopping-time analysis; and a binomial overshoot bound usable elsewhere. The constant $M$ is not made explicit in the paper. A formal proof would give one, and sharper constants are welcome.

Difficulty

The offline decomposition and the sufficient condition are bookkeeping with counts and one concentration bound. The hard step is Theorem 2: showing that the budget ratio $K_t/(n-t)$ stays within $\delta$ of its attracting threshold until a bounded expected number of periods before the end. Near the horizon a single selection moves the ratio by about $1/(n-t)$, so the band becomes easy to leave. Equivalently, the target $\delta(n-\tau_0-u)$ that the deviation process must exceed shrinks to zero. A standard martingale or drift argument with a fixed band therefore does not give a bound uniform in $n$. The paper combines the mean-reverting drift of the deviation process with an exponential tail bound (its Proposition 4) and a Lyapunov argument. A second subtlety is uniformity: every constant must depend on $\epsilon$ (and $\delta$) only, never on $m$, the $a_j$, $n$ or $k$.

Formalization scope

The source is arXiv:1710.07719v2; its printed page numbers equal the PDF page numbers.

Representation.

• Ability levels are Fin m, with index 0 the largest value $a_1$; Lean index $i$ is the paper's $i+1$.
• Each instance carries $a$ strictly decreasing and positive, $f$ positive with $\sum f=1$.
• Expectations are finite sums over sequences $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ weighted by $\prod_tf(x_t)$, so no measure theory is needed.
• Policies are deterministic selection rules $\sigma(x,t)$ that are non-anticipating and feasible. $V^*_{\mathrm{on}}$ is a maximum over this finite set. The paper allows randomized policies; for this finite problem the optimal values coincide (p. 39). In any case, restricting to deterministic policies can only lower $V^*_{\mathrm{on}}$ and so does not weaken the goal.
• $V^*_{\mathrm{off}}$ is defined as an expected maximum over selection vectors, not by the sort formula. The sort formula is a milestone.

Quantifiers. The constant $M$ in the goal is chosen after $\epsilon$ and before $m$, the instance, $n$ and $k$. A statement with $M$ chosen after the instance, or after $n$, is trivial (regret $\le a_1n$) and is excluded.

Corrections to the printed text, disclosed in the items.

1. In Theorem 2 and Corollary 1, $M$ depends on the auxiliary $\delta\in(0,\epsilon)$ as well, because $\tau$ does. $\delta$ is quantified before $M$. The goal itself is $\delta$-free.
2. Lemma 2's conditions $p+\varepsilon\le k/n$, $k/n\le p-\varepsilon$ are stated as $(p+\varepsilon)n\le k$, $k\le(p-\varepsilon)n$, the form used in its proof. This avoids a false case at $n=0$.
3. The BR rule is applied at every time $t+1\in\{1,\dots,n\}$; p. 11 writes $\{1,\dots,n-1\}$.
4. $\tau$ is capped at $n$, which matters only when $n=0$.
5. In Proposition 5 the recursions are imposed for $\kappa\ge1$ (boundary conditions at $\kappa=0$), and only identity (49) is stated.

Infrastructure. The model definitions (instance, offline value, online policies, counts, thresholds, action index) and the binomial overshoot lemma are reusable for other finite-support online selection and revenue-management results. All of the following are welcome:

• proofs of individual milestones;
• an explicit constant;
• a formal derivation of $V^*_{\mathrm{on}}(n,k)=v_n(0,k)$ connecting Proposition 5 to $V^*_{\mathrm{on}}$.

Selected references

• A. Arlotto, I. Gurvich, Uniformly Bounded Regret in the Multi-Secretary Problem, arXiv:1710.07719v2, 2018; Stochastic Systems 9(3), 2019. https://arxiv.org/abs/1710.07719
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001