Completed

Optimization·Captain: viratkota

Kelly's Criterion: the optimal fraction for an even-money betResearch Paper

Motivation

In 1956 Kelly answered a question that looks like gambling and is really about information: if a channel gives you a noisy advance signal about a sequence of bets, how much is that signal worth? His answer was that the maximum exponential rate of growth of a gambler's capital equals the rate of transmission over the channel -- so information rate and capital growth rate are the same quantity in different units. The betting fraction that achieves it is now called the Kelly criterion, and it is the basis of a large practical literature on position sizing.

The result is short, entirely explicit, and has no analytic subtleties -- which makes it a good formalization target and a surprising gap: the platform currently has fifteen missions on bandit algorithms and none on optimal growth.

Setting

This mission formalizes the simplest case of Kelly's Section 4: an even-money bet with no track take, won independently with probability p and lost with probability q = 1 - p. A gambler stakes a fixed fraction l of current wealth on each bet, so wealth is multiplied by 1 + l on a win and 1 - l on a loss. The exponential rate of growth is

G(l) = p \log(1+l) + q \log(1-l).

Kelly shows this is maximised at l = p - q, with maximum value 1 + p log p + q log q in bits. We state G in nats (natural logarithm), so the maximum carries an additive log 2; dividing by log 2 recovers Kelly's bit-valued form, which is exactly 1 - H(p) for the binary entropy H. The maximiser is unaffected by the choice of base.

What is being asked

The goal theorem is that l = 2p - 1 maximises G over the admissible range (-1, 1) when the bet is favourable (p > 1/2). Milestones supply the maximum value (Kelly's information-rate identity), the admissibility of the maximiser, and the concavity that makes the first-order condition sufficient.

Source

J. L. Kelly Jr., A New Interpretation of Information Rate, Bell System Technical Journal 35 (1956) 917-926, Section 4 ("the simplest case"). The growth-rate expression and the maximiser l = p - q are stated there; the maximum value in bits is Kelly's eq. for G_max.

The identity and maximiser were checked numerically before drafting: for p = 0.55, 0.6, 0.7, 0.9 the claimed maximum matches log 2 + p log p + q log q to six decimals, and a grid search over (-1, 1) at 1e-5 resolution returns 2p - 1 in every case.

4 thms2 active usersReviewed

Completed

Functional Analysis Harmonic Analysis·Captain: Elsie66

Bochner's Theorem: Positive-Definite FunctionsTextbook

Motivation

Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function $f:\mathbb R\to\mathbb C$ is positive-definite if, for every finite family of points $x_1,\dots,x_n$ and complex coefficients $c_1,\dots,c_n$ , the Hermitian quadratic form $\sum_{i,j}\overline{c_i}c_j f(x_i-x_j)$ is real and nonnegative. This single algebraic condition is exactly what makes $f$ realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.

Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a necessary condition for such a representation, but exactly characterizes it. A continuous, normalized ( $f(0)=1$ ) function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure $\nu$ on $\mathbb R$ — i.e. $f$ is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where $f$ is additionally Lebesgue-integrable, so that $\nu$ has an explicit continuous density given directly by the ordinary Fourier transform of $f$ .

Setting

Fix IsPositiveDefinite f as above, for $f:\mathbb R\to\mathbb C$ (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, $f(-x)=\overline{f(x)}$ (IsPositiveDefinite.conj_neg), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with f continuous and normalized. No further hypothesis (in particular, no integrability of f) is assumed for the general representation theorem: the representing measure $\nu$ need not be absolutely continuous (e.g. for a periodic $f$ , $\nu$ is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that f is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is fourierTransform f, the (real part of the) Fourier transform of f — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers f from it.

Formalization targets

Goal — Bochner's theorem, general case

f \text{ continuous, positive-definite, } f(0)=1 \;\Longrightarrow\; \exists\, \nu \text{ a probability measure on } \mathbb R,\; \forall x,\; f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi).

The central representation theorem: no integrability hypothesis on $f$ , so $\nu$ may be any probability measure, not necessarily a density.

Milestone — Bochner's theorem, `L¹` (density) case

f \text{ continuous, integrable, positive-definite, } f(0)=1 \;\Longrightarrow\; \tau:=\text{fourierTransform } f \text{ is continuous}, \;\tau \ge 0,\; \int \tau = 1, \text{ and } f(x) = \int e^{i2\pi\xi x}\tau(\xi)\,d\xi.

The special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.

Significance

Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.

Difficulty

The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from f, a strongly continuous unitary representation of $\mathbb R$ on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since f need not be integrable and $\nu$ need not have a density. The L¹ milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: IsPositiveDefinite.conj_neg) that a positive-definite function is Hermitian-symmetric.

Formalization scope

IsPositiveDefinite is formalized exactly as the finite Hermitian-form condition above, over Fin n → ℝ point families and Fin n → ℂ coefficients, matching the standard convention in the literature, with f : ℝ → ℂ — the fully general, complex-valued statement, not restricted to real-valued kernels. fourierTransform f ξ is defined as the real part of ∫ Complex.exp(-i2πξ x) * f(x) dx; this is provably the exact (not merely real-part-of) Fourier transform once f is positive-definite, since Hermitian symmetry forces the integral to be real already.

Selected references

Bochner's theorem, Wikipedia — states the general locally-compact-abelian-group form and sketches the unitary-representation proof; a good map of the territory before diving into either target.
Salomon Bochner, Vorlesungen über Fouriersche Integrale, Akademische Verlagsgesellschaft, 1932.
Gustav Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
Walter Rudin, Fourier Analysis on Groups, Interscience, 1962, Chapter 1.

8 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: sr

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$ . Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$ . It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$ .

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$ . A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$ ; here vertices are labeled $0, \dots, N-1$ . A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$ -set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$ . This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$ -set is a graph with neither a $k$ -clique nor an independent $k$ -set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$ ", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

R(k) > 2^{k/2}, \qquad k \ge 3

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$ -set.

Stronger: the three steps of the proof, as separate targets

Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$ ,

\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.

Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.

Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$ -set in $G$ is at most

\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$ .

Difficulty

The central difficulty is that the bad events — "the $k$ -set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$ -sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$ ; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$ -set ( $2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$ ; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$ -set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$ -sets of $G$ .

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$ . The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$ , is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic- $k$ -set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$ ; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$ .
Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$ , for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$ ; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$ ; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$ .

5 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook

Motivation

Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.

Setting

The basic problem (§1.2 of the book): a discrete-time system

x_{k+1} = f_k(x_k, u_k, w_k), \qquad k = 0, 1, \dots, N-1,

with state $x_k \in S$ , control $u_k$ constrained to a finite nonempty set $U_k(x_k) \subseteq C$ , and disturbance $w_k$ drawn from a finite space $W$ with conditional probabilities $p_k(w \mid x_k, u_k)$ . A policy is a sequence $\pi = \{\mu_0, \mu_1, \dots\}$ of feedback maps $\mu_k : S \to C$ ; it is admissible if $\mu_k(x) \in U_k(x)$ everywhere. Its expected cost from $x_0$ is

J_\pi(x_0) = \mathbb{E}\Big[ g_N(x_N) + \sum_{k=0}^{N-1} g_k(x_k, \mu_k(x_k), w_k) \Big].

In the Lean development these are BertsekasDPModel, BertsekasDPPolicyCost (backward recursion on remaining stages), and the DP recursion BertsekasDPValue:

J_N = g_N, \qquad J_k(x) = \min_{u \in U_k(x)} \mathbb{E}_w\big[ g_k(x,u,w) + J_{k+1}(f_k(x,u,w)) \big].

Section 1.6 of the book develops the minimax variant, where the disturbance is chosen antagonistically from a finite membership set $W_k(x,u)$ ; the mission mirrors it with BertsekasMinimaxDPModel, BertsekasMinimaxPolicyCost, BertsekasMinimaxValue.

Target

J_0(x_0) \;=\; \min_{\pi \text{ admissible}} J_\pi(x_0), \qquad \text{with the minimum attained,}

formalized as BertsekasDP.dp_algorithm_optimality: the DP value at the horizon is an IsLeast of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (minimax_selection_interchange) and the minimax DP validity (minimax_dp_algorithm).

Significance

The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).

Difficulty

The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its $> -\infty$ proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.

Formalization scope

Finite disturbance space (Fintype W), finite nonempty control-constraint sets (Finset, inf'), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on $\mathbb{N}$ ; only stages $0,\dots,N-1$ matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly $N$ remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. ISBN 1-886529-26-4. (Prop. 1.3.1, §1.2–1.3, §1.6.) http://www.athenasc.com/dpbook.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957.

5 thms2 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times XIII: Coupling from the PastTextbook

Motivation

Every sampling guarantee in this series so far is approximate: run the chain for $t_{\mathrm{mix}}(\varepsilon)$ steps and the output is within $\varepsilon$ of stationarity. In 1996 Propp and Wilson showed that, astonishingly, one can often sample exactly from the stationary distribution of a chain — with no error at all and no knowledge of the mixing time — by running the chain not forward from the present but from the past. Their algorithm, coupling from the past (CFTP), drives all states simultaneously with the same sequence of random update maps drawn from times $-1,-2,-3,\dots$ ; as soon as the composed map from some time $-t$ collapses the entire state space to a single value, that value is an exact sample from $\pi$ . Chapter 22 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009; the chapter is by Propp and Wilson themselves) presents the algorithm, the monotone shortcut that makes it practical for huge state spaces, and the proof of exactness. This mission — the final one of the series — formalizes that correctness proof.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$ . A random mapping representation of $P$ is a probability distribution $\nu$ on update functions $f:V\to V$ that reproduces the transition probabilities in one step:

\nu\{f: f(x)=y\}\;=\;P(x,y)\qquad\text{for all }x,y.

Sampling $f\sim\nu$ and applying it to the current state is exactly one $P$ -step — simultaneously from every possible current state.

CFTP draws i.i.d. maps $f_{-1},f_{-2},\dots\sim\nu$ indexed by past times and composes them forward from the past up to time zero:

F^0_{-t}\;=\;f_{-1}\circ f_{-2}\circ\cdots\circ f_{-t}.

Note the order: extending the horizon deeper into the past prepends new randomness inside the composition, while the maps near time $0$ stay fixed — this is the crucial asymmetry between running from the past and running into the future. The composition has coalesced when $F^0_{-t}$ is a constant map — all starting states have been funneled to one common value — and the algorithm outputs that value. In the monotone variant, $V$ carries a partial order with a bottom state $\hat0$ and a top state $\hat1$ and every update map is monotone; then it suffices to track the two extreme trajectories.

Formalization targets

Goal

Correctness of coupling from the past (Propp–Wilson; §22.2–22.3), the capstone of the series: if $\nu$ is a random mapping representation of $P$ , $\pi$ is stationary for $P$ , and coalescence is almost sure, then for every state $y$ the probability that the CFTP composition has coalesced to the value $y$ within $t$ steps from the past tends, as $t\to\infty$ , to exactly $\pi(y)$ — the output of the algorithm is an exact sample from the stationary distribution, with no mixing-time error term.

Milestones

Proposition 1.5 / §22.3 — every finite Markov chain has a random mapping representation: a suitable $\nu$ always exists.
Coalescence (§22.3) — if some finite composition of update maps collapses the state space with positive probability, then coalescence is almost sure: the probability that $F^0_{-t}$ is not yet constant tends to $0$ as $t\to\infty$ .
Monotone CFTP (§22.2) — if the state space has a bottom $\hat0$ and a top $\hat1$ and every update map is monotone, then the composition is constant as soon as it merely identifies $\hat0$ and $\hat1$ : checking two trajectories certifies coalescence of all of them.

Significance

The results. CFTP is one of the most striking algorithmic ideas probability has produced: a Las Vegas algorithm whose output distribution is exactly $\pi$ , side-stepping every mixing-time estimate of the previous twelve missions. The monotone shortcut is what made it explode in practice — for the Ising model of Mission IX the $2^n$ trajectories collapse to two, and Propp–Wilson famously drew exact Ising samples on large grids at the critical temperature. CFTP remains the foundation of exact-simulation methods across statistical physics, spatial statistics, and randomized algorithms.

Formalizing it. The correctness argument is short but famously slippery — the standard pitfall (running the coupling into the future yields a biased sample) is precisely a statement about the order of composition, which a formal proof pins down mercilessly. Nothing about exact sampling exists in any proof-assistant library. Formalized CFTP correctness is a fitting keystone: it consumes the random-map representation (Chapter 1), stationarity (Mission I), and the almost-sure-coalescence analysis, and certifies the algorithm practitioners actually run.

Difficulty

The whole content lies in managing the composition order and the limiting argument without measure theory. The probability space at horizon $t$ is the finite product of $t$ copies of $\nu$ (tuples of update maps, weighted by products); the key observation — for fixed $t$ , the law of $F^0_{-t}$ applied to any fixed start equals the law of $t$ forward steps — is a finite re-indexing argument. Exactness then follows from a sandwich: on the event of coalescence by time $t$ , the output equals $F^0_{-t}(x)$ for every $x$ ; choosing the start according to $\pi$ shows the output law differs from $\pi$ by at most the non-coalescence probability, and the hypothesis drives that to zero. Formalizing this needs care at exactly the point where informal proofs wave: the event "coalesced by $-t$ " is increasing in $t$ because the maps near zero are shared between horizons — the tuple encoding must make this monotonicity provable. The coalescence milestone is a geometric-trials argument (independent blocks each collapse with probability bounded below), and the monotone milestone is an induction showing monotonicity of compositions plus the squeeze between the extreme trajectories. All randomness is finite products of a finite distribution; limits are limits of explicit real sequences.

Formalization scope

Update-map distributions are functions $(V\to V)\to\mathbb R$ with the distribution predicate of Mission I; the random-map representation condition is a finite-sum identity. The composition $F^0_{-t}$ is encoded by a tuple $F:\mathrm{Fin}\,t\to(V\to V)$ with $F(i)$ the map used at time $-(i{+}1)$ , folded so that the last entry applies first — the from-the-past order. Coalescence probabilities and output probabilities are finite sums over tuples of products of $\nu$ -weights; "coalescence is almost sure" is the statement that the non-coalescence probability tends to $0$ , and the goal's conclusion is a limit of real sequences (Filter.Tendsto), not a measure-theoretic almost-sure statement. The monotone milestone is stated abstractly for any finite partial order with OrderBot and OrderTop and any tuple of monotone maps — reusable beyond CFTP. No measure theory, filtrations, or i.i.d. infrastructure is required anywhere.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (Chapter 22, by J. G. Propp and D. B. Wilson). https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
J. G. Propp, D. B. Wilson, Exact sampling with coupled Markov chains and applications to statistical mechanics, Random Structures Algorithms 9 (1996). https://doi.org/10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O
D. B. Wilson, How to couple from the past using a read-once source of randomness, Random Structures Algorithms 16 (2000). https://doi.org/10.1002/(SICI)1098-2418(200003)16:2<85::AID-RSA1>3.0.CO;2-H

5 thms2 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times II: The Convergence TheoremTextbook

Motivation

The first mission of this series established that an irreducible finite Markov chain has a unique stationary distribution $\pi$ . The present mission, covering Chapters 3–4 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009), answers the two questions that make that fact useful. First, the inverse problem of sampling: given a target distribution $\pi$ — uniform over proper colorings, a Gibbs measure, a posterior — how does one build a chain whose stationary distribution is $\pi$ ? The Metropolis and Glauber constructions of Chapter 3 are the universal answers, and they are the engine of Markov chain Monte Carlo across statistical physics, Bayesian statistics, and approximate counting. Second, the convergence question: in what sense, and how fast, does an irreducible aperiodic chain approach $\pi$ ? Chapter 4 introduces the total variation distance, proves the Convergence Theorem — geometric convergence to stationarity — and defines the mixing time, the parameter the entire remainder of the book estimates.

Setting

All chains live on a finite state space $V$ and are presented by row-stochastic matrices, with the definitions of Mission I. The total variation distance between distributions $\mu$ and $\nu$ is

\|\mu-\nu\|_{\mathrm{TV}} = \max_{A\subseteq V}\,|\mu(A)-\nu(A)|,

the maximal discrepancy over events. A coupling of $\mu$ and $\nu$ is a distribution on $V\times V$ whose marginals are $\mu$ and $\nu$ . For a chain $P$ with stationary $\pi$ one sets

d(t)=\max_x \|P^t(x,\cdot)-\pi\|_{\mathrm{TV}},\qquad \bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}},

and the mixing time is $t_{\mathrm{mix}}(\varepsilon)=\min\{t : d(t)\le\varepsilon\}$ , with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$ .

The Metropolis chain for a target $\pi$ and a symmetric proposal chain $\Psi$ accepts a proposed move $x\to y$ with probability $1\wedge \pi(y)/\pi(x)$ ; a general (not necessarily symmetric) base chain is handled by the ratio $\bigl(\pi(y)\Psi(y,x)\bigr)/\bigl(\pi(x)\Psi(x,y)\bigr)\wedge 1$ . The Glauber dynamics for a distribution $\pi$ on configurations $V^{\text{sites}}$ picks a uniform site and re-samples its value from $\pi$ conditioned on the rest.

Formalization targets

Goal

$\text{$P$ irreducible and aperiodic}\;\Longrightarrow\;\exists\,\alpha\in(0,1),\ C>0:\quad d(t)\le C\alpha^{t}.$

This is Theorem 4.9, the Convergence Theorem. It asserts only the geometric shape of convergence, leaving all quantitative rates to later missions, which is why it is the goal.

Milestones

The milestones are the chapter's working parts: stationarity and reversibility of the Metropolis chain for symmetric and general base chains (§3.2, Exercise 3.1), stationarity and reversibility of the Glauber dynamics (§3.3, Exercise 3.2); the three characterizations of total variation distance — the half- $\ell^1$ formula (Proposition 4.2 with Remark 4.3), the supremum over $[-1,1]$ -bounded test functions (Proposition 4.5), and the coupling characterization with an optimal coupling attaining it (Proposition 4.7 with Remark 4.8); the comparison $d\le\bar d\le 2d$ (Lemma 4.11) and submultiplicativity $\bar d(s+t)\le\bar d(s)\bar d(t)$ (Lemma 4.12); the standard mixing-time consequences $d(\ell\, t_{\mathrm{mix}}(\varepsilon))\le(2\varepsilon)^\ell$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil\log_2\varepsilon^{-1}\rceil\, t_{\mathrm{mix}}$ (§4.5); and the equality of distance to stationarity for a group walk and its inverse walk (Lemma 4.13 and Corollary 4.14).

Significance

The results. The Convergence Theorem is the qualitative foundation on which quantitative mixing theory stands: it guarantees that $t_{\mathrm{mix}}(\varepsilon)$ is finite, so every bound in Missions III–XIII is a bound on a well-defined quantity. The TV characterizations are used constantly — the coupling characterization is the engine of Mission III, the half- $\ell^1$ formula of every explicit computation. The Metropolis and Glauber stationarity results justify the chains analyzed in Missions III (colorings, hardcore), VIII (path coupling) and IX (Ising). Submultiplicativity of $\bar d$ is what makes $t_{\mathrm{mix}}$ a meaningful single number.

Formalizing them. None of this exists in Mathlib: there is no total variation distance for finitely supported distributions, no coupling theory, no mixing time, no MCMC correctness statement. The definition layer published here (TV distance, $d$ , $\bar d$ , $t_{\mathrm{mix}}$ , couplings, Metropolis, Glauber) is imported by every subsequent mission of the series.

Difficulty

The tempting proof of Theorem 4.9 via spectral decomposition fails twice: it needs reversibility, which the theorem does not assume, and spectral machinery that arrives only in Mission VII. The book's proof is the Doeblin decomposition: by Proposition 1.7 some power satisfies $P^r(x,y)\ge\delta\pi(y)$ , so $P^r=(1-\theta)\Pi+\theta Q$ with $\Pi$ the rank-one matrix of rows $\pi$ , and induction gives $P^{rk}=(1-\theta^k)\Pi+\theta^kQ^k$ . The formal work is matrix algebra with careful bookkeeping of the remainder chain $Q$ , plus the monotonicity of $d$ needed to interpolate between multiples of $r$ . For Proposition 4.7 the delicate half is constructing the optimal coupling: mass $\mu\wedge\nu$ on the diagonal and the normalized product of the positive parts off it, with the degenerate case $\mu=\nu$ handled separately. The Glauber stationarity statement must be phrased with care because configurations outside the support of $\pi$ have junk rows; the formalization asserts stochasticity only at supported configurations, and detailed balance globally.

Formalization scope

Total variation distance is defined as the supremum over events, $\bigsqcup_{A}\,|\mu(A)-\nu(A)|$ over Finset V, exactly as in (4.1); the half- $\ell^1$ formula is a milestone, not the definition. The mixing time is sInf of the set $\{t : d(t)\le\varepsilon\}$ in $\mathbb N$ (junk value $0$ if empty — impossible under the goal theorem). Couplings are distributions on the product with prescribed marginals; no probability-space machinery is used. The mixing-time inequalities are stated with the integer-rounding slack made explicit (e.g. $\lceil\log_2\varepsilon^{-1}\rceil$ via Nat.ceil of a real logarithm) so that no statement is true only "up to rounding". The Metropolis definitions use total real division, so the hypotheses require $\pi>0$ pointwise; this matches the book, which divides by $\pi(x)$ throughout.

Welcome contributions beyond the milestones: simp lemmas for tvDist, monotonicity of $d$ and $\bar d$ in $t$ , and triangle-inequality infrastructure — all reused by Missions III–XIII.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
N. Metropolis, A. Rosenbluth, M. Rosenbluth, A. Teller, E. Teller, Equation of state calculations by fast computing machines, J. Chem. Phys. 21 (1953). https://doi.org/10.1063/1.1699114
W. Doeblin, Exposé de la théorie des chaînes simples constantes de Markov à un nombre fini d'états, Rev. Math. Union Interbalkan. 2 (1938).

14 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6

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

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

conversely, these conditions together with feasibility imply optimality.

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

8 thms1 active userReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

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

Why throughput matters

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

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

Network and allocations

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

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

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

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

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

Formalization targets

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

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

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

What the result gives

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

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

Why the proof is difficult

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

Formalization scope

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

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

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

Selected references

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

10 thms1 active userReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Optimality and Duality Theory for Stochastic Optimization Problems with Nonlinear Dominance Constraints 1: Under Uniform Dominance, Optimal Solutions Have Concave Utility and L∞ MultipliersResearch Paper

Motivation

Stochastic programs often optimize a decision that changes several random outcomes at once. A reference outcome may be acceptable even when no fixed threshold captures its risk: one wants the new outcome to be preferable under every increasing concave assessment of gains. Second order stochastic dominance expresses that comparison. Dentcheva and Ruszczyński study optimization with several such constraints, each imposed on a nonlinear outcome operator, and show how the constraint multipliers can be represented by utility functions rather than scalar penalties (Dentcheva–Ruszczyński, 2004). Their earlier paper, Optimization with stochastic dominance constraints, treats the pure dominance case without the nonlinear decision map; the present result adds decision dependent outcomes, multiple constraints, and split variables. Ogryczak and Ruszczyński's second performance function supplies the stochastic order used here (Ogryczak–Ruszczyński, 2002).

The utility interpretation matters when a modeler wants a certificate explaining why a solution satisfies a risk preference expressed by dominance. The theorem identifies a concave utility for each binding dominance constraint and an essentially bounded multiplier for each comparison between the split outcome and the outcome produced by the decision. The source is a revised April 2003 author manuscript, later published in Mathematical Programming in 2004; the page and equation numbers below follow that manuscript (author manuscript).

Setting

Work on a probability space $(\Omega,\mathcal F,P)$ . An integrable random outcome is a measurable real function with finite expected absolute value; $\mathcal L^1$ denotes these outcomes, and $\mathcal L^\infty$ denotes essentially bounded ones. The decisions lie in a convex set $Z$ inside a separable locally convex Hausdorff real vector space $\mathcal Z$ . An integrable objective outcome $H(z)$ and integrable constraint outcomes $G_i(z)$ depend continuously in the $\mathcal L^1$ norm on $z$ . Almost every realized map $z\mapsto H(z)(\omega)$ and $z\mapsto G_i(z)(\omega)$ is concave and continuous on all of $\mathcal Z$ . Fixed integrable outcomes $Y_i$ serve as references; the $i$ th comparison is required over a bounded interval $[a_i,b_i]$ .

For an outcome $X$ , its second performance function is the area below its distribution function:

F_2(X;\eta)=\int_{-\infty}^{\eta}P\{X\le\xi\}\,d\xi.

The split program (11)–(14) chooses $z\in Z$ and $X=(X_1,\ldots,X_m)\in(\mathcal L^1)^m$ to maximize $\mathbb E H(z)$ , subject to $F_2(X_i;\eta)\le F_2(Y_i;\eta)$ for every $\eta\in[a_i,b_i]$ , and $X_i\le G_i(z)$ almost surely. Larger outcomes are preferred, so a dominating $X_i$ has the smaller $F_2$ curve. The split variables expose the dominance and decision coupling as separate constraints (manuscript, pp. 3–4).

The utility cone $\mathcal U_1([a,b])$ consists of concave nondecreasing functions $u:\mathbb R\to\mathbb R$ that vanish for $t\ge b$ and are affine with a nonnegative slope for $t\le a$ . Given $u_i$ in these cones and $\theta_i\in\mathcal L^\infty$ , the Lagrangian is

L(z,X,u,\theta)=\mathbb E\!\left[H(z)+\sum_{i=1}^m\bigl(u_i(X_i)-u_i(Y_i)+\theta_i(G_i(z)-X_i)\bigr)\right].

Uniform dominance means one decision $\tilde z\in Z$ makes every dominance inequality uniformly strict on its interval: for each $i$ , $F_2(Y_i;\eta)-F_2(G_i(\tilde z);\eta)$ has a positive lower bound over $[a_i,b_i]$ (Definition 1, p. 7).

Formalization targets

Utility and bounded multiplier characterization

Theorem 2 is the goal. Under uniform dominance, every optimum $(\hat z,\hat X)$ of the split program admits $\hat u_i\in\mathcal U_1([a_i,b_i])$ and nonnegative $\hat\theta_i\in\mathcal L^\infty$ with

L(\hat z,\hat X,\hat u,\hat\theta)=\max_{z\in Z,\,X\in(\mathcal L^1)^m}L(z,X,\hat u,\hat\theta),

\mathbb E\hat u_i(\hat X_i)=\mathbb E\hat u_i(Y_i),\qquad \hat\theta_i\bigl(\hat X_i-G_i(\hat z)\bigr)=0\quad\text{almost surely}.

Conversely, an attained Lagrangian maximum satisfying the split constraints and these complementarity equations is a primal optimum. The milestone list follows the source's measure multiplier equations (23)–(24), the measure to utility identity (25), Theorem 1's expected concave subgradient characterization, and the converse's weak duality inequality (manuscript, pp. 5, 8–10).

Significance

The result gives a concrete optimality certificate in a program whose constraints compare entire outcome distributions. Each utility multiplier represents the active part of one dominance constraint. Each $\theta_i$ accounts for the almost sure inequality linking a split outcome to the decision. The equalities show exactly where those constraints are complementary, while the Lagrangian maximum compares the proposed solution with all integrable split outcomes. The paper derives a dual problem from the same Lagrangian in its following section (manuscript, p. 11).

The mathematical theorem is proved in the paper. This mission seeks a machine checked version of its definitions, measure identity, subgradient statement, and both directions of Theorem 2. The published second performance definition is reused as a reference; the nonlinear split program and its utility and measure Lagrangians require a development specific to this paper. The 2003 pure dominance mission contains related local drafts, but those items are not published and cannot currently be imported as platform theorems.

Difficulty

The dominance inequality contains a continuum of thresholds for each outcome. A scalar multiplier at one threshold cannot capture the whole constraint, while the dual object for continuous functions on $[a_i,b_i]$ is a measure. The split inequality lives in $\mathcal L^1$ , where the nonnegative cone has empty interior, so an ordinary interior point argument applied to all constraints at once does not match the paper's setting. The source also needs a subgradient of expected concave utility represented by an almost surely selected, essentially bounded random vector; the conclusion is stronger than merely knowing that the expected objective has a deterministic supporting functional (manuscript, pp. 5–9).

Formalization scope

The Lean development keeps the general separable locally convex Hausdorff decision space, the convex set $Z$ , and a finite index type for the $m$ dominance constraints. Operators are function representatives with explicit integrability, continuity in $\mathcal L^1$ , and samplewise concavity and continuity. Almost sure comparisons use the probability measure $P$ ; the null set for each realization condition precedes the quantifier over decisions. Split outcomes range only over integrable functions, and utility multipliers range over the exact cone $\mathcal U_1([a_i,b_i])$ . The $\mathcal L^\infty$ condition includes almost sure strong measurability and essential boundedness. Maxima in Theorems 1 and 2 are attained maxima, expressed by membership and comparison against every competitor, never a real supremum with a default value.

The source prints a strictly positive affine slope in its definition of $\mathcal U_1$ , but immediately calls this class a cone and later uses the zero measure. The formalization uses $c\ge0$ ; with $c>0$ , Theorem 2 is false for a slack dominance constraint. Uniform dominance is expressed as a positive lower bound rather than a real infimum. The measure milestone uses finite nonnegative measures supported on closed intervals, including endpoint atoms. These conditions exclude default zero integrals, an empty interval disguised by an infimum, and a vacuous utility class. Contributions to the measure to utility correspondence, integration identities, and expected concave subgradient infrastructure can be reused beyond this program.

Selected references

D. Dentcheva and A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Mathematical Programming (2004), DOI; revised author manuscript, April 2003.
D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, manuscript submitted for publication (2002), cited as reference [6] in the 2003 author manuscript.
W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean risk models, SIAM Journal on Optimization 13 (2002), DOI.

7 thms1 active userReviewed

Machine Learning Statistics·Captain: mikedeng1

Optimal Rates for the Regularized Least-Squares Algorithm III: Against Every Algorithm, a Single Distribution in P(b, c) Keeps the Expected Excess Risk above ℓ^(−cB/(cB+1)) for B > b (Theorem 3)Research Paper

Why individual lower rates

Regularized least squares (RLS) in a reproducing kernel Hilbert space is a basic estimator of nonparametric regression and of kernel-based learning. Its learning rate is the speed at which the expected excess risk goes to zero as the sample size $\ell$ grows. A rate is useful only if it is known to be optimal, and optimality is a lower-bound statement about all learning algorithms.

Caponnetto and De Vito (Found. Comput. Math. 7 (2007)) prove two kinds of lower bound. The first is a minimax lower rate (their Theorem 2): for every algorithm and every $\ell$ , some distribution in the prior is hard. Their Section 2 (p. 6) points out a weakness of this notion: the bad distribution may change with $\ell$ . A practitioner, however, faces one fixed unknown distribution and asks how the error decreases as data accumulate. The individual lower rate answers that question. It asks for a single distribution, chosen against the algorithm but not depending on $\ell$ , on which the expected excess risk stays above $a_\ell$ along infinitely many $\ell$ .

The notion comes from nonparametric regression. Györfi, Kohler, Krzyżak and Walk (A Distribution-Free Theory of Nonparametric Regression, Springer 2002, §3, Theorem 3.3) proved individual lower rates for classes of smooth regression functions. Theorem 3 of Caponnetto–De Vito carries the result to vector-valued RKHS with the spectral priors $\mathcal P(b, c)$ . Theorem 1 of the same paper shows that these priors are learned by RLS at rate $\ell^{-bc/(bc+1)}$ .

Setting

The input space $X$ is Polish. The output space $Y$ is a real Hilbert space of finite dimension $d$ . The hypothesis space $\mathcal H$ is a separable real Hilbert space of functions $f : X \to Y$ in which evaluation is continuous, so that $f(x) = K_x^* f$ for bounded operators $K_x : Y \to \mathcal H$ . Hypothesis 1 asks that $(x, t) \mapsto \langle K_t v, K_x w\rangle_{\mathcal H}$ be measurable and that $\operatorname{Tr}(K_x^*K_x) \le \kappa$ for every $x$ .

A distribution $\rho$ on $Z = X \times Y$ has marginal $\rho_X$ and conditional distributions $\rho(\cdot \mid x)$ . The risk of $f \in \mathcal H$ is

\mathcal E[f] = \int_Z \|f(x) - y\|_Y^2 \, d\rho(x, y).

Hypothesis 2 asks for square-integrable outputs, a minimizer $f_{\mathcal H}$ of $\mathcal E$ over $\mathcal H$ , and a Bernstein-type moment bound on the noise $y - f_{\mathcal H}(x)$ with constants $M, \Sigma$ .

The operator $T = \int_X K_x K_x^*\, d\rho_X(x)$ on $\mathcal H$ satisfies $\langle Tf, g\rangle = \int_X \langle f(x), g(x)\rangle_Y \, d\rho_X$ . Its nonzero eigenvalues are $t_1 \ge t_2 \ge \dots$ , with orthonormal eigenvectors $e_n$ .

For positive constants $M, \Sigma, R, \alpha, \beta$ and parameters $1 < b < \infty$ , $1 \le c \le 2$ , the prior $\mathcal P(b, c)$ (Definition 1) is the set of probability measures $\rho$ satisfying three conditions:

Hypothesis 2 holds for the minimal-norm minimizer $f_{\mathcal H}$ ;
$f_{\mathcal H} = T^{(c-1)/2} g$ with $\|g\|_{\mathcal H}^2 \le R$ (a source condition);
the eigenvalues satisfy $\alpha \le n^b t_n \le \beta$ for all $n \ge 1$ .

A learning algorithm is a sequence of maps $f_\ell : Z^\ell \to \mathcal H$ , and $f^\ell_{\mathbf z}$ is its output on a sample $\mathbf z$ of size $\ell$ drawn from $\rho^\ell$ .

Formalization targets

Goal: Theorem 3 (p. 11)

For every $B > b$ ,

\inf_{\{f_\ell\}}\ \sup_{\rho \in \mathcal P(b, c)}\ \limsup_{\ell \to \infty} \frac{\mathbb E_{\mathbf z \sim \rho^\ell}\big(\mathcal E[f^\ell_{\mathbf z}] - \mathcal E[f_{\mathcal H}]\big)}{\ell^{-cB/(cB+1)}} > 0 .

Equivalently, there is $C > 0$ such that every algorithm admits one $\rho \in \mathcal P(b, c)$ with expected excess risk at least $C\ell^{-cB/(cB+1)}$ for infinitely many $\ell$ . The constant may depend on the prior and on $B$ , but not on the algorithm.

Milestones

Proposition 7 (pp. 25–26). A fair sign $s$ observed as $y = sg + n$ with i.i.d. $\mathcal N(0, \sigma^2)$ noise has Bayes error $\Phi(-\|g\|/\sigma)$ .
$\mathcal P' \subset \mathcal P(b, c)$ (pp. 26–27). This concerns distributions with marginal $\nu$ and conditional distribution $\mathcal N(m^{(s)}(x), \sigma^2\mathrm{Id})$ , where

m^{(s)} = \sum_n s_n\sqrt{\gamma_n/t_n}\,e_n, \qquad \gamma_n = n^{-(Bc+1)}\tfrac{\epsilon}{\epsilon+1}\alpha^c R,

with $\epsilon = (B - b)c$ and $s \in \{\pm1\}^\infty$ . Every such distribution belongs to the prior. 3. (63) (p. 27). Under these distributions, $\mathcal E[f] - \mathcal E[m^{(s)}] = \sum_n (c_n - s_n)^2\gamma_n$ with $c_n = \sqrt{t_n/\gamma_n}\langle f, e_n\rangle$ . 4. (68) (p. 28, corrected). $\sum_{\ell\gamma_n \le 1} \gamma_n \ge \tfrac{u^{1/(Bc+1)}}{2Bc}\,\ell^{-Bc/(Bc+1)}$ for $\ell \ge (2Bc)^{Bc+1}/u$ , where $u = \tfrac{\epsilon}{\epsilon+1}\alpha^c R$ . 5. (67) (pp. 28–30). Averaged over independent fair signs $S$ , the expected number of sign errors over $\{n : \ell\gamma_n \le 1\}$ , weighted by $\gamma_n$ , is at least $\Phi(-1/\sigma)\sum_{\ell\gamma_n \le 1}\gamma_n$ .

Significance

Theorem 3 shows that no algorithm, RLS included, converges on every fixed distribution of $\mathcal P(b, c)$ faster than $\ell^{-cB/(cB+1)}$ , for any $B > b$ . For $c > 1$ this exponent is arbitrarily close to the exponent $bc/(bc+1)$ of the upper rate of Theorem 1, so RLS with the regularization parameter of Theorem 1 is near-optimal even in the individual sense. The paper notes (p. 6) that full individual optimality would still need an upper rate in expectation or an individual lower rate in probability; that question is outside this mission.

The theorem is proved on paper and has been cited widely. To our knowledge no part of it has been machine-checked. A formalization would produce:

a checked reduction from a learning lower bound to Gaussian sign testing;
a Lean model of Gaussian-noise regression with vector outputs;
an explicit, checked version of the corrected computation (68).

Difficulty

A minimax argument picks a hard distribution for each $\ell$ , and that is not allowed here: the distribution must be fixed before $\ell$ varies. The obvious repair, taking the worst distribution for one $\ell$ and keeping it, fails, because a distribution that is hard at sample size $\ell$ can be easy at sample size $10\ell$ .

What has to be shown is a lower bound that holds for one distribution simultaneously along infinitely many sample sizes. Bounds that hold separately at each $\ell$ , with a distribution that may depend on $\ell$ , do not combine into such a bound.

A second difficulty arises in any reduction to a coordinatewise testing problem: each observation $y_i$ depends on all spectral coordinates of the regression function at once, so testing one coordinate is not literally the problem of Proposition 7.

Formalization scope

$\mathcal H$ is Mathlib's RKHS ℝ H X Y, with $K_x$ = RKHS.kerFun H x and $Y$ finite-dimensional. The paper's $\Sigma$ is written Sig.

The operator $T$ . It is never formed as an operator-valued integral. It enters through its quadratic form and through an eigen-system $(e_n, t_n)$ with summable weights.
Indexing. Indices start at $0$ , so the paper's $t_n$ is t (n-1).
The prior. InPrior encodes $\rho \in \mathcal P(b, c)$ , including "probability measure".
Expectations. Expectations are lintegrals of nonnegative quantities, and samples are Fin ℓ → X × Y under the product measure.
Algorithms. A learning algorithm is a family of maps from samples to $\mathcal H$ , and it must be measurable.
Added hypothesis. $\mathcal P(b, c)$ is assumed nonempty. The proof starts from "an arbitrary $\rho_0 \in \mathcal P(b, c)$ ", and with an empty prior the supremum is over the empty set and the statement fails.
The noise. Gaussian noise with covariance $\sigma^2\mathrm{Id}$ is $\sigma\xi$ with $\xi \sim$ stdGaussian Y.
$S^d$ . It is read as the surface area of the unit sphere of $\mathbb R^d$ .

Two parts of the print are corrected, and both corrections are stated in the items.

(68). The printed constant $v = u^{-Bc/(Bc+1)}/(2Bc)$ and threshold $2Bc(2Bcu)^{Bc}$ come from dropping the factor $u$ in an integral, and the printed inequality fails for $u < 1/2$ . The corrected constant is $u^{1/(Bc+1)}/(2Bc)$ , with threshold $(2Bc)^{Bc+1}/u$ .
(67). It is stated with the explicit constant $C = \Phi(-1/\sigma)$ that the proof obtains.

The goal mentions none of $\mathcal P'$ , $m^{(s)}$ , $\gamma_n$ or $\Phi$ . It is the lower rate (3) for the full prior $\mathcal P(b, c)$ with $a_\ell = \ell^{-cB/(cB+1)}$ . A formalization that fixed the algorithm, let the distribution depend on $\ell$ , or let the constant depend on the algorithm would prove a different, weaker statement.

A complete development needs:

Gaussian measures on finite-dimensional inner product spaces, and the distribution function of the standard normal;
conditional distributions on Polish products;
infinite products of fair coins;
series in Hilbert spaces with orthogonal terms.

Reusable pieces include Proposition 7, the Bayes-error monotonicity argument on p. 29, and the identification of the risk minimizer of a Gaussian-noise model. Contributions on any milestone are welcome, as are proofs of the measurability facts (elements of $\mathcal H$ are measurable under Hypothesis 1).

Selected references

A. Caponnetto and E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
L. Györfi, M. Kohler, A. Krzyżak and H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer Series in Statistics, 2002 (§3, Theorem 3.3; Lemma 3.2).
R. DeVore, G. Kerkyacharian, D. Picard and V. Temlyakov, Approximation methods for supervised learning, Found. Comput. Math. 6 (2006) 3–58.

8 thms1 active userReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

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

Motivation

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

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

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

Setting

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

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

The minimal divergence is

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (pp. 15–16)

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

13 thms1 active userReviewed

Machine Learning Statistics·Captain: mikedeng1

Optimal Rates for the Regularized Least-Squares Algorithm II: No Learning Algorithm Converges Faster than ℓ^(−bc/(bc+1)) Uniformly over P(b, c) — the Minimax Lower Rate (Theorem 2)Research Paper

Why lower bounds for kernel regression matter

Regularized least squares (RLS), also called kernel ridge regression, is one of the standard estimators of statistical learning: given a sample of input–output pairs, it fits a function from a reproducing kernel Hilbert space by minimizing the empirical squared error plus a multiple of the squared norm. Caponnetto and De Vito (FoCM 2007) proved that, over a class of distributions described by two parameters — the decay of the eigenvalues of the kernel's covariance operator and the smoothness of the regression function relative to it — RLS with a well-chosen regularization parameter converges at the rate $\ell^{-bc/(bc+1)}$ in the sample size $\ell$ (their Theorem 1). An upper rate on its own does not say whether another method could do better. This mission formalizes the matching minimax lower rate (their Theorem 2): when the output space is finite dimensional, no learning algorithm whatsoever converges faster than $\ell^{-bc/(bc+1)}$ uniformly over the class. Together the two theorems say that RLS is rate-optimal, and they are the reference point for later work on spectral regularization, early stopping and distributed kernel methods.

The paper's lower bound adapts the minimax analysis of DeVore, Kerkyacharian, Picard and Temlyakov (FoCM 2006) to the vector-valued RKHS setting.

Setting

Inputs $x$ lie in a Polish space $X$ and outputs $y$ in a real Hilbert space $Y$ of finite dimension $d$ . The hypothesis space $\mathcal H$ is a separable Hilbert space of functions $f : X \to Y$ in which evaluation is continuous; $K_x : Y \to \mathcal H$ is the adjoint of evaluation at $x$ , so $f(x) = K_x^* f$ . Hypothesis 1 asks that $(x,t) \mapsto \langle K_t v, K_x w\rangle_{\mathcal H}$ be measurable and that $\operatorname{Tr}(K_x^*K_x) \le \kappa$ for every $x$ .

A distribution $\rho$ on $Z = X \times Y$ has risk $\mathcal E[f] = \int \|f(x) - y\|^2\, d\rho$ . Hypothesis 2 asks that $\int\|y\|^2 d\rho < \infty$ , that the risk has a minimizer $f_{\mathcal H} \in \mathcal H$ (taken of minimal norm), and that the noise $y - f_{\mathcal H}(x)$ satisfies a Bernstein moment condition with constants $M, \Sigma$ . With $\rho_X$ the marginal of $\rho$ , the operator $T = \int K_x K_x^*\, d\rho_X(x)$ on $\mathcal H$ has the quadratic form $\langle Tf, g\rangle = \int \langle f(x), g(x)\rangle\, d\rho_X$ and a spectral decomposition $T = \sum_n t_n \langle\cdot, e_n\rangle e_n$ .

The prior $\mathcal P(b,c)$ (Definition 1, with fixed positive $M, \Sigma, R, \alpha, \beta$ , $1 < b < \infty$ and $1 \le c \le 2$ ) is the set of probability measures $\rho$ satisfying Hypothesis 2 with $M, \Sigma$ such that

$T$ has infinitely many positive eigenvalues $t_1 \ge t_2 \ge \dots$ with $\alpha \le n^b t_n \le \beta$ (a capacity condition);
$f_{\mathcal H} = T^{(c-1)/2} g$ for some $g$ with $\|g\|^2 \le R$ (a source condition).

Formalization targets

Goal: Theorem 2 (p. 11)

\lim_{\tau \to 0}\ \liminf_{\ell \to \infty}\ \inf_{f_\ell}\ \sup_{\rho \in \mathcal P(b,c)}\ \mathbb P_{\mathbf z \sim \rho^\ell}\Big[\mathcal E[f^\ell_{\mathbf z}] - \mathcal E[f_{\mathcal H}] > \tau\, \ell^{-\frac{bc}{bc+1}}\Big] = 1,

the infimum over all learning algorithms $f_\ell : Z^\ell \to \mathcal H$ . The constant in front of the rate is left free, so the goal asserts only the exponent.

Milestones

Proposition 4 (p. 21): for $f = T^{(c-1)/2}g$ , $\|g\|^2 \le R$ , the explicit distribution $\rho_f$ with marginal $\nu$ (the marginal of some $\rho_0 \in \mathcal P(b,c)$ ) and $2d$ -point conditional law is a probability measure with regression function $f$ , and lies in $\mathcal P(b,c)$ when $\min(M,\Sigma) \ge 2(4d+1)\sqrt{\kappa^c R}$ .
Proposition 4, (54): $\mathcal K(\rho_f, \rho_{f'}) \le \frac{16}{15 d L^2}\|\sqrt T(f - f')\|^2$ with $L = 4\sqrt{\kappa^c R}$ .
Proposition 6 (p. 24): for $m > 16$ there are $N \ge e^{m/24}$ sign vectors in $\{-1,+1\}^m$ with pairwise $\sum_n(\sigma_i^n - \sigma_j^n)^2 \ge m$ .
Proposition 5 (pp. 22–23): for small $\epsilon$ there are $N_\epsilon \ge e^{\gamma\epsilon^{-1/(bc)}}$ functions in the source class with $\epsilon \le \|\sqrt T(f_i - f_j)\|^2 \le 4\epsilon$ .
Theorem 5 (p. 24): for every algorithm some $\rho_* \in \mathcal P(b,c)$ has $\mathbb P[\text{excess risk} > \epsilon/4] \ge \min\{N^*/(N^*+1),\ e^{-3/e}\sqrt{N^*}\, e^{-4\ell\epsilon/(15 d\kappa^c R)}\}$ , $N^* = e^{\gamma\epsilon^{-1/(bc)}}$ .

Significance

The result. Theorem 2 shows that the exponent $bc/(bc+1)$ attained by RLS cannot be improved by any estimator over $\mathcal P(b,c)$ when $\dim Y < \infty$ ; for $c = 1$ RLS is optimal up to a logarithmic factor. It separates what is a property of the problem class from what is a property of the algorithm: improvements to kernel methods must change the class (stronger assumptions) rather than the rate. The construction — a packing of the source class measured in the $\sqrt T$ -norm, combined with a KL bound for an explicit noise model — is the template reused in many later lower bounds for kernel and inverse-problem estimators.

Formalizing it. The result has been proved since 2007; no machine-checked version exists. A formal proof needs the information-theoretic lower-bound machinery (a Fano-type inequality for many hypotheses), a Varshamov–Gilbert-type packing of the Hamming cube, KL divergence between explicit mixtures, and the spectral description of the covariance operator of a vector-valued RKHS. Each of these is reusable well beyond this paper. The mission also makes precise the paper's implicit conventions (see below), which a pen-and-paper reader fills in silently.

Difficulty

The upper half of the argument is not the hard part; the hard part is that the lower bound is uniform over all measurable algorithms, which no direct computation reaches. The step that does not follow from the paper alone is Theorem 5: its proof invokes Lemma 3.3 and Eq. 3.12 of DeVore et al., a Fano-type inequality bounding the probability of correct identification among $N$ hypotheses with pairwise KL divergence at most a given level. That lemma is not stated in the paper and is not in Mathlib; it must be formalized. A second obstacle is the packing (Proposition 6), whose proof is a probabilistic union bound with Hoeffding's inequality. A naive attempt to prove Theorem 2 by exhibiting a single bad distribution fails: for any fixed $\rho$ some algorithm (the constant one returning $f_{\rho}$ ) has zero excess risk, so the bad distribution must depend on the algorithm, and the order of quantifiers is essential.

Formalization scope

Mathlib's RKHS ℝ H X Y provides the function space with continuous evaluation, RKHS.kerFun is $K_x$ , and InformationTheory.klDiv is the Kullback–Leibler information. The operator $T$ is never built as an operator-valued Bochner integral: it is recorded through its quadratic form $\int\langle f(x), g(x)\rangle d\rho_X$ and an eigen-system indexed by $\mathbb N$ from $0$ (the paper's $t_n$ is t (n-1)). The trace in Hypothesis 1 is a series over a Hilbert basis of $Y$ ; the conditional law in Hypothesis 2 is Measure.condKernel, and the moment integral there is a lintegral. $\mathcal E[f_{\mathcal H}]$ in the goal is $\inf_{f \in \mathcal H}\mathcal E[f]$ .

Conventions and added hypotheses, each implicit on the page:

$\mathcal P(b,c)$ is assumed nonempty; the proof fixes $\rho_0 \in \mathcal P(b,c)$ , and over an empty prior the supremum is over the empty set and the statement is false.
Algorithms are measurable maps $Z^\ell \to \mathcal H$ ; this is the reading under which the probability in the goal is defined, and it restricts the infimum relative to "all mappings".
The constants $M, \Sigma, R, \alpha, \beta, \kappa$ are positive; the basis $(v_j)$ of $Y$ in Proposition 4 is orthonormal.
Proposition 4's " $\|g\|^2 \le R$ " for $f'$ is read as $\|g'\|^2 \le R$ ; Proposition 6's " $i \ne, j$ " as $i \ne j$ ; (56) is required for $i \ne j$ . The proof's variance display on p. 22 is wrong for $d \ge 2$ , but the conclusion of Proposition 4 holds.

The goal is the $\varepsilon$ – $\tau$ – $L$ unfolding of the limit and mentions neither $\rho_f$ , the KL bound nor the packing, so it cannot be discharged by any of the milestones' constructions in isolation; the distribution $\rho$ is chosen after the algorithm, never before it.

Contributions welcome: a general Fano/DeVore-type lemma for finitely many hypotheses, the Varshamov–Gilbert bound, KL ≤ χ² for finite mixtures, and lemmas relating covForm to the excess risk.

Selected references

A. Caponnetto, E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
R. DeVore, G. Kerkyacharian, D. Picard, V. Temlyakov, Approximation methods for supervised learning, Found. Comput. Math. 6 (2006) 3–58. https://doi.org/10.1007/s10208-004-0158-6
L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794

7 thms1 active userReviewed

Functional Analysis Machine Learning Statistics·Captain: mikedeng1

Optimal Rates for the Regularized Least-Squares Algorithm I: With λ Tuned to the Effective Dimension, Regularized Least Squares Attains the Rate ℓ^(−bc/(bc+1)) Uniformly over P(b, c) (Theorem 1)Research Paper

Motivation

Regularized least squares (RLS, also called kernel ridge regression or Tikhonov regularization) is the simplest learning algorithm built on a reproducing kernel Hilbert space. Given $\ell$ examples $(x_i,y_i)$ drawn independently from an unknown distribution $\rho$ , it returns the function in a hypothesis space $\mathcal H$ that minimizes the empirical squared error plus $\lambda$ times the squared norm. It is used in regression, in multi-task learning with vector-valued outputs, and as the reference case for spectral regularization methods.

The basic statistical question is how fast the excess risk of the RLS estimator goes to zero as $\ell$ grows, and how to choose $\lambda=\lambda_\ell$ to get that speed. Caponnetto and De Vito (FoCM 2007) answered it for a family of priors $\mathcal P(b,c)$ described by two numbers: the decay rate $b$ of the eigenvalues of the covariance operator of the input distribution and the regularity $c$ of the target function. Their Theorem 1 gives the upper rate $\ell^{-bc/(bc+1)}$ ; Theorems 2 and 3 show that no algorithm does better when the output space is finite dimensional. This mission formalizes the upper rate.

Timeline. Cucker and Smale (2002) and De Vito, Caponnetto and Rosasco (2005) gave rates for RLS that did not depend on the eigenvalue decay of $\rho_X$ . Zhang (2005) introduced the effective dimension $\mathcal N(\lambda)$ as the complexity measure. Caponnetto and De Vito (authors' copy dated 2006, published 2007) combined it with a source condition to obtain rates that are optimal over $\mathcal P(b,c)$ , for vector-valued outputs. Steinwart, Hush and Scovel (2009) and Fischer and Steinwart (2020) later extended the analysis to other norms and to $c<1$ .

Setting

The input space $X$ is a Polish space and the output space $Y$ is a real separable Hilbert space. The hypothesis space $\mathcal H$ is a real separable Hilbert space of functions $f:X\to Y$ in which evaluation at each point is continuous. For $x\in X$ , $K_x:Y\to\mathcal H$ is the adjoint of evaluation at $x$ , so $f(x)=K_x^*f$ . Hypothesis 1 adds a measurability condition and a uniform trace bound $\operatorname{Tr}(K_x^*K_x)\le\kappa$ .

A distribution $\rho$ on $Z=X\times Y$ has marginal $\rho_X$ and conditional laws $\rho(\cdot\mid x)$ . The expected risk of $f\in\mathcal H$ is $\mathcal E[f]=\int\|f(x)-y\|_Y^2\,d\rho$ . Hypothesis 2 asks that $\mathbb E\|y\|^2<\infty$ , that $\mathcal E$ attains its infimum over $\mathcal H$ at some $f_{\mathcal H}$ (the minimizer of minimal norm is used), and that the noise $y-f_{\mathcal H}(x)$ satisfies a Bernstein moment condition with constants $M,\Sigma$ .

The covariance operator $T=\int_XK_xK_x^*\,d\rho_X$ is positive and trace class, with $\langle Tf,f\rangle_{\mathcal H}=\int_X\|f(x)\|_Y^2\,d\rho_X$ and eigen-decomposition $T=\sum_nt_n\langle\cdot,e_n\rangle e_n$ , $t_1\ge t_2\ge\dots>0$ . The prior $\mathcal P(b,c)$ , for $1<b<\infty$ and $1\le c\le2$ , consists of the $\rho$ satisfying Hypothesis 2, with $f_{\mathcal H}=T^{(c-1)/2}g$ for some $\|g\|^2\le R$ (source condition), and with $\alpha\le n^bt_n\le\beta$ for all $n$ (eigenvalue decay).

The RLS estimator $f_{\mathbf z}^\lambda$ minimizes $\frac1\ell\sum_i\|f(x_i)-y_i\|_Y^2+\lambda\|f\|_{\mathcal H}^2$ over $\mathcal H$ .

Formalization targets

Goal: Theorem 1, $1<b<+\infty$

With $\lambda_\ell=\ell^{-b/(bc+1)}$ and $a_\ell=\ell^{-bc/(bc+1)}$ for $c>1$ , and $\lambda_\ell=a_\ell=(\log\ell/\ell)^{b/(b+1)}$ for $c=1$ ,

\lim_{\tau\to\infty}\limsup_{\ell\to\infty}\sup_{\rho\in\mathcal P(b,c)}\mathbb P_{\mathbf z\sim\rho^\ell}\Big[\mathcal E[f_{\mathbf z}^{\lambda_\ell}]-\mathcal E[f_{\mathcal H}]>\tau a_\ell\Big]=0.

The statement fixes the rate, not the constants: the threshold $\tau$ absorbs every constant of the prior.

Milestones

Proposition 1 iii)–v): the excess risk is $\|\sqrt T(f-f_{\mathcal H})\|^2$ ; the regularized expected and empirical risks have unique minimizers $f^\lambda=(T+\lambda)^{-1}Tf_{\mathcal H}$ and $f_{\mathbf z}^\lambda=(T_{\mathbf x}+\lambda)^{-1}g_{\mathbf z}$ .
Proposition 2: a Bernstein inequality for means of i.i.d. Hilbert-space-valued variables.
Theorem 4: with probability $\ge1-\eta$ ,

\mathcal E[f_{\mathbf z}^\lambda]-\mathcal E[f_{\mathcal H}]\le3C_\eta\Big(\mathcal A(\lambda)+\frac{\kappa^2\mathcal B(\lambda)}{\ell^2\lambda}+\frac{\kappa\mathcal A(\lambda)}{\ell\lambda}+\frac{\kappa M^2}{\ell^2\lambda}+\frac{\Sigma^2\mathcal N(\lambda)}{\ell}\Big),

provided $\ell\ge2C_\eta\kappa\mathcal N(\lambda)/\lambda$ and $\lambda\le\|T\|$ , where $C_\eta=32\log^2(6/\eta)$ , $\mathcal A(\lambda)=\mathcal E[f^\lambda]-\mathcal E[f_{\mathcal H}]$ , $\mathcal B(\lambda)=\|f^\lambda-f_{\mathcal H}\|^2$ and $\mathcal N(\lambda)=\operatorname{Tr}[(T+\lambda)^{-1}T]$ . 4. Proposition 3: on $\mathcal P(b,c)$ , $\mathcal A(\lambda)\le\lambda^c\|T^{(1-c)/2}f_{\mathcal H}\|^2$ , $\mathcal B(\lambda)\le\lambda^{c-1}\|T^{(1-c)/2}f_{\mathcal H}\|^2$ and $\mathcal N(\lambda)\le\frac b{b-1}\beta^{1/b}\lambda^{-1/b}$ .

Significance

The result. Theorem 1 says that RLS with $\lambda_\ell$ chosen from $(b,c)$ achieves the rate $\ell^{-bc/(bc+1)}$ uniformly over the prior, and the companion lower bounds show this is the minimax rate for $1<c\le2$ and finite-dimensional $Y$ . The rate interpolates between the parametric rate $1/\ell$ (fast eigenvalue decay, smooth target) and slower nonparametric rates, and it identifies the effective dimension, rather than the dimension of $\mathcal H$ , as the quantity that governs complexity. Theorem 4 is a non-asymptotic bound of independent use; it is the template for later analyses of spectral regularization, gradient descent with early stopping, and random-feature approximations of kernel methods.

The formalization. The result is proved on paper; no machine-checked proof of a kernel ridge regression rate is known to exist. A formal development requires a Bernstein inequality in Hilbert spaces, spectral calculus for a trace-class operator defined from a measure, and the operator-perturbation argument of Theorem 4. Two printed constants are corrected here: Theorem 4's proof yields $3C_\eta$ , not $C_\eta$ , and Proposition 3's bound on $\mathcal N(\lambda)$ has $\beta^{1/b}$ in place of $\beta$ . The paper also states Theorem 1 for $b=+\infty$ ; that branch fails for $1\le c<2$ and is not posed.

Difficulty

The obvious argument bounds $\|f_{\mathbf z}^\lambda-f^\lambda\|_{\mathcal H}$ by uniform concentration of $T_{\mathbf x}$ around $T$ and multiplies by $\|\sqrt T\|$ . That gives a variance term that ignores the eigenvalue decay of $T$ , and hence a rate that does not improve with $b$ . The optimal rate needs the variance measured through $\mathcal N(\lambda)$ , which requires controlling $\sqrt T(T_{\mathbf x}+\lambda)^{-1}$ in operator norm with high probability. This in turn needs concentration of $(T+\lambda)^{-1/2}(T-T_{\mathbf x})$ in Hilbert–Schmidt norm, and the condition $\ell\gtrsim\mathcal N(\lambda)/\lambda$ under which the empirical operator is close enough to $T$ . The noise is unbounded, so only the moment condition (9) is available, and the concentration step must use moment bounds rather than boundedness.

Formalization scope

$\mathcal H$ is Mathlib's RKHS ℝ H X Y, and $K_x$ is RKHS.kerFun H x. The trace in Hypothesis 1 is computed in a fixed Hilbert basis of $Y$ . $\rho_X$ is the first marginal and $\rho(\cdot\mid x)$ is condKernel. The operator $T$ is not built as an operator-valued integral. It enters through its quadratic form $\int\langle f(x),g(x)\rangle\,d\rho_X$ and through an eigen-system $(e_n,t_n)$ , indexed from $0$ , so (17) reads $\alpha\le(n+1)^bt_n\le\beta$ . The effective dimension is $\sum_nt_n/(t_n+\lambda)$ . Samples are Fin ℓ → X × Y under the product measure, and probabilities of events are outer measures. "With probability at least $1-\eta$ " is stated as "the bad event has measure at most $\eta$ ". The noise condition and the moments of Proposition 2 are integrals of nonnegative functions with values in $[0,\infty]$ .

The hypotheses the paper uses but does not display are added: positivity of $M,\Sigma,R,\alpha,\beta,\kappa$ , and integrability of the random variable in Proposition 2. The RLS estimator of the goal is any family of minimizers of (18) for $\ell\ge2$ ; at $\ell=1$ and $c=1$ the parameter $\lambda_1=0$ is degenerate. The goal quantifies uniformly: $L$ is chosen before $\rho$ , and the estimator is fixed before $\rho$ . The goal must not be replaced by a statement about $\mathcal A,\mathcal B,\mathcal N$ or by Theorem 4's event: it is the uniform rate for the estimator itself.

Reusable infrastructure: Hilbert-space Bernstein inequalities (Proposition 2 alone is a valuable target), spectral calculus for compact positive operators given by a quadratic form, and the representer/normal equation for vector-valued RLS. Contributions of proofs for any milestone, and of supporting lemmas about trace-class operators and effective dimension, are welcome.

Selected references

A. Caponnetto, E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
F. Cucker, S. Smale, On the mathematical foundations of learning, Bull. Amer. Math. Soc. 39 (2002) 1–49. https://doi.org/10.1090/S0273-0979-01-00923-5
E. De Vito, A. Caponnetto, L. Rosasco, Model selection for regularized least-squares algorithm in learning theory, Found. Comput. Math. 5 (2005) 59–85. https://doi.org/10.1007/s10208-004-0134-1
T. Zhang, Learning bounds for kernel regression using effective data dimensionality, Neural Comput. 17 (2005) 2077–2098. https://doi.org/10.1162/0899766054323008
I. Pinelis, Optimum bounds for the distributions of martingales in Banach spaces, Ann. Probab. 22 (1994) 1679–1706. https://doi.org/10.1214/aop/1176988477
I. Steinwart, D. Hush, C. Scovel, Optimal rates for regularized least squares regression, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/038.pdf
S. Fischer, I. Steinwart, Sobolev norm learning rates for regularized least-squares algorithms, J. Mach. Learn. Res. 21 (2020) 1–38. https://jmlr.org/papers/v21/19-734.html

9 thms1 active userReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

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

Timeline.

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2.4, equation (2.3)

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

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

Milestones (PART 1 of §3)

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

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

Selected references

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

14 thms1 active userReviewed

Combinatorics Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVII: Goemans–Williamson Rounding of the MAXCUT SDP Relaxation Has Expected Value at Least 0.878 Times the Maximum CutTextbook

Motivation

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

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

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

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

Milestones

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

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

Companion: Theorem 6.13 (Nesterov)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

6 thms1 active userReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVI: Random Coordinate Descent RCD(γ) on a Strongly Convex Coordinate-Smooth Function Has Rate (1 − 1/κ_γ)^tTextbook

Motivation

When a problem has millions of variables, even one full gradient can be too expensive to compute, while a single partial derivative $\partial f/\partial x_i$ is often cheap: in regularized regression, support vector machines and many structured problems, updating one coordinate costs a small fraction of a full gradient step. Coordinate descent methods exploit this by moving along one coordinate at a time. They are among the oldest optimization schemes and were for a long time analysed only for cyclic orders and only asymptotically.

Nesterov (2012) showed that choosing the coordinate at random, with probabilities depending on the coordinate-wise smoothness constants, gives global, non-asymptotic rates that can beat full gradient descent in total work. This mission formalizes that analysis as presented in §6.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 338–342, and in particular its linear rate for strongly convex functions (Theorem 6.8).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be differentiable, write $\nabla_i f(x)=\frac{\partial f}{\partial x_i}(x)$ and let $e_i$ be the $i$ -th standard basis vector. The function is directionally smooth with constants $\beta_1,\dots,\beta_n>0$ if

|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le\beta_i|u|\qquad\text{for all } i\in[n],\ x\in\mathbb R^n,\ u\in\mathbb R,

equivalently, each one-variable restriction $u\mapsto f(x+ue_i)$ is $\beta_i$ -smooth.

For a real exponent $c$ , the weighted norms are

\|x\|_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{c}x_i^2},\qquad \|x\|^*_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{-c}x_i^2}.

For $\alpha>0$ , $f$ is $\alpha$ -strongly convex w.r.t. a norm $\|\cdot\|$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y$ . The point $x^*$ is a minimizer of $f$ .

For $\gamma\ge0$ , RCD( $\gamma$ ) starts at $x_1\in\mathbb R^n$ and iterates

x_{s+1}=x_s-\frac{1}{\beta_{i_s}}\nabla_{i_s}f(x_s)\,e_{i_s},

where $i_1,i_2,\dots$ are drawn independently from $p_\gamma(i)=\beta_i^\gamma/\sum_{j}\beta_j^\gamma$ . The case $\gamma=0$ is uniform sampling; $\gamma=1$ samples proportionally to $\beta_i$ .

Formalization targets

Goal: Theorem 6.8 (p. 341)

Let $\gamma\ge0$ , let $f$ be $\alpha$ -strongly convex w.r.t. $\|\cdot\|_{[1-\gamma]}$ and directionally smooth with constants $\beta_i$ , and let $\kappa_\gamma=\sum_i\beta_i^\gamma/\alpha$ . Then for every $t\ge0$

\mathbb E f(x_{t+1})-f(x^*)\le\Big(1-\frac{1}{\kappa_\gamma}\Big)^t\big(f(x_1)-f(x^*)\big).

Milestones

Lemma 6.9 (p. 341): for $f$ $\alpha$ -strongly convex w.r.t. any norm, $f(x)-f(x^*)\le\frac{1}{2\alpha}\|\nabla f(x)\|_*^2$ .
One coordinate step (p. 340): $f\big(x-\frac{1}{\beta_i}\nabla_i f(x)e_i\big)-f(x)\le-\frac{1}{2\beta_i}(\nabla_i f(x))^2$ .
Expected decrease (p. 340): $\mathbb E_{i_s}f(x_{s+1})-f(x_s)\le-\frac{1}{2\sum_i\beta_i^\gamma}\big(\|\nabla f(x_s)\|^*_{[1-\gamma]}\big)^2$ .
Lemma 6.9 in the weighted norm (p. 342): $\big(\|\nabla f(x)\|^*_{[1-\gamma]}\big)^2\ge2\alpha(f(x)-f(x^*))$ .
Contraction (pp. 341–342): one step multiplies the expected gap by at most $1-1/\kappa_\gamma$ .

Companion: Theorem 6.7 (pp. 339–340)

For $f$ convex and directionally smooth, and $t\ge2$ ,

\mathbb E f(x_t)-f(x^*)\le\frac{2R_{1-\gamma}^2(x_1)\sum_i\beta_i^\gamma}{t-1},\qquad R_{1-\gamma}(x_1)=\sup_{f(x)\le f(x_1)}\|x-x^*\|_{[1-\gamma]}.

Significance

Theorem 6.8 says random coordinate descent converges linearly, with a rate governed by $\sum_i\beta_i^\gamma/\alpha$ instead of the global smoothness constant. For $\gamma=1$ , directional smoothness implies $f$ is $\beta$ -smooth with $\beta\le\sum_i\beta_i$ , so for functions whose global smoothness constant is of the order of $\sum_i\beta_i$ , RCD(1) attains the accuracy of gradient descent after the same number of iterations (book, p. 340, comparing Theorem 6.7 with Theorem 3.3), while each iteration touches a single coordinate. The same per-step inequalities underlie later accelerated and parallel coordinate methods.

These results are proved in the literature (Nesterov 2012; Bubeck 2015). Their contribution here is a machine-checked version. As far as a search of the Prove2Me catalogue shows, no coordinate descent rate of this kind has been formalized there; a Euclidean-norm special case of Lemma 6.9 exists on the platform as a separate result, but not the arbitrary-norm lemma or the weighted-norm instance used here.

Difficulty

The main obstacle is bookkeeping of the randomness: the per-step inequality holds for each fixed iterate, while the theorem is about the expectation over the whole sequence of draws $i_1,\dots,i_t$ , so the pointwise contraction has to be passed through the tower of conditional expectations. In the strongly convex case this is linear and exact; for Theorem 6.7 the recursion on $\delta_s=\mathbb Ef(x_s)-f(x^*)$ is quadratic, and since $\delta_s$ is an expectation while the gradient norm at $x_s$ is random, the pointwise inequality does not transfer to $\delta_s$ verbatim. A second point is geometric: strong convexity, the dual norm and the sampling distribution must use matching weights ( $\beta_i^{1-\gamma}$ against $\beta_i^{\gamma}$ ), and a mismatch silently changes the constant.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map $g$ with HasGradientAt f (g x) x, so $\nabla_i f(x)=g(x)_i$ . Lemma 6.9 is stated for a finite-dimensional real normed space with the Fréchet derivative and the operator norm as the dual norm.
Powers $\beta_i^c$ are real powers. The theorems assume $n\ge1$ , $\alpha>0$ and $\beta_i>0$ , which the book uses implicitly; $\gamma\ge0$ is the book's.
RCD(γ) is a deterministic function of the drawn coordinates, and the expectation over $t$ independent draws from $p_\gamma$ is the finite sum $\sum_{(i_1,\dots,i_t)\in[n]^t}\prod_s p_\gamma(i_s)\,F(i_1,\dots,i_t)$ . No measure theory or integrability conventions are involved.
The minimizer $x^*$ is assumed to exist, as the book does throughout; its uniqueness, which the book assumes "only for sake of notation", is not used.
In Theorem 6.7 the supremum $R_{1-\gamma}(x_1)$ is passed as any real upper bound $R$ on the sublevel set, which is equivalent when the supremum is finite and avoids Lean's value $0$ for an unbounded supremum.
Directional smoothness is required at every $x$ and $u$ , and $p_\gamma$ is fixed by the $\beta_i$ ; neither is weakened to hold only along the iterates, which would change the theorem.

A complete development needs the one-dimensional descent lemma (3.5), weighted Cauchy–Schwarz for the dual pair $\|\cdot\|_{[c]},\|\cdot\|^*_{[c]}$ , and a decomposition of the finite expectation over $[n]^{t+1}$ into the last draw and the first $t$ . The weighted-norm and finite-expectation lemmas are reusable for other randomized coordinate and sampling methods. Proofs of the milestones and of either theorem are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §6.4, pp. 338–342.
Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2):341–362, 2012. doi:10.1137/100802001
P. Richtárik and M. Takáč, Parallel coordinate descent methods for big data optimization, Mathematical Programming 156:433–484, 2016. arXiv:1212.0873

7 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (p. 17)

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

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

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

Central milestone: Theorem 1 (p. 15)

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

Milestones

In attack order:

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Standing assumptions and handled gaps:

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

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

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

Selected references

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

14 thms1 active userReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XV: SVRG with η = 1/(10β) and k = 20κ Contracts the Expected Optimality Gap by 0.9 per EpochTextbook

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$ , and define the finite-sum objective and its gradient by

f(x)=\frac1m\sum_{i=1}^m f_i(x),\qquad G(x)=\frac1m\sum_{i=1}^m \nabla f_i(x).

Each component is $\beta$ -smooth when its gradient is $\beta$ -Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$ . The average $f$ is $\alpha$ -strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$ . The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$ , and $\kappa=\beta/\alpha$ .

An epoch begins at an anchor $y$ . Its first inner iterate is $x_1=y$ . For $t=1,\ldots,k$ , draw $i_t$ uniformly from $\{1,\ldots,m\}$ , independently across steps and epochs, and update

x_{t+1}=x_t-\eta\bigl(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)+G(y)\bigr).

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$ . In particular, this average uses $x_1$ through $x_k$ , while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$ . The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$ ,

\mathbb E f(y^{(s+1)})-f(x^*) \le 0.9^s\bigl(f(y^{(1)})-f(x^*)\bigr).

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$ . The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$ . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$ . The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$ . Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$ , so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$ . The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$ , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$ , and integrality of $20\beta/\alpha$ , make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$ . Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$ . Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

10 thms1 active userReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XIV: Stochastic Mirror Descent on a β-Smooth Function with Noise σ Has Rate Rσ√(2/t) + βR²/tTextbook

Motivation

Many optimization problems in statistics and machine learning ask to minimize an expected loss $f(x)=\mathbb E_\xi\,\ell(x,\xi)$ , or an average $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ over a large data set. Exact gradients of such an $f$ are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.

Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order $1/\sqrt t$ and a smoothness term of order $1/t$ . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . Gradients are linear forms $g$ on $E$ , the value of $g$ at $v$ is written $g^\top v$ , and the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be compact and convex.

A mirror map is a function $\Phi$ on an open convex set $\mathcal D$ with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . It is strictly convex and differentiable on $\mathcal D$ , its gradient $\nabla\Phi$ takes every value, and $\|\nabla\Phi(x)\|_*\to\infty$ as $x$ approaches the boundary of $\mathcal D$ . Its Bregman divergence is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ . The map is 1-strongly convex on $\mathcal X\cap\mathcal D$ if $D_\Phi(y,x)\ge\frac12\|x-y\|^2$ there. A function $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

A stochastic oracle returns, at a query point $x$ , a random linear form $\tilde g(x)$ . When the query point is itself random, the book requires the conditional expectation given the query point, $\mathbb E(\tilde g(x)\mid x)$ , to be a subgradient of $f$ at $x$ . In the smooth case it requires $\mathbb E(\tilde g(x)\mid x)=\nabla f(x)$ together with the variance bound $\mathbb E(\|\tilde g(x)-\nabla f(x)\|_*^2\mid x)\le\sigma^2$ .

S-MD with step $\gamma$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, writing $\tilde g_s=\tilde g(x_s)$ , iterates

x_{s+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}\ \gamma\,\tilde g_s^\top x+D_\Phi(x,x_s).

Let $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , and let $x^*$ minimize $f$ on $\mathcal X$ .

Formalization targets

Goal: Theorem 6.3

Let $f$ be convex and $\beta$ -smooth, and let the oracle have variance at most $\sigma^2$ . Then for every $t\ge1$ , S-MD with step $1/(\beta+1/\eta)$ and $\eta=\frac R\sigma\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^t x_{s+1}\Big)-f(x^*)\le R\sigma\sqrt{\frac2t}+\frac{\beta R^2}{t}.

Milestones (the proof's four displays)

For points $x_s,x_{s+1}\in\mathcal X\cap\mathcal D$ and $\eta>0$ , the smoothness step is

f(x_{s+1})-f(x_s)\le\tilde g_s^\top(x_{s+1}-x_s)+\tfrac\eta2\|\nabla f(x_s)-\tilde g_s\|_*^2+(\beta+1/\eta)D_\Phi(x_{s+1},x_s).

If $x_{s+1}$ is the S-MD step, the mirror step is

\tfrac{1}{\beta+1/\eta}\tilde g_s^\top(x_{s+1}-x^*)\le D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})-D_\Phi(x_{s+1},x_s).

Combining the two gives a pathwise bound on $f(x_{s+1})$ with the cross term $(\tilde g_s-\nabla f(x_s))^\top(x^*-x_s)$ . Taking expectations gives the expected one-step bound

\mathbb Ef(x_{s+1})-f(x^*)\le(\beta+1/\eta)\,\mathbb E\big(D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})\big)+\frac{\eta\sigma^2}{2}.

Companion: Theorem 6.1 and (4.10)

For a convex $f$ with $\mathbb E(\|\tilde g(x)\|_*^2\mid x)\le B^2$ , S-MD with $\eta=\frac RB\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^tx_s\Big)-\min_{\mathcal X}f\le RB\sqrt{2/t}.

This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors $g_s$ :

\sum_{s\le t}g_s^\top(x_s-x)\le\frac{R^2}{\eta}+\frac{\eta}{2\rho}\sum_{s\le t}\|g_s\|_*^2.

Significance

Theorem 6.3 says exactly how much smoothness helps under noise. As $\sigma\to0$ it recovers the $\beta R^2/t$ rate of deterministic smooth optimization. For large $t$ the noise term $R\sigma\sqrt{2/t}$ dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging $m$ independent oracle answers divides the variance by $m$ , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by $\sqrt m$ while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.

These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.

Difficulty

The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point $x_s$ is random, so unbiasedness enters only through the conditional expectation given $x_s$ . Making the cross term vanish requires pulling the $\sigma(x_s)$ -measurable vector $x^*-x_s$ out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When $\nabla\Phi$ blows up at the boundary of $\mathcal D$ , the Bregman terms $D_\Phi(x^*,x_s)$ are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer $x^*$ may lie on the boundary of $\mathcal D$ , where $\Phi$ is not part of the book's data. Treating $\mathbb E$ informally, or assuming $x^*\in\mathcal D$ , skips exactly these points.

Formalization scope

Spaces and gradients. $E$ is a finite-dimensional real normed space. Gradients are explicit maps Φ' f' : E → (E →L[ℝ] ℝ), $g^\top v$ is g v, and $\|\cdot\|_*$ is the operator norm. $\beta$ -smoothness is stated with derivatives relative to $\mathcal X$ . $\Phi$ is a total function, constrained only by the mirror-map axioms on $\mathcal D$ .
Runs and oracle. S-MD is a run predicate. For every outcome, $x_1$ minimizes $\Phi$ on $\mathcal X\cap\mathcal D$ , and $x_{s+1}$ is some minimizer of the step objective. The oracle is a predicate on the random sequences $(x_s,\tilde g_s)$ : each $x_s$ is measurable, and the conditional expectations are taken given $\sigma(x_s)$ . Every conditioned quantity is integrable.
Conclusions. Every bound on an expectation also asserts integrability. Without it, the Lean integral of a non-integrable function is $0$ and the bound could hold trivially.
Standing assumptions. The book's $R^2=\sup(\Phi-\Phi(x_1))$ is replaced by any upper bound $R^2$ . The minimizer $x^*\in\mathcal X$ exists (p. 242). $\mathcal X$ is compact and convex (Chapter 4), and convex functions are closed (p. 236).
Positivity side conditions. $R,\sigma,B>0$ and $t\ge1$ make the step sizes and bounds defined, and $\beta\ge0$ .

A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let $x_{s+1}$ be an arbitrary point of $\mathcal X\cap\mathcal D$ would make the theorems false, and are not used either.

A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, https://arxiv.org/abs/1405.4980 (Chapter 6, pp. 329–333; Chapter 4, pp. 297–307).
O. Dekel, R. Gilad-Bachrach, O. Shamir, L. Xiao, Optimal distributed online prediction using mini-batches, Journal of Machine Learning Research 13:165–202, 2012. https://jmlr.org/papers/v13/dekel12a.html
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277

6 thms1 active userReviewed

Machine Learning Optimal Transport Statistics·Captain: mikedeng1

Robust Wasserstein Profile Inference and Applications to Machine Learning 3: The Scaled Robust Wasserstein Profile n^(ρ/2)·R_n(θ*) Is Asymptotically Stochastically Bounded by R̄(ρ)Research Paper

Motivation

Many statistical parameters are defined implicitly, as the root $\theta_*$ of an estimating equation $\mathbb E[h(W, \theta_*)] = \mathbf 0$ : a mean, a quantile, a regression coefficient, the minimizer of an expected loss. Owen's empirical likelihood builds confidence regions for such parameters by asking how far the empirical distribution of the data must be reweighted before the equation holds, and the profile of that distance has a chi-squared limit (Owen, Empirical Likelihood, 2001).

Blanchet, Kang and Murthy replace reweighting by transport: they measure how much the data must be moved, in the sense of optimal transport, before the equation holds. The resulting Robust Wasserstein Profile (RWP) function plays the role of the empirical-likelihood profile, and its value at the true parameter is exactly the smallest radius of a Wasserstein ball around the data that contains a distribution satisfying the estimating equation. Its asymptotic law is therefore what is needed to choose the radius of Wasserstein distributionally robust estimators, such as the square-root LASSO and regularized logistic regression, in a data-driven way (arXiv:1610.05627, §§1, 3, 4). This mission formalizes the paper's main limit theorem, Theorem 3.

Setting

Let $c : \mathbb R^m \times \mathbb R^m \to [0, \infty]$ be a cost. The optimal transport cost between probability laws $P$ and $Q$ on $\mathbb R^m$ is

D_c(P, Q) = \inf\{ \mathbb E_\pi[c(U, W)] : \pi_U = P,\ \pi_W = Q \},

the infimum over all joint laws $\pi$ of a pair $(U, W)$ with the given marginals (Eq. (7)). In this mission $c(u, w) = \|w - u\|_q^\rho$ with $\rho \ge 1$ and $q \in (1, \infty]$ , and $p$ denotes the conjugate exponent, $1/p + 1/q = 1$ .

Let $h : \mathbb R^m \times \mathbb R^l \to \mathbb R^r$ be an estimating function, and let $W, W_1, W_2, \dots$ be i.i.d. random vectors in $\mathbb R^m$ with $\mathbb E[h(W, \theta_*)] = \mathbf 0$ . With $\mathbb P_n$ the empirical distribution of $W_1, \dots, W_n$ , the RWP function is

R_n(\theta) = \inf\{ D_c(P, \mathbb P_n) : \mathbb E_P[h(W, \theta)] = \mathbf 0 \}. \qquad (16)

Write $D_w h(w, \theta_*)$ for the $r \times m$ Jacobian of $w \mapsto h(w, \theta_*)$ , and $\|\zeta^T D_w h(w, \theta_*)\|_p$ for the $\ell_p$ norm of the row vector $\zeta^T D_w h(w, \theta_*) \in \mathbb R^m$ , $\zeta \in \mathbb R^r$ . The assumptions are:

A1) $c(u, w) = \|u - w\|_q^\rho$ , $\rho \ge 1$ ;
A2) $\mathbb E[h(W, \theta_*)] = \mathbf 0$ and $\mathbb E\|h(W, \theta_*)\|_2^2 < \infty$ ;
A3) $h(\cdot, \theta_*)$ is continuously differentiable;
A4) for every $\zeta \ne 0$ , $\mathbb P(\|\zeta^T D_w h(W, \theta_*)\|_p > 0) > 0$ .

A sequence $X_n$ is asymptotically stochastically bounded by $X$ , written $X_n \lesssim_D X$ , if $\limsup_n \mathbb E[f(X_n)] \le \mathbb E[f(X)]$ for every continuous, bounded, non-decreasing $f$ .

Formalization targets

Goal: Theorem 3 (p. 15)

Let $H \sim \mathcal N(\mathbf 0, \mathbb E[h(W, \theta_*) h(W, \theta_*)^T])$ . Under A1)–A4),

n^{\rho/2} R_n(\theta_*; \rho) \lesssim_D \bar R(\rho),

where for $\rho > 1$

\bar R(\rho) = \max_{\zeta \in \mathbb R^r} \Big\{ \rho \zeta^T H - (\rho - 1)\, \mathbb E\|\zeta^T D_w h(W, \theta_*)\|_p^{\rho/(\rho - 1)} \Big\},

and for $\rho = 1$

\bar R(1) = \max_{\zeta :\ \mathbb P(\|\zeta^T D_w h(W, \theta_*)\|_p > 1) = 0} \zeta^T H.

The formal goal also asserts that $R_n(\theta_*)$ is finite and measurable and that both maxima are attained; these are facts the paper's statement presupposes.

Milestones (proof of Theorem 3, App. A.3)

Proposition 3 (p. 13): strong duality, $R_n(\theta) = \sup_\lambda \{ -\frac1n \sum_i \sup_u \{\lambda^T h(u, \theta) - c(u, W_i)\} \}$ when $\mathbf 0 \in \operatorname{int} \operatorname{conv} h(\mathbb R^m, \theta)$ .
(31)–(32) (p. 32): $n^{\rho/2} R_n(\theta_*) = \sup_\zeta \{ -\zeta^T H_n - M_n(\zeta) \}$ , with $H_n = n^{-1/2} \sum_i h(W_i, \theta_*)$ and the random penalty $M_n$ .
Lemma 2 (p. 32): the supremum in (31) localizes to a compact set of $\zeta$ with high probability.
(42) (p. 36): $\max_\Delta \{ v^T \Delta - \|\Delta\|_q^\rho \} = \|v\|_p^{\rho/(\rho-1)} (1/\rho)^{1/(\rho-1)} (1 - 1/\rho)$ .
Lemma 3 (p. 34): a uniform law of large numbers for the localized penalty.

Significance

Theorem 3 gives the rate $n^{-\rho/2}$ at which the RWP function at the true parameter vanishes and an explicit random variable bounding its rescaled limit. The $(1-\alpha)$ -quantile $\eta_\alpha$ of $\bar R(\rho)$ yields a radius $\delta = n^{-\rho/2}\eta_\alpha$ for which the Wasserstein ball around $\mathbb P_n$ contains, with asymptotic probability at least $1 - \alpha$ , a law satisfying the estimating equation at $\theta_*$ (§3.1, (19)); this is the paper's prescription for the regularization parameter of square-root LASSO and of regularized logistic regression (§4). Example 3 (p. 14) shows the bound is sharp for the mean: $n^{\rho/2} R_n(\theta_*) \Rightarrow \sigma_W^\rho |N(0, 1)|^\rho$ . Matching lower bounds (Propositions 4 and 5) need further assumptions and are not part of this mission.

The result is proved in the paper; no machine-checked version of it, or of any RWP or empirical-likelihood limit theorem, is known to exist. A formalization would check the duality argument for the problem of moments, the passage from the dual representation to a localized maximization, and the continuous-mapping step, and would produce reusable statements: strong duality for transport-cost moment problems, the closed form of the conjugate of $\|\cdot\|_q^\rho$ , and a uniform law of large numbers over a compact parameter set.

Difficulty

The obvious route is to apply the central limit theorem to $H_n$ and pass to the limit inside the dual representation (31). This fails as stated, for two reasons. First, the supremum in (31) is over all of $\mathbb R^r$ , and convergence of the objective on compact sets does not control the supremum; Lemma 2 is needed, and it uses A4) through a lower bound on $\mathbb E\|\bar\zeta^T Dh(W)\|_p^p$ that is uniform over the unit sphere. Second, the penalty $M_n$ involves the derivative of $h$ at points $W_i + n^{-1/2}\Delta u$ that are not localized, with no moment assumption on $Dh$ ; the proof must truncate to $\|W_i\|_p \le c_0$ and to a specific near-optimal $\Delta$ , and then remove the truncation. The case $\rho = 1$ differs: the inner supremum is $0$ or $+\infty$ , and the limit becomes a maximization over a constraint set.

Formalization scope

Vectors are Fin k → ℝ; $\ell_q$ and $\ell_p$ norms are Mathlib's PiLp norms, so $q = \infty$ is allowed, with $q \in (1, \infty]$ and p.HolderConjugate q. The samples are a sequence W : ℕ → Ω → (Fin m → ℝ), mutually independent (iIndepFun) and identically distributed with W 0, which plays the role of $W$ ; $R_n$ uses $W_0, \dots, W_{n-1}$ through the published empiricalDistribution. Distinct samples are not assumed in Theorem 3; Proposition 3 and (31) keep the §3.1 assumption of distinct samples. Transport costs and $R_n$ are $[0, \infty]$ -valued lower Lebesgue integrals and infima; $\bar R(\rho)$ is computed in the extended reals with the moment $\mathbb E\|\cdot\|_p^{\rho/(\rho-1)}$ in $[0, \infty]$ . $H$ 's law is multivariateGaussian 0 Cov on EuclideanSpace ℝ (Fin r).

The goal is a conjunction: finiteness of $R_n(\theta_*)$ for $n \ge 1$ , its a.e.-measurability, attainment of the maxima in $\bar R(\rho)$ , and the limsup bound. Without the first three, a real-valued formalization could hold for the wrong reason (an infinite $R_n$ converted to $0$ , a non-measurable integrand integrated to $0$ , or an unbounded supremum replaced by $0$ ); the conjunction rules this out.

Readings of the page recorded in the items: A1) says $q \ge 1$ while (17) and the proof of Lemma 2 use $q > 1$ , and $q \in (1,\infty]$ is used; Proposition 3 is stated for a cost that is finite everywhere, the setting of §3, because for a cost that is infinite on part of the space the interior condition on $h(\mathbb R^m, \theta)$ does not imply the Slater condition used in App. B; Lemmas 2 and 3 state the standing assumptions A1), A3) and i.i.d. sampling that their statements leave implicit. The localized weak limit (45) is not a milestone: its penalty $M'_n$ depends on a $\zeta$ -dependent near-optimal direction that is not stated precisely enough on the page.

Needed infrastructure: the multivariate central limit theorem (Mathlib has the real-valued one), Hölder duality for PiLp norms, a strong-duality theorem for moment problems (Proposition 7, quoted from Isii and Karlin–Studden), and a uniform law of large numbers. The duality results and the conjugate formula (42) are reusable beyond this mission. Proofs of any milestone, and lemmas that serve them, are welcome.

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
A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. https://arxiv.org/abs/1604.01446
K. Isii, On sharpness of Tchebycheff-type inequalities, Ann. Inst. Statist. Math. 14, 1962. https://doi.org/10.1007/BF02868641
C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

12 thms1 active userReviewed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 1: Strong Duality — the Worst-Case Expectation over an Optimal-Transport Ball on a Polish Space Equals Its Dual over (λ, φ)Research Paper

Motivation

A probability model $\mu$ for a random element $X$ is rarely known exactly. Distributionally robust performance analysis replaces the single expectation $E_\mu[f(X)]$ by its worst case over all models within a prescribed distance of $\mu$ . When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of $\mu$ . That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.

Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.

Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on $\mathbb R^d$ . Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as $C[0,T]$ and $D[0,T]$ .

Setting

Let $S$ be a Polish space with Borel σ-algebra $\mathcal B(S)$ , and let $\mu$ be a probability measure on $S$ (the baseline model).

Cost (A1). $c : S\times S\to[0,\infty)$ is lower semicontinuous, and $c(x,y)=0$ if and only if $x=y$ .
Performance function (A2). $f : S\to\mathbb R$ is upper semicontinuous and $\mu$ -integrable.
Budget. $\delta>0$ .

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ whose first marginal is $\mu$ and whose transport cost satisfies $\int c\,d\pi\le\delta$ . The second marginal of $\pi$ is the alternative model. The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ , and the primal value is

I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}.

The universal σ-algebra $\mathcal U(S)$ is the intersection of the completions of $\mathcal B(S)$ under all probability measures. Write $m\mathcal U(S;\bar{\mathbb R})$ for the $\mathcal U(S)$ -measurable functions $S\to[-\infty,\infty]$ . The dual feasible set $\Lambda_{c,f}$ consists of the pairs $(\lambda,\varphi)$ with $\lambda\ge0$ , $\varphi\in m\mathcal U(S;\bar{\mathbb R})$ and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$ . The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ , and the dual value is $J=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\}$ . Finally,

\varphi_\lambda(x)=\sup_{y\in S}\{f(y)-\lambda c(x,y)\}\in\mathbb R\cup\{\infty\}.

Formalization targets

Goal: Theorem 1

Under (A1) and (A2):

strong duality,

\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\};

there is $\lambda^*\ge0$ such that $(\lambda^*,\varphi_{\lambda^*})$ is a dual optimizer;
a feasible $\pi^*$ and a feasible $(\lambda^*,\varphi_{\lambda^*})$ with finite $J(\lambda^*,\varphi_{\lambda^*})$ are optimal with $I(\pi^*)=J(\lambda^*,\varphi_{\lambda^*})$ if and only if the complementary slackness conditions hold:

f(y)-\lambda^*c(x,y)=\varphi_{\lambda^*}(x)\ \ \pi^*\text{-a.s.},\qquad \lambda^*\Big(\int c\,d\pi^*-\delta\Big)=0.

The "if" direction is stated without the finiteness assumption.

Milestones

Weak duality $I\le J$ (5). Lemma 15. Strong duality with a primal optimizer on compact $S$ , first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of $\varphi_\lambda$ (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):

I=\inf_{\lambda\ge0}\Big\{\lambda\delta+E_\mu\Big[\sup_{y\in S}\{f(y)-\lambda c(X,y)\}\Big]\Big\}.

Significance

The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline $\mu$ . A modeller can therefore evaluate it by sampling from $\mu$ . Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from $x$ to maximizers of $f(z)-\lambda^*c(x,z)$ , and the budget is exhausted whenever $\lambda^*>0$ .

Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on $\mathbb R^m$ ). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.

Difficulty

The obvious route copies Kantorovich duality. That route fails here because the feasible set $\Phi_{\mu,\delta}$ fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces $S_n\times S_n$ . The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.

A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, $\varphi_\lambda$ need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction $y\in S_\pi$ from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces $C[0,T]$ and $D[0,T]$ .

Formalization scope

Space and costs. S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.
Extended reals. $I$ , $J$ , $I(\pi)$ , $J(\lambda,\varphi)$ and $\varphi_\lambda$ live in EReal. The integral of an extended-real function is $\int\varphi^+-\int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$ . A coupling with $\int f^-\,d\pi=\infty$ therefore never raises $I$ , which is the paper's reading in footnote 2.
Measurability and integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such $\varphi$ the lower integral equals the integral against the completion of $\mu$ .
Variants. The dual feasible set takes a set $K$ : with $K=S$ it is (6b), and with $K=S_\pi$ it is (29).
Hidden hypothesis. The "only if" part of Theorem 1(b) carries the hypothesis $J(\lambda^*,\varphi_{\lambda^*})<\infty$ . Without it the equivalence fails when $I=J=\infty$ .
Ruled-out trivializations. A primal that fixes both marginals (or neither), a dual over Borel-measurable $\varphi$ , and a Bochner integral for $\int f\,d\pi$ (which is $0$ off $L^1(\pi)$ ) all describe different problems and are ruled out by the definitions.
Infrastructure and contributions. Needed: Fenchel duality on $C_b(S\times S)$ and its dual $M(S\times S)$ (Riesz–Markov–Kakutani), Prokhorov's theorem, Sion's minimax theorem, and Jankov–von Neumann selection. Several are on the platform or in Mathlib, and all are reusable beyond this mission. Proofs of the milestones in any order, and of the posed Bertsekas–Shreve tools, are welcome.

Selected references

J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
D. Bertsekas and S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 7. MIT open copy
C. Villani, Optimal Transport: Old and New, Springer, 2008. doi:10.1007/978-3-540-71050-9

19 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2.1 (p. 10)

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

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

then

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

Milestones on the way

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

10 thms1 active userReviewed

Machine Learning Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 6: The Expected Maximum Discrepancy Lies Between R_n(F)/2 − 2√(2/n) and R_n(F) + 4√(2/n)Research Paper

Motivation

Data-dependent risk bounds in statistical learning theory control the gap between the expected loss of a learned function and its empirical loss by a complexity penalty that is computed from the training data. The first such penalties were the maximum discrepancy of a function class (Bartlett, Boucheron and Lugosi, Model selection and error estimation, Machine Learning 48, 2002) and its Rademacher complexity (Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Trans. Inf. Theory 47, 2001; Koltchinskii and Panchenko 2000). The maximum discrepancy compares the behaviour of the class on two fixed halves of the sample; the Rademacher complexity compares it on two random halves. Bartlett and Mendelson (JMLR 3, 2002), Lemma 3, show that these two quantities are equivalent up to a factor 2 and an additive $O(1/\sqrt n)$ . This mission formalizes that lemma from the published JMLR article (pp. 463–482); the proof is its Appendix A.

Setting

Let $\mu$ be a probability measure on a measurable space $\mathcal X$ and let $X_1,\dots,X_n$ be independent samples from $\mu$ . Let $F$ be a class of measurable functions $f:\mathcal X\to[-1,1]$ . Let $\sigma_1,\dots,\sigma_n$ be independent uniform $\{\pm1\}$ -valued random variables, independent of the sample.

The Rademacher complexity of $F$ is

R_n(F) = \mathbf E\sup_{f\in F}\left|\frac2n\sum_{i=1}^n\sigma_i f(X_i)\right|.

For even $n$ , the maximum discrepancy of $F$ is the random variable

\hat D_n(F) = \sup_{f\in F}\left(\frac2n\sum_{i=1}^{n/2}f(X_i) - \frac2n\sum_{i=n/2+1}^n f(X_i)\right),

with no absolute value, and the expected maximum discrepancy is $D_n(F)=\mathbf E\hat D_n(F)$ . The class is closed under negation if $f\in F$ implies $-f\in F$ , and $-F=\{-f:f\in F\}$ .

The proof works with the conditional supremum function

s(N) = \frac2n\,\mathbf E\left[\sup_{f\in F}\sum_{i=1}^n\sigma_i f(X_i)\;\middle|\;\sum_{i=1}^n\sigma_i=N\right],

defined for the values $N$ that $\sum_i\sigma_i$ can take.

Formalization targets

Goal: Lemma 3, first and second displays

For every even $n\ge2$ ,

\frac{R_n(F)}{2} - 2\sqrt{\frac2n} \le D_n(F) \le R_n(F) + 4\sqrt{\frac2n},

and if $F$ is closed under negation,

R_n(F) - 4\sqrt{\frac2n} \le D_n(F).

Milestones (Appendix A, pp. 479–480)

$R_n(F)\ge\mathbf E\,s(\sum_i\sigma_i)$ , with equality when $F$ is closed under negation.
$D_n(F) = s(0)$ .
$|s(N_1)-s(N_2)|\le 4|N_2-N_1|/n$ .
$|\mathbf E s(N)-s(\mathbf EN)|\le\mathbf E|s(N)-s(\mathbf EN)|\le4\sqrt{2/n}$ for $N=\sum_i\sigma_i$ .
$R_n(F)=R_n(F\cup-F)\le D_n(F\cup-F)+4\sqrt{2/n}$ .
$D_n(F\cup-F)\le 2D_n(F)+D_n(\{f_0,-f_0\})$ for any $f_0\in F$ (a corrected form of the printed step, see below).

Significance

Lemma 3 makes the maximum discrepancy and the Rademacher complexity interchangeable in risk bounds: a bound in terms of one gives a bound in terms of the other with an explicit additive loss. The maximum discrepancy can be computed by a single empirical risk minimization on a relabelled sample, while the Rademacher complexity has the structural properties (monotonicity, convex-hull invariance, contraction) that make it easy to bound for concrete classes; the lemma transfers the second kind of estimate to the first quantity.

The lemma is proved in the paper; no machine-checked proof of it, or of the comparison between fixed and random half-sample splits, is known to exist. Formalizing it requires the exchangeability argument for i.i.d. samples, the conditioning of a uniform sign vector on its sum, and a moment bound for the Rademacher sum $\sum_i\sigma_i$ , all with explicit constants.

Difficulty

The heart of the proof is that, conditioned on the number of positive signs, a uniform sign vector splits the i.i.d. sample into two random subsets of fixed sizes, and every split of the same sizes has the same law as the fixed split. Making this precise requires a permutation-invariance argument for product measures applied to a supremum over an arbitrary class, where measurability is not automatic. The step from classes closed under negation to general classes is where the printed argument is loose: since $\hat D_n$ has no absolute value, $\hat D_n(F\cup-F)$ is a maximum of two suprema that may be negative, and the naive bound $D_n(F\cup-F)\le2D_n(F)$ fails.

Formalization scope

The Lean development lives in the namespace RadGauss.Discrepancy. Sign vectors are Fin n → Bool (true ↦ 1, false ↦ -1) and expectations over signs are finite averages over all $2^n$ sign vectors; $s(N)$ is the average over the sign vectors with sum $N$ . $R_n$ takes values in $[0,\infty]$ (a lower Lebesgue integral of an $[0,\infty]$ -valued supremum), while $\hat D_n$ , $D_n$ and $s$ are real, because the maximum discrepancy is signed. Inequalities of the form $a-c\le D$ are written $a\le D+c$ with real terms embedded by ENNReal.ofReal; this is equivalent to the printed form since $D_n(F)\ge0$ for nonempty $F$ .

Hypotheses added to the page, all disclosed in each item:

the sample size is even, $n=2m$ with $m\ge1$ , since $\hat D_n$ needs half sums;
$F$ is nonempty (the supremum over the empty class is $-\infty$ in the paper and $0$ in Lean);
every $f\in F$ is measurable, and for every sign vector $\sigma$ the map $x\mapsto\sup_{f\in F}\sum_i\sigma_if(x_i)$ is measurable. This is the measurability guard: without it the Bochner integrals defining $D_n$ and $s$ would silently be $0$ .

Corrections of printed statements:

The Lipschitz bound on $s$ is printed for $0\le n_2<n_1\le n$ but used for negative values of $\sum_i\sigma_i$ ; it is stated for every pair of attainable values.
The printed step $D_n(F\cup-F)\le2D_n(F)$ is false for the signed $\hat D_n$ of p. 464 ( $F=\{f\}$ , $f(X)$ uniform on $\{\pm1\}$ , $n=2$ gives $1\le0$ ); the milestone states it with the additional term $D_n(\{f_0,-f_0\})\le2/\sqrt n$ . The goal itself remains true.
The third display of Lemma 3, $P\{|\hat D_n(F)-D_n(F)|\ge\epsilon\}\le2\exp(-\epsilon^2n/2)$ , is false as printed ( $F=\{f\}$ as above, $n=2$ , $\epsilon=2$ : the probability is $1/2>2e^{-4}$ ) and is not part of the mission.

A formalization in which $D_n$ or $s$ is a junk value (non-integrable or non-measurable suprema, an empty class, an odd sample size with truncated $n/2$ ) would make the goal trivial or meaningless; the hypotheses above rule that out, and the class $F=\{0\}$ satisfies all of them.

Welcome contributions include general lemmas on the invariance of $\mathbf E\sup_{f\in F}\Phi_f(X_{\pi(1)},\dots,X_{\pi(n)})$ under permutations $\pi$ of an i.i.d. sample, conditioning of uniform sign vectors on their sum, and the bound $\mathbf E|\sum_i\sigma_i|\le\sqrt n$ . These are reusable well beyond this mission.

Selected references

P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47 (2001) 1902–1914. https://doi.org/10.1109/18.930926
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

10 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3 (p. 134)

If the protection levels satisfy

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

then $p$ is optimal.

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

8 thms1 active userReviewed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Proposition 5

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

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

Milestones, in proof order

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

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

Significance

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

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

15 thms1 active userReviewed

Probability

Missions

Kelly's Criterion: the optimal fraction for an even-money betResearch Paper

Motivation

Setting

What is being asked

Source

Bochner's Theorem: Positive-Definite FunctionsTextbook

Motivation

Setting

Formalization targets

Goal — Bochner's theorem, general case

Milestone — Bochner's theorem, L¹ (density) case

Significance

Difficulty

Formalization scope

Selected references

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: the probabilistic lower bound

Stronger: the three steps of the proof, as separate targets

Significance

Difficulty

Formalization scope

Selected references

Context: where this sits in the formalization landscape

Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times XIII: Coupling from the PastTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times II: The Convergence TheoremTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Why throughput matters

Network and allocations

Formalization targets

What the result gives

Why the proof is difficult

Formalization scope

Selected references

Optimality and Duality Theory for Stochastic Optimization Problems with Nonlinear Dominance Constraints 1: Under Uniform Dominance, Optimal Solutions Have Concave Utility and L∞ MultipliersResearch Paper

Motivation

Setting

Formalization targets

Utility and bounded multiplier characterization

Significance

Milestone — Bochner's theorem, `L¹` (density) case

Goal: Theorem 1, $1<b<+\infty$