Statistics

Completed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 2: The Domain of Residual Life Time Attraction of the Exponential Law Is D(Λ) ∩ D₀Research Paper

Motivation

A lifetime observed only after it has survived to a high age is described by its residual life: the additional time until failure, conditional on survival so far. Reliability analysis asks whether these conditional distributions settle into a stable shape after scaling and shifting. Extreme-value theory asks a related question about the largest observation in a large independent sample. Balkema and de Haan identify an exact connection between these questions for the exponential residual-life limit and the Gumbel maxima limit in Theorem 3 of their 1974 article. The connection lets one recognize the asymptotic form of old-age lifetimes from the domain of attraction of sample maxima, provided the lifetime distribution has no finite upper endpoint.

The article studies several residual-life limits. This mission isolates its exponential case, where the limiting conditional excess has distribution function $\Pi(x)=1-e^{-x}$ for $x\ge0$ . The other continuous family $\Gamma_\alpha$ and the paper's discrete limits have separate hypotheses and attraction domains; they are outside this theorem.

Setting

Let $X$ have a probability distribution function $F$ on $\mathbb R$ , and let its survival function be $R(x)=\Pr(X>x)=1-F(x)$ . For a threshold $t$ with $R(t)>0$ , the residual-life distribution function is

F_t(x)=\Pr(X-t\le x\mid X>t)=\frac{\Pr(t<X\le t+x)}{R(t)}.

It is zero for $x<0$ . The class $D_0$ consists of the distributions with $R(x)>0$ for every real $x$ . This says that the upper endpoint is infinite and makes $F_t$ meaningful at every threshold.

A law $F$ belongs to the domain of residual-life attraction $D_r(G)$ when $F\in D_0$ and there are a positive scale $a(t)$ and a shift $b(t)$ such that $F_t(b(t)+xa(t))$ converges weakly to $G(x)$ as $t\to\infty$ . The shift here acts on $X-t$ , the residual lifetime. Weak convergence means convergence at every continuity point of the limiting distribution function; it does not require convergence at a jump.

For maxima, $F$ belongs to the domain of attraction $D(G)$ if there are sequences $a_n>0$ and $b_n$ for which $F(a_nx+b_n)^n$ converges weakly to $G(x)$ as $n\to\infty$ . The power is the distribution function of the maximum of $n$ independent observations after the indicated normalization. The relevant limit laws are the exponential residual-life law and the Gumbel law:

\Pi(x)=\begin{cases}0,&x<0,\\1-e^{-x},&x\ge0,\end{cases}\qquad \Lambda(x)=e^{-e^{-x}}\quad(x\in\mathbb R).

These definitions and formulas come from the introduction and §2 of the published article, printed pages 792–793 and 798.

Formalization targets

Theorem 3: the exact domain identity

The goal is the identity stated on printed page 798:

D_r(\Pi)=D(\Lambda)\cap D_0.

Both inclusions are required. In particular, membership in the maxima domain alone is insufficient: the maximum of a sample can have a Gumbel limit even when the underlying distribution has a finite upper endpoint, while residual life cannot be conditioned on survival beyond that endpoint. The $D_0$ condition is therefore part of the mathematical claim.

Supporting targets

The milestone list follows the statements used in the article's treatment of Theorem 3: the convergence-of-types remark on page 795; Lemma 3's asymptotic ratio $R(x-0)/R(x+0)\to1$ ; the tail criterion $nR(b_n+xa_n)\to e^{-x}$ associated with Gumbel attraction; the inclusion $D(\Lambda)\cap D_0\subseteq D_r(\Pi)$ ; and the passage from this tail limit on $x>0$ to all $x\in\mathbb R$ . The last step retains the same normalization sequences. The article presents the criterion in one direction and relies on its converse at the end; the formal milestone records both directions with the same sequences.

Significance

The identity translates a conditional limit at a moving high threshold into a classical maxima-domain statement. A theorem about sample extremes can therefore characterize whether normalized remaining lifetime is asymptotically exponential. Conversely, observing exponential residual-life attraction determines a Gumbel maxima limit once the tail normalization is extended across the real line. The condition $D_0$ marks exactly where the conditional lifetime exists; omitting it would misstate the equivalence.

The article proves the result mathematically. The Lean targets here provide a precise representation of its distributions, normalizations, and limiting claims, with Theorem 3 still posed for formal proof. A complete development would add proofs of the supporting tail and convergence-of-types statements, then establish both inclusions. The definitions of weak convergence at continuity points, survival functions, and attraction domains can also support later formalizations of the paper's Pareto and discrete cases.

Difficulty

The simple comparison $F(a_nx+b_n)^n\approx e^{-nR(a_nx+b_n)}$ only relates the two limits after a suitable normalization is already available. The reverse direction starts with conditional residual-life convergence indexed by real thresholds, whereas maxima attraction needs a sequence indexed by integers. Sampling thresholds must preserve the tail asymptotics despite possible atoms. More seriously, the residual-life statement initially yields the required scaled-tail convergence only for positive arguments. The maxima limit must hold on the whole real line. A proof confined to that half-line cannot establish $D(\Lambda)$ ; the continuation across its left boundary is the central difficulty highlighted by the article on printed pages 798–799.

Formalization scope

Lean represents $F$ as the cumulative distribution function of a probability measure on $\mathbb R$ and uses real-valued probabilities of intervals for $R$ and $F_t$ . The residual-life denominator is positive wherever $D_r$ is asserted. The extrema normalization is indexed by natural numbers, while the residual-life normalization is indexed by real thresholds. The scale is positive at every index; only large indices affect the limit. Weak convergence is encoded at every continuity point of the limit. As $\Pi$ and $\Lambda$ are continuous, their particular domain conditions amount to convergence at every real argument.

The paper uses two shift conventions: $F_t(b(t)+xa(t))$ shifts $X-t$ , while the scaled-tail expressions $R(b_n+xa_n)$ shift $X$ . Each statement uses the convention of its source passage. The convergence-of-types remark makes explicit the antitonicity and right-continuity of its limiting tails and states its identity where both arguments lie in the half-line on which convergence is known. Gnedenko's criterion is formalized as an equivalence: the printed sentence states the forward implication, and the conclusion of Theorem 3 uses the converse. The page-799 expression $R(b(t)+xa(t))/(t)$ has a missing $R$ in the denominator; the formal statement uses the intended $R(t)$ , consistent with conditional probability and with equation (11). These choices prevent a zero-denominator quotient or an out-of-domain limit identity from trivializing a target. In particular, $D_0$ is part of the definition of $D_r(G)$ : without it a law with a finite upper endpoint would have $R(t)=0$ for large $t$ , the conditional distribution would be the junk quotient $0/0=0$ , and the domain would be mis-specified. In Lemma 3 the limit $G$ is the distribution function of a probability measure, assumed continuous on all of $\mathbb R$ .

The development needs measure-theoretic cumulative distributions and interval probabilities, filters for limits, and real exponential identities. The domain definitions and scaled-tail predicate are reusable beyond this theorem. Contributions that prove the stated milestones, or supply general lemmas about weak convergence and normalized tails, fit the scope.

Selected references

A. A. Balkema and L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2(5), 792–804 (1974). DOI: 10.1214/aop/1176996548.
B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44(3), 423–453 (1943). DOI: 10.2307/1968974.

11 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 3: F Is in the Domain of Residual Life Time Attraction of Π_{p,c} iff It Is Tail Equivalent to a Discrete Law with Gap Ratios → e^{pc} and Tail Ratios → e^{−p}Research Paper

Residual life at great age

A component that has survived to age $t$ has a residual life time $X - t$ , and in reliability, actuarial work and the analysis of excesses over high thresholds the question is what its conditional law looks like when $t$ is large. Balkema and de Haan (Ann. Probab. 2 (1974), 792–804) answered this in full generality: after an affine normalization, the only possible limit laws are the exponential law $\Pi$ , the Pareto-type laws $\Gamma_\alpha$ , and a two-parameter family of discrete laws $\Pi_{p,c}$ . The continuous half of their classification became the Pickands–Balkema–de Haan theorem behind the peaks-over-threshold method of extreme-value statistics. The discrete half is less known, and this mission treats it: Theorem 5 of the paper (§3, p. 800) describes exactly which lifetimes are attracted to $\Pi_{p,c}$ .

Discrete limits appear only when the normalization is allowed both a scale and a shift. They describe lifetimes that live, asymptotically, on a lattice-like set of ages whose spacing grows geometrically, with a fixed fraction of survivors failing at each lattice point.

The source is the published article in The Annals of Probability (DOI 10.1214/aop/1176996548); page numbers below are the journal's.

Setting

Let $X$ be a real random variable with law $\mu$ , distribution function $F$ and tail $R(x) = 1 - F(x) = P\{X > x\}$ , and assume $F(x) < 1$ for every $x$ . The residual life distribution function at age $t$ is (1), p. 792,

F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t+x])}{\mu((t,\infty))}.

A family of distribution functions $H_t$ converges weakly to $G$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$ . The domain of residual life time attraction $D_r(G)$ (p. 798) is the set of $F$ with $F(x) < 1$ for all $x$ for which some $a(t) > 0$ and $b(t)$ give

F_t(b(t) + x a(t)) \to G(x) \quad \text{weakly as } t \to \infty.

For $p > 0$ and $c \ge 0$ the discrete limit law is (p. 793), for $x \ge 0$ ,

\Pi_{p,c}(x) = 1 - \exp\Big(-p\Big[1 + \frac{\log(1+cx)}{cp}\Big]\Big) \ (c > 0), \qquad \Pi_{p,0}(x) = 1 - \exp\Big(-p\Big[1 + \frac{x}{p}\Big]\Big),

and $\Pi_{p,c}(x) = 0$ for $x < 0$ ; $[\,\cdot\,]$ is the integer part. Its tail takes the values $e^{-p}, e^{-2p}, \dots$ and jumps at $(e^{kpc} - 1)/c$ , $k = 0, 1, \dots$ (at $kp$ if $c = 0$ ).

A distribution function $F_0 = 1 - R_0$ is discrete with jump sequence $t_0 < t_1 < \cdots$ if the $t_n$ are unbounded, each carries positive mass and there is no other mass. Two distribution functions with $F_i(x) < 1$ for all $x$ are tail equivalent if $1 - F_1(x) \sim 1 - F_2(x)$ as $x \to \infty$ . The conditions of §3 are

\text{(12a)}\ \ \frac{t_{n+1} - t_n}{t_n - t_{n-1}} \to e^{pc}, \qquad \text{(12b)}\ \ \frac{R_0(t_{n+1})}{R_0(t_n)} \to e^{-p}.

Formalization targets

Goal: Theorem 5 (p. 800)

For $p > 0$ and $c \ge 0$ ,

F \in D_r(\Pi_{p,c}) \iff F \text{ is tail equivalent to a discrete } F_0 \text{ whose jumps satisfy (12a) and whose tail satisfies (12b).}

Milestones

(§3, pp. 799–800) A discrete $F$ satisfying (12a) and (12b) lies in $D_r(\Pi_{p,c})$ .
(§3, p. 800) If $F_1$ is tail equivalent to $F_2 \in D_r(\Pi_{p,c})$ , then $F_1 \in D_r(\Pi_{p,c})$ . Milestones 1 and 2 give the "if" half.
(Proof of Theorem 5, p. 800) If $F \in D_r(\Pi_{p,c})$ , there are $b_n \uparrow \infty$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ and a discrete $F_0$ , tail equivalent to $F$ , with $R_0(t_n) = R(b_n)$ at its jumps.
(Proof of Theorem 5, pp. 800–801) Such an $F_0$ satisfies (12b) and (12a). Milestones 3 and 4 give the "only if" half.

Significance

Theorem 5, together with Theorems 1, 3 and 4 of the paper, completes the description of residual-life attraction: every nondegenerate limit is of one of the listed types, and each type's domain of attraction is identified. For the discrete types the answer is a statement purely about the geometry of the atoms of an approximating law, which makes membership checkable for concrete lifetimes (geometric-type laws on $\{0, 1, 2, \dots\}$ fall under $c = 0$ , laws on a geometric grid $\{\lambda^n\}$ under $c > 0$ ). It also explains why discrete limits are invisible when only a scale normalization is allowed.

The theorem has been proved since 1974; it has not been formalized. A machine-checked development would supply weak convergence of distribution functions at continuity points, residual-life normalizations and tail equivalence as reusable objects, and would check a proof that the paper compresses into a page, including a convergence-of-types step on a half line that the paper cites from its own §1.

Difficulty

The "if" half is close to a computation, but the computation is about weak convergence to a step function: the normed tails converge only off the jumps, and the normalization must be extended from the jump times $t_n$ to all real ages $t$ .

The "only if" half is the core. From $F \in D_r(\Pi_{p,c})$ alone one has to manufacture the atoms $t_n$ of a discrete law that $F$ itself need not have. The obvious attempt, reading the atoms off the jumps of $F$ , fails because $F$ may be continuous: membership in $D_r(\Pi_{p,c})$ only says that $F$ drops by a factor close to $e^{-p}$ over short stretches, relative to the normalization, and never by an intermediate factor. Making "never by an intermediate factor" precise uniformly in the age $t$ , with normalizations $a(t), b(t)$ about which nothing but their existence is known, is where the work lies; the same lack of control over $a(t)$ is what makes the gap ratio (12a) hard to extract.

Formalization scope

A law is a measure μ : Measure ℝ with IsProbabilityMeasure μ; the tail $R(x)$ is (μ (Set.Ioi x)).toReal, and $F_t(x)$ is μ((t, t+x]) / μ((t,∞)). $D_r(G)$ (InDr) includes $F(x) < 1$ for all $x$ , normalizations $a(t) > 0$ for all real $t$ , and "weakly" means convergence at every continuity point of $G$ and nowhere else; requiring convergence at the jumps of $\Pi_{p,c}$ would make $D_r(\Pi_{p,c})$ empty. $\Pi_{p,c}$ (piPC) is defined by cases $c = 0$ / $c > 0$ with Int.floor, so that $c = 0$ is not the junk value of a division by zero; it is used only with $p > 0$ , $c \ge 0$ . A discrete law with jump sequence $t$ (IsDiscreteWithJumps) has $t$ strictly increasing and tending to $\infty$ , positive mass at each $t_n$ and no mass elsewhere. (12a) is indexed from $n = 1$ . Tail equivalence (TailEquiv) includes $F_i(x) < 1$ for both laws.

Conventions and disclosed readings:

The page proves the "if" direction by showing convergence to a function of the type of $1 - \Pi_{p,c}$ ; since $D_r$ lets $a, b$ be chosen freely, milestone 1 is stated with $\Pi_{p,c}$ itself.
The proof of Theorem 5 uses the normalization (2)–(3) of p. 794, where $b(t)$ shifts $X$ rather than $X - t$ ; milestone 3 only asserts the existence of the sequence $b_n$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ , so no convention enters its statement.
" $F_0$ only takes the values $F(b_n)$ " is formalized as $R_0(t_n) = R(b_n)$ for all $n$ , the form the next paragraph of the page uses. This identity is a hypothesis of milestone 4, as on the page, and cannot be dropped: a law tail equivalent to $F$ may carry extra atoms of vanishing relative mass, at which (12a) and (12b) fail.
The page identifies the limit of the gap ratios as the scale constant $A$ of a functional equation; milestone 4 states it as $e^{pc}$ , the gap ratio of the jumps of $\Pi_{p,c}$ .
Theorem 5 prints "distribution fuction"; this typo is kept in the quoted text only.

No statement is trivialized: $D_r(\Pi_{p,c})$ is nonempty (the geometric law on $\{0,1,2,\dots\}$ lies in $D_r(\Pi_{p,0})$ ), and Theorem 5 is not a definitional unfolding, since $D_r$ is defined by weak convergence and the right-hand side by discrete approximation.

A complete development needs: weak convergence of distribution functions at continuity points, a convergence-of-types lemma on a half line (the Remark after Lemma 1 of the paper, p. 795), and elementary facts on step functions. The first two are reusable across the whole paper and across extreme-value theory. Contributions of either half of the theorem, or of the convergence-of-types lemma, are welcome.

Selected references

A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
B. V. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

9 thms2 active usersReviewed

Algorithmic Game Theory Machine Learning Probability·Captain: mikedeng1

Asymptotic Calibration: The Regret-Balancing Randomised Forecast on the Grid {0, 1/k, …, 1} with k ≥ 1/ε² Is ε-Calibrated against Every Adaptive NatureResearch Paper

Motivation

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$ , the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$ , where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$ ; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$ . The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$ .

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$ , and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$ , in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$ . Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$ , and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$ , the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$ . The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$ :

\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$ , choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

\Pr\{C_t<\varepsilon\}>1-\varepsilon.

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$ . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$ . Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$ ; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$ : the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$ . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$ ; nonnegative weights make its numerator zero as well. At horizon $0$ , the weighted calibration score is $0$ . The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$ . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.

14 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research I: Time-Mean Speed Equals Space-Mean Speed plus σₛ²/v̄ₛ, so v̄ₜ ≥ v̄ₛ with Equality Only Without Speed VariationResearch Paper

Why two traffic speed averages differ

A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).

The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).

Traffic streams and their two distributions

A road's traffic stream is divided into $C$ subsidiary streams, indexed by $i=1,\ldots,C$ . Stream $i$ has flow $q_i$ , the number of vehicles passing a point per unit time, and speed $v_i$ . Its concentration is $k_i=q_i/v_i$ , the number of vehicles occupying a unit road length. Total flow and concentration are $Q=\sum_i q_i$ and $K=\sum_i k_i$ . The time frequency $f_i=q_i/Q$ weights each stream by how often its vehicles pass a point. The space frequency $f'_i=k_i/K$ weights it by the fraction of vehicles present along the road.

The time-mean speed is $\bar v_t=\sum_i q_i v_i/Q=\sum_i f_i v_i$ . The space-mean speed is $\bar v_s=\sum_i k_i v_i/K=\sum_i f'_i v_i$ . Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as $\sigma_s^2=\sum_i k_i(v_i-\bar v_s)^2/K$ , and the corresponding coefficient of variation as $c_s=\sigma_s/\bar v_s$ (equations (1)–(3), (7), pp. 328–331).

These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count $C$ is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.

Formalization targets

The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):

\bar v_t=\bar v_s+\frac{\sigma_s^2}{\bar v_s},\qquad \bar v_s\le\bar v_t,\qquad \bar v_t=\bar v_s\iff v_i=v_j\text{ for every }i,j.

The subsidiary targets follow the paper's order. Equation (4) says $k_i v_i=q_i$ for each stream, giving equation (5), $Q=K\bar v_s$ . Appendix II then uses the centered identity $\sum_i f'_i(v_i-\bar v_s)=0$ and rewrites the time mean as $\bar v_t=(\sum_i f'_i v_i^2)/\bar v_s$ . These three claims are the mission milestones. Equation (8) is included as a companion formulation:

\bar v_t=\bar v_s(1+c_s^2).

The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).

What the result supplies

The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and $\bar v_s$ is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.

The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes $\sum_i v_i^2/\sum_i v_i$ . The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).

Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.

Where the formal proof needs care

The relation looks like a routine identity for weighted means, but the two weight systems are coupled through $k_i=q_i/v_i$ . One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.

The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.

Formalization scope

Lean uses Fin C for the streams and real numbers for $q_i$ , $v_i$ , $k_i$ , both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require $0<C$ , $0<q_i$ , and $0<v_i$ for every $i$ . These requirements make $Q$ , $K$ , and $\bar v_s$ positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering $v_1<\cdots<v_C$ .

The variance is defined from equation (7), $\sum_i k_i(v_i-\bar v_s)^2/K$ . Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since $f_i$ and $f'_i$ are explicit finite weights.

A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II 1 (1952), 325–362. DOI: 10.1680/ipeds.1952.11259.

5 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments I: Greedy Sampling with Density-Zero Forced Draws Earns max(α, β) per Draw from Any Two Populations with Finite MeansResearch Paper

Motivation

An experimenter can draw observations from two populations $A$ and $B$ , one at a time, and wants the sum of the observations to be as large as possible. The populations might be two treatments, two seed varieties or two manufacturing processes; their means are unknown. Each draw both earns a reward and tells the experimenter something about the population it came from. This is the two-armed bandit problem. Herbert Robbins posed it in its modern form in his 1952 address to the American Mathematical Society, Some aspects of the sequential design of experiments, the paper usually credited with founding the field.

Section 2 of that paper asks a basic question (display (12), p. 532): is there any sampling rule whose average reward per draw approaches the larger of the two means, whatever the populations are? Robbins answers yes, for any two populations with finite means, using one explicit rule: forced sampling along a sparse schedule, greedy choice otherwise. This mission formalizes that answer.

Timeline:

1933. Thompson proposes a randomized rule for choosing between two treatments (Biometrika 25).
1952. Robbins states the problem for general populations and gives the rule $\bar R$ with $\lim_n L_n(A,B,\bar R) = 0$ for any two populations with finite means. The argument is only indicated ("it can be shown").
1985. Lai and Robbins replace $o(n)$ loss by the optimal logarithmic regret for parametric families (Adv. Appl. Math. 6).
2020. Lattimore and Szepesvári give the textbook account of explore-then-commit and $\varepsilon$ -greedy rules, which descend from forced sampling (Bandit Algorithms).

Setting

Population $A$ has distribution function $F$ and population $B$ has $G$ , with expectations

\alpha = \int_{-\infty}^{\infty} x\,dF(x), \qquad \beta = \int_{-\infty}^{\infty} x\,dG(x),

assumed to exist, i.e. to be finite (display (1), p. 529). Nothing else is assumed about $F$ and $G$ .

A sampling rule $R$ draws $x_1, x_2, \dots$ one at a time; the population of the $i$ -th draw may depend on $x_1, \dots, x_{i-1}$ , and given that choice $x_i$ is a fresh draw from the chosen population. Write $S_n = x_1 + \cdots + x_n$ . The loss of $R$ after $n$ draws (display (9), p. 531) is

L_n(A, B, R) = \max(\alpha, \beta) - E\!\left(\frac{S_n}{n}\right),

the average shortfall per draw compared with someone who knows the better population and samples only from it.

The forcing schedule (display (13), p. 532) is a pair of disjoint, strictly increasing sequences of positive integers

1 = a_1 < a_2 < \cdots, \qquad 2 = b_1 < b_2 < \cdots

of density zero: the fraction of the integers $1, \dots, n$ that are an $a$ or a $b$ tends to $0$ .

The rule $\bar R$ : at draw $i$ , sample $A$ if $i$ is an $a$ , sample $B$ if $i$ is a $b$ , and otherwise sample $A$ if the mean of the previous observations from $A$ is strictly larger than the mean of the previous observations from $B$ , and $B$ if it is not (a tie goes to $B$ ).

Formalization targets

Goal: Section 2, Eq. (16)

For every pair of populations with finite means and every forcing schedule,

\lim_{n\to\infty} L_n(A, B, \bar R) = 0.

The goal is about the specific rule $\bar R$ and every schedule, not about the mere existence of a rule. It contains no rate and no constant, so it stays valid when the rule is analysed more finely.

Milestone: Eq. (14), almost-sure average

\lim_{n\to\infty} \frac{S_n}{n} = \max(\alpha, \beta) \quad\text{with probability } 1.

Milestone: Eq. (15), expected average

\lim_{n\to\infty} E\!\left(\frac{S_n}{n}\right) = \max(\alpha, \beta).

The goal follows from (15) by the definition (9); the paper's chain is (14) ⇒ (15) ⇒ (16).

Significance

The result. The theorem answers question (12) and shows that "learning while earning" costs nothing in the long run, per draw, under no assumption beyond finite means: no bounded support, no variance, no parametric family. It is the first consistency result for an adaptive allocation rule, and it fixes the benchmark later refined by logarithmic-regret theory. In modern terms, a forced-exploration greedy policy has regret $o(n)$ on every two-armed bandit with integrable rewards.

Formalizing it. The paper gives no proof; it says the results "can be shown". A machine-checked proof records the argument in full. The platform already has finite-horizon regret bounds for $\varepsilon$ -greedy with bounded rewards (FoundationsRL.Bandits.epsilon_greedy_regret_bound), consistency in the stronger Lai–Robbins sense as a definition (ConsistentBanditPolicy), and a forced-sample tail bound for the Lasso bandit (BastaniBayati.LassoBandit.forced_sample_estimator_tail). None of these covers a deterministic greedy rule, almost-sure convergence, or unbounded rewards with only a first moment, and none of them proves (14)–(16).

Difficulty

The obvious argument is: each population is sampled infinitely often because of the forced draws, so each running mean converges by the strong law, so greedy eventually picks the better population, and the forced draws are negligible. Two steps are not routine.

First, the strong law applies to i.i.d. sequences, while the observations from $A$ arrive at random, history-dependent times. The values seen from $A$ have to be identified, in law, with an i.i.d. sequence that is independent of the times at which they are used.

Second, passing from (14) to (15) needs uniform integrability of $S_n/n$ , and only first moments are available. No second moment is assumed, so variance bounds are not available.

When $\alpha = \beta$ greedy need not settle on either population; the statement must hold anyway, and an argument that waits for greedy to "lock in" does not cover this case.

Formalization scope

The populations are a published two-armed BanditAlgorithm.StochasticBandit 2. $A$ is arm 0 and $B$ is arm 1; $\alpha$ and $\beta$ are banditArmMean. A rule is a published BanditPolicy 2, and $E$ is the integral against the published infinite-horizon law banditTrajMeasure, whose coordinate $t$ is the paper's draw $t+1$ . Explicit readings of the paper's phrases:

"the expectations exist" means both reward laws are Integrable. This is the only assumption on the populations: the class $D$ of the paper is left arbitrary, and $\alpha = \beta$ is allowed.
"density 0" means #({1,…,n} ∩ (range a ∪ range b)) / n → 0 in $\mathbb R$ . The sequences are infinite and 0-indexed (a 0 = 1, b 0 = 2).
"according as … exceeds or does not exceed": $A$ exactly when mean $_A$ > mean $_B$ , so ties go to $B$ .
"with probability 1" is ∀ᵐ under the trajectory law, and "lim" is Tendsto … atTop along $n \in \mathbb N$ .
$S_n/n$ uses real division; its value at $n = 0$ plays no role.

Trivializing formalizations are excluded. Without integrability the means and expectations are junk zeros; this is ruled out by the integrability hypothesis. Replacing $\bar R$ by "there exists a rule" would weaken the goal to (12). Finite forcing sets would make the statement false.

The needed infrastructure is a representation of the adaptive sampling process by per-population i.i.d. reward sequences, the strong law along random subsequences, and a uniform-integrability argument for averages under only a first moment. All three are reusable for other forced-exploration and greedy policies. Contributions of these general lemmas as separate theorems are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933), 285–294. https://doi.org/10.2307/2332286
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

A Stochastic Approximation Method: If M Is Nondecreasing, M(θ) = α and M′(θ) > 0, the Robbins–Monro Iterates with Steps of Type 1/n Converge to θ in Mean SquareResearch Paper

Motivation

Many problems in statistics and engineering ask for the level $\theta$ at which an unknown function takes a prescribed value $\alpha$ : the dose at which a fraction $\alpha$ of subjects respond, the setting at which a noisy device reaches a target output, the $\alpha$ -quantile of a distribution that can only be probed by yes/no experiments. When the function can only be observed through noisy measurements, classical root-finding does not apply. Robbins and Monro (Ann. Math. Statist. 22 (1951) 400–407) proposed a recursive procedure that uses one noisy observation per step and proved that it converges in mean square. The paper started the field of stochastic approximation, which today underlies stochastic gradient descent, temporal-difference learning and adaptive control.

Timeline. Robbins and Monro (1951) prove mean-square convergence for bounded responses under conditions (5′) or (33)–(35). Kiefer and Wolfowitz (1952) adapt the scheme to finding a maximum. Blum (1954) proves almost-sure convergence under weaker moment conditions. Dvoretzky (1956) gives a general convergence theorem covering both schemes. Later work (Robbins and Siegmund, 1971; Ljung, 1977; Kushner and Clark, 1978; Benaïm, 1999) develops the supermartingale and ODE methods.

Setting

To each real level $x$ corresponds a random response $Y(x)$ with distribution function $H(y \mid x)$ , and the regression function is

M(x) = \int_{-\infty}^{\infty} y \, dH(y \mid x).

The responses are bounded: there is $C > 0$ with $\Pr[|Y(x)| \le C] = 1$ for all $x$ (condition (4)). Fix constants $\alpha, \theta$ and positive step sizes $a_n$ . The Robbins–Monro process starts at an arbitrary constant $x_1$ and sets

x_{n+1} - x_n = a_n(\alpha - y_n), \qquad \Pr[y_n \le y \mid x_n] = H(y \mid x_n),

so $y_n$ is a fresh response observed at the current level $x_n$ . The quantity of interest is the mean squared error $b_n = E(x_n - \theta)^2$ .

A sequence $\{a_n\}$ is of type $1/n$ if

\sum_{n=1}^{\infty} a_n^2 < \infty \quad (6), \qquad \sum_{n=2}^{\infty} \frac{a_n}{a_1 + \cdots + a_{n-1}} = \infty \quad (26);

$a_n = 1/n$ is the standard example. The proof also uses $d_n = E[(x_n-\theta)(M(x_n)-\alpha)]$ , $e_n = E[\int (y-\alpha)^2\,dH(y\mid x_n)]$ and $A_n = |x_1 - \theta| + [C+|\alpha|](a_1 + \cdots + a_{n-1})$ .

Formalization targets

Goal: Theorem 2 (p. 405)

If $\{a_n\}$ is of type $1/n$ , (4) holds, and $M$ is nondecreasing with $M(\theta) = \alpha$ and $M'(\theta) > 0$ , then, whatever $x_1$ ,

\lim_{n \to \infty} E(x_n - \theta)^2 = 0.

Milestones

The one-step identity (14): $b_{n+1} - b_n = a_n^2 e_n - 2a_n d_n$ .
The signs and bound after (14): $d_n \ge 0$ and $0 \le e_n \le [C+|\alpha|]^2$ .
(17)–(18): $\sum a_n^2e_n$ and $\sum a_n d_n$ converge, and $b = \lim b_n = b_1 + \sum a_n^2e_n - 2\sum a_nd_n$ exists with $b \ge 0$ .
Lemma 1: if $d_n \ge k_n b_n$ with $k_n \ge 0$ and $\sum a_n k_n = \infty$ , then $b = 0$ .
(22): $\Pr[|x_n - \theta| \le A_n] = 1$ .
(24): $d_n \ge \bar k_n b_n$ , where $\bar k_n$ is the infimum of $(M(x)-\alpha)/(x-\theta)$ over $0 < |x-\theta| \le A_n$ .
(27): (26) implies $\sum a_n = \infty$ .
Lemma 2: if $\bar k_n \ge K/A_n$ for some $K > 0$ and large $n$ , and (26) holds, then $b = 0$ .
(42): under (33)–(35), $(M(x)-\alpha)/(x-\theta) \ge \delta M'(\theta)/2A_n$ on $0 < |x-\theta| \le A_n$ .

Companion results

Theorem 1 (p. 404: the same conclusion under (5′), $M(x) \le \alpha - \delta$ for $x < \theta$ and $M(x) \ge \alpha + \delta$ for $x > \theta$ ); convergence in probability under the hypotheses of Theorem 2 (p. 401); the quantile estimator of §4, (48); and (30), that $c'/n \le a_n \le c''/n$ gives a sequence of type $1/n$ .

Significance

Theorem 2 is the first convergence theorem for a recursive root-finding procedure under noise. It shows that a procedure using no knowledge of $M$ or of the noise distribution, beyond a monotone crossing and a positive slope at the root, is consistent. Section 4 turns it into a distribution-free consistent estimator of a quantile from response/nonresponse data, the up-and-down designs of bioassay and sensitivity testing. Its step-size conditions, $\sum a_n^2 < \infty$ with a divergence condition, remain the standard conditions for stochastic gradient methods.

The theorem has been proved since 1951 and strengthened many times. As far as is known it has no machine-checked proof, and Mathlib has no stochastic approximation theory. Formalizing it requires conditional laws given by Markov kernels, integration against a composition of a measure with a kernel, and deterministic series arguments. A finished formalization would be a base for formalizing the almost-sure theorems (Blum, Robbins–Siegmund) and the ODE method.

Difficulty

The obvious argument fails at one step. Monotonicity of $M$ and a positive derivative at $\theta$ do not give a uniform positive lower bound on the slope $(M(x)-\alpha)/(x-\theta)$ : away from $\theta$ the slope can decay to $0$ , for example when $M$ is bounded, as (4) forces. So the drift towards $\theta$ is not uniformly strong, and the newcomer's first idea, a uniform contraction $b_{n+1} \le (1 - c\,a_n) b_n + O(a_n^2)$ , is not available under (33)–(35). This is why the theorem needs the divergence condition (26), which is stronger than $\sum a_n = \infty$ , and not only (6). On the formal side, the expectations come from integrating against the joint law of $(x_n, y_n)$ , and they need integrability bounds before any identity can be used.

Formalization scope

Everything is in the namespace RobbinsMonroSA.Conv, over a probability space $(\Omega, P)$ with IsProbabilityMeasure P. Indices are 0-based: Lean's x 0, a 0 are the paper's $x_1$ , $a_1$ , and Lean's bigA … n is the paper's $A_{n+1}$ . The committed conventions are:

$H$ is a Kernel ℝ ℝ with IsMarkovKernel H (each $H(\cdot\mid x)$ is a probability law, measurable in $x$ ).
(4) is 0 < C ∧ ∀ x, H x [-C, C] = 1. It is a hypothesis of every item that mentions an expectation, and it is what keeps the Bochner integrals defining $b_n$ , $d_n$ , $e_n$ and $M$ from defaulting to $0$ .
(8) is the joint-law equation: the law of $(x_n, y_n)$ is the law of $x_n$ composed with $H$ . (7) holds surely, and $x_n$ , $y_n$ are measurable. No Markov property or filtration beyond (8) is assumed.
Every " $= \infty$ " for a series ((19), (26), (27)) is divergence of partial sums to $+\infty$ . " $b = 0$ " is $b_n \to 0$ .
$M'(\theta) > 0$ is HasDerivAt M M' θ with 0 < M'.
The infimum $\bar k_n$ of (23) is never formed. (24) and (25) are stated with lower bounds on $(M(z)-\alpha)/(z-\theta)$ over $0<|z-\theta|\le A_n$ . This avoids the junk value $0$ that Lean's real infimum gives on the empty range ( $A_n = 0$ ), where the paper's infimum is $+\infty$ .

The standing assumptions of §3, (4), (5) and (6), are hypotheses of Lemma 1, Lemma 2 and the displays of §3 whose proofs use them. In Theorems 1 and 2, (5) follows from (5′) or from (33)–(34), and (6) is part of "type $1/n$ ".

The goal cannot be trivialized. It mentions neither $d_n$ , $e_n$ , $A_n$ nor any constant, and the process must satisfy (8) for every $n$ . Without (8), $y_n$ would be arbitrary and the statement false; with $y_n = M(x_n)$ it would be deterministic.

Contributions welcome: proofs of the milestones, reusable lemmas on integrating against μ ⊗ₘ κ, and a proof that $a_n = 1/n$ satisfies (26).

Selected references

H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23 (1952), 462–466. https://doi.org/10.1214/aoms/1177729392
J. R. Blum, Approximation methods which converge with probability one, Ann. Math. Statist. 25 (1954), 382–386. https://doi.org/10.1214/aoms/1177728794
A. Dvoretzky, On stochastic approximation, Proc. Third Berkeley Symp. Math. Statist. Prob. 1 (1956), 39–55. https://projecteuclid.org/euclid.bsmsp/1200501645
H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics (1971), 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709 (1999), 1–68. https://doi.org/10.1007/BFb0096509

11 thms2 active usersReviewed

Probability·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every $n$ , not just in the limit.

Timeline.

1933–1944. Kolmogorov and Smirnov introduce the statistics, prove that their laws do not depend on the continuous distribution, and find the limit laws, e.g. $\lim_n P(D_n^->\lambda)=\exp(-2\lambda^2)$ . Smirnov (1944) also gives the exact law of the one-sided statistic and the expansion $P(D_n^->\lambda)=\exp(-2\lambda^2)\bigl(1-\frac{2\lambda}{3\sqrt n}+O(n^{-1})\bigr)$ .
1956. Dvoretzky, Kiefer and Wolfowitz prove $P(D_n^->\lambda)\le C\exp(-2\lambda^2)$ for every $n$ , with an unspecified constant $C$ (Ann. Math. Statist. 27).
1958. Birnbaum and McCarty conjecture that $C=1$ is admissible.
1979–1985. Explicit constants: $C\le306$ (Devroye and Wise), $C\le29$ (Shorack and Wellner), $C\le2\sqrt2$ (Hu).
1990. Massart proves the conjecture under a mild lower bound on $\lambda$ , and deduces the two-sided bound with the optimal constant $2$ (Ann. Probab. 18).

Setting

Let $x_1,\dots,x_n$ ( $n\ge1$ ) be independent, identically distributed real random variables with a continuous distribution function $F$ . The empirical distribution function is

\hat F_n(x)=\frac1n\sum_{i=1}^n\mathbb 1_{(x_i\le x)},

and the centred, normalised empirical process is $Z_n=\sqrt n(\hat F_n-F)$ . The statistics are

D_n^+=\sup_{x\in\mathbb R}Z_n(x),\qquad D_n^-=\sup_{x\in\mathbb R}\bigl(-Z_n(x)\bigr),\qquad D_n=\sup_{x\in\mathbb R}|Z_n(x)|.

In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), $F$ is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter $\lambda$ is written l.

The proof works with Smirnov's point probabilities $p_{\lambda,n}(j)=\lambda\sqrt n\,(j+\lambda\sqrt n)^{j-1}(n-j-\lambda\sqrt n)^{n-j}n^{-n}\binom nj$ , whose sum over $0\le j<n-\lambda\sqrt n$ is $P(D_n^->\lambda)$ , with Csáki's density $f_\lambda(s)=\frac{\lambda}{\sqrt{2\pi}}s^{-3/2}(1-s)^{-1/2}\exp\bigl(-\frac{\lambda^2}{2s(1-s)}\bigr)$ of the first passage of a Brownian bridge at level $\lambda$ , and with the ratio $C_{\lambda,n}=\exp(2\lambda^2)P(D_n^->\lambda)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge1$ and every $\lambda\ge\sqrt{\log(2)/2}\wedge\gamma n^{-1/6}$ , with $\gamma=1.0841$ ,

P(D_n^->\lambda)\le\exp(-2\lambda^2).

Here $\wedge$ is the minimum. The constant $1$ in front of the exponential is the point of the theorem; the threshold on $\lambda$ is the paper's.

Milestones

The milestones follow the proof in the paper's order of attack:

the reduction to the uniform law, and Smirnov's exact formula (2.3);
the identity $\int_0^1f_\lambda=\exp(-2\lambda^2)$ (2.4);
the local comparison of $p_{\lambda,n}(j)$ with $f_\lambda$ : (2.7), Lemma 2, Claims 1–3, and Proposition 1;
the midpoint bound for log-convex integrands (Lemma 3) and the closed forms of Lemma 4;
the nonasymptotic expansion (2.11), the negativity of its right side $\eta_n$ , and with them Theorem 1 for $n\ge39$ , $\lambda\le\sqrt n/2$ ;
Proposition 2 on the slope of $C_{\lambda,n}$ , the crude bounds (2.13)–(2.14), and the finite grid check (2.15) for $n\le38$ .

Companions

The equality in law of $D_n^+$ and $D_n^-$ , Comment 1 ((1.4) whenever $\exp(-2\lambda^2)\le1/2$ ), the reduction $P(D_n>\lambda)\le2P(D_n^->\lambda)$ , and Corollary 1:

P(D_n>\lambda)\le2\exp(-2\lambda^2)\qquad(\lambda>0).

Significance

The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, $1$ and $2$ , which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.

Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified $C$ . The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, $\eta_{39}$ ); turning those into checked certificates is part of the work.

Difficulty

The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison $P(\tau_n=t)\le\frac1nf_\lambda(t-\varepsilon/3)$ is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time $t$ is close to $\varepsilon=\lambda/\sqrt n$ . Controlling that factor uniformly in $j$ while keeping the leading constant exactly $1$ is what forces the delicate constants ( $\theta=0.4833$ , $\beta=0.826$ , $\mu=0.4345$ , $\gamma=1.0841$ ). For small $n$ the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on $\lambda\mapsto C_{\lambda,n}$ plus a finite numerical check over a grid; neither half suffices alone.

Formalization scope

Conventions:

$n\ge1$ ; the sample is indexed by Fin n; $F$ is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.
Probabilities are measures of events in $[0,\infty]$ and are compared with ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in $[-1,1]$ , hence a genuine real supremum.
$p_{\lambda,n}(j)$ uses an integer power at $j-1$ , so that $p_{\lambda,n}(0)=(1-\varepsilon)^n$ . $C_{\lambda,n}$ is defined from the exact formula (2.3); it equals $\exp(2\lambda^2)P(D_n^->\lambda)$ by the (2.3) milestone, so the analytic milestones carry no probability.
Statements that the page gives through derivatives of $C_{\lambda,n}$ (Proposition 2(i), (iii)) are stated as monotonicity and as an increment bound, because $C_{\lambda,n}$ has kinks.

Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of $j$ ), (2.8) (swapped numerators) and Proposition 2(i) (" $\ge0$ " for nonincreasing) are corrected; Claim 2 carries the hypothesis $\varepsilon\le3s'$ , without which the corrected claim is false; Lemma 3 uses strict inequalities $\delta<s<1-\delta$ ; Comment 1 makes the implicit $\lambda>0$ explicit; (2.14) carries Proposition 2's standing range $n\ge2$ , $0<\lambda<\sqrt n$ .

The goal does not mention $p_{\lambda,n}$ , $f_\lambda$ , $C_{\lambda,n}$ , the case split at $n=39$ , or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.

Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on $]0,1[$ ; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Ann. Probab. 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
A. Dvoretzky, J. Kiefer, J. Wolfowitz, Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator, Ann. Math. Statist. 27:642–669, 1956. https://doi.org/10.1214/aoms/1177728174
Z. W. Birnbaum, R. C. McCarty, A distribution-free upper confidence bound for P(Y<X), based on independent samples of X and Y, Ann. Math. Statist. 29:558–562, 1958.
N. V. Smirnov, Approximate laws of distribution of random variables from empirical data, Uspekhi Mat. Nauk 10:179–206, 1944.
E. Csáki, Investigations concerning the empirical distribution function, Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 23:239–327, 1974; English translation in Selected Transl. Math. Statist. Probab. 15:229–317, 1981.
G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986.

23 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality II: Binomial Tail Bound P(S − np > nε) ≤ exp(−nε²/(2(p + ε/3)(q − ε/3))) for 0 < ε ≤ qResearch Paper

Motivation

Exponential bounds for the tails of the binomial distribution are among the most frequently used tools in probability, statistics and the analysis of algorithms: they control the number of successes in independent trials, the deviation of an empirical frequency from its mean, and, through counting arguments, the empirical distribution function itself. The two classical bounds are Hoeffding's inequality, which ignores the variance, and Bernstein's inequality, which uses the variance $pq$ but loses accuracy for large deviations. Both are recorded in Shorack and Wellner, Empirical Processes with Applications to Statistics (1986), p. 440.

In his 1990 paper establishing the tight constant $2$ in the Dvoretzky–Kiefer–Wolfowitz inequality, P. Massart obtained, as a by-product of the proof, a binomial tail bound that implies both classical inequalities and, in his words, "does not seem to be known" (Massart 1990, p. 1271). Its ingredient, a lower bound for the Cramér transform of the Bernoulli law (Lemma 1), is also used in the proof of the main DKW result. This mission formalizes that by-product: Theorem 2, Lemma 1 and the Cramér–Chernoff bound (Comment 3) through which they are combined.

Setting

Fix an integer $n \ge 0$ and a success probability $p \in [0,1]$ , and write $q = 1 - p$ . A random variable $S$ has the binomial distribution $\mathcal B(n,p)$ if it counts the successes in $n$ independent trials, each succeeding with probability $p$ : $P(S = k) = \binom nk p^k q^{n-k}$ for $k = 0,\dots,n$ . Its mean is $np$ . The quantity of interest is the upper tail $P(S - np > n\varepsilon)$ for a deviation $\varepsilon$ with $0 < \varepsilon \le q$ (for $\varepsilon > q$ the event is empty).

Two auxiliary functions appear in Lemma 1. For $0 < \varepsilon \le q < 1$ (so that $p > 0$ ),

h(p,\varepsilon) = (p+\varepsilon)\log\frac{p+\varepsilon}{p} + (q-\varepsilon)\log\frac{q-\varepsilon}{q},

which is the Cramér transform of the Bernoulli law with parameter $p$ at the point $p + \varepsilon$ , i.e. the relative entropy between the Bernoulli laws with parameters $p+\varepsilon$ and $p$ . For $t \ge 0$ ,

\varphi(t) = t - \frac{t^2}{2(1 + 2t/3)} - \log(1+t).

In the Lean development these are MassartDKW.Binom.h and MassartDKW.Binom.phi.

Formalization targets

Goal: Theorem 2 (p. 1271)

If $S$ has the binomial distribution $\mathcal B(n,p)$ and $q = 1 - p$ , then for every $\varepsilon$ with $0 < \varepsilon \le q$ ,

P(S - np > n\varepsilon) \le \exp\!\left(-\frac{n\varepsilon^2}{2(p+\varepsilon/3)(q-\varepsilon/3)}\right).

Milestones

Lemma 1(i) (p. 1272): $\varphi$ is positive, increasing and convex on $[0,\infty)$ , with $\varphi(t)/t \to 1/4$ as $t \to \infty$ .
Lemma 1(ii) (p. 1272): for $0 < \varepsilon \le q = 1 - p < 1$ and $t = \varepsilon/(q-\varepsilon)$ ,

h(p,\varepsilon) \ge \frac{\varepsilon^2}{2(p+\varepsilon/3)(q-\varepsilon/3)} + \frac{\varepsilon\varphi(t)}{t}.

Comment 3 (p. 1273): for $S \sim \mathcal B(n,p)$ , $P(S - np > n\varepsilon) \le \exp(-n\,h(p,\varepsilon))$ .

Significance

The result. Theorem 2 has the shape of Bernstein's inequality with the variance proxy $pq + \varepsilon/3$ replaced by the smaller $(p+\varepsilon/3)(q-\varepsilon/3)$ ; the second factor shrinks as $\varepsilon$ approaches $q$ , so the bound is sharper in the large-deviation range, and it implies both Bernstein's and Hoeffding's inequalities for binomial tails. Lemma 1(ii) is a quantitative lower bound on the Bernoulli relative entropy, with an explicit nonnegative correction term $\varepsilon\varphi(t)/t$ , which is reusable wherever Chernoff bounds for Bernoulli sums are converted into closed-form exponents. In the paper, the same lemma is a step of the proof of the tight Dvoretzky–Kiefer–Wolfowitz inequality.

Formalizing it. The result is proved on the page, by a short calculus argument for Lemma 1 and the classical Cramér–Chernoff computation for Comment 3. To our knowledge none of the three statements has a machine-checked proof. The work this mission asks for is formalizing that known proof: the analysis of $\varphi$ (signs of derivatives, the limit at infinity), the inequality between $h$ and the explicit quadratic term, the exponential-moment computation for the binomial law in Mathlib's measure-theoretic setting, and the bookkeeping of the boundary cases $\varepsilon = q$ , $p = 0$ and $n = 0$ .

Difficulty

The obvious route to Theorem 2 is to bound the binomial moment generating function and optimize; this reproduces Comment 3, and the exponent it gives is the transcendental function $h(p,\varepsilon)$ , not the rational expression in the theorem. The step that needs care is the comparison of $h$ with $\varepsilon^2/[2(p+\varepsilon/3)(q-\varepsilon/3)]$ uniformly in $0 < \varepsilon \le q$ : a second-order Taylor expansion of $h$ in $\varepsilon$ gives only the local behaviour near $\varepsilon = 0$ , and a bound proved by Taylor expansion alone does not survive up to $\varepsilon = q$ , where the second logarithm of $h$ degenerates and $t = \varepsilon/(q-\varepsilon)$ blows up. The endpoint $\varepsilon = q$ therefore has to be treated as a limit.

Formalization scope

The binomial law is Mathlib's ProbabilityTheory.binomial n p : Measure ℕ with p : unitInterval; $S$ is an $\mathbb N$ -valued map on a probability space $(\Omega, P)$ with HasLaw S (binomial n p) P. Probabilities are values of the measure in $[0,\infty]$ , compared with real bounds through ENNReal.ofReal. The event is the strict upper tail $\{(n:\mathbb R)\varepsilon < S - np\}$ . The goal assumes only $0 < \varepsilon \le 1 - p$ , as on the page: $n = 0$ and $p = 0$ are allowed, and the denominator $2(p+\varepsilon/3)(q-\varepsilon/3)$ is positive on the whole range.

Conventions and added hypotheses ( $q$ is written out as $1 - p$ throughout):

Lean's $\log 0 = 0$ and $x/0 = 0$ : $h$ is only meaningful for $p > 0$ , so Lemma 1(ii) and Comment 3 assume $0 < p$ (the page's $q < 1$ ). The goal does not.
Lemma 1(ii) is stated in two cases. For $\varepsilon < q$ , $t = \varepsilon/(q-\varepsilon)$ is a real number. For $\varepsilon = q$ , $t = \infty$ and the correction term is its limit $\varepsilon/4$ ; reading $t = \varepsilon/0 = 0$ in Lean would give a weaker statement, which is ruled out.
"Positive" in Lemma 1(i) is stated for $t > 0$ , since $\varphi(0) = 0$ ; "increasing" is strict monotonicity on $[0,\infty)$ .

A formalization that states the goal with the exponent $n\,h(p,\varepsilon)$ , or assumes Lemma 1 or Comment 3 as hypotheses, or restricts to $\varepsilon < q$ , is not this theorem: the goal carries the explicit constants and the full range $0 < \varepsilon \le q$ .

Needed infrastructure: elementary real analysis of $\log$ (derivatives, monotonicity from derivative sign, limits at infinity), the moment generating function of the binomial law (or of a sum of independent Bernoulli variables) and Markov's inequality. The bound on the Bernoulli relative entropy and the binomial Chernoff bound are reusable beyond this mission. Contributions welcome: proofs of the three milestones, and helper lemmas computing $\mathbb E[e^{\theta S}] = (q + pe^\theta)^n$ for Mathlib's binomial.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
G. R. Shorack and J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986 (p. 440: Hoeffding's and Bernstein's inequalities for binomial tails). https://doi.org/10.1137/1.9780898719017
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58:13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

5 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

The Data-Driven Newsvendor Problem: New Bounds and Insights I: The SAA Order Is ε-Optimal with Probability at Least 1 − 2exp(−Nε²min(b,h)/((18 + 8ε)(b + h)))Research Paper

Motivation

The newsvendor problem is the basic model of stocking under uncertain demand: an order quantity is fixed before a random demand is observed, and every unit short or left over is penalized. Its solution is a quantile of the demand distribution. In practice that distribution is unknown and only a sample of past demands is available. The standard remedy, sample average approximation (SAA), replaces the expectation by the empirical average over the sample and orders the corresponding sample quantile. The practical question is how many observations make the SAA order nearly as good as the true optimum, without assuming anything about the demand distribution.

Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) gave the first distribution-free answer, using Hoeffding's inequality. Levi, Perakis and Uichanco (Oper. Res. 63(6), 2015) improved it with Bernstein's inequality. The improvement matters most when the service level is high, which is the typical case in inventory practice. This mission formalizes that improved bound, Theorem 2 of the 2015 paper.

Setting

A retailer orders $q\in\mathbb R$ units before a real demand $D$ with law $\mu$ and cdf $F(q)=\Pr(D\le q)$ is realized. Unmet demand costs $b>0$ per unit (underage cost) and unsold stock costs $h>0$ per unit (overage cost). The expected cost is

C(q)=\mathbb E\big[b(D-q)^+ + h(q-D)^+\big],

which is finite when $\mathbb E|D|<\infty$ . The critical quantile is $q^*=\inf\{q:F(q)\ge b/(b+h)\}$ , and it minimizes $C$ .

An order $q$ is $\epsilon$ -optimal when its relative regret $(C(q)-C(q^*))/C(q^*)$ is at most $\epsilon$ , i.e. $C(q)\le(1+\epsilon)C(q^*)$ . The set of such orders is $S_\epsilon$ . The function $C$ is convex with one-sided derivatives

\partial_+C(q)=-b+(b+h)F(q),\qquad \partial_-C(q)=-b+(b+h)\Pr(D<q).

The LRS interval is

S^{LRS}_\epsilon=\Big\{q:\partial_-C(q)\le\tfrac\epsilon3\min(b,h)\ \text{and}\ \partial_+C(q)\ge-\tfrac\epsilon3\min(b,h)\Big\}.

Given an i.i.d. sample $D^1,\dots,D^N$ from $\mu$ , the empirical cdf is $\hat F_N(q)=\frac1N\sum_k\mathbf 1[D^k\le q]$ , and the SAA solution is the sample quantile

\hat Q_N=\inf\{q:\hat F_N(q)\ge b/(b+h)\}.

It is a random variable through the sample.

Formalization targets

Goal: Theorem 2 (improved LRS bound)

For every demand law with $\mathbb E|D|<\infty$ , every $N\ge1$ and every $0<\epsilon\le1$ ,

\Pr\big(\hat Q_N\notin S_\epsilon\big)\le 2\exp\Big(-\frac{N\epsilon^2}{18+8\epsilon}\cdot\frac{\min\{b,h\}}{b+h}\Big).

Milestones, in the order of the paper's proof

(§2, p. 7) $C$ is convex, and its one-sided derivatives are the two formulas above.
(Theorem EC.1) Bernstein's inequality for i.i.d. bounded variables: $\Pr\big(\frac1N\sum_iX^i-\mathbb E X^1\ge t\big)\le\exp\big(-Nt^2/(2\sigma^2+2tc/3)\big)$ .
(Proposition EC.1) For every $\gamma>0$ , $\Pr\big(\partial_-C(\hat Q_N)\le\gamma\text{ and }\partial_+C(\hat Q_N)\ge-\gamma\big)\ge1-2\exp\big(-3N\gamma^2/(6bh+8\gamma(b+h))\big)$ .
(Display (3)) For $0<\epsilon\le1$ , $S^{LRS}_\epsilon\subseteq S_\epsilon$ .

Significance

The earlier LRS bound has the exponent $-\frac29N\epsilon^2\big(\min\{b,h\}/(b+h)\big)^2$ . Theorem 2 replaces the square by the first power. When the critical ratio $b/(b+h)$ approaches $1$ (high service levels), $\min\{b,h\}/(b+h)$ is small, and the required sample size drops accordingly. Raising the service level from 95% to 99% multiplies the sample size the LRS bound requires by 25, but the sample size Theorem 2 requires only by 5 (p. 9). The bound holds for every demand distribution, with no density, continuity or support assumption.

The milestones are reusable on their own. One is the one-sided derivative formula for the expected newsvendor cost. Another is Bernstein's inequality for i.i.d. bounded variables, which Mathlib does not have; it has Hoeffding's inequality. The third is a distribution-free concentration statement for sample quantiles. The result is proved in the paper. To our knowledge none of these statements is formalized; this mission produces machine-checked versions.

Difficulty

A Hoeffding-type argument yields only the squared dependence on $\min\{b,h\}/(b+h)$ . The improvement needs the variance $F(1-F)$ of the indicator $\mathbf 1[D\le q]$ , which is small near extreme quantiles. Bernstein's inequality applies at a fixed point $q$ . The sample quantile, however, is random, and $F$ can jump. The event that $\hat Q_N$ falls left of the target quantile therefore has to be reduced to deviations of $\hat F_N$ at deterministic points, with care at atoms of $D$ , where $\partial_+C$ and $\partial_-C$ differ. The final step from the derivatives to the relative regret requires convexity of $C$ and a lower bound on $C(q^*)$ that holds for every distribution.

Formalization scope

Model. The demand law is a probability measure μ on ℝ, with no sign restriction (the page's $q\ge0$ plays no role here). $F$ is Mathlib's cdf μ, and $\Pr(D<q)$ is μ (Set.Iio q). The realized cost is the published InventoryControl.newsboyLoss h b q d, and $C$ is a Bochner integral. Every statement that evaluates $C$ assumes Integrable id μ ( $\mathbb E|D|<\infty$ ). This is the standing assumption under which $C$ is an expectation. It also rules out the trivializing formalization in which a non-integrable cost integrates to $0$ and every order is $\epsilon$ -optimal.
Quantiles. $q^*$ and $\hat Q_N$ are infima (sInf) of sets that are nonempty and bounded below under the hypotheses, never argmins or choice functions. The sample is x : Fin N → ℝ under the product measure Measure.pi (fun _ => μ), with $N\ge1$ ; the indices are 0-based.
Probabilities. "With probability at least $1-p$ " is stated as an upper bound $p$ on the outer measure of the failure set.
$\epsilon$ -optimality is the multiplicative form $C(q)\le(1+\epsilon)C(q^*)$ , which avoids dividing by $C(q^*)$ .
Pinned hypotheses.
- The goal and milestone 4 are stated for $0<\epsilon\le1$ . The paper says "for any $\epsilon>0$ ", but both statements fail for large $\epsilon$ . Take $b=h=1$ , $N=1$ and $D\in\{0,M\}$ with $\Pr(D=M)=0.005$ . Then $q^*=0$ , and the order $M$ has relative regret $198$ , yet at $\epsilon=150$ the bound promises a failure probability of about $1.9\cdot10^{-4}$ .
- In Theorem EC.1, the centred bound $|X^1-\mathbb EX^1|\le c$ is added to the printed $|X^1|\le c$ . It holds for the indicators to which the paper applies the inequality.

A complete development needs the following:

the one-sided derivatives of a convex integral functional;
Bernstein's inequality for product measures;
the quantile-to-cdf reduction for the empirical and the true cdf;
the convexity estimate behind (3).

The Bernstein inequality and the sample-quantile concentration are useful beyond this mission. Contributions to any milestone are welcome.

Selected references

R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6), 2015. https://doi.org/10.1287/opre.2015.1422. Statements are cited from the authors' accepted manuscript (MIT DSpace), body pp. 7–9 and e-companion pp. ec5–ec6.
R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4), 2007. https://doi.org/10.1287/moor.1070.0272
S. N. Bernstein, Theory of Probability, Moscow, 1927.
P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.

7 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers VI: The Group-Lasso Block Update Is Zero iff ‖Aᵢᵀv‖₂ ≤ λ/ρ, Otherwise Ridge with ν‖xᵢ‖₂ = λ/ρTextbook

Why distributed model fitting

Fitting a statistical model usually means solving a convex problem of the form

\text{minimize}\quad l(Ax-b)+r(x),

where $A\in\mathbb R^{m\times n}$ holds one training example per row and one feature per column, $b\in\mathbb R^m$ is the response, $l$ is a convex loss and $r$ a convex regularizer. Least squares, the lasso, logistic regression and the support vector machine are all of this form. When either dimension is very large, or the data are stored on many machines, the problem has to be solved by processors that each see only a block of $A$ .

Chapter 8 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) shows how ADMM does this in two ways: by splitting $A$ by rows (splitting across examples, §8.2), which turns the problem into a global consensus problem, and by splitting it by columns (splitting across features, §8.3), which turns it into a sharing problem. In both cases the method is only practical because the individual updates have closed forms or reduce to small standard problems. This mission formalizes those closed forms, culminating in the update for the group lasso.

Setting

Vectors are in $\mathbb R^n$ with the Euclidean norm $\|\cdot\|_2$ ; $\|x\|_1=\sum_j|x_j|$ . Throughout, $\rho>0$ is the ADMM penalty parameter and $\lambda>0$ a regularization weight.

Splitting across examples. Partition $A$ and $b$ by rows into $N$ blocks $A_i\in\mathbb R^{m_i\times n}$ , $b_i\in\mathbb R^{m_i}$ . With scaled dual variables $u_i$ and averages $\bar x=\frac1N\sum_ix_i$ , $\bar u=\frac1N\sum_iu_i$ , the consensus ADMM iteration is

x_i^{k+1}=\operatorname*{argmin}_{x_i}\Bigl(l_i(A_ix_i-b_i)+\tfrac{\rho}{2}\|x_i-z^k+u_i^k\|_2^2\Bigr),\quad z^{k+1}=\operatorname*{argmin}_{z}\Bigl(r(z)+\tfrac{N\rho}{2}\|z-\bar x^{k+1}-\bar u^k\|_2^2\Bigr),

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z^{k+1}$ . For the lasso, $l(w)=\frac12\|w\|_2^2$ and $r=\lambda\|\cdot\|_1$ .

Splitting across features. Partition $x=(x_1,\dots,x_N)$ with $x_i\in\mathbb R^{n_i}$ and $A=[A_1\cdots A_N]$ with $A_i\in\mathbb R^{m\times n_i}$ , so $Ax=\sum_iA_ix_i$ . Introducing $z_i=A_ix_i$ gives a sharing problem; its ADMM $z$ -update minimizes $l(\sum_iz_i-b)+\sum_i\frac\rho2\|A_ix_i-z_i+u_i\|_2^2$ . Writing $\overline{Ax}=\frac1N\sum_iA_ix_i$ and $\bar z$ for the average of the $z_i$ , this reduces to a single problem in $\bar z\in\mathbb R^m$ , all dual variables coincide, and each block update minimizes

\tfrac{\rho}{2}\|A_ix_i-v\|_2^2+r_i(x_i)

for a vector $v\in\mathbb R^m$ assembled from the previous iterate. For the group lasso, $r_i(x_i)=\lambda\|x_i\|_2$ (not squared).

Soft thresholding is $S_\kappa(a)=a-\kappa$ for $a>\kappa$ , $0$ for $|a|\le\kappa$ , $a+\kappa$ for $a<-\kappa$ .

Formalization targets

Goal: the group-lasso block update (§8.3.2, pp. 69–70)

Let $h(x)=\frac\rho2\|A_ix-v\|_2^2+\lambda\|x\|_2$ on $\mathbb R^{n_i}$ and $x(\nu)=(A_i^TA_i+\nu I)^{-1}A_i^Tv$ . Then

0\in\operatorname*{argmin}h\iff\|A_i^Tv\|_2\le\lambda/\rho,

and then $0$ is the only minimizer; if $\|A_i^Tv\|_2>\lambda/\rho$ , there is exactly one $\nu>0$ with $\nu\|x(\nu)\|_2=\lambda/\rho$ , the point $x(\nu)$ minimizes $h$ , and every minimizer is of this form.

Milestones

Ridge $x_i$ -update (§8.2.1, p. 65): $x_i^{k+1}=(A_i^TA_i+\rho I)^{-1}(A_i^Tb_i+\rho(z^k-u_i^k))$ , the unique minimizer.
Soft-thresholding $z$ -update (§8.2.1, p. 65): $z^{k+1}=S_{\lambda/(\rho N)}(\bar x^{k+1}+\bar u^k)$ componentwise.
Reduction to $\bar z$ and equal duals (§8.3, p. 68): minimizers of the $N$ -block $z$ -update are exactly the vectors $z_i=\bar z+A_ix_i+u_i-\overline{Ax}-\bar u$ with $\bar z$ solving the $\bar z$ -update, and then $u_i^{k+1}=\overline{Ax}^{k+1}+\bar u^k-\bar z^{k+1}$ for every $i$ .
Feature-split lasso $\bar z$ -update (§8.3.1, p. 69): $\bar z^{k+1}=(b+\rho\overline{Ax}^{k+1}+\rho u^k)/(N+\rho)$ .
Lasso zero test, corrected (§8.3.1, p. 69): $0$ minimizes $\frac\rho2\|A_ix-v\|_2^2+\lambda\|x\|_1$ iff $\|A_i^Tv\|_\infty\le\lambda/\rho$ .
Eigendecomposition identity (§8.3.2, p. 70): if $A_i^TA_i=Q\,\mathbf{diag}(\mu)Q^T$ with $Q$ orthogonal, then $\|x(\nu)\|_2=\|\mathbf{diag}(\mu+\nu\mathbf 1)^{-1}Q^TA_i^Tv\|_2$ for $\nu>0$ .
SVM $\bar z$ -update (§8.3.4, pp. 70–71): the minimizer of $\mathbf 1^T(N\bar z+\mathbf 1)_++\frac\rho2\|\bar z-\overline{Ax}-u\|_2^2$ is a shifted soft thresholding of $v=\overline{Ax}+u$ .

Significance

The goal result says that a group-lasso block either switches off entirely, which is how group sparsity arises, or solves a ridge regression whose ridge parameter is the unique root of a scalar monotone equation; this is what makes the distributed group lasso implementable with one cached factorization per block and a bisection. The milestones are the remaining closed forms that turn the two distributed schemes of Chapter 8 into concrete algorithms, and the reduction of milestone 3 is the structural fact that lets feature splitting carry a single dual variable.

The book derives these facts in running text and states them without proof. None of them is formalized on Prove2Me, and the book's printed zero test for the lasso (p. 69) uses the wrong norm; a machine-checked collection of the correct updates removes that kind of error from the record and gives later ADMM missions a verified library of update formulas.

Difficulty

Each statement is a characterization of all minimizers of a nonsmooth convex function, not a check that a formula satisfies a stationarity equation. For the goal, the nonsmooth term $\lambda\|x\|_2$ has a kink at $0$ , $h$ need not be strictly convex when $A_i$ has a nontrivial kernel, and the existence and uniqueness of the parameter $\nu$ is part of the claim rather than an assumption: the obvious move of assuming a suitable $\nu$ and checking the formula proves nothing about the case split or about uniqueness, and the singular case of $A_i^TA_i$ is exactly where naive arguments break. Milestone 3 must handle an arbitrary convex loss $l$ , with no closed form at all.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n); matrices are Matrix (Fin m) (Fin n) ℝ acting through Matrix.toEuclideanLin; blocks are indexed by Fin N (0-based); the regularization weight $\lambda$ is lam; the eigenvalue vector the book also calls $\lambda$ (p. 70) is μ. " $x$ minimizes $F$ " is Mathlib's IsMinOn F Set.univ x. Iteration superscripts are dropped: each statement is about one update with the previous iterate given. Explicit choices:

$\rho>0$ , $\lambda>0$ and $N\ge1$ are hypotheses wherever the book uses them.
Closed forms are stated as "minimizer $\iff$ formula", which contains existence and uniqueness; the book's "the solution" in §8.3.2 is stated as existence and uniqueness of $\nu$ plus a characterization of every minimizer, with no invertibility hypothesis on $A_i^TA_i$ .
$(A_i^TA_i+\nu I)^{-1}$ is Mathlib's matrix inverse, used only for $\nu>0$ , where it is the true inverse.
The loss in milestone 3 is real valued and convex, as in (8.1).
The lasso zero test is stated with $\|\cdot\|_\infty$ ; the book prints $\|\cdot\|_2$ , which is false for the $\ell_1$ term.
The SVM $\bar z$ -update uses the coefficient $\rho/2$ printed on p. 70, which matches the printed thresholds $N/\rho$ .
The book's "assuming $A_i$ is tall" (p. 70) is not imposed; the identity holds without it.

A statement that only checks that $x(\nu)$ satisfies the optimality equation, or that assumes the parameter $\nu$ exists, does not capture the goal; the goal asserts existence and uniqueness of $\nu$ and describes every minimizer of $h$ .

Contributions welcome: subgradient calculus for $\|\cdot\|_2$ and $\|\cdot\|_1$ in EuclideanSpace, first-order optimality for convex quadratics plus a convex nonsmooth term, and the monotonicity of $\nu\mapsto\nu\|(M+\nu I)^{-1}c\|_2$ for positive semidefinite $M$ ; these are reusable for every proximal and ADMM update.

Selected references

S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1):1–122, 2011. https://doi.org/10.1561/2200000016
M. Yuan, Y. Lin, Model selection and estimation in regression with grouped variables, Journal of the Royal Statistical Society B 68(1):49–67, 2006. https://doi.org/10.1111/j.1467-9868.2005.00532.x
R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x

10 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers IV: The Covariance-Selection X-Update Is Q·diag((λᵢ + √(λᵢ² + 4ρ))/(2ρ))·QᵀTextbook

Why closed-form ADMM updates for ℓ1 problems

Many estimation problems in statistics, machine learning and signal processing minimize a smooth loss plus a nonsmooth ℓ1-type regularizer: the lasso, basis pursuit, least absolute deviations, Huber fitting, the group lasso, and ℓ1-penalized maximum likelihood for Gaussian graphical models. Chapter 6 of Boyd, Parikh, Chu, Peleato and Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Found. Trends Mach. Learn. 3(1), 2011), shows that the alternating direction method of multipliers (ADMM) splits each of these problems into a step that touches only the loss and a step that touches only the regularizer, and that each step has a closed form. The practical value of ADMM on these problems rests entirely on those closed forms: an iteration is one cached linear solve, one projection, or one thresholding.

The capstone is sparse inverse covariance selection (§6.5), the ℓ1-penalized Gaussian maximum-likelihood problem of Banerjee, El Ghaoui and d'Aspremont (2008), also solved by the graphical lasso of Friedman, Hastie and Tibshirani (2008). Its ADMM X-update minimizes a log-determinant objective over positive definite matrices, and the book shows that it is solved exactly by one symmetric eigenvalue decomposition.

Setting

All vectors are real and $\|\cdot\|_2$ is the Euclidean norm. For $\kappa\in\mathbb R$ the soft thresholding operator is $S_\kappa(a)=a-\kappa$ if $a>\kappa$ , $0$ if $|a|\le\kappa$ , and $a+\kappa$ if $a<-\kappa$ , applied componentwise to vectors and entrywise to matrices. The vector soft thresholding operator on $\mathbb R^m$ is $\mathcal S_\kappa(a)=(1-\kappa/\|a\|_2)_+a$ , with $\mathcal S_\kappa(0)=0$ . The Huber penalty is $g^{\mathrm{hub}}(a)=a^2/2$ for $|a|\le1$ and $|a|-1/2$ for $|a|>1$ , summed over components for vectors.

In scaled-form ADMM for minimizing $f(x)+g(z)$ subject to $Ax+Bz=c$ , with penalty $\rho>0$ and scaled dual variable $u$ , the updates are

x^{k+1}=\operatorname*{argmin}_x\bigl(f(x)+\tfrac\rho2\|Ax+Bz^k-c+u^k\|_2^2\bigr),\quad z^{k+1}=\operatorname*{argmin}_z\bigl(g(z)+\tfrac\rho2\|Ax^{k+1}+Bz-c+u^k\|_2^2\bigr),

followed by $u^{k+1}=u^k+Ax^{k+1}+Bz^{k+1}-c$ . "The update is given by formula $F$ " means $F$ is the unique minimizer of the corresponding subproblem.

For sparse inverse covariance selection, $S\in\mathbb R^{n\times n}$ is symmetric (the empirical covariance), $\lambda>0$ is the regularization weight, $\|M\|_F^2=\sum_{ij}M_{ij}^2$ , $\|M\|_1=\sum_{ij}|M_{ij}|$ , and $\mathbb S^n_{++}$ is the set of symmetric positive definite matrices, the domain of $\log\det$ . ADMM alternates

X^{k+1}=\operatorname*{argmin}_{X\in\mathbb S^n_{++}}\Bigl(\operatorname{Tr}(SX)-\log\det X+\tfrac\rho2\|X-Z^k+U^k\|_F^2\Bigr),\qquad Z^{k+1}=\operatorname*{argmin}_Z\Bigl(\lambda\|Z\|_1+\tfrac\rho2\|X^{k+1}-Z+U^k\|_F^2\Bigr),

and $U^{k+1}=U^k+X^{k+1}-Z^{k+1}$ .

Formalization targets

Goal: the X-update in closed form (§6.5, p. 47)

Let $S$ and $Z-U$ be symmetric, $\rho>0$ , and $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu_1,\dots,\mu_n)\,Q^T$ with $Q^TQ=QQ^T=I$ . Then

X=Q\,\mathrm{diag}\Bigl(\frac{\mu_i+\sqrt{\mu_i^2+4\rho}}{2\rho}\Bigr)Q^T

is positive definite and is the unique minimizer of $\operatorname{Tr}(SX')-\log\det X'+\frac\rho2\|X'-Z+U\|_F^2$ over $X'\in\mathbb S^n_{++}$ .

Milestones

Scalar root (p. 47): for $\rho>0$ , $t=(\mu+\sqrt{\mu^2+4\rho})/(2\rho)$ is positive and $\rho t-1/t=\mu$ .
Equation (6.5) (p. 47): the matrix $X$ above is positive definite and $\rho X-X^{-1}=\rho(Z-U)-S$ .
First-order condition (p. 47): a positive definite $X$ minimizes the X-objective over $\mathbb S^n_{++}$ if and only if $S-X^{-1}+\rho(X-Z+U)=0$ .
Z-update (p. 47): $Z_{ij}=S_{\lambda/\rho}(X_{ij}+U_{ij})$ is the unique minimizer of $\lambda\|Z\|_1+\frac\rho2\|X-Z+U\|_F^2$ .
Huber z-update (§6.1.1, p. 40): with $v=Ax-b+u$ , $z=\frac{\rho}{1+\rho}v+\frac1{1+\rho}S_{1+1/\rho}(v)$ minimizes $g^{\mathrm{hub}}(z)+\frac\rho2\|Ax-z-b+u\|_2^2$ .
Basis pursuit (§6.2, p. 41): if $AA^T$ is invertible, $(I-A^T(AA^T)^{-1}A)(z-u)+A^T(AA^T)^{-1}b$ is the projection of $z-u$ onto $\{x\mid Ax=b\}$ .
Lasso (§6.4, p. 43): $(A^TA+\rho I)^{-1}(A^Tb+\rho(z-u))$ minimizes $\frac12\|Ax-b\|_2^2+\frac\rho2\|x-z+u\|_2^2$ , and $S_{\lambda/\rho}(x+u)$ minimizes $\lambda\|z\|_1+\frac\rho2\|x-z+u\|_2^2$ .
Group lasso (§6.4.2, p. 45): blockwise $\mathcal S_{\lambda/\rho}(x_i+u_i)$ minimizes $\lambda\sum_i\|z_i\|_2+\frac\rho2\sum_i\|x_i-z_i+u_i\|_2^2$ .

Significance

The closed forms are what make ADMM competitive on these problems. For the lasso the x-update is a ridge regression whose factorization is computed once; for basis pursuit it is a cached projection; the ℓ1 step is a componentwise threshold. For covariance selection the X-update costs one eigenvalue decomposition, and the book (p. 46) cites Scheinberg, Ma and Goldfarb (2010) as showing that ADMM outperforms state-of-the-art methods on this problem. The goal also yields that $X^{k+1}$ is always positive definite, so the iterates remain in the domain of $\log\det$ without a line search.

All statements here are classical and their proofs are elementary convex analysis and linear algebra. A search of the platform found no machine-checked version of any of them. Formalizing them produces verified proximity operators (soft thresholding, vector soft thresholding, Huber, projection onto an affine set) and a verified matrix-function argument for $\log\det$ that later missions on ADMM, proximal methods and Gaussian graphical models can import.

Difficulty

The vector updates reduce to separable one-dimensional problems or to a normal equation, and the difficulty there is bookkeeping: uniqueness, the case $a=0$ of vector soft thresholding, and the three regimes of the Huber prox.

The goal is harder. The book's argument says that $X$ satisfies the gradient equation "and thus minimizes the X-minimization objective". Checking the equation is algebra; the claim to be proved is minimality over the open cone $\mathbb S^n_{++}$ , which needs the convexity (indeed strict convexity, for uniqueness) of $-\log\det$ on positive definite matrices and the identification of its gradient with $-X^{-1}$ along symmetric directions. Mathlib has determinants and positive definiteness; a usable convexity statement for $\log\det$ on $\mathbb S^n_{++}$ is not among the platform's published results. Showing that $X$ satisfies (6.5) alone does not establish the goal.

Formalization scope

Carriers. Vectors are EuclideanSpace ℝ (Fin n), matrices Matrix (Fin m) (Fin n) ℝ acting by Matrix.toEuclideanLin. The Frobenius norm and the entrywise ℓ1 norm are written as explicit sums, not through Mathlib's matrix norm instances. The vector ℓ1 norm is the platform definition HighDimStat.SparseLinear.l1Norm.
Updates as unique minimizers. Each update is stated as: the book's formula is the unique minimizer of the subproblem (IsUniqueMinimizerOn). Iterates are not defined; the subproblem's data ( $z^k$ , $u^k$ , $x^{k+1}$ ) are arbitrary.
Domain of log det. The X-objective is minimized over Matrix.PosDef only. Singular or indefinite matrices are never competitors, so Real.log of a nonpositive determinant plays no role.
Explicit hypotheses. $S$ and $Z-U$ are assumed symmetric in the goal and the first-order condition; $S$ need not be positive semidefinite. $\rho>0$ everywhere. Basis pursuit assumes $\det(AA^T)\ne0$ , which the book uses without stating. The book's $\lambda>0$ is relaxed to $\lambda\ge0$ in the thresholding statements, which contain the book's case.
Eigendecomposition. The goal holds for every orthogonal $Q$ and real $\mu$ with $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu)Q^T$ , not for one decomposition chosen by Mathlib.
Names. The book uses $\lambda$ for both the regularization weight and the eigenvalues; Lean calls them lam and μ.
Typo. The book prints $u^k$ in the group-lasso block update; the block $u_i^k$ is stated.
Ruled out. A goal that only asserts that $X$ satisfies (6.5), or that minimizes over a set extended by Real.log of nonpositive determinants, is not the book's claim; the goal states unique minimality over $\mathbb S^n_{++}$ .
Not stated. Least absolute deviations and the generalized lasso updates (same pattern as milestones 5 and 7), the overlapping group lasso, and the two-step termination claim for Huber fitting on p. 40 (whose formula $x^{\mathrm{ls}}=(A^TA)^{-1}b$ is misprinted).

Contributions welcome: convexity and strict convexity of $-\log\det$ on $\mathbb S^n_{++}$ and its derivative; a general "prox of a separable function is componentwise" lemma; and the projection onto an affine set.

Selected references

S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
O. Banerjee, L. El Ghaoui, A. d'Aspremont, Model Selection Through Sparse Maximum Likelihood Estimation for Multivariate Gaussian or Binary Data, Journal of Machine Learning Research 9, 2008, pp. 485–516. https://jmlr.org/papers/v9/banerjee08a.html
J. Friedman, T. Hastie, R. Tibshirani, Sparse Inverse Covariance Estimation with the Graphical Lasso, Biostatistics 9(3), 2008, pp. 432–441. https://doi.org/10.1093/biostatistics/kxm045
K. Scheinberg, S. Ma, D. Goldfarb, Sparse Inverse Covariance Selection via Alternating Linearization Methods, Advances in Neural Information Processing Systems 23, 2010 (reference [148] of the book).
R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society B 58(1), 1996, pp. 267–288. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
M. Yuan, Y. Lin, Model Selection and Estimation in Regression with Grouped Variables, Journal of the Royal Statistical Society B 68(1), 2006, pp. 49–67. https://doi.org/10.1111/j.1467-9868.2005.00532.x

13 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 1: Every Nondegenerate Limit Law of the Normed Residual Life Time Is of Type Π, Π_γ, Γ_α or Γ_{γ,α}Research Paper

Motivation

A component with a random lifetime $X$ that has survived to age $t$ still has a random residual life time $X - t$ . Reliability engineering, actuarial science and the statistics of exceedances over high thresholds all ask how the conditional law of $X - t$ given $X > t$ behaves when the age $t$ is large. If $X$ is exponential, the residual life has the same law at every age (lack of memory). In general it changes with $t$ , and the natural question, as in the limit theory of sample maxima, is which laws can arise as limits once the residual life is suitably rescaled and shifted.

A. A. Balkema and L. de Haan answered this question in Residual Life Time at Great Age (The Annals of Probability 2, 1974). The answer — a short list of limit types — later underlies the peaks-over-threshold method of extreme value statistics, where the continuous limit laws reappear as the generalized Pareto family (Pickands, 1975). This mission formalizes the classification theorem of the paper, Theorem 1, together with the steps of its proof in §1.

Setting

Let $X$ be a real random variable with distribution function $F$ and distribution tail $R(x) = 1 - F(x) = P\{X > x\}$ . Throughout, $R(x) > 0$ for every $x$ (equivalently $F(x) < 1$ for all $x$ ), so that the conditioning event $\{X > t\}$ never has probability zero. The residual life distribution function at age $t$ is

F_t(x) = P\{X - t \le x \mid X > t\}, \tag{1}

which vanishes for $x < 0$ .

A family of distribution functions $H_t$ converges weakly to $G$ as $t \to \infty$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$ . A distribution function $G$ is nondegenerate if it is not the distribution function of a point mass. $G$ is of type $K$ if $G(x) = K(ax + b)$ for all $x$ , with $a > 0$ and $b$ real.

The limit laws are the following distribution functions, all equal to $0$ for $x < 0$ ; for $x \ge 0$ ,

\Pi(x) = 1 - e^{-x}, \qquad \Gamma_\alpha(x) = 1 - (1+x)^{-\alpha},

\Pi_\gamma(x) = 1 - \exp\big(-\gamma\,[1 + x]\big), \qquad \Gamma_{\gamma,\alpha}(x) = 1 - \exp\big(-\gamma\,[1 + \alpha\log(1+x)]\big),

with $\alpha, \gamma > 0$ and $[a]$ the integer part of $a$ . The first two are continuous; the last two are discrete, with jumps where $1 + x$ , respectively $1 + \alpha\log(1+x)$ , crosses an integer.

The lemmas of §1 use a second normalization, which shifts $X$ instead of $X - t$ :

P\Big(\frac{X - b(t)}{a(t)} > x \;\Big|\; X > t\Big) = \min\Big(1, \frac{R(b(t) + x a(t))}{R(t)}\Big) \to S(x) \quad \text{weakly}, \tag{2–3}

where $1 - S$ is a nondegenerate distribution function. The two normalizations differ by $b(t) \mapsto b(t) + t$ .

Formalization targets

Goal: Theorem 1 (p. 796)

If $F(x) < 1$ for all $x$ , $a(t) > 0$ , and

F_t\big(b(t) + x a(t)\big) \to G(x) \quad \text{weakly as } t \to \infty

for a nondegenerate distribution function $G$ , then $G$ is of type $\Pi$ , $\Pi_\gamma$ , $\Gamma_\alpha$ or $\Gamma_{\gamma,\alpha}$ for some $\alpha, \gamma > 0$ .

Milestones (§1, pp. 794–797)

Lemma 1. Under (2), for each continuity point $y$ of $S$ with $0 < S(y) < 1$ there are $A(y) \ge 1$ and $B(y)$ with

S(x)\,S(y) = S\big(B(y) + xA(y)\big) \quad \text{whenever } S(x) < 1. \tag{4}

Corollary. $S(x) > 0$ for all $x$ .
Lemma 2. An unbounded non-increasing $H$ on $(x_0, \infty)$ that agrees with $S$ where $S < 1$ and solves $H(x)H(y) = H(B(y) + xA(y))$ agrees with $S$ where $H < 1$ .
Case 1 of the proof: if $A(y) = 1$ for every $y$ in the set $Y$ of continuity points with $S(y) < 1$ , then $1 - S$ is of type $\Pi$ or $\Pi_\gamma$ .
The commutation identity of Case 2: $B(y_1) + A(y_1)B(y_2) = B(y_2) + A(y_2)B(y_1)$ for $y_1, y_2 \in Y$ .
Case 2 of the proof: if $A(y) > 1$ for some $y \in Y$ , then $1 - S$ is of type $\Gamma_\alpha$ or $\Gamma_{\gamma,\alpha}$ .
The closing display: each of the four laws $G = 1 - S$ reproduces itself, $\min\big(1, S(B(t) + xA(t))/S(t)\big) = S(x)$ for every $t > 0$ and suitable $A(t) > 0$ , $B(t)$ ; so all four types occur as limits.

Significance

Theorem 1 is to residual lives what the extremal types theorem of Fisher–Tippett and Gnedenko is to maxima: it reduces the asymptotic analysis of the residual life to a four-type list, and with it the question of domains of attraction (§§2–3 of the paper) becomes well posed. The continuous types $\Pi$ and $\Gamma_\alpha$ are, after a change of parameters, the exponential and Pareto members of the generalized Pareto family used to model exceedances over high thresholds; the discrete types $\Pi_\gamma$ and $\Gamma_{\gamma,\alpha}$ show that once a shift is allowed, lattice-like tails produce limits with atoms, a phenomenon that the scale-only Theorem 2 excludes.

The theorem has been proved since 1974. It is not formalized in any proof assistant known to us, and Mathlib has neither weak convergence of distribution functions in the form used here, nor types, nor the residual-life limit laws. A formal development provides these objects, the functional equation (4) and its solution on a half line, and a checked proof that the four-type list is exactly right — including the discrete types, which are easy to lose in an informal treatment.

Difficulty

The obvious approach is to pass to the limit in the identity relating the residual lives at ages $t$ and $b(t)$ , obtaining a Cauchy-type functional equation for $S$ , and to solve it. Two features block a direct application of the classical solution. First, the limit is a minimum with $1$ , so convergence carries no information on the half line where $S = 1$ : equation (4) holds only where $S(x) < 1$ , and it does not determine $S$ by itself (the paper exhibits $S_0(x) = e^{-x}$ for $x \ge 1$ , $S_0 = 1$ for $x < 1$ , which satisfies (4) with $A = 1$ , $B(y) = y$ , yet $1 - S_0$ is of no limit type); Lemma 2 is needed to recover $S$ where $S = 1$ . Second, the solutions of the shifted equation $\varphi(x) + \varphi(y) = \varphi(B(y) + x)$ for a monotone $\varphi$ are not only linear: a periodic perturbation is possible, and its analysis produces the discrete laws through the integer part. A proof that assumes continuity of $S$ misses $\Pi_\gamma$ and $\Gamma_{\gamma,\alpha}$ .

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$ ; $R(x) = \mu((x,\infty))$ and $F_t(x) = \mu((t, t+x])/\mu((t,\infty))$ , with probabilities taken as real numbers. Every statement assumes $\mu((x,\infty)) > 0$ for all $x$ , the paper's standing assumption; Lean's division by zero would otherwise make the conditional laws meaningless. The normalizations satisfy $a(t) > 0$ for all $t$ (only large $t$ matter). A limit distribution function is the distribution function of a probability measure $\nu$ on $\mathbb R$ , so no mass escapes to $\pm\infty$ ; nondegenerate means $\nu$ is not a point mass; the limit tail is $S(x) = \nu((x,\infty))$ , which is right-continuous. Weak convergence is convergence at the continuity points of the limit and nowhere else. The integer part is Int.floor. Each limit law is defined to be $0$ for $x < 0$ .

Theorem 1 is stated in the normalization (1) of the theorem, the lemmas and cases in the normalization (2) of §1, as printed. Theorem 1 names its fourth family $\Gamma_{\alpha,\gamma}$ ; it is the introduction's $\Gamma_{\gamma,\alpha}$ . In Lemma 2 the left endpoint $x_0$ may be $-\infty$ (Case 1 applies the lemma on the whole line), and the condition that $B(y) + xA(y)$ lies in $(x_0, \infty)$ for $x > x_0$ is written out, since (8) presupposes it. "A pair $(A(y), B(y))$ in Lemma 1" and " $A(y) = 1$ ", " $A(y) > 1$ " are stated through pairs satisfying (4); the proof of Lemma 1 shows the pair is unique. The commutation identity is posed without the Case 2 assumption, which its derivation does not use. No hypothesis of the paper is dropped and none is added beyond these readings.

The statement is not trivialized by dropping nondegeneracy (a point-mass limit is always attainable), by requiring convergence at every $x$ (which would exclude the discrete types), or by defining the limit laws without the integer part (which would turn the discrete types into continuous ones); the formalization does none of these.

A complete development needs: the residual-life distribution function and the normed tail, weak convergence of distribution functions, types, the four limit laws; then monotone solutions of Cauchy-type functional equations on half lines, with their periodic perturbations. The functional-equation results and the closing-display computations are reusable beyond this mission, for instance for the scale-only Theorem 2 and for the domain-of-attraction results of §§2–3. Proofs of any milestone, of alternative routes to Theorem 1, and of the closing display for each family separately are welcome.

Selected references

A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548 (the source of every statement of this mission: the published article).
B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966.

10 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 4: α₁ ≤ tF′(t)/(1 − F(t)) ≤ α₂ for t ≥ t₀ Sandwiches P{(X − t)/t ≤ x | X > t} Between Γ_{α₁}(x) and Γ_{α₂}(x)Research Paper

Motivation

The residual life time of a lifetime $X$ at age $t$ is the remaining life $X - t$ given survival past $t$ . Its distribution at great age is a basic object in reliability, insurance and the statistics of extremes: excess-of-loss reinsurance prices the part of a claim above a retention level, and peaks-over-threshold methods fit a model to the observations exceeding a high level. Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974), 792–804, doi:10.1214/aop/1176996548) determined every possible limit law of the suitably normed residual life time as $t \to \infty$ and the domains of attraction of these laws; Pickands (1975) obtained the continuous part of the same picture, which is the probabilistic basis of the generalized Pareto approximation used in practice.

Limit theorems describe the behaviour only as $t \to \infty$ . Section 4 of the paper gives approximation results for finite $t$ . In extreme-value theory, von Mises (1936) gave a sufficient condition for attraction to the Fréchet law $\Phi_\alpha$ : $tF'(t)/(1 - F(t)) \to \alpha$ . Theorem 6 of the paper is a non-asymptotic, two-sided counterpart for the residual life time: two-sided bounds on the scaled hazard rate give two-sided bounds on the residual life distribution at every age past a threshold. This mission formalizes Theorem 6 (p. 801).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F(x) = P\{X \le x\}$ . For an age $t$ with $P\{X > t\} > 0$ , the residual life distribution function is

F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t + x])}{\mu((t, \infty))}, \qquad x \in \mathbb R,

which is $0$ for $x < 0$ . For $t > 0$ the residual life scaled by the age has distribution function $P\{(X - t)/t \le x \mid X > t\} = F_t(xt)$ .

For $\alpha > 0$ the Pareto-type law $\Gamma_\alpha$ is

\Gamma_\alpha(x) = 1 - (1 + x)^{-\alpha} \quad (x \ge 0), \qquad \Gamma_\alpha(x) = 0 \quad (x < 0).

It is the law of $Y - 1$ when $P\{Y > y\} = y^{-\alpha}$ for $y \ge 1$ . $F$ has a positive density $F'$ for $t \ge t_0$ if $F$ is differentiable at every $t \ge t_0$ with derivative $F'(t) > 0$ . The quantity $F'(t)/(1 - F(t))$ is the hazard rate of $X$ at $t$ , and $tF'(t)/(1 - F(t))$ is the hazard rate scaled by the age.

Formalization targets

Goal: Theorem 6 (p. 801)

Let $F$ have a positive density $F'$ for $t \ge t_0$ , and let $\alpha_1, \alpha_2 > 0$ satisfy $\alpha_1 \le tF'(t)/(1 - F(t)) \le \alpha_2$ for $t \ge t_0$ . Then for all $t \ge t_0$ and all real $x$ ,

\Gamma_{\alpha_1}(x) \;\le\; P\Big\{\frac{X - t}{t} \le x \;\Big|\; X > t\Big\} \;\le\; \Gamma_{\alpha_2}(x).

The smaller constant gives the lower bound: a smaller scaled hazard rate means a heavier tail and hence a larger chance that the remaining life is long. For a Pareto tail $1 - F(t) = Ct^{-\alpha}$ one may take $\alpha_1 = \alpha_2 = \alpha$ , and both inequalities are equalities.

Milestone: the integrated hazard bounds (proof of Theorem 6, p. 801)

For $t \ge t_0$ and $x > 0$ ,

\alpha_1 \int_t^{(1+x)t} \frac{du}{u} \le \int_t^{(1+x)t} \frac{F'(u)}{1 - F(u)}\,du \le \alpha_2 \int_t^{(1+x)t} \frac{du}{u}.

Significance

The theorem turns a pointwise condition on the hazard rate, which can be checked on a density, into a bound on the whole conditional distribution of the residual life, valid at every age $t \ge t_0$ rather than only in the limit. If moreover $tF'(t)/(1 - F(t)) \to \alpha$ , then $\alpha_1, \alpha_2$ can be taken arbitrarily close to $\alpha$ for large $t_0$ , which recovers the convergence $P\{(X - t)/t \le x \mid X > t\} \to \Gamma_\alpha(x)$ with an explicit error at finite ages. Such bounds are what a practitioner fitting a Pareto tail above a threshold needs to quantify the approximation.

The result is classical and its proof is short; it is not open. As far as is known, no machine-checked version exists, and Mathlib has no theory of residual life distributions or of the limit laws of Balkema and de Haan. A formal proof would provide reusable pieces: the identity between the integrated hazard rate and $-\log(1 - F)$ for a distribution function with a density, and the comparison of a residual life distribution with a Pareto law. The other missions of this series formalize the paper's limit theorems, for which this mission's objects (the residual life distribution and $\Gamma_\alpha$ ) are shared.

Difficulty

The mathematics is elementary; the work lies in the regularity bookkeeping that the printed proof leaves implicit. The density is only assumed to exist pointwise, so the fundamental theorem of calculus must be applied to $-\log(1 - F)$ with a derivative that is not assumed continuous, and its integrability on $[t, (1+x)t]$ has to come from the hazard bounds themselves. That $1 - F$ stays positive, that $t_0 > 0$ , and that the case $x \le 0$ is trivial all have to be derived from the hypotheses rather than assumed. Finally, the conditional probability must be identified with $1 - R((1+x)t)/R(t)$ , where $R = 1 - F$ , through the measure of intervals.

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$ , and $F$ is Mathlib's ProbabilityTheory.cdf μ. The probability $P\{(X - t)/t \le x \mid X > t\}$ is residualLife μ t (x * t) $= \mu((t, t + xt])/\mu((t, \infty))$ . $\Gamma_\alpha$ is a real function defined by cases, with Real.rpow for the power. The density is an explicit function $f$ with $F$ having derivative $f(t) > 0$ at every $t \ge t_0$ , the derivative taken within $[t_0, \infty)$ . This is a right derivative at $t_0$ and the ordinary derivative for $t > t_0$ . It is the weakest reading of "positive density $F'$ for $t \ge t_0$ ", and it admits the exact Pareto law with $t_0 = 1$ , whose distribution function has no two-sided derivative at $1$ . The bounds are stated for $t \cdot f(t)/(1 - F(t))$ with Lean's real division.

No hypothesis is added to the printed theorem, and no printed slip was found. The conditions $t_0 > 0$ and $F(t) < 1$ follow from the hypotheses: for $t \le 0$ the ratio is not $\ge \alpha_1 > 0$ , and a positive derivative on $[t_0, \infty)$ makes $F$ strictly increasing there. Lean's convention $a/0 = 0$ therefore never acts at the ages concerned. The conclusion is stated for all real $x$ , as printed; for $x \le 0$ all three quantities are $0$ . The milestone does not assume the hazard rate integrable: it is bounded and measurable on $[t, (1+x)t]$ , and a non-integrable integrand would make the inequality false rather than trivially true. A formalization that dropped the density hypothesis, replaced $F'$ by deriv without differentiability, or let the bounds hold only on a set not containing every $t \ge t_0$ would not be this theorem; all three are excluded by the statement.

A proof needs the fundamental theorem of calculus for derivatives within a half-line (in Mathlib), the identity $\int_t^{(1+x)t} du/u = \log(1+x)$ , and the chain rule for $\log(1 - F)$ . Proofs of the milestone and the goal are welcome, as are sorry-free lemmas showing that $\Gamma_\alpha$ is a distribution function and that the Pareto law satisfies the hypotheses with $\alpha_1 = \alpha_2$ .

Selected references

A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
L. de Haan, A. Ferreira, Extreme Value Theory: An Introduction, Springer, 2006. https://doi.org/10.1007/0-387-34471-3

4 thms2 active usersReviewed

Completed

Operations Research Optimal Transport Probability·Captain: mikedeng1

Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric: Performance Guarantees and Tractable Reformulations III: Asymptotic Consistency of Wasserstein Robust SolutionsResearch Paper

Motivation

Many decisions in operations research and machine learning minimize an expected cost $\mathbb E^{P}[h(x,\xi)]$ whose distribution $P$ is unknown and is seen only through $N$ independent samples. The sample-average approximation replaces $P$ by the empirical distribution and is known to produce decisions with poor out-of-sample performance when $N$ is small. Distributionally robust optimization instead minimizes the worst-case expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take this set to be a ball in the Wasserstein metric around the empirical distribution, and show that such balls deliver both finite-sample certificates and asymptotic consistency. This mission formalizes the statistical half of that paper: Section 3 and Appendix A.

A data-driven method should, at a minimum, be consistent: as the sample grows, its optimal value and decisions should approach those of the true problem. For Wasserstein balls this requires a measure concentration inequality for empirical distributions in the Wasserstein metric, which was supplied by Fournier and Guillin (PTRF 2015). The paper combines that inequality with the Kantorovich–Rubinstein duality and the Borel–Cantelli lemma.

Setting

Let $E$ be $\mathbb R^m$ with an arbitrary norm $\|\cdot\|$ and its Borel $\sigma$ -algebra. A decision $x$ ranges over a feasible set $X\subseteq\mathbb R^n$ ; the random vector $\xi$ has distribution $P$ , supported on the uncertainty set $\Xi\subseteq E$ ; the loss is $h:\mathbb R^n\times E\to\mathbb R$ . The true problem (1) has optimal value

J^\star=\inf_{x\in X}\mathbb E^P[h(x,\xi)].

The Wasserstein distance between distributions $Q_1,Q_2$ with finite first moment is

d_W(Q_1,Q_2)=\inf\Big\{\int\|\xi_1-\xi_2\|\,\Pi(d\xi_1,d\xi_2):\ \Pi\text{ a coupling of }Q_1\text{ and }Q_2\Big\}.

Given samples $\hat\xi_1,\dots,\hat\xi_N$ drawn independently from $P$ (joint law $P^N$ , and $P^\infty$ for the infinite sequence), the empirical distribution is $\widehat P_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$ , and the Wasserstein ball $\mathbb B_\varepsilon(\widehat P_N)$ is the set of distributions $Q$ on $\Xi$ with $d_W(\widehat P_N,Q)\le\varepsilon$ . The distributionally robust program (5) has optimal value

\widehat J_N=\inf_{x\in X}\ \sup_{Q\in\mathbb B_\varepsilon(\widehat P_N)}\mathbb E^Q[h(x,\xi)],

and an optimizer of it is written $\widehat x_N$ .

The light-tail condition (Assumption 3.3) asks for an exponent $a>1$ with $A=\mathbb E^P[\exp(\|\xi\|^a)]<\infty$ . Under it, and for $m\ne2$ , Theorem 3.4 (Fournier–Guillin) gives constants $c_1,c_2>0$ with

P^N\{d_W(P,\widehat P_N)\ge\varepsilon\}\le\begin{cases}c_1e^{-c_2N\varepsilon^{\max\{m,2\}}},&\varepsilon\le1,\\ c_1e^{-c_2N\varepsilon^{a}},&\varepsilon>1,\end{cases}\tag{7}

for all $N\ge1$ , $\varepsilon>0$ . Solving the right-hand side $=\beta$ for $\varepsilon$ gives the radius

\varepsilon_N(\beta)=\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/\max\{m,2\}}\text{ if }N\ge\frac{\log(c_1\beta^{-1})}{c_2},\qquad\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/a}\text{ otherwise}.\tag{8}

Formalization targets

Goal: Theorem 3.6 (asymptotic consistency)

Let $\beta_N\in(0,1)$ with $\sum_N\beta_N<\infty$ and $\varepsilon_N(\beta_N)\to0$ , and use the radius $\varepsilon_N(\beta_N)$ in (5).

(i) If $h(x,\cdot)$ is upper semicontinuous on $\Xi$ and $|h(x,\xi)|\le L(1+\|\xi\|)$ on $X\times\Xi$ , then $P^\infty$ -almost surely

\widehat J_N\ge J^\star\ \text{for all large }N\quad\text{and}\quad\widehat J_N\to J^\star.

(ii) If moreover $X$ is closed and $h(\cdot,\xi)$ is lower semicontinuous on $X$ , then $P^\infty$ -almost surely every accumulation point of $(\widehat x_N)$ is an optimal solution of (1).

Milestones

Theorem 3.5 (finite sample guarantee). For fixed $N\ge1$ and $\beta\in(0,1)$ , with radius $\varepsilon_N(\beta)$ ,

P^N\big\{\mathbb E^P[h(\widehat x_N,\xi)]>\widehat J_N\big\}\le\beta.

Lemma A.1. An upper semicontinuous $h$ on $\Xi$ with $h(\xi)\le L(1+\|\xi\|)$ is the pointwise limit on $\Xi$ of a non-increasing sequence of Lipschitz functions.
Lemma 3.7 (convergence of distributions). Any data-dependent $\widehat Q_N\in\mathbb B_{\varepsilon_N(\beta_N)}(\widehat P_N)$ satisfies

P^\infty\Big\{\lim_{N\to\infty}d_W(P,\widehat Q_N)=0\Big\}=1.

Theorem 3.2 (Kantorovich–Rubinstein duality, $d_W(Q_1,Q_2)=\sup\{\int f\,dQ_1-\int f\,dQ_2:\ f\ 1\text{-Lipschitz}\}$ ), which the proof of (i) uses, enters as a reference item: the open platform theorem WassersteinDRO.Duality.kantorovich_rubinstein, stated on the whole space for all Borel probability measures. It is not a milestone, because that statement is more general than the paper's version on $\mathcal M(\Xi)$ (the two agree for distributions in $\mathcal M(\Xi)$ by extending Lipschitz functions from $\Xi$ to the whole space).

A companion item, Example 1 (1), records that upper semicontinuity cannot be dropped in (i): for $\Xi=[0,1]$ , $P=\delta_0$ and $h=\mathbb 1_{(0,1]}(\xi)$ one has $J^\star=0$ but $\widehat J_N\ge1$ for every radius $\varepsilon>0$ .

Significance

Theorem 3.5 makes the robust optimal value an upper confidence bound on the out-of-sample cost of the robust decision. Theorem 3.6 shows that this protection does not cost consistency: with radii shrinking at a rate governed by summable confidence levels, such as $\beta_N=e^{-\sqrt N}$ , both the certificate and the decisions converge to their true counterparts. Together they are the statistical justification for the Wasserstein ambiguity sets that the rest of the paper reformulates as finite convex programs, and they are cited as the reference consistency results for Wasserstein distributionally robust optimization.

All results here are proved in the paper. None of them, nor the Fournier–Guillin inequality, is formalized on Prove2Me or in Mathlib to our knowledge. The mission adds machine-checked versions of the finite-sample and consistency statements, a monotone Lipschitz approximation lemma for semicontinuous functions with linear growth (useful wherever Lipschitz duality has to be extended to semicontinuous integrands), and a convergence lemma for measures in shrinking Wasserstein balls.

Difficulty

The obvious argument for (i) bounds the worst-case expectation by the true expectation plus a Lipschitz constant times the radius. That fails, because $h$ is only upper semicontinuous in $\xi$ , not Lipschitz, and has no Lipschitz constant to multiply. The expectations of a merely semicontinuous loss must be controlled uniformly over every distribution in the ball, including data-dependent worst-case distributions, and the almost-sure convergence of the empirical distribution alone does not give this. Example 1 of the paper shows that each regularity hypothesis is needed. On the formal side, the Wasserstein distance is an infimum over couplings on a Polish space; even its triangle inequality (gluing of couplings) and the Kantorovich–Rubinstein duality are substantial.

Formalization scope

$E$ is a finite-dimensional real normed space with its Borel $\sigma$ -algebra (BorelSpace), and $m$ is its dimension; decisions live in EuclideanSpace ℝ (Fin n). The definitions $d_W$ (type $p=1$ ), $\widehat P_N$ , $\mathbb B_\varepsilon(\widehat P_N)$ , $\mathbb E^Q$ and the worst-case expectation are the published WassersteinDRO.Duality definitions. The optimal values $J^\star$ and $\widehat J_N$ are extended reals. Standing conventions and pinned hypotheses:

"Supported on $\Xi$ " is $P(\Xi^c)=0$ ; $\Xi$ is neither closed nor convex in general. The samples lie in $\Xi$ almost surely, and optimizers and ball selections are required only for samples in $\Xi$ .
The constants $c_1,c_2>0$ enter as any constants for which (7) holds, which is how (8) is defined from Theorem 3.4. The theorem of Fournier and Guillin is not part of this mission, and $m\ne2$ is assumed because (7) and (8) are printed only for $m\ne2$ .
The loss is real-valued. In Theorem 3.5 it is assumed $P$ -integrable on $X$ , because the worst-case expectation counts only distributions under which the loss is integrable. In Theorem 3.6 the linear growth bound makes this automatic.
Probabilities "at least $1-\beta$ " are stated as bounds on the outer measure of the failure event, and " $P^\infty$ -almost surely" as an almost-everywhere statement for the product measure on sequences.
The paper's " $\widehat J_N\downarrow J^\star$ " is stated as eventual domination $\widehat J_N\ge J^\star$ plus convergence, which is what its proof establishes; monotonicity in $N$ is not claimed.

A statement in which (7) could not hold for any constants would make the goal vacuous. The concentration inequality is satisfiable (for instance by a Dirac distribution with any constants), and $\varepsilon_N(\beta)$ is defined by the paper's formula, not chosen freely.

Welcome contributions: the triangle inequality and Kantorovich–Rubinstein duality for $d_W$ , the Borel–Cantelli step for product measures, Lemma A.1, and the Fatou argument of (ii).

Selected references

P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018); source version arXiv:1505.05116v3. https://arxiv.org/abs/1505.05116v3
N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
L. V. Kantorovich and G. S. Rubinstein, On a space of totally additive functions, Vestnik Leningrad. Univ. 13 (1958).
C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
D. Bertsimas, V. Gupta and N. Kallus, Robust sample average approximation, Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445

12 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Optimal Estimation of Executive Compensation by Linear Programming I: Least Absolute Deviations under Ranking Constraints Equal a Linear ProgramResearch Paper

Motivation

A firm may know salary bounds and the ranking of positions without having a reliable sample of individual salaries suitable for least-squares estimation. Charnes, Cooper and Ferguson used that kind of partial information to estimate a salary formula from ratings assigned to job factors. Their 1955 paper gives a model in which weights respect the job hierarchy while the implied salaries approach specified salary levels as closely as possible. It then turns the sum of absolute deviations into a linear program that can be handled by the methods available for constrained optimization. The setting and transformation are in §§4–6 of the published paper.

The question here is a precise one: does the transformed program have the same optimal value and the same optimal salary weights as the original absolute-deviation problem? This matters because a linear-program solution should answer the compensation-estimation problem stated before the transformation, even though the transformed program has additional variables and a different feasible set. The mission also records the paper's seven-position numerical example, where the reported salary formula can be checked directly against the table of factor ratings.

Setting

There are $n$ rated factors and $L\ge1$ job levels ordered from highest to lowest. The rating $x_{ik}$ is the amount of factor $i$ required at level $k$ , and $a_i$ is the nonnegative weight assigned to that factor. The estimated salary at level $k$ is

S_k(a)=\sum_{i=1}^{n}a_i x_{ik}.

The salary formula applied to a person's factor amounts $y_i$ is $s=\sum_i a_i y_i$ . For the ranked positions, feasible weights satisfy the four parts of the paper's system (2): each $a_i\ge0$ ; the top-level salary is at most the ceiling $s_M$ ; successive salaries descend, $S_{k+1}(a)\le S_k(a)$ ; and the bottom-level salary is at least the floor $s_m$ . These are one-sided ceiling and floor bounds. They do not force the fitted salaries to equal the bounds.

The firm specifies target salaries $s_k$ at a finite set $K$ of levels, which includes the ceiling and floor levels in the examples and may include intermediate levels. The absolute-deviation objective of (3) is

D(a)=\sum_{k\in K}|S_k(a)-s_k|.

The original problem minimizes $D$ over the feasible weights. At a specified level, let $w_k=S_k(a)-s_k$ . The split-variable program of (4)–(5) introduces $u_k,v_k\ge0$ with $w_k=u_k-v_k$ and minimizes $P(u,v)=\sum_{k\in K}(u_k+v_k)$ . The split variables are constrained only for levels in $K$ . The salary constraints (2) continue to apply to $a$ . This is the paper's transformed linear program, with a feasible set that contains many choices of $(u,v)$ above the same weight vector Charnes, Cooper and Ferguson, §§4–5.

Formalization targets

Equivalence of the two programs

The main target is the paper's claim that the two problems have equal minimal values and that minimizers correspond §6, p. 143. In the formal statement, equal values are expressed by equality of attainable objective thresholds:

\forall t\in\mathbb R,\qquad [\exists a\text{ feasible}:D(a)\le t] \quad\Longleftrightarrow\quad [\exists(a,u,v)\text{ LP-feasible}:P(u,v)\le t].

The goal also says that $a$ minimizes $D$ exactly when the triple formed from $a$ and the positive and negative parts of $w$ minimizes $P$ . Every LP minimizer projects to a minimizer of $D$ . These clauses give the value and solution correspondence the authors use when they call the two problems equivalent.

Supporting claims and numerical result

Three milestones follow the paper's exposition. First, every feasible weight vector has a split-variable lift with the same objective. Second, every transformed feasible point projects to an original feasible weight vector with no larger original objective. Third, the minimal values agree §§5–6, pp. 141–143. Each is recorded under the unnumbered sentence from which it was extracted; the paper has no numbered lemmas.

Two companion statements record other claims: opposite coefficient columns cannot both occur among selected independent simplex columns, and the Table I data have the reported optimum. For the latter, targets are 16 at $R_1$ , 10 at $R_5$ , and 4 at $R_7$ , measured in thousands of dollars. Equation (7) assigns weights $(4,0,0,16,0,4,0,28,0)/11$ , yielding the minimum deviation $14/11$ §7, pp. 145–148. A further companion checks the redundant $R_2\le R_1$ ranking row.

Significance

The equivalence justifies using a linear-program output as an estimate for the earlier salary problem: the transformed objective reaches the same value, and its optimal weight vectors solve the original problem. The numerical claim supplies a fully specified instance with seven job levels and nine factors, including the exact fitted salaries. Without the correspondence, optimizing the enlarged variable set could give no assurance that its weights minimize the deviations the firm intended to measure.

The mathematical result was argued in the 1955 paper; this mission asks for a machine-checked formulation and proof of that known result. The statements compile as open Lean theorems, so compilation alone does not establish their truth. Closing them would add a reusable treatment of absolute-deviation objectives under finite linear inequalities and an exact certificate for the paper's worked example. The consistency claim in the appendix is a separate mission because it concerns perturbations of another linear program, not this transformation.

Difficulty

The split-variable program permits $u_k$ and $v_k$ to be simultaneously positive even when their difference is fixed. Consequently, simply identifying the two feasible sets would misstate the transformation: one has extra degrees of freedom. A proof must relate their objective values and then account for optimal solutions on both sides. The numerical example has a separate difficulty. Substituting the reported weights verifies a feasible objective of $14/11$ , but does not by itself rule out another feasible weight vector with a smaller deviation. The global lower bound is part of the companion theorem.

Formalization scope

The Lean development represents factor and level vectors by functions on Fin n and Fin L, and sums explicitly over finite indices. Paper level 1 is Lean index 0; paper level $L$ is the final Fin L index. The assumption $L\ge1$ is explicit because both the top and bottom level are named. No sign, monotonicity, or boundedness assumptions are imposed on the ratings beyond what the paper states. The weights are componentwise nonnegative. Intermediate target salaries enter the objectives through $K$ but add no constraints to (2), matching the paper's treatment of $R_5$ .

A minimizer is a feasible point whose objective is no larger than that of every feasible point. The equality of minimal values uses the threshold formula above, so an empty feasible set cannot inherit a spurious real infimum. The transformed feasible set is exactly the split-variable system of (4)–(5); defining it as only the image of a chosen lift would make the principal comparison empty of content. The Table I constants are exact rational values in units of $1{,}000$ . The paper rounds some displayed salaries, while Lean records their exact fractions. The generic column-independence companion is stated for an arbitrary finite matrix, with the basis and zero nonbasic coordinates explicit.

The shared definition module provides the salary map, feasibility predicates, objectives, minimizers, and example data. A full development can contribute proofs of the three milestones, the main equivalence, the column claim, the numerical lower bound, and the redundant-row fact. The finite absolute-deviation and split-variable statements can also serve later formalizations with other linear constraints.

Selected references

A. Charnes, W. W. Cooper, and R. O. Ferguson, Optimal Estimation of Executive Compensation by Linear Programming, Management Science 1(2), 138–151, 1955. DOI 10.1287/mnsc.1.2.138.

5 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

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

Motivation

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

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

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

Setting

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

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

The minimal divergence is

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (pp. 15–16)

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

13 thms2 active usersReviewed

Completed

Machine Learning Optimal Transport Optimization·Captain: mikedeng1

Robust Wasserstein Profile Inference and Applications to Machine Learning 2: ℓp-Regularized Logistic Regression and the Hinge-Loss SVM Are Wasserstein DRO under a Label-Preserving Transport CostResearch Paper

Motivation

Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty $\|\beta\|_p$ whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).

Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price $\kappa$ for flipping a label, and obtained regularized logistic regression only in the limit $\kappa \to \infty$ . The result formalized here is the exact statement at $\kappa = \infty$ , together with the analogous statement for the hinge loss.

Setting

Training data are pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with predictors $X_i \in \mathbb R^d$ and labels $Y_i \in \{-1,+1\}$ , $n \ge 1$ . Their empirical distribution is $P_n = \frac1n\sum_{i=1}^n \delta_{(X_i,Y_i)}$ , a probability measure on $Z = \mathbb R^d \times \mathbb R$ .

For a cost $c : Z \times Z \to [0,\infty]$ , the optimal transport cost between probability measures $P$ and $Q$ on $Z$ is

D_c(P,Q) = \inf\big\{\mathbb E_\pi[c(U,W)] : \pi \text{ a probability measure on } Z\times Z,\ \pi_U = P,\ \pi_W = Q\big\}.

The cost used here is the label-preserving cost: for $q \in [1,\infty]$ ,

N_q\big((x,y),(u,v)\big) = \|x - u\|_q \text{ if } y = v, \qquad +\infty \text{ otherwise}.

Every distribution $P$ with $D_{N_q}(P,P_n) < \infty$ has the same label distribution as $P_n$ ; only the predictors are perturbed. The exponent $p$ is the conjugate of $q$ , $1/p + 1/q = 1$ .

The losses are the log-exponential loss $\log(1 + e^{-y\beta^T x})$ and the hinge loss $(1 - y\beta^T x)^+$ , for a coefficient vector $\beta \in \mathbb R^d$ . The worst-case expected loss at radius $\delta \ge 0$ is $\sup\{\mathbb E_P[l] : D_{N_q}(P,P_n) \le \delta\}$ , the supremum over probability measures $P$ on $Z$ .

Formalization targets

Goal: Theorem 2 (p. 11)

For every $\delta \ge 0$ and every $\beta \in \mathbb R^d$ ,

\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[\log(1 + e^{-Y\beta^T X})\big] = \frac1n\sum_{i=1}^n \log(1 + e^{-Y_i\beta^T X_i}) + \delta\|\beta\|_p,

\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[(1 - Y\beta^T X)^+\big] = \frac1n\sum_{i=1}^n (1 - Y_i\beta^T X_i)^+ + \delta\|\beta\|_p,

and consequently the two identities obtained by taking $\inf_{\beta}$ on both sides, which is how the paper prints the theorem.

Milestones

Proposition 1 (p. 10): strong duality, $\sup_{P: D_c(P,P_n)\le\delta}\mathbb E_P[l] = \min_{\gamma\ge0}\{\gamma\delta + \frac1n\sum_i\varphi_\gamma(X_i,Y_i)\}$ with $\varphi_\gamma(z_0) = \sup_z\{l(z) - \gamma c(z,z_0)\}$ , for a lower semicontinuous cost vanishing on the diagonal, an upper semicontinuous loss and $\delta > 0$ .
Logistic inner supremum (proof of Theorem 2, p. 30): $\sup_x\{\log(1+e^{-y_0\beta^T x}) - \lambda\|x - x_0\|_q\}$ equals the loss at $x_0$ if $\|\beta\|_p \le \lambda$ and $+\infty$ otherwise.
Logistic outer minimisation (p. 30): the infimum over $\lambda \ge 0$ of $\delta\lambda$ plus the average of these suprema equals the regularized empirical loss.
Hinge inner supremum (pp. 30–31) and 5. hinge outer minimisation (p. 31): the same two steps for the hinge loss.

Significance

The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty $\delta\|\beta\|_p$ has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in $\ell_\infty$ give an $\ell_1$ penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for $\rho = 1$ .

The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in $[0,\infty]$ ), a checked version of the duality step specialised to this cost, and the treatment of boundary cases ( $\delta = 0$ , $\beta = 0$ , $q \in \{1,\infty\}$ ) that the paper does not discuss.

Difficulty

The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on $\mathbb R^{d+1}$ , with a cost that takes the value $+\infty$ and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms $\ell_p$ and $\ell_q$ , including $q = 1$ and $q = \infty$ , and for the hinge loss a minimax exchange over $\alpha \in [0,1]$ . Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary $\lambda = \|\beta\|_p$ .

Formalization scope

Predictors are Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis $Y_i \in \{-1,+1\}$ , which Theorem 2 inherits from Example 2; the cost $N_q$ is defined on all of $\mathbb R^d\times\mathbb R$ .
The $\ell_q$ norm is the norm of PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; $q = 1$ and $q = \infty$ are included, and no further restriction on $q$ is imposed.
The transport cost is an infimum in $[0,\infty]$ over probability measures on $Z\times Z$ with both marginals fixed. Expectations are lower Lebesgue integrals of the nonnegative losses, and the worst case is a supremum in $[0,\infty]$ over probability measures. The empirical distribution is the published platform definition WassersteinDRO.Regularization.empiricalDistribution.
Readings. The paper prints the SVM identity without $\inf_\beta$ on the right; the goal states the per- $\beta$ identities (what the proof establishes) and the identities of infima with $\inf_\beta$ on both sides. The proof's displays write the transport norm as $\|\cdot\|_p$ and the penalty as $\|\beta\|_q$ , the reverse of the theorem; milestones use the theorem's convention. The logistic chain's printed indicators $\mathbf 1_{\{\lambda>\|\beta\|\}}$ , $\infty\mathbf 1_{\{\lambda\le\|\beta\|\}}$ should read $\ge$ and $<$ ; the stated end-to-end identity is unaffected. Proposition 1 is stated with a fixed nonnegative loss and $\delta > 0$ .
A trivializing formalization is ruled out: a cost infimum over sub-probability couplings or with one marginal free, or a Bochner expectation that vanishes on non-integrable laws, would make the worst case $+\infty$ or $0$ ; the definitions here fix both marginals, use probability measures only and integrate in $[0,\infty]$ . At $\delta = 0$ the ball is $\{P_n\}$ and both sides reduce to the empirical loss.
Infrastructure needed: optimal-transport duality with extended-valued lower semicontinuous costs (reusable well beyond this mission), Hölder equality cases for PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.

Selected references

J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019; arXiv:1610.05627v4. https://arxiv.org/abs/1610.05627
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, NIPS 2015. https://arxiv.org/abs/1509.09259

12 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Proposition 5

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

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

Milestones, in proof order

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

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

Significance

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

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

15 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

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

Why learn demand while pricing?

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

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

Market, demand, and policy

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

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

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

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

Formalization targets

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

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

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

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

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

What the result provides

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

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

Main difficulty

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

Formalization scope

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

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

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

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

Selected references

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

13 thms2 active usersReviewed

Completed

Machine Learning Optimization Probability·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1, Eq. (2)

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

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

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

Milestones (Appendix A)

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

A complete development needs:

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

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

Selected references

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

15 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Simultaneously Learning and Optimizing Using Controlled Variance Pricing 1: Controlled Variance Pricing Has Regret O(T^α + T^(1−α) log T)Research Paper

Motivation

A firm that sets prices without knowing how demand responds to them has to learn the demand curve from its own sales. Each price it charges is both a revenue decision and an experiment. The natural policy, certainty equivalent pricing, re-estimates the demand parameters after every period and charges the price that would be optimal if the estimates were exact. den Boer and Zwart show that this policy can fail: with positive probability its prices settle at a suboptimal value, because they converge too fast for the estimates to keep improving (den Boer–Zwart 2014, Proposition 1, the subject of the companion mission). The same phenomenon was found by Lai and Robbins (1982) for a linear control problem.

Their remedy, Controlled Variance Pricing (CVP), keeps certainty equivalent pricing but forces the sample variance of the chosen prices to decay no faster than $t^{\alpha-1}$ . The main result is that this small amount of enforced exploration gives regret $O(T^\alpha + T^{1-\alpha}\log T)$ , hence $O(T^{1/2+\delta})$ for every $\delta > 0$ , for a broad class of demand models that are specified only through their first two moments. Keskin and Zeevi (2014) later placed CVP in a larger family of semi-myopic policies with $\sqrt T\log T$ regret for linear demand.

Setting

A seller chooses in each period $t = 1, 2, \dots$ a price $p_t \in [p_l, p_h]$ , with $0 < p_l < p_h$ , and then observes demand $d_t$ . Demand at price $p$ has mean $h(a_0^{(0)} + a_1^{(0)}p)$ and variance $\sigma^2 v(h(a_0^{(0)} + a_1^{(0)}p))$ , where the link $h$ and variance function $v$ are known and $C^2$ on $[0,\infty)$ , $\dot h > 0$ , and the parameter $a^{(0)} = (a_0^{(0)}, a_1^{(0)})$ with $a_0^{(0)} > 0 > a_1^{(0)}$ is unknown. The noise $e_t = d_t - h(a_0^{(0)} + a_1^{(0)}p_t)$ is a martingale difference with conditional variance $\sigma^2 v(\cdot)$ and a uniformly bounded conditional moment of some order $r > 3$ .

The expected revenue is $r(p, a) = p\,h(a_0 + a_1p)$ . Near $a^{(0)}$ it has a unique maximizer $p(a)$ in the open interval $(p_l, p_h)$ with $\partial_p^2 r < 0$ there, and $p_{\mathrm{opt}} = p(a^{(0)})$ . The regret of a policy is

\operatorname{Regret}(T) = \mathbb E\Big[\sum_{t=1}^T r(p_{\mathrm{opt}}, a^{(0)}) - r(p_t, a^{(0)})\Big].

The estimate $\hat a_t$ is the maximum quasi-likelihood estimate (MQLE), the root of the quasi-score equation (3), $\sum_{i\le t} \frac{\dot h}{\sigma^2 v(h)}(1, p_i)^\top(d_i - h(\hat a_0 + \hat a_1 p_i)) = 0$ . With $\bar p_t$ and $\operatorname{Var}(p)_t$ the sample mean and variance of $p_1,\dots,p_t$ , the taboo interval is $\mathrm{TI}(t) = (\bar p_t - w_t, \bar p_t + w_t)$ with $w_t = \sqrt{c[(t+1)^\alpha - t^\alpha](t+1)/t}$ . CVP starts from two distinct prices $p_1, p_2$ , fixes $\alpha \in (0,1)$ and $0 < c < 2^{-\alpha}(p_1-p_2)^2\min\{1,(3\alpha)^{-1}\}$ , and for $t \ge 2$ : if $\hat a_t$ does not exist or has the wrong signs, it charges whichever of $p_1, p_2$ is farther from $\bar p_t$ ; otherwise it charges $p(\hat a_t)$ if that keeps $\operatorname{Var}(p)_{t+1} \ge c(t+1)^{\alpha-1}$ , and the best price outside $\mathrm{TI}(t)$ if not.

Formalization targets

Goal: Theorem 1

\operatorname{Regret}(T, \mathrm{CVP}) = O\big(T^\alpha + T^{1-\alpha}\log T\big) \qquad (1/2 < \alpha < 1),

stated as: there is $K > 0$ , depending on the model, $\alpha$ , $c$ and the initial prices but not on $T$ , with $\operatorname{Regret}(T) \le K(T^\alpha + T^{1-\alpha}\log T)$ for all $T \ge 1$ . The constant is left free, so the statement survives any sharpening of the constants.

Milestones

Proposition 2: $\operatorname{Var}(p)_t \ge c\,t^{\alpha-1}$ for all $t \ge 2$ along every CVP path.
Lemma 1: $\lambda_{\max}(P_t) \le (1+p_h^2)t$ and $t\operatorname{Var}(p)_t \le (1+p_h^2)\lambda_{\min}(P_t)$ for the design matrix $P_t = \sum_{i\le t}(1,p_i)^\top(1,p_i)$ .
Proposition 3: $\hat a_t$ eventually exists, $\hat a_t \to a^{(0)}$ a.s., and for some $\rho_0$ , $\mathbb E[T_{\rho_0}^{1/2}] < \infty$ and $\mathbb E[\|\hat a_t - a^{(0)}\|^2\mathbf 1_{t > T_{\rho_0}}] = O(\log t/t^\alpha)$ .
Eq. (11): in the normal–linear case, $\mathbb E\|\hat a_t - a^{(0)}\|^2 = O(\log t / t^\alpha)$ .
Eqs. (17), (18), (20): the quadratic revenue gap, the local Lipschitz bound on $p(a)$ , and $|p_{t+1} - p(\hat a_t)| \le |\mathrm{TI}(t)|$ for large $t$ .
The closing bound $\mathbb E[(p_t - p_{\mathrm{opt}})^2] = O(t^{\alpha-1} + \log t/t^\alpha)$ .

Significance

The theorem shows that a policy that is certainty equivalent almost all of the time, with a single interpretable tuning parameter $\alpha$ , attains regret $O(T^{1/2+\delta})$ in generalized linear demand models, without distributional assumptions beyond two moments. It explains the role of $\alpha$ precisely: $T^\alpha$ is the cost of exploration and $T^{1-\alpha}\log T$ the cost of estimation error. Proposition 2 and Lemma 1 are reusable for any policy that enforces a variance floor on its actions, and (11) is a self-contained rate for least squares under adaptively chosen designs.

The result is proved in the paper, with Proposition 3 delegated to den Boer and Zwart (2012) for general links. To our knowledge none of it has been machine-checked. A formalization would verify the delegated consistency argument, fix the conditions under which it applies (see Formalization scope), and provide a Lean development of adaptive least squares and quasi-likelihood rates that the related Keskin–Zeevi missions also need.

Difficulty

The deterministic parts are short. The difficulty is Proposition 3. The prices are chosen adaptively from past data, so the regressors are not independent of the noise, and standard rates for (quasi-)likelihood estimates do not apply. The natural argument, bounding $\|\hat a_t - a^{(0)}\|^2$ by $Q_t/\lambda_{\min}(P_t)$ with $Q_t$ a self-normalized martingale quadratic form, needs a bound $\mathbb E[Q_t] = O(\log t)$ that holds in expectation and not only almost surely, as in Lai and Wei (1982). For a non-linear link the MQLE is defined only implicitly, and its existence near $a^{(0)}$ has to be shown first, with a moment bound on the last time it fails. That is the random time $T_\rho$ . Turning almost-sure consistency into a rate in expectation is where most of the work lies.

Formalization scope

All declarations live in the namespace CVPricing.Regret. Periods are 1-based. Prices, demands and parameters are real; $a = (a_0, a_1) \in \mathbb R \times \mathbb R$ with the Euclidean norm (euclidNorm), not Mathlib's sup norm. The design matrix, sample mean and $t\operatorname{Var}(p)_t$ are the published Keskin–Zeevi definitions fisherOf, avgPriceOf, infoMetricOf. Every $O(\cdot)$ is "there is $K > 0$ such that for all $t$ ", with $K$ quantified after the model data. Rates are stated for $t \ge 2$ and the regret for $T \ge 1$ . $h$ and $v$ are total functions constrained on $[0,\infty)$ . A root of (3) counts only where $\hat a_0 + \hat a_1 p_i \ge 0$ for every observed $p_i$ . CVP is a predicate on a realized path that allows every maximizer in (7) and (8).

Disclosed deviations from the page:

the model requires $a_0^{(0)} + a_1^{(0)}p_h > 0$ (printed: $\ge 0$ ), because in the boundary case the policy's case (c) fires infinitely often and the proof of Theorem 1 does not cover it;
(3) is assumed to have at most one root (the page notes roots need not be unique, and the policy cannot select the root nearest $a^{(0)}$ );
the neighbourhood assumption is read as a unique maximizer over $[p_l, p_h]$ lying in $(p_l, p_h)$ ;
the demand process is given by its conditional mean, its conditional variance and (2), with integrable noise moments, not by a fixed law $D(p)$ ;
the initial prices are deterministic.

Corrected slips: Proposition 2 is stated for $c \le 2^{-\alpha}(p_1-p_2)^2\min\{1/2,(3\alpha)^{-1}\}$ , because the printed range fails at $t=2$ ( $\operatorname{Var}(p)_2 = (p_1-p_2)^2/4$ , not $/2$ ). Theorem 1 keeps the printed range. Eq. (20) is stated for $p_{t+1}$ and for $t$ beyond an explicit threshold.

The goal does not assume the variance bound, consistency or (20). The policy contains the variance check and the taboo interval, and the regret is the expectation over the actual price process. A statement that assumed any of these, or that dropped the taboo step, would be trivial or false. Contributions are welcome on adaptive least squares (Sherman–Morrison and determinant-ratio bounds), martingale last-time moment bounds, and the implicit-function step (18).

Selected references

A. V. den Boer, B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
A. V. den Boer, B. Zwart, Mean square convergence rates for maximum quasi-likelihood estimators, Stochastic Systems 4(2):375–403, 2014 (cited as 2012 working paper). https://doi.org/10.1214/12-SSY086
T. L. Lai, C. Z. Wei, Least squares estimates in stochastic regression models with applications to identification and control of dynamic systems, Annals of Statistics 10(1):154–166, 1982. https://doi.org/10.1214/aos/1176345697
T. L. Lai, H. Robbins, Iterated least squares in multiperiod control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/S0196-8858(82)80005-5
N. B. Keskin, A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014. https://doi.org/10.1287/opre.2014.1294

13 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Simultaneously Learning and Optimizing Using Controlled Variance Pricing 2: Certainty Equivalent Pricing Fails to Converge to the Optimal Price with Positive ProbabilityResearch Paper

Why myopic pricing is a problem

A seller who does not know how demand responds to price has to learn the demand curve from its own sales while it is selling. The most natural policy is certainty equivalent pricing (also called myopic pricing or passive learning): after every period, estimate the unknown demand parameters from all data collected so far, and charge the price that would be optimal if the estimates were the truth. It is simple, uses all data, and is what a price manager would do without further thought.

den Boer and Zwart (Management Science 60(3):770–783, 2014) show that this policy can fail. In the linear-demand, Gaussian-noise model, the prices it produces fail to converge to the optimal price with positive probability: the policy is not strongly consistent. The result motivates the paper's main contribution, controlled variance pricing, which adds just enough price dispersion to keep learning (treated in the companion mission of this series).

The phenomenon has a history in adaptive control:

1976. Anderson and Taylor study the linear system $y_t = a_0 + a_1x_t + \epsilon_t$ controlled by a certainty equivalent rule that steers $y_t$ to a target, and examine by simulation the statistical properties of the least squares estimates it produces (Econometrica 44(6), 1976).
1982. Lai and Robbins (Adv. Appl. Math. 3(1), 1982) prove that there are parameter values for which the certainty equivalent controls converge with positive probability to a value different from the optimal control.
2014. den Boer and Zwart adapt the argument to revenue maximization with linear demand, without the conditions Lai and Robbins place on the initial inputs and the input bounds: any two different initial prices in $[p_l, p_h]$ give the failure with positive probability.

Setting

A monopolist sells one product in periods $t = 1, 2, \dots$ at prices $p_t$ from an interval $[p_l, p_h]$ with $0 < p_l < p_h$ . The demand in period $t$ is

d_t = a_0^{(0)} + a_1^{(0)} p_t + e_t ,

where $e_1, e_2, \dots$ are independent $N(0, \sigma^2)$ random variables. The parameters are unknown to the seller and satisfy $\sigma > 0$ , $a_0^{(0)} > 0$ , $a_1^{(0)} < 0$ , $a_0^{(0)} + a_1^{(0)}p_h \ge 0$ . The expected revenue at price $p$ is $r(p, a_0, a_1) = p(a_0 + a_1p)$ , maximized at the optimal price

p_{\mathrm{opt}} = -\frac{a_0^{(0)}}{2a_1^{(0)}}, \qquad p_l < p_{\mathrm{opt}} < p_h .

Certainty equivalent pricing charges two different initial prices $p_1 \ne p_2$ in $[p_l, p_h]$ . After $t \ge 2$ periods it computes the least squares estimates $\hat a_t = (\hat a_{0t}, \hat a_{1t})$ , the solution of the normal equations $\sum_{i \le t}(1, p_i)^{\mathsf T}(d_i - \hat a_{0t} - \hat a_{1t}p_i) = 0$ , and charges

p_{t+1} = \arg\max_{p \in [p_l, p_h]} p\,(\hat a_{0t} + \hat a_{1t}p),

with $p_{t+1} = p_h$ when the estimated slope $\hat a_{1t}$ is nonnegative.

Formalization targets

Goal: Proposition 1

P\big(p_t \not\to p_{\mathrm{opt}}\big) > 0 .

The goal states only the failure of convergence, for every admissible parameter and every pair of different initial prices; it does not fix where the prices go.

Stronger: the prices stick at the boundary

P\big(p_t = p_h \ \text{for all } t \ge 3\big) > 0 .

This is what the paper's argument establishes; since $p_{\mathrm{opt}} < p_h$ it implies the goal.

Milestones

The milestones are the displayed steps of the appendix proof, in attack order: the determinant of the coefficient matrix of the linear system (12); the bound $P(\sup_{t \ge 3}|(t-2)^{-1}\sum_{i=3}^t e_i| > \epsilon) \le 8\sigma^2\epsilon^{-2} < 1$ for $\epsilon > \sqrt 8\,\sigma$ ; positivity of the probability of an explicit event $A_\delta$ on the noise for large $\delta$ ; the case $t = 2$ (the first fitted line pushes $p_3$ to $p_h$ ); the representation $\hat a_t - a^{(0)} = (\bar e_t - \bar p_tC_t/V_t,\ C_t/V_t)$ of the least squares error; recursive and closed forms of $V_t$ and $C_t$ ; and the deterministic induction that every noise path in $A_\delta$ keeps the price at $p_h$ forever.

Significance

The result is the standard counterexample to certainty equivalence in dynamic pricing. It shows that estimation and optimization cannot be separated naively: a policy that always exploits its current estimate can lock itself into a price at which the data no longer move the estimate enough to correct it. Every later policy in this literature that forces exploration (controlled variance pricing, semi-myopic policies, constrained iterated least squares) is designed against this failure, and its necessity is argued by pointing to results of this kind.

The result is proved in the paper; nothing here is open. To our knowledge it has no machine-checked proof. Formalizing it adds:

a verified pathwise analysis of the least squares recursion along a price path, reusable for other proofs about adaptive estimation with two parameters;
a verified maximal bound for running means of i.i.d. Gaussian noise, of the kind used in many consistency proofs;
a clean probabilistic statement of the failure, against which consistency results for exploration policies can later be contrasted.

Difficulty

The obvious heuristic, "with positive probability the first two observations are so noisy that the fitted slope is wrong", is not enough: one bad estimate is corrected by later data unless the policy stops generating informative data. The proof has to control the whole infinite future. It does so by showing that on a single event, defined through the first two noise values and a uniform bound on all later running means, the price stays at $p_h$ forever, which requires the closed form of the least squares estimate along a price path that is constant from period 3 on. That event involves infinitely many noise variables, so its probability is positive only through a maximal inequality, and independence between $(e_1, e_2)$ and the later noise. A second subtlety is the choice of constants: the size of the band $\delta$ enters the conditions on $(e_1, e_2)$ , so the order in which $\delta$ and the set of admissible $(e_1, e_2)$ are chosen matters (the printed proof picks them in a circular order; a non-circular choice exists).

Formalization scope

Model. CVPricing.CertEquiv.Model bundles $p_l, p_h, a_0^{(0)}, a_1^{(0)}, \sigma$ with the standing assumptions of §2 as fields, including $p_l < p_{\mathrm{opt}} < p_h$ (the paper's neighbourhood assumption specialized to linear demand). The noise is the referenced published definition RobustBooking.Shared.GaussianNoise (measurable, mutually independent, each $N(0, \sigma^2)$ ); its Lean index $k$ is period $k+1$ , so the paper's $e_i$ is ε (i - 1).
Policy. cePrice is a deterministic recursion on a noise path, so the random price process is obtained by evaluating it at $\omega$ . Periods are 1-based. The least squares estimate is the referenced KeskinZeevi.SufficientConditions.lsEstimateOf, the solution of the normal equations (4), unique whenever $p_1 \ne p_2$ . The certainty equivalent rule is the projection of $-\hat a_{0t}/(2\hat a_{1t})$ onto $[p_l, p_h]$ when $\hat a_{1t} < 0$ , and $p_h$ when $\hat a_{1t} \ge 0$ ; the latter is the convention the paper's proof adopts for wrong-signed estimates.
Corrected slips. The definition of the event $A$ is printed with " $\delta|\bar e_t| \le \delta$ " (read $|\bar e_t| \le \delta$ ) and with its second line missing a factor $\delta$ on the term $(2p_h - p_1 - p_2)$ ; both are restored as in (12) and the last display of the proof. The intercept of the first fitted line is printed without $a_0^{(0)}$ ; the correct intercept is stated, and the printed condition remains sufficient for $p_3 = p_h$ .
WLOG. The steps of the proof assume $p_1 < p_2$ and are stated under that ordering; the goal and the stronger statement cover $p_1 \ne p_2$ .
No trivialization. The goal is a statement about the Gaussian law of the noise: a theorem that exhibits one bad noise path, or that assumes $P(A) > 0$ , does not prove it. The event in the goal is a set of outcomes whose measurability is not asserted.
Welcome contributions. Kolmogorov's maximal inequality for sums of independent square-integrable variables; least squares identities for two-parameter regression; the independence argument separating $(e_1, e_2)$ from the later noise.

Selected references

A. V. den Boer, B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
T. L. Lai, H. Robbins, Iterated least squares in multiperiod control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/S0196-8858(82)80005-5
T. W. Anderson, J. B. Taylor, Some experimental results on the statistical properties of least squares estimates in control problems, Econometrica 44(6):1289–1302, 1976. https://doi.org/10.2307/1914261
Y. S. Chow, H. Teicher, Probability Theory: Independence, Interchangeability, Martingales, 3rd ed., Springer, 2003. https://doi.org/10.1007/978-1-4612-1950-7

15 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems 1: Finite-Sample Confidence Region for the Mean and CovarianceResearch Paper

Motivation

An optimization model often needs a probability distribution for an uncertain cost or demand, while a practitioner has only a finite sample from that distribution. Replacing the distribution by the empirical one can hide uncertainty in its estimated mean and covariance. Delage and Ye use a finite-sample confidence region for these two moments to justify a distributional ambiguity set in data-driven stochastic programming Delage and Ye, 2010. The present mission concerns the confidence region itself: it asks how far the population moments can be from the sample estimates when the normalized random vector has bounded support.

The source for every theorem index and page number here is the authors' draft dated 20 February 2008, not an independently checked pagination of the published article. Its §4 starts from independent observations and Assumption 4, then obtains a sample-mean bound, a covariance bound around the known mean, and finally the joint bound for estimates computed entirely from the sample.

Setting

Let $\xi\in\mathbb R^m$ have distribution $P$ , mean $\mu=\mathbb E_P[\xi]$ , and covariance $\Sigma=\mathbb E_P[(\xi-\mu)(\xi-\mu)^\mathsf T]$ . Assume $\Sigma$ is positive definite. For $M\ge1$ independent observations $\xi_1,\ldots,\xi_M$ , the empirical mean and empirical covariance in this section are

\widehat\mu=\frac1M\sum_{i=1}^M\xi_i,\qquad \widehat\Sigma=\frac1M\sum_{i=1}^M(\xi_i-\widehat\mu)(\xi_i-\widehat\mu)^\mathsf T.

The divisor is $M$ , including for the covariance; the paper's earlier discussion of an unbiased estimator with divisor $M-1$ does not govern §4. When the true mean is known, write $\widehat\Sigma(\mu)=M^{-1}\sum_i(\xi_i-\mu)(\xi_i-\mu)^\mathsf T$ . Matrix order $A\preceq B$ means $B-A$ is positive semidefinite. The squared Mahalanobis distance of a vector $v$ is $v^\mathsf T\Sigma^{-1}v$ .

Assumption 4 bounds the normalized observations: for some $R\ge0$ , $(\xi-\mu)^\mathsf T\Sigma^{-1}(\xi-\mu)\le R^2$ with probability one. Equivalently, $\zeta=\Sigma^{-1/2}(\xi-\mu)$ lies almost surely in a Euclidean ball of radius $R$ ; it has mean zero and covariance $I$ . The sample law is $P^M$ , the product measure of $M$ identical copies. These choices make the probability in each target an assertion about genuinely independent observations.

Formalization targets

Simultaneous confidence region

For $0<\delta<1$ , set

\alpha(t)=\frac{R^2}{\sqrt M}\left(\sqrt{1-\frac m{R^4}}+\sqrt{\log(1/t)}\right),\qquad \beta(t)=\frac{R^2}{M}\left(2+\sqrt{2\log(1/t)}\right)^2.

Theorem 2 is the goal. Write $a=\alpha(\delta/4)$ and $b=\beta(\delta/2)$ , and assume $a+b<1$ . The target is the simultaneous event

(\widehat\mu-\mu)^\mathsf T\Sigma^{-1}(\widehat\mu-\mu)\le b, \qquad \Sigma\preceq\frac{\widehat\Sigma}{1-a-b}, \qquad \frac{\widehat\Sigma}{1+a}\preceq\Sigma

with probability at least $1-\delta$ . The last denominator is a correction: printed (12c) says $1-a$ , while the authors' union-bound display on draft p. 13 says $1+a$ . The printed version fails, for example, for symmetric $\pm1$ observations, whose sample covariance is $1-\widehat\mu^2$ and for which its claimed lower bound would require an implausibly large sample-mean square. The proof's displayed bound gives the stated $1+a$ draft pp. 13–14.

Supporting results

Lemma 2 bounds the normalized sample mean. Corollary 1 turns it into the Mahalanobis bound for $\widehat\mu-\mu$ . Lemma 3 gives a two-sided matrix bound for $M^{-1}\sum_i\zeta_i\zeta_i^\mathsf T$ ; Corollary 2 transfers that bound to $\widehat\Sigma(\mu)$ . A separate theorem item states the centring identity $\widehat\Sigma(\mu)=\widehat\Sigma+(\widehat\mu-\mu)(\widehat\mu-\mu)^\mathsf T$ . The final milestone is the rank-one matrix inequality used in Theorem 2's proof. Their statements follow the draft's §4.1–4.2.

Significance

The joint region places both true moments inside explicit data-dependent matrix inequalities at a chosen confidence level. That is the statistical input for the paper's later moment-based distributional uncertainty sets. The result is known in the source; this mission asks for machine-checked proofs of its corrected statement and its supporting concentration and matrix results. The Lean items are currently open theorem statements, so a successful draft compilation does not constitute formal verification of the inequalities.

Related platform results include a proved two-sided constant-bound McDiarmid inequality (UnderstandingML.mcdiarmid_inequality_pi) and an open per-coordinate upper-tail version (StabGen.Uniform.mcdiarmid_inequality). Neither is identical to the cited Theorem 1 of this draft, so the milestone list starts with the paper's Lemma 2 and does not restate Theorem 1.

Difficulty

The known-mean covariance estimate is a sum of outer products of normalized observations. Controlling its largest and smallest eigenvalues together requires concentration of a matrix-valued statistic, rather than a separate scalar bound for each entry. Once the true mean is replaced by $\widehat\mu$ , the covariance changes by a rank-one matrix; the mean bound must control that correction in Loewner order. A direct replacement of $\widehat\Sigma(\mu)$ by $\widehat\Sigma$ therefore does not preserve both sides of Corollary 2 automatically.

Formalization scope

Vectors are Fin m → ℝ, and matrices are real Fin m × Fin m matrices. The Euclidean squared length is a dot product; Lean's generic norm on functions is a supremum norm and is not used for it. The Loewner order is (B - A).PosSemidef. The distribution has a probability measure and coordinatewise finite $L^2$ moments, so its real-valued mean and covariance integrals are well defined. The true covariance is positive definite, reflecting the section's nonsingularity assumption. Samples have the product law $P^M$ . The chapter's normalized case records zero mean, identity covariance, and the almost-sure ball bound.

Every statistical result assumes $0<\delta<1$ ; the logarithms and confidence levels are then in their intended domain. Positive $M$ rules out division by zero in empirical averages. Lemma 3 carries the paper's explicit sample-size threshold, and the goal reads “ $M$ large enough” as $a+b<1$ , which keeps the upper covariance denominator positive. The expression under the other square root is nonnegative in every satisfiable positive-dimensional normalized setting, because $\mathbb E\|\zeta\|_2^2=m\le R^2$ . It is not an added assumption. The probability conclusions use $\ge1-\delta$ , which is what the paper's proofs show despite the phrase “greater than.”

The goal assumes the source's distributional and support conditions, not the probability conclusions of its supporting corollaries. This prevents a vacuous route that merely postulates the desired confidence event. A complete proof will need reusable product-measure concentration facts, moment and matrix algebra, and a positive-definite quadratic-form bridge. Contributions to those components and to each milestone are in scope. Corollary 3's data-derived radius is excluded because the draft's conditioning argument does not establish its claimed confidence level. Corollary 4 as a probability statement, Theorem 3, and Corollary 5 depend on it; Remark 2 concerns a separate Gaussian eigenvalue density.

Selected references

Erick Delage and Yinyu Ye, Distributionally Robust Optimization under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 595–612, 2010; source used here: authors' draft of 20 February 2008. DOI.

7 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

Kullback–Leibler Upper Confidence Bounds for Optimal Sequential Allocation I: kl-UCB Draws a Suboptimal Arm log(T)/d(μ_a, μ*) + O(√log T) Times in One-Parameter Exponential FamiliesResearch Paper

Motivation

In a stochastic multi-armed bandit a player repeatedly chooses one of $K$ distributions ("arms") and observes a reward drawn from it; the goal is to collect as much reward as possible, which amounts to pulling suboptimal arms as rarely as possible. Lai and Robbins (1985) showed that any reasonable strategy must pull a suboptimal arm $a$ at least $\log T / \mathrm{KL}$ times up to horizon $T$ , where $\mathrm{KL}$ is a Kullback–Leibler divergence between arm $a$ and the best arm, and Burnetas and Katehakis (1996) extended the bound to general models. Strategies matching this rate are called asymptotically optimal.

The popular UCB algorithms of Auer, Cesa-Bianchi and Fischer (2002) use Hoeffding-type confidence bounds and are not asymptotically optimal outside special cases. Cappé, Garivier, Maillard, Munos and Stoltz (Ann. Statist. 41(3), 2013; arXiv:1210.1136) analyse kl-UCB, which replaces the Hoeffding radius by a Kullback–Leibler confidence region, and prove a finite-horizon bound whose leading term is exactly the Lai–Robbins constant. This mission formalizes that result for one-parameter exponential families (Theorem 1), the main-text steps of its proof skeleton, and its two corollaries for bounded rewards.

Timeline: Lai and Robbins (1985) lower bound and asymptotically optimal index policies; Agrawal (1995) sample-mean based index policies; Auer, Cesa-Bianchi and Fischer (2002) finite-time analysis of UCB1; Garivier and Cappé (2011) kl-UCB for bounded rewards; Cappé et al. (2013) the unified analysis formalized here.

Setting

A canonical exponential family $\mathcal D = \{\nu_\theta : \theta\in\Theta\}$ is given by a dominating measure $\rho$ on $\mathbb R$ and a function $b$ , with densities $\frac{d\nu_\theta}{d\rho}(x) = \exp(x\theta - b(\theta))$ . The parameter set $\Theta$ is the natural parameter space $\{\theta : \int e^{x\theta}\,d\rho(x) < \infty\}$ , assumed to be an open interval (the family is regular), and $b$ is twice differentiable. The mean of $\nu_\theta$ is $\dot b(\theta)$ , an increasing function, so $\nu_\theta$ is determined by its mean $\mu$ in the open interval $I = \dot b(\Theta) = (\mu_-,\mu_+)$ . The divergence (11) is

d(\mu,\mu') = \mathrm{KL}(\nu_{\dot b^{-1}(\mu)},\nu_{\dot b^{-1}(\mu')}) = (\dot b^{-1}(\mu)-\dot b^{-1}(\mu'))\mu - b(\dot b^{-1}(\mu)) + b(\dot b^{-1}(\mu')),

extended by continuity to the closure $\bar I = [\mu_-,\mu_+]$ , possibly with the value $+\infty$ .

There are $K\ge2$ arms with laws $\nu_{\theta_1},\dots,\nu_{\theta_K}\in\mathcal D$ and means $\mu_1,\dots,\mu_K$ ; $\mu^\star = \max_a \mu_a$ . At each round $t\ge1$ the player picks an arm $A_t$ based on the past and receives a reward drawn from $\nu_{A_t}$ . $N_a(t)$ is the number of pulls of arm $a$ in rounds $1,\dots,t$ , and $\hat\mu_a(t)$ the mean of the rewards obtained from arm $a$ so far.

kl-UCB (Algorithm 2) with a nondecreasing exploration function $f$ pulls each arm once and then, for $t\ge K$ , pulls an arm maximizing the index

U_a(t) = \sup\Bigl\{\mu\in\bar I : d(\hat\mu_a(t),\mu) \le \frac{f(t)}{N_a(t)}\Bigr\}. \tag{12}

Formalization targets

Goal: Theorem 1 (p. 14)

With $f(t) = \log t + 3\log\log t$ for $t\ge3$ and $f(1)=f(2)=f(3)$ , for every suboptimal arm $a$ and every horizon $T\ge3$ ,

\mathbb E[N_a(T)] \le \frac{\log T}{d(\mu_a,\mu^\star)} + 2\sqrt{\frac{2\pi\sigma^2_{a,\star}(d'(\mu_a,\mu^\star))^2}{(d(\mu_a,\mu^\star))^3}}\sqrt{\log T+3\log\log T} + \Bigl(4e+\frac{3}{d(\mu_a,\mu^\star)}\Bigr)\log\log T + 8\sigma^2_{a,\star}\Bigl(\frac{d'(\mu_a,\mu^\star)}{d(\mu_a,\mu^\star)}\Bigr)^2 + 6,

where $\sigma^2_{a,\star} = \max\{\mathrm{Var}(\nu_\theta) : \mu_a\le \mathrm E(\nu_\theta)\le\mu^\star\}$ and $d'$ is the derivative in the first argument.

Milestones

The decomposition (5) of the event $\{A_{t+1}=a\}$ (p. 9).
The split of $\mathbb E[N_a(T)]$ after (7) (p. 9).
The passage to local times (8) (pp. 9–10): the overestimation term is bounded by $\sum_{n=1}^{T-K}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$ , a sum over fixed sample sizes.
The general bound (10) with $n_0$ of (9) (p. 10).
The deviation bound (13) for an empirical mean with a random number of summands (p. 14).
Lemma 1 (p. 17): the moment-generating function of a distribution on $[0,1]$ is dominated by Bernoulli and Gaussian ones.

Companions

Corollary 1 (p. 17, kl-UCB with the Bernoulli divergence for arbitrary rewards in $[0,1]$ ) and Corollary 2 (p. 18, UCB with radius $\sqrt{f(t)/(2N_a(t))}$ ), stated as separate theorems.

Significance

Theorem 1 shows that kl-UCB is asymptotically optimal in every regular one-parameter exponential family (Bernoulli, Poisson, Gaussian with known variance, exponential, Gamma with known shape), and it does so with an explicit bound valid at every horizon, not only in the limit. Corollary 2 improves the constants of the classical UCB1 analysis, and Corollary 1 shows that the Bernoulli kl-UCB index is uniformly better than UCB for all bounded rewards.

The result is proved in the paper; its proofs are in the supplemental article (DOI 10.1214/13-AOS1119SUPP, Appendix A), not in the main text. No machine-checked version exists. The platform has a formal analysis of a Bernoulli KL-UCB variant with another exploration function (Lattimore–Szepesvári's Theorem 10.6), which is a different statement. The formalization adds the general exponential-family index, the random-sample-size deviation bound (13) and the full finite-time constant.

Difficulty

The obvious argument bounds $\mathbb P\{\mu^\star \ge U_{a^\star}(t)\}$ by a union bound over the possible values of $N_{a^\star}(t)$ , which costs a factor $t$ and destroys the logarithmic rate. The deviation bound (13) has to control an empirical mean whose number of summands is chosen by the algorithm itself, losing only a factor $e\lceil\varepsilon\log t\rceil$ over the fixed-sample Chernoff bound; this is the step that needs the strategy to be non-anticipating. The second-order terms depend on the curvature of $d$ between $\mu_a$ and $\mu^\star$ , measured by $\sigma^2_{a,\star}$ and $d'$ , and the explicit constants must be tracked through every step. The empirical mean can be an endpoint of $\bar I$ (Bernoulli rewards at small sample sizes), where $d$ is only defined as a limit.

Formalization scope

The rewards are a stack $X_{a,k}$ (the $(k+1)$ -st reward of arm $a$ ), mutually independent and i.i.d. per arm, the representation of §2.2; this is the platform's RegretBandits.Stochastic.IsStochasticBandit, and the law of $X_{a,0}$ is pinned to $\nu_{\theta_a}$ . Arms are Fin K. The exponential family is the platform's OptimalBAI.OptProportions.ExpFamily (with $\ddot b>0$ , i.e. strict convexity, which the page derives); the natural-parameter-space condition is a separate hypothesis. A run of kl-UCB is a pathwise predicate: rounds $1,\dots,K$ pull every arm once and later rounds pull an argmax of the index, ties broken by any rule. The arm choices are measurable and non-anticipating (a measurable function of the arms and rewards already observed). The index (12) is a real supremum over a set containing the empirical mean, so it is never a junk value, and the divergence at an empirical mean on the boundary of $\bar I$ is computed in $[0,+\infty]$ . Statement (13) is made for $t\ge2$ : at $t=1$ its printed right-hand side is $0$ .

A trivializing formalization is ruled out: the run predicate forces both initialization and argmax, the index sets are nonempty and bounded, the reward stack is independent under the probability measure, and the Bernoulli divergence is never evaluated at $0$ or $1$ .

A complete development needs exponential-family calculus (convex conjugate of $b$ , continuity of $d$ up to the boundary), Chernoff bounds for exponential families, a peeling/maximal inequality for random sample sizes, and the counting arguments of §3.1. The deviation bound and the counting arguments are reusable for every index policy on the platform.

Selected references

O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3):1516–1541, 2013. https://doi.org/10.1214/13-AOS1119 ; arXiv:1210.1136v4, https://arxiv.org/abs/1210.1136
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6:4–22, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Mach. Learn. 47:235–256, 2002. https://doi.org/10.1023/A:1013689704352
A. Garivier, O. Cappé, The KL-UCB algorithm for bounded stochastic bandits and beyond, COLT 2011. https://arxiv.org/abs/1102.2490
R. Agrawal, Sample mean based index policies with O(log n) regret for the multi-armed bandit problem, Adv. Appl. Probab. 27:1054–1078, 1995. https://doi.org/10.2307/1427934

12 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network III: Sigmoid Networks with Small Weights GeneralizeResearch Paper

Motivation

A classifier built from a neural network produces a real score and predicts a binary label from its sign. A network can have many hidden units, so a guarantee based only on the number of parameters can be uninformative even when its output weights are small. Bartlett's 1998 paper asks whether a classifier's margin on training examples and the total magnitude of its weights can control its probability of error without fixing the number of units. Its Theorem 28 gives such a statement for two-layer networks whose activation is bounded and nondecreasing. The paper also discusses why this parameter-magnitude view supports weight decay and early stopping as learning heuristics, while leaving their algorithmic behavior outside the theorem's scope (Bartlett 1998, pp. 526, 534–535).

The theorem combines two results in the same paper. Theorem 2 turns the fat-shattering dimension of a real-valued function class into a margin generalization bound. Corollary 24 controls that dimension for finite combinations of affine-input units when the sum of the absolute combination weights is bounded. Lemmas 19, 22, and 23 supply covering estimates along that path. These are the milestones of this mission, with the source statements preserved in the milestone record (Bartlett 1998, pp. 527, 532–534).

Setting

An input is a vector $x\in\mathbb R^n$ , represented in Lean as Fin n → ℝ. A label is $y\in\{-1,+1\}$ ; Lean's Bool is converted by pm, where true means $+1$ . A probability distribution $P$ lives on labeled inputs. From an independent sample $z=((x_i,y_i))_{i=1}^m$ , the empirical margin error at scale $\gamma>0$ is the fraction of indices with $y_i h(x_i)<\gamma$ . The population error is the probability that $\operatorname{sgn}(h(x))\ne y$ , where $\operatorname{sgn}(0)=+1$ . The inequality in the empirical error is strict, as in the paper's definition (Bartlett 1998, p. 526).

Fix a bounded nondecreasing activation $\sigma:\mathbb R\to[-1,1]$ . The first-layer class $F$ contains every $x\mapsto\sigma(w\cdot x+w_0)$ , with an arbitrary weight vector and bias. The network class $H$ contains all finite sums $\sum_{i=1}^N\alpha_i f_i$ with $f_i\in F$ and $\sum_i|\alpha_i|\le A$ . Thus $A$ bounds the output layer's total weight magnitude, while $N$ can vary without an imposed width limit. The bias $w_0$ is part of every unit. For a class $G$ , $\operatorname{fat}_G(\eta)$ records the largest length of an input sequence whose every sign pattern can be realized with separation at least $\eta$ around one vector of thresholds (Bartlett 1998, pp. 526, 533–534).

Formalization targets

Two-layer generalization

For $0<\gamma\le1$ , $0<\delta<1/2$ , $A\ge1$ , and an independent sample of length $m\ge1$ , the goal is one universal $c>0$ such that, with probability at least $1-\delta$ , every $h\in H$ satisfies

\operatorname{er}_P(h)<\widehat{\operatorname{er}}_z^\gamma(h)+ \sqrt{\frac{c}{m}\left( \frac{A^2n}{\gamma^2}\log\!\left(\frac{32A}{\gamma}\right)(\log m)^2+ \log\!\left(\frac1\delta\right)\right)}.

The paper prints $\log(A/\gamma)$ in this display. That term vanishes at $A=\gamma=1$ , although the class can then contain halfspace classifiers with nonzero sample complexity. The proof obtains a positive factor at that corner through Corollary 24 at scale $\gamma/16$ , giving $\log(32A/\gamma)$ . The goal states this correction and records the printed statement separately in the moderation notes. The constant precedes all network, distribution, margin, confidence, and sample parameters in Lean; it cannot be selected after observing the instance (Bartlett 1998, pp. 533–534).

Capacity and margin milestones

Corollary 24 bounds $\operatorname{fat}_H(\eta)$ by a constant multiple of $M^2A^2n\eta^{-2}\log(MA/\eta)$ when the activation has range $[-M/2,M/2]$ . Theorem 2 then converts a finite fat dimension at scale $\gamma/16$ into a simultaneous bound on population error for all members of $H$ . The three covering lemmas track how shattering, pseudodimension, and an $\ell_1$ weight budget affect covers in sample $\ell_1$ , $\ell_\infty$ , and $\ell_2$ distances. Each bound retains the scale and explicit constants printed by the paper, subject to the stated corrections to undefined or false boundary cases (Bartlett 1998, pp. 527, 532–533).

Significance

The goal gives a width-independent generalization guarantee for a chosen network when its empirical margin error and total output weight are small. It applies to the entire class $H$ at once, so choosing a network after inspecting the sample does not turn the bound into a claim about only one fixed predictor. It does not assert that a learning algorithm finds such a network or that the displayed constants are optimal. Bartlett notes that later work had improved a logarithmic factor, and that empirical agreement with neural-network performance remained an open experimental question at the time (Bartlett 1998, pp. 534–535).

The paper proves the mathematical result. This mission asks for a machine-checked proof of its corrected formal statement and the stated supporting results; the draft theorem files currently contain proof obligations. A completed development would also make the fat dimension and strict external sample-cover definitions available for other margin analyses. Those objects differ from the platform's fixed-architecture neural networks and closed-ball covering numbers, so they are defined here with the conventions of this paper.

Difficulty

Counting hidden units gives no finite width-independent capacity bound, because $H$ permits arbitrarily many terms. Bounding each unit separately also does not control the full combination class: different small contributions can produce distinct values on a sample. The challenging step is relating covers of the base class to covers of all finite combinations under the total absolute-weight constraint, and then relating those covers back to fat-shattering. Even once a finite capacity estimate is available, the probability statement must hold simultaneously for every $h\in H$ , including a network selected after sampling (Bartlett 1998, pp. 532–534).

Formalization scope

Lean uses $\mathbb N\cup\{\infty\}$ for fat dimensions and covering numbers, so an unbounded class cannot acquire a spurious dimension zero. Covers are external finite sets of real functions and use the strict distance $<\varepsilon$ of Definition 3. Sample $\ell_1$ and $\ell_2$ distances are normalized by $m$ . Pseudodimension is the supremum of positive-scale fat dimensions, matching the paper's right limit. Theorems assume $m\ge1$ , and sample indices are zero-based. The network class is generated from its weights rather than supplied as an arbitrary set satisfying the desired bound.

The paper says it ignores measurability issues and assumes all sets considered are measurable (Bartlett 1998, p. 526). The goal makes the event of a violating network measurable. Its individual network functions are measurable from monotonicity of $\sigma$ and finite sums; the restated Theorem 2 has explicit hypotheses for measurable class members, the violating event, and the double-sample event in its proof. Theorem 2 additionally restricts $d=\operatorname{fat}_H(\gamma/16)$ to $d\le34m$ , where its printed logarithmic bound remains valid. Corollary 24 uses $n\ge1$ because a zero-dimensional input still permits a biased constant unit. Lemma 23 uses $d\ge1$ and $0<\gamma<emM/d$ in place of the printed $\gamma\ge0$ : at $\gamma=0$ or $d=0$ , or for $\gamma\ge emM/d$ , the printed strict inequality fails, while on the rest of the printed range it is kept. These are recorded as corrections rather than attributed to the printed wording.

The deeper-network part of Theorem 28 is outside this proposal. Its printed chain through Corollary 27 has an unresolved range issue when the input box bound $B$ is smaller than the activation range, and the displayed $\log n$ factor also vanishes at $n=1$ . This mission's goal is Part 1 and uses none of those claims. Contributions that establish the corrected covering lemmas, the capacity corollary, or the simultaneous margin bound fit the present proof frontier (Bartlett 1998, pp. 533–534).

Selected references

P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Transactions on Information Theory 44(2), 525–536, 1998. DOI.

15 thms2 active usersReviewed

Missions

Residual Life Time at Great Age 2: The Domain of Residual Life Time Attraction of the Exponential Law Is D(Λ) ∩ D₀Research Paper

Motivation

Setting

Formalization targets

Theorem 3: the exact domain identity

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Residual Life Time at Great Age 3: F Is in the Domain of Residual Life Time Attraction of Π_{p,c} iff It Is Tail Equivalent to a Discrete Law with Gap Ratios → e^{pc} and Tail Ratios → e^{−p}Research Paper

Residual life at great age

Setting

Formalization targets

Goal: Theorem 5 (p. 800)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Asymptotic Calibration: The Regret-Balancing Randomised Forecast on the Grid {0, 1/k, …, 1} with k ≥ 1/ε² Is ε-Calibrated against Every Adaptive NatureResearch Paper

Motivation

Setting

Formalization targets

Main theorem

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Some Theoretical Aspects of Road Traffic Research I: Time-Mean Speed Equals Space-Mean Speed plus σₛ²/v̄ₛ, so v̄ₜ ≥ v̄ₛ with Equality Only Without Speed VariationResearch Paper

Why two traffic speed averages differ

Traffic streams and their two distributions

Formalization targets

What the result supplies

Where the formal proof needs care

Formalization scope

Selected references

Some Aspects of the Sequential Design of Experiments I: Greedy Sampling with Density-Zero Forced Draws Earns max(α, β) per Draw from Any Two Populations with Finite MeansResearch Paper

Motivation

Setting

Formalization targets

Goal: Section 2, Eq. (16)

Milestone: Eq. (14), almost-sure average

Milestone: Eq. (15), expected average

Significance

Difficulty

Formalization scope

Selected references

A Stochastic Approximation Method: If M Is Nondecreasing, M(θ) = α and M′(θ) > 0, the Robbins–Monro Iterates with Steps of Type 1/n Converge to θ in Mean SquareResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 405)

Milestones

Companion results

Significance

Difficulty

Formalization scope

Selected references

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality II: Binomial Tail Bound P(S − np > nε) ≤ exp(−nε²/(2(p + ε/3)(q − ε/3))) for 0 < ε ≤ qResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 1271)

Milestones

Significance