All missions

Motivation

A convex program is useful in practice only if its optimal value responds reasonably to small changes in the data. Lagrangian and Fenchel duality theory makes this precise: the dual problem attains its optimum and has no duality gap exactly when the primal value function does not fall off infinitely steeply under small perturbations. A constraint qualification is a checkable condition on the data that guarantees this good behaviour; Slater's condition (a strictly feasible point) is the best-known example in finite dimensions.

R. T. Rockafellar's 1967 paper Duality and Stability in Extremum Problems Involving Convex Functions (Pacific J. Math. 21 (1967) 167–187) develops Fenchel-type duality for the problem of minimizing $f(x) - g(Ax)$ in general locally convex spaces. It introduces the notion of a stably set problem, shows that stability is equivalent to strong duality with an attained dual optimum (its Theorem 3), and gives in Theorem 1 a general sufficient condition for stability. Theorem 1 is the infinite-dimensional analogue of Slater's condition and is the form in which the result is usually applied: one exhibits a single point where $f$ is finite and $g$ is finite and continuous.

Timeline. Fenchel (1951) proved the duality theorem for $A = I$ in $\mathbb{R}^n$ under relative-interior conditions. Brøndsted (1964) and Moreau (1966–67) extended conjugate duality to paired locally convex spaces. Rockafellar's 1967 paper (this mission) added the linear map $A$, the perturbation function $h$, the notion of stability, and Theorem 1. The perturbational approach was later systematized in Rockafellar's Conjugate Duality and Optimization (SIAM, 1974).

Setting

Let $E$ and $F$ be real locally convex Hausdorff topological vector spaces and $A : E \to F$ a continuous linear map. Let $f : E \to [-\infty, +\infty]$ and $g : F \to [-\infty, +\infty]$.

• $f$ is convex if its epigraph $\{(x, \mu) \mid x \in E, \mu \in \mathbb{R}, \mu \ge f(x)\}$ is a convex subset of $E \times \mathbb{R}$; it is proper if $f(x) > -\infty$ for all $x$ and $f(x) < +\infty$ for some $x$. $g$ is concave if $-g$ is convex, and proper concave if $g < +\infty$ everywhere and $g > -\infty$ somewhere.
• Throughout, $f$ is lower semicontinuous proper convex and $g$ is upper semicontinuous proper concave. Their effective domains are $C = \{x \mid f(x) < +\infty\}$ and $D = \{y \mid g(y) > -\infty\}$.
• The primal problem is

$$(P) \qquad \text{minimize } f(x) - g(Ax) \text{ over } x \in E,$$

and its perturbations are $(P(z))$: minimize $f(x) - g(Ax - z)$, for $z \in F$. The perturbation function is $h(z) = \inf (P(z)) = \inf_x \{ f(x) - g(Ax - z) \} \in [-\infty, +\infty]$, so $h(0) = \inf (P)$. $(P)$ is consistent if $h(0) < +\infty$.

• When $h(0)$ is finite, the directional derivative is $h'(0; z) = \lim_{\varepsilon \downarrow 0} [h(\varepsilon z) - h(0)]/\varepsilon$.
• $(P)$ is unstably set if $h(0)$ is finite and every neighbourhood of $0$ contains vectors $z$ with $h'(0; z)$ a negative number of arbitrarily large magnitude ($-\infty$ included). $(P)$ is stably set if it is consistent but not unstably set.

Formalization targets

Goal: Theorem 1 (p. 175)

Suppose there exists $x \in E$ such that $f$ is finite at $x$ and $g$ is finite and continuous at $Ax$. Then

$$(P) \text{ is stably set} \quad\text{and}\quad \text{there is a neighbourhood } U \text{ of } 0 \text{ on which } z \mapsto \inf (P(z)) \text{ is continuous}.$$

The neighbourhood $U$ is left unspecified, as in the paper.

Milestones (in the order the proof uses them)

1. (4.4) $\{z \mid h(z) < +\infty\} = \{Ax - y \mid f(x) < +\infty,\ g(y) > -\infty\} = A(C) - D$.
2. (4.5) $A(C)$ meets $\operatorname{int} D$, and $0 \in A(C) - \operatorname{int} D \subseteq \operatorname{int}(A(C) - D)$.
3. Epigraph of $h$ has interior (p. 176): the hypograph $G = \{(y, \mu) \mid g(y) \ge \mu > -\infty\}$ has nonempty interior, $(Ax, \lambda) - G$ lies in the epigraph of $h$ for every $(x, \lambda)$ in the epigraph of $f$, and so the epigraph of $h$ has nonempty interior.
4. Continuity on the interior of the domain (p. 176): $0 \in \operatorname{int}\{h < +\infty\}$ and $h$ is continuous there.
5. (4.6) For a convex $h$ with $h(0)$ finite: $h(z) \ge h(0) + h'(0; z)$ and $h'(0; z) \ge -h'(0; -z)$ for all $z$.

Significance

The result. Combined with the paper's Theorem 3, Theorem 1 yields: if $f$ is finite at some $x$ where $g$ is finite and continuous at $Ax$, then $\inf (P) = \max (P^*)$, with the dual maximum attained. This is the standard sufficient condition for Fenchel–Rockafellar duality in infinite dimensions, used in calculus of variations, optimal control, and the convex analysis of integral functionals. The continuity half of Theorem 1 says that the optimal value depends continuously on translations of the constraint data near the unperturbed problem, a basic sensitivity statement.

Formalizing it. The theorem is proved (1967) and appears in many textbooks, but there is no machine-checked version on this platform. Mathlib contains continuity criteria for real-valued convex functions on open sets of normed or finite-dimensional spaces (ConvexOn.continuousOn_tfae, ConvexOn.continuousOn_interior), but nothing for extended-real-valued convex functions on general topological vector spaces, no perturbation function, and no notion of a stably set problem. A complete development would provide reusable infrastructure: the epigraph-interior continuity criterion for $[-\infty, +\infty]$-valued convex functions and the elementary calculus of one-sided directional derivatives.

Difficulty

The obvious argument says: $g$ is continuous at $Ax$, so $h(z) \le f(x) - g(Ax - z)$ is bounded above near $0$, hence $h$ is continuous at $0$ and its directional derivatives are bounded. Two steps of this fail without care. First, the passage from "bounded above near a point" to "continuous" requires convexity of $h$ (Lemma 2 of the paper, proved in the companion mission) and a continuity criterion valid in an arbitrary topological vector space, with values in $[-\infty, +\infty]$; the normed-space proofs in Mathlib do not apply. Second, $h$ may take the value $-\infty$, and the derivative may be $-\infty$ in some directions; the bookkeeping of extended-real arithmetic (where $(+\infty) + (-\infty)$ is not defined mathematically and is given a junk value in Lean) has to be done honestly. Finally, upper bounds on $h'(0;\cdot)$ must be converted into lower bounds, which is where the second inequality of (4.6) enters; an upper bound alone does not give stability.

Formalization scope

All values are in Lean's EReal. Convexity is convexity of the epigraph with real second coordinate (the paper's definition, p. 170); concavity is convexity of $-g$. Properness is stated as in the paper. The perturbation function is the EReal infimum ⨅ x, f x - g (A x - z); under properness the undefined form $(+\infty) - (+\infty)$ never arises. The directional derivative (4.3) is the lower limit of the difference quotient along $\varepsilon \to 0^+$, which equals the paper's limit whenever it exists (always, for convex $h$ with $h(0)$ finite). "Unstably set" quantifies over all neighbourhoods of $0$ and all real $M$, with $h'(0;z) < -M$ allowing $-\infty$. "Stably set" is $h(0) < +\infty$ together with "not unstably set", so $\inf (P) = -\infty$ is stably set, as the paper says on p. 176. Continuity is with respect to the order topology of EReal, and "continuous at $Ax$" is continuity of $g$ itself at that point, not of its restriction to $D$.

The paper's standing setting (§3) includes dual spaces $E^*, F^*$, the adjoint $A^*$ and the conjugates $f^*, g^*$. Neither Theorem 1 nor its proof uses them, so they are omitted and the theorem is stated for every pair of real locally convex Hausdorff spaces, which includes every paired setting. The lower and upper semicontinuity of $f$ and $g$ are standing hypotheses of the paper and are kept, although the proof does not use them. Inequality (4.6) is stated for an arbitrary convex function finite at $0$, the generality in which the paper invokes it. No statement was repaired.

A definition of "stably set" that already presumed finiteness or continuity of $h$ near $0$, or that tested the derivative only in a fixed set of directions, would make the first conclusion of Theorem 1 trivial; the definition used here is the paper's p. 175 definition verbatim, applied to an arbitrary function $h$. The definitions are local to this mission; the companion missions on Theorem 3 and Theorem 6 of the same paper define the same objects in their own namespaces. Contributions are welcome on the milestones in any order, and in particular on a general continuity criterion for extended-real-valued convex functions on topological vector spaces, which is reusable well beyond this mission.

Selected references

• R. T. Rockafellar, Duality and stability in extremum problems involving convex functions, Pacific J. Math. 21 (1967) 167–187. https://doi.org/10.2140/pjm.1967.21.167
• A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964), no. 2.
• W. Fenchel, Convex Cones, Sets and Functions, lecture notes, Princeton University, 1951.
• J. J. Moreau, Fonctionnelles convexes, Séminaire Leray, Collège de France, 1966–67.
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524

Motivation

Bin packing asks for the minimum number of unit-capacity bins into which a list of items with sizes in $[0,1]$ can be packed. It is one of the basic NP-hard problems of combinatorial optimization and operations research, and its stochastic version, where the item sizes are random, has a large literature (Coffman and Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, 1991). A first question about the random optimum is how strongly it concentrates around its typical value.

A short history of that question, as Talagrand recounts it on p. 151 of the source:

• Late 1980s. Martingale methods (Rhee–Talagrand; McDiarmid, On the method of bounded differences, 1989) give $P(|B_N - \mathbb E B_N| \ge t) \le 2\exp(-2t^2/N)$ for $N$ i.i.d. items. The exponent ignores the item sizes.
• 1994. Since $B_N$ behaves like $\sum_i X_i$ when the items are small, the right exponent should be of order $t^2/(N\operatorname{var} X_1)$, or at least $t^2/(N\,\mathbb E X_1^2)$. The second form was proved by W. Rhee (Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385) using non-trivial bin-packing theory.
• 1995. Talagrand (Publ. Math. IHÉS 81, Chapter 6) derives the $t^2/(N\,\mathbb E X_1^2)$ bound in a few lines from his convex hull distance inequality, using only trivial facts about bin packing.

This mission formalizes that chapter.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$. A point $x = (x_1,\dots,x_N) \in \Omega^N$ is a list of item sizes. A packing into $k$ bins is a map $\sigma : \{1,\dots,N\} \to \{1,\dots,k\}$ with $\sum_{i:\sigma(i)=j} x_i \le 1$ for every bin $j$. The bin packing number $B_N(x)$ is the least $k$ for which a packing exists ($N$ bins always suffice; $B_N = 0$ when $N = 0$).

Further notation, as in Lean (TalagrandConc.BinPacking):

• $\|x\|_2 = (\sum_{i \le N} x_i^2)^{1/2}$ (l2Norm);
• for real $a$, the level set $A(a) = \{y \in \Omega^N : B_N(y) \le a\}$ (levelSet);
• for $A \subseteq \Omega^N$ and $x \in \Omega^N$, $U_A(x) = \{s \in \{0,1\}^N : \exists y \in A,\ s_i = 0 \Rightarrow x_i = y_i\}$, its convex hull $V_A(x) \subseteq \mathbb R^N$, and the convex hull distance $f_c(A,x)$, the Euclidean distance from $0$ to $V_A(x)$, valued in $[0,+\infty]$ (U, V, convexDist);
• $\mu$ a probability measure on $[0,1]$, $P = \mu^{\otimes N}$ the product probability on $[0,1]^N$, whose coordinates $X_1,\dots,X_N$ are i.i.d. items with law $\mu$, and $\mathbb E X_1^2 = \int \omega^2\,d\mu(\omega)$ (secondMoment);
• $M$ is a median of $B_N$ if $P(B_N \le M) \ge 1/2$ and $P(B_N \ge M) \ge 1/2$ (IsMedian).

Formalization targets

Goal: Theorem 6.5 (p. 152)

For every median $M$ of $B_N$ and every $u$ with $0 \le u \le 8\sqrt2\,N\,\mathbb E X_1^2$,

$$P\big(|B_N(X_1,\dots,X_N) - M| \ge 1 + u\big) \le 8\exp\Big(-\frac{u^2}{64\,N\,\mathbb E X_1^2}\Big).$$

Milestones

1. Lemma 6.1 (p. 151): $B_N(x_1,\dots,x_N) \le 2\sum_{i\le N} x_i + 1$.
2. Lemma 6.2, Eq. (6.2) (p. 151): for $a > 0$ and all $x$, $B_N(x) \le a + 2\|x\|_2\, f_c(A(a),x) + 1$.
3. Lemma 6.3, Eq. (6.3) (p. 152): $P(\|x\|_2 \ge 2\sqrt N(\mathbb E X_1^2)^{1/2}) \le \exp(-2N\,\mathbb E X_1^2)$.
4. Proposition 6.4, Eq. (6.4) (p. 152): for all $t > 0$, $a > 0$,

$$P(B_N \le a)\,P\big(B_N \ge a + 4t\sqrt N(\mathbb E X_1^2)^{1/2} + 1\big) \le e^{-t^2/4} + e^{-2N\,\mathbb E X_1^2}.$$

The goal keeps the paper's explicit constants $8$, $64$ and $8\sqrt2$.

Significance

The result. Theorem 6.5 shows that the random optimum $B_N$ fluctuates on the scale $\sqrt{N\,\mathbb E X_1^2}$ rather than $\sqrt N$. For small items ($\mathbb E X_1^2 \to 0$) this is much sharper than the martingale bound, and it is the scale of the fluctuations of $\sum_i X_i$, which is a lower bound on $B_N$. Chapter 6 is also the first application in Part II of the paper, and its scheme recurs in the later chapters: a deterministic lemma relating the functional to $f_c$ of a level set, a tail bound for an auxiliary factor, and Theorem 4.1.1 to finish.

Formalizing it. The result is proved (Talagrand 1995; Rhee 1994 by another route). No machine-checked proof is known to exist: the platform has no random bin packing statement and no general-$\Omega$ form of Talagrand's convex distance inequality. A complete development gives a checked concentration bound for an NP-hard combinatorial optimum, plus a bin-packing layer (the optimum as a minimum over assignments, Lemma 6.1, monotonicity in the item set) that other formalizations can reuse.

Difficulty

The obvious route is a bounded-differences argument: changing one item changes $B_N$ by at most one. That route yields only the exponent $t^2/N$, because it cannot see that small items change little. Replacing the Hamming geometry by one weighted by item sizes is the point. The weights $x_i$ depend on the point $x$ itself, so no fixed weighted Hamming distance works. The convex hull distance $f_c$ controls every weighting at once, and the resulting factor $\|x\|_2$ is random and must be controlled separately (Lemma 6.3). In Lean, the further difficulty is the probabilistic input: Theorem 4.1.1 / Eq. (4.1.2) for a general (non-finite) $\Omega = [0,1]$ is not available, and the convex-hull minimax step (Lemma 4.1.2) behind Lemma 6.2 must be formalized too.

Formalization scope

• $\Omega = [0,1]$ is Mathlib's unitInterval. Coordinates are Fin N (0-based). $P$ is Measure.pi (fun _ : Fin N => μ) for μ : Measure unitInterval with IsProbabilityMeasure μ. No density is assumed.
• $B_N$ is sInf {k : ℕ | IsPacking x k}, an exact minimum over assignments Fin N → Fin k, not a heuristic such as First Fit. Zero-size items are allowed, as in the paper.
• $f_c$ is an infimum in ℝ≥0∞ with the Euclidean norm written out ($+\infty$ for an empty set; Mathlib's default norm on Fin N → ℝ is the sup norm). Lemma 6.2 is stated in ℝ≥0∞.
• Probabilities are ℝ≥0∞-valued. Every event in the statements ($\{B_N \le a\}$, $\{\|x\|_2 \ge c\}$) is Borel. The paper's measurability convention matters only inside the proofs.
• Theorem 6.5 makes the paper's implicit $u \ge 0$ explicit, and it is stated for every median, not for a chosen one. Lean's $u^2/0 = 0$ matters only in the degenerate case $N\,\mathbb E X_1^2 = 0$, which forces $u = 0$. There the bound is $8$.
• Not admissible: weakening the range of $u$ (the bound fails for large $u$ when $\mathbb E X_1^2$ is small), replacing $\mathbb E X_1^2$ by $1$, or defining $B_N$ through a heuristic or a real-valued sInf.
• Infrastructure needed: Talagrand's inequality (4.1.2) on a general product probability space (posed on the platform only in a finite-alphabet form) and Lemma 4.1.2. Both are welcome as separate contributions. A Chebyshev/exponential-moment bound gives Lemma 6.3.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 6, pp. 151–152. https://doi.org/10.1007/BF02699376
• W. Rhee, Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385.
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, LMS Lecture Note Series 141, Cambridge Univ. Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
• E. G. Coffman Jr., G. S. Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, Wiley, 1991.

Motivation

In convex optimization, a dual problem supplies a bound on what a primal minimization problem can achieve. The bound can be useful even when no minimizer is known, but an equality of the primal and dual values says more: it certifies that the bound is exact. In applications, one also wants a dual variable that actually attains the bound, since that variable can act as a multiplier or a sensitivity certificate. Rockafellar's 1967 paper asks when such an attained equality follows from the behavior of the primal value under small changes to the problem Rockafellar 1967.

The paper works with locally convex spaces paired with their continuous duals, rather than limiting the question to finite-dimensional vectors or normed spaces. In this setting, ordinary finite-dimensional constraint qualifications need not describe the relevant behavior. Theorem 3 gives a criterion in terms of the perturbation function itself. It also states the corresponding criterion with the primal and dual roles reversed Rockafellar 1967, §5.

Setting

Let $E$ and $E'$ be real locally convex Hausdorff spaces in topological duality, with pairing $\langle x,x'\rangle_E$. Let $F$ and $F'$ be another such pair. Each pairing represents every continuous linear functional on either member uniquely by a point of the other member. Let $A:E\to F$ be continuous linear, and let its continuous adjoint $A^*:F'\to E'$ satisfy $\langle Ax,y'\rangle_F=\langle x,A^*y'\rangle_E$.

The primal data are a lower semicontinuous proper convex function $f:E\to[-\infty,+\infty]$ and an upper semicontinuous proper concave function $g:F\to[-\infty,+\infty]$. Here proper means that $f$ never takes $-\infty$ and is finite somewhere, while $g$ never takes $+\infty$ and is finite somewhere. Convexity means convexity of the real epigraph, and concavity means convexity of $-g$. Their conjugates are $f^*(x')=\sup_x(\langle x,x'\rangle_E-f(x))$ and $g^*(y')=\inf_y(\langle y,y'\rangle_F-g(y))$ Rockafellar 1967, §2.

The primal problem $(P)$ minimizes $f(x)-g(Ax)$ over $E$. Its dual $(P^*)$ maximizes $g^*(y')-f^*(A^*y')$ over $F'$. A translation $z\in F$ changes the primal objective to $f(x)-g(Ax-z)$, giving

$$h(z)=\inf_{x\in E}\{f(x)-g(Ax-z)\},\qquad h(0)=\inf(P).$$

The primal problem is stably set when it is consistent, meaning $h(0)<+\infty$, and when directional rates of change of $h$ at zero cannot be arbitrarily negative in every neighborhood of zero. The instability test is made only when $h(0)$ is finite. Consequently $h(0)=-\infty$ counts as stable, as the paper explicitly observes Rockafellar 1967, §4–5. The dual stability condition is the same definition applied to the dual's minimization form $(P')$, with perturbations in $E'$.

Formalization targets

The goal is both directions of Theorem 3, including the dual statement:

$$(P)\text{ stably set}\quad\Longleftrightarrow\quad \inf(P)=\max(P^*),$$ $$\min(P)=\sup(P^*)\quad\Longleftrightarrow\quad (P^*)\text{ stably set}.$$

The symbols $\max$ and $\min$ assert that the stated value is attained. A statement equating only an infimum and a supremum would omit part of the theorem. The mission's milestones are the convexity of $h$ (Lemma 2), the equivalence between stability and a nonempty subdifferential $\partial h(0)$, the criterion linking a subgradient to inequality (5.1), and weak duality (Lemma 1). Each is a claim stated in the paper's proof or as a numbered lemma Rockafellar 1967, pp. 174, 178–179.

Significance

The theorem turns a local property of the optimal-value function into an exact, attained duality statement. A dual optimum has operational meaning: its point $y'\in F'$ is a continuous linear response to perturbations $z\in F$, expressed through $\langle z,y'\rangle_F$. The converse says that attained exact duality already forces the same stability property. The dual half adds a symmetric criterion for attainment of the primal minimum Rockafellar 1967, Theorem 3.

The 1967 result is proved in the cited paper; this mission asks for its Lean formalization. A complete development would give reusable definitions for paired locally convex spaces, extended-real conjugates, epigraph convexity, and perturbation-based stability. The milestone statements expose the intermediate mathematical claims separately, so later formalizations can use the parts they need without importing the entire theorem.

Difficulty

Weak duality by itself gives only an inequality. It does not supply a dual point achieving the primal infimum, and equality of two extended-real lattice values does not establish attainment. The central issue is that a perturbation function can have a finite value at zero yet fall at arbitrarily steep rates in nearby directions; then no continuous linear support at zero need exist. Infinite primal values bring two additional cases: inconsistency when $h(0)=+\infty$, and the paper's stable case when $h(0)=-\infty$. The dual half requires the topology on $E'$ because the translated dual problem is perturbed there Rockafellar 1967, §§4–5.

Formalization scope

The Lean representation uses EReal for all objective and conjugate values; its complete lattice gives the paper's $\pm\infty$ values for unbounded or empty extrema. Spaces are arbitrary locally convex Hausdorff real topological vector spaces equipped with a pairing that identifies each space with the continuous linear dual of the other. The adjoint is continuous linear data constrained by the pairing identity. Properness rules out endpoint arithmetic of the form $+\infty-(+\infty)$ in the primal and dual objectives. The conjugates are defined from $f$ and $g$; their regularity is not assumed separately.

Stability is encoded using the positive one-sided lower limit of directional difference quotients, which equals the paper's limit for convex $h$. It requires consistency and excludes arbitrarily negative rates in every neighborhood. It is not defined by $\partial h(0)\ne\varnothing$: that equivalence is an independent milestone. Attained extrema are represented by greatest and least elements of the ranges of the objective functions, rather than by equality of lattice values alone. The formalization includes both halves of Theorem 3 and all four listed milestones. Contributions toward general convex analysis on paired spaces and toward the extended-real endpoint cases are useful beyond this mission.

Selected references

• R. T. Rockafellar, Duality and Stability in Extremum Problems Involving Convex Functions, Pacific Journal of Mathematics 21 (1967), 167–187. DOI: 10.2140/pjm.1967.21.167.

Motivation

A product probability space $(\Omega^N, P)$, $P=\mu^{\otimes N}$, concentrates its mass: a set $A$ of non-negligible measure is "close" to most points. How closeness is measured decides what the statement can be used for. The Hamming distance (Chapter 2 of the paper) counts coordinates in which a point differs from $A$; it gives Gaussian concentration, but only for functions that are Lipschitz for one fixed weighting of the coordinates. Chapter 4 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), introduces the convex hull distance, which controls every weighted Hamming distance at once with weights chosen after seeing the point. This one inequality is what the second half of the paper uses for the longest increasing subsequence, bin packing, suprema of linear forms, the chromatic number of random graphs, the random assignment problem and the travelling salesman problem, and it is the form in which "Talagrand's inequality" is usually quoted in probability and combinatorics.

History (paper, p. 125). The author first proved the deviation inequality of Theorem 13.2 of the paper for symmetric $\pm1$ variables; W. B. Johnson and G. Schechtman extended it, and their one-dimensional lemma (Lemma 4.1.3 here) led to the abstract setting of Theorem 4.1.1. Section 4.2 sharpens the exponent $1/4$ by replacing $f_c^2/4$ with an exactly optimised penalty $f_\alpha$.

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer and $P=\mu^{\otimes N}$ on $\Omega^N$. For $A\subseteq\Omega^N$ and $x\in\Omega^N$ let

$$U_A(x)=\{(s_i)_{i\le N}\in\{0,1\}^N;\ \exists y\in A,\ s_i=0\Rightarrow x_i=y_i\},$$

the set of $0$–$1$ vectors marking a superset of the coordinates in which $x$ differs from some point of $A$. Let $V_A(x)$ be its convex hull in $\mathbb R^N$; it contains $0$ exactly when $x\in A$. The convex hull distance $f_c(A,x)$ is the Euclidean distance from $0$ to $V_A(x)$, and the enlargement of $A$ is

$$A_t^c=\{x\in\Omega^N;\ f_c(A,x)\le t\}$$

(the superscript $c$ stands for "convexity", not for a complement). For $\alpha\ge0$ and $u\in[0,1]$ put

$$\xi(\alpha,u)=\alpha(1-u)\log(1-u)-(\alpha+1-\alpha u)\log\Big(\frac{1+\alpha-\alpha u}{1+\alpha}\Big),$$

and let $f_\alpha(A,x)=\inf\{\sum_{i\le N}\xi(\alpha,s_i);\ s\in V_A(x)\}$; it plays the role of $f_c^2(A,x)$.

Formalization targets

Goal: Theorem 4.2.4

For $\alpha>0$ and every $A\subseteq\Omega^N$,

$$\int\exp f_\alpha(A,x)\,dP(x)\le\frac{1}{P(A)^{\alpha}}.$$

The constant is exact (no unspecified constants), and the statement holds for every probability space $\Omega$ and every $N$.

Milestones

• Lemma 4.1.2: $x\in A_t^c$ iff for every real $(\alpha_i)$ some $y\in A$ has $\sum\{\alpha_i;\ x_i\ne y_i\}\le t(\sum\alpha_i^2)^{1/2}$.
• Lemma 4.1.3: $\inf_{0\le\lambda\le1}r^{-\lambda}\exp\frac{(1-\lambda)^2}{4}\le2-r$ for $0\le r\le1$.
• Lemma 4.2.1: $\inf_{0\le\lambda\le1}r^{-\lambda\alpha}\exp\xi(\alpha,1-\lambda)=1+\alpha-\alpha r$ for $0<r<1$.
• Lemma 4.2.2: $\xi(\alpha,\cdot)$ is increasing and convex on $[0,1]$ and $\xi(\alpha,u)\ge\frac{\alpha}{2(\alpha+1)}u^2$.
• Lemma 4.2.3: $1+\alpha-\alpha a\le a^{-\alpha}$ and $a+(1-a)\exp\xi(\alpha,1)\le a^{-\alpha}$.
• Eq. (4.2.6): $P(A_t^c)\ge1-P(A)^{-\alpha}\exp\big(-\frac{\alpha t^2}{2(\alpha+1)}\big)$.
• Corollary 4.2.5: for $t\ge\sqrt{2\log(1/P(A))}$, $P(A_t^c)\ge1-\exp\big(-\frac12(t-\sqrt{2\log(1/P(A))})^2\big)$.
• Theorem 4.3.1 (two-point space, uniform $\mu$, $\alpha\ge1$): $\int\exp\big(\frac{\alpha}{\alpha+1}f_c^2(A,x)\big)\,dP(x)\le P(A)^{-\alpha}$.

Significance

The result. At $\alpha=1$, Lemma 4.2.2 gives $\xi(1,u)\ge u^2/4$, so the goal contains Theorem 4.1.1,

$$\int\exp\tfrac14f_c^2(A,x)\,dP(x)\le\frac1{P(A)},\qquad P(A_t^c)\ge1-\frac1{P(A)}e^{-t^2/4},$$

the convex distance inequality itself. For general $\alpha$ it improves the coefficient of $t^2$ from $1/4$ to the optimal $1/2$ (Corollary 4.2.5), and since $\xi(\alpha,1)=\log(1+\alpha)$ grows with $\alpha$, it simultaneously controls the number of coordinates in which $x$ must be changed to reach $A$, recovering features of the $q$-point inequalities of Chapter 3. Every Part II application of the paper rests on Theorem 4.1.1 or on this sharpening.

Formalizing it. All results here are proved in the paper (the goal's proof is "an obvious adaptation" of that of Theorem 4.1.1, by induction on $N$). None of them has a machine-checked proof for a general probability space. Theorem 4.1.1 itself is posed on the platform, still open, for finite alphabets and finite sets (Talagrand.Eexp_mul_mass_le_one, Talagrand.mass_mul_mass_le_exp); it is not posed again here. A proof of the goal settles it for arbitrary $\Omega$ and arbitrary measurable $A$.

Difficulty

The function $x\mapsto f_\alpha(A,x)$ is not a sum of one-coordinate terms, so no tensorization of a one-dimensional inequality applies directly. Bounding $f_\alpha(A,x)$ pointwise by the distance to a single nearby point of $A$ gives only Hamming-type bounds with a fixed weighting, which is exactly what the convex hull distance is designed to beat; the inequality has to hold for the infimum over the whole hull. The one-coordinate estimate the paper uses is the exact identity of Lemma 4.2.1, which leaves no slack. A further obstacle is analytic: $V_A(x)$ is a convex hull in $\mathbb R^N$ of a set indexed by the possibly uncountable set $A$, and its infima must be compared across dimensions $N$ and $N+1$.

Formalization scope

• $\Omega^N$ is Fin N → Ω; $P$ is Measure.pi (fun _ : Fin N => μ) with IsProbabilityMeasure μ.
• $U_A(x)$ is a set of Fin N → ℝ with values in $\{0,1\}$; $V_A(x)$ is convexHull ℝ (U A x). The $\ell^2$ norm is written out as $\sqrt{\sum_i s_i^2}$: Mathlib's norm on Fin N → ℝ is the sup norm.
• $f_c$ and $f_\alpha$ take values in $[0,\infty]$ (ℝ≥0∞); both are $+\infty$ when $A=\varnothing$. $\exp(+\infty)=+\infty$ (EReal.exp), $P(A)^{-\alpha}=+\infty$ when $P(A)=0$. No real-valued infimum or Bochner integral is used, so no junk value can make a bound hold for free.
• $\xi(\alpha,1)=\log(1+\alpha)$ relies on $0\cdot\log0=0$, which Mathlib's Real.log 0 = 0 provides.
• Measurability. The paper ignores measurability (pp. 81–82). Here $A$ and $x\mapsto f_\alpha(A,x)$ are assumed measurable (explicit hypotheses), integrals are ∫⁻, and $P(A_t^c)$ is the measure of an arbitrary set, i.e. its outer probability, as the paper prescribes.
• $\alpha>0$ in the goal; $t\ge0$ for the enlargement; $P(A)>0$ in Corollary 4.2.5, where the paper's hypothesis on $t$ is otherwise unsatisfiable. In §4.3, $\Omega=\{0,1\}$ is Bool with PMF.uniformOfFintype.
• A trivializing formalization is ruled out: restricting $\Omega$ to a finite type or $A$ to a finite set would give a strictly weaker statement (and the finite case of Theorem 4.1.1 is already posed elsewhere).
• Needed infrastructure: convex hulls of $0$–$1$ vectors and their behaviour under adding a coordinate, Hölder's inequality for ∫⁻, Fubini for Measure.pi on Fin (N+1), and the one-variable calculus of $\xi$. The definitions module is the substrate the Part II chapters of the paper use; proofs of the one-variable lemmas and of the induction step are welcome independently.
• Corollary 4.3.2 is not included: the paper derives it from Theorem 4.3.1 by optimising over $\alpha\ge1$, which only covers $t\ge2\sqrt{\log(1/P(A))}$, and the printed range $t\ge\sqrt{\log(1/P(A))}$ is not established on the page.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Section 2, Eq. (16)

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

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

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

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

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

Milestone: Eq. (15), expected average

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

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

Significance

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

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

Difficulty

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

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

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.

The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.

Setting

Fix an integer $n\ge1$ of variables, an arbitrary number $m$ of equality constraints, a real matrix $A\in\mathbb R^{m\times n}$, and vectors $b\in\mathbb R^m$ and $c\in\mathbb R^n$. The primal problem minimizes $c^Tx$ over $Ax=b$, $x\ge0$. Its dual problem maximizes $b^Ty$ over $A^Ty+s=c$, $s\ge0$. The dual slack is $s$. The development reuses a published general-form LP model and specializes it to this pair.

The strictly feasible pairs $F^0$ are the pairs $(x,s)$ satisfying the two feasibility systems for some dual multiplier $y$, with every coordinate of $x$ and $s$ strictly positive. The multiplier is allowed to vary with the pair. Write $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$, and $e$ for the vector of ones. The duality measure is $\mu=x^Ts/n$. For $0<\beta<1$, the Euclidean central-path neighborhood is

$$N_2(\beta)=\{(x,s)\in F^0:\|Xs-\mu e\|_2\le\beta\mu\}.$$

The search direction $(d_x,d_y,d_s)$ at $(x,s)$ with parameter $\gamma$ solves the three equations $Sd_x+Xd_s=\gamma\mu e-Xs$, $Ad_x=0$, and $A^Td_y+d_s=0$. A step of length $\theta$ yields $(x+\theta d_x,s+\theta d_s)$. Algorithm 1 begins in $N_2(1/4)$. It takes a predictor direction with $\gamma=0$ to the greatest step whose entire path remains in $N_2(1/2)$, then takes one full corrector direction with $\gamma=1$. The resulting pair starts the next iteration. The algorithm stops when $x^Ts\le2^{-t}$; its starting gap is at most $2^t$ report, pp. 4 and 6–7.

Formalization targets

Theorem 1: termination

For every real precision parameter $t$, every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration $k$ with

$$k\le\left\lceil2(\log2)8^{1/4}\sqrt n\,t\right\rceil, \qquad (x^k)^Ts^k\le2^{-t}.$$

The paper states the iteration order as $O(\sqrt n\,t)$. The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.

Source milestones

The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.

Significance

Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with $\sqrt n$, rather than with $n$, in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.

The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.

Difficulty

The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products $x_js_j$ away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.

Formalization scope

Vectors are functions on Fin n, and $A$ is a finite matrix. The report's indices $1,\ldots,n$ correspond to Lean indices $0,\ldots,n-1$. The norm in $N_2$ and in Lemmas 1–2 is explicitly $\ell_2$: Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and $\log$ is natural logarithm. The hypothesis $n\ge1$ gives meaning to $\mu=x^Ts/n$; no sign condition on $t$ is imposed, since for $t\le0$ the starting pair already meets the stopping test.

The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at $n=1$ there may be no continuing run under this literal algorithm rule; the goal retains $n\ge1$ and makes this limitation explicit. The denominator $\|Pq\|_2$ in Lemma 4 can vanish. The formal lower bound uses its limiting value $1/2$ in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes $n\ge2$, because its printed lower bound on the predictor length fails at $n=1$.

The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds $2^{-t}$; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.

Selected references

• Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. Technical-report PDF. The PDF used here is the technical report, so all page and result indices refer to that version.

Motivation

A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.

Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.

Setting

A manufacturer produces at unit cost $c$. A retailer sells at the fixed retail price $p$. Leftover units are salvaged at $c_3$ per unit. Each unit of unmet demand costs the retailer a goodwill penalty $g \ge 0$ and the manufacturer an additional penalty $g_1 \ge 0$; write $g_2 = g + g_1$. The data satisfy $c_3 < c < p$.

The manufacturer chooses a policy $(c_1, c_2, R)$: the retailer pays $c_1$ per unit ordered and may return up to the fraction $R \in [0,1]$ of its order $Q$ for a credit $c_2$ per unit. The paper assumes

$$c_3 < c < c_1 < p, \qquad c_3 < c_2 \le c_1 < p. \qquad (1),\ (2)$$

Demand $X \ge 0$ is random with distribution function $F$. Three expected profits are defined as functions of the order $Q$: $EP_T(Q)$, equation (3), the profit of a company store in which the manufacturer sells directly; $EP_R(Q)$, equation (6), the independent retailer's profit under the policy; and $EP_M(Q)$, equation (8), the manufacturer's profit when the retailer orders $Q$. An optimal order for a profit function is a $Q \ge 0$ maximizing it over $[0,\infty)$. The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.

The Lean development uses the same letters: Costs carries $c, c_3, p, g, g_1$; Costs.Admissible K c1 c2 R is (1)–(2) with $0 \le R \le 1$; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; $F$ is cdf D for a demand law D.

Formalization targets

Goal: Theorem 3

A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of $c_1$ and $c_2$. Precisely, for every price $c_1$ with $c < c_1 < p$ there is a credit $c_2$ with

$$c_3 < c_2 < c_1, \qquad c_1 = (p+g) - \frac{(p+g_2-c)(p+g-c_2)}{p+g_2-c_3} \quad (11),$$

such that the policy $(c_1, c_2, R = 1)$ coordinates the channel for every continuous demand distribution on $[0,\infty)$ with finite mean. The credit is chosen before, and independently of, the demand law.

Milestones

1. (4)–(5): the company store has an optimal order, and $Q$ is optimal iff $F(Q) = (p+g_2-c)/(p+g_2-c_3)$.
2. (7): under an admissible policy, $Q$ is optimal for the retailer iff $0 = -c_1 + p + g - F(Q)[p+g-c_2] - F((1-R)Q)[(1-R)(c_2-c_3)]$.
3. (9)–(10): an admissible policy coordinates the channel iff (10) holds at every system-optimal order.
4. (11): with $R = 1$ and $c_2 < c_1$, coordination holds iff (11) holds, whatever the demand law.
5. Appendix, proof of Theorem 3: for $c < c_1 < p$, (11) has a solution $c_2$ with $c_3 < c_2 < c_1$.

Significance

The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs $(c_1, c_2)$ then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.

Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for $c_3 < c_2$ establishes only $c_2 > c_3 - g_1$, which suffices only when $g_1 = 0$, although the claim holds for all $g_1 \ge 0$. And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost $c_r > v \ge 0$, which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.

Difficulty

The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on $[0,\infty)$, including the boundary $Q = 0$. Coordination is a statement about sets of maximizers, not about one first-order condition: when $F$ is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where $F$ increases. The naive reading "both first-order conditions hold at $Q^*_T$" proves one inclusion only.

Formalization scope

Demand is a probability measure D on $\mathbb R$ with D (Iio 0) = 0 and finite mean (IsDemand), and $F$ is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy $g, g_1 \ge 0$, implicit in the paper. $R$ is a fraction in $[0,1]$. Optimal orders are maximizers over $Q \ge 0$ that are themselves $\ge 0$. Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator $p + g_2 - c_3$ is positive under these assumptions, so no division is degenerate.

The goal is not the algebraic statement "there is $c_2 \in (c_3, c_1)$ solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of $c_2$.

A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity $EP_R = k \cdot EP_T + \text{const}$ under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.

Selected references

• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003, 227–339. https://doi.org/10.1016/S0927-0507(03)11006-7
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

Why add-with-carry generators

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep $r$ machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as $2^{640}$ when the base $b$ is near $2^{32}$ (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base-$b$ digits of a fraction $k/m$ written backwards, so the period of the generator is the period of a repeating base-$b$ expansion, i.e. the multiplicative order of $b$ modulo $m$.

Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus $m$ (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.

Setting

Fix a base $b \ge 2$ and two lags $r$ and $s$ with $0 < s < r$. A state (or seed vector) is

$$x = (x_1, x_2, \dots, x_r, c),$$

where each $x_i \in \{0, 1, \dots, b-1\}$ is a base-$b$ digit and $c \in \{0, 1\}$ is the carry bit. The digit $x_1$ is the oldest one. The add-with-carry map $f$ (p. 465) is

$$f(x_1, \dots, x_r, c) = \begin{cases} (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c,\ 0) & \text{if } x_{r+1-s} + x_1 + c < b,\\ (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c - b,\ 1) & \text{if } x_{r+1-s} + x_1 + c \ge b, \end{cases}$$

and the generated sequence of a seed $x$ is $x, f(x), f^2(x), \dots$. Reading off the last digit of each state gives a digit stream $x_1, \dots, x_r, x_{r+1}, x_{r+2}, \dots$ obeying $x_n = x_{n-r} + x_{n-s} + c \bmod b$, with the carry updated at each step. The two trivial seeds are $(0, \dots, 0, 0)$ and $(b-1, \dots, b-1, 1)$. The modulus of the generator is

$$m = b^r + b^s - 1 .$$

For $0 \le k < m$ and $j \ge 1$, the $j$-th base-$b$ digit of $k/m$ after the point is $d_j(k/m) = \lfloor b \cdot (b^{j-1} k \bmod m) / m \rfloor$. The order $\operatorname{ord}_m(b)$ is the least $p \ge 1$ with $b^p \equiv 1 \pmod m$, and $b$ is a primitive root of a prime $m$ when $\operatorname{ord}_m(b) = m - 1$.

Formalization targets

Goal: the period is the order of $b$

Let $m = b^r + b^s - 1$ be prime, and let $x$ be any seed other than the two trivial seeds. Then $f^r(x)$ is a periodic point of $f$ and

$$\min\{p \ge 1 : f^{p}(f^{r}(x)) = f^{r}(x)\} = \operatorname{ord}_m(b).$$

This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base $b$ for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular $b$, $r$, $s$ and does not assume that $b$ is a primitive root. When it is, the period is $b^r + b^s - 2$, the value announced in §2.

Milestones

1. §4.1 (p. 467): for $\gcd(k, m) = \gcd(b, m) = 1$, $p > 0$ is a period of the base-$b$ expansion of $k/m$ iff $\operatorname{ord}_m(b) \mid p$.
2. §4.1 (p. 467): if $b$ is a primitive root of the prime $m$, every proper fraction $k/m$ has least period $m - 1$.
3. p. 472: $f(x) = x$ iff $x$ is a trivial seed.
4. p. 472: $f^r(x)$ is periodic for every seed.
5. §4.2 (p. 468): for every seed other than $(b-1, \dots, b-1, 1)$ and every $C$, there is $0 \le k < m$, positive iff the seed is nonzero, with

$$x_n = d_{C+1-n}(k/m) \qquad (r + 1 \le n \le C).$$

6. p. 472, Method 3: $x$ is periodic iff $c = 0$ and $x_r \cdots x_{s+1} \ge x_{r-s} \cdots x_1$, or $c = 1$ and $x_r \cdots x_{s+1} \le x_{r-s} \cdots x_1$ (digit strings read as base-$b$ integers).
7. §2 (p. 465): the instance $b = 10$, $r = 2$, $s = 1$, period $108$.
8. §7 (p. 477): the instance $b = 6$, $r = 21$, $s = 2$, period $6^{21} + 6^2 - 2$.

Significance

The result. The goal reduces the period of the generator, a property of a dynamical system on $2b^r$ states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses $b, r, s$: search for primes $m = b^r + b^s - 1$ and check the order of $b$. Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus $m$. Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.

Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base-$b$ expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.

Difficulty

The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: $f$ is not linear over $\mathbb{Z}/b$, and the state $(x_1, \dots, x_r, c)$ does not live in a group in any evident way. The link to the order of $b$ modulo $m$ goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed $(b-1, \dots, b-1, 1)$, whose digits are those of $m/m = 1$, has to be excluded.

A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by $r$ (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.

Formalization scope

• Representation. All declarations are in namespace CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of $0 < s$ and $s < r$. A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so $c \le 1$ holds by typing. Lean index $i$ is the paper's $x_{i+1}$: x 0 is $x_1$ (the digit the step drops), and the partner digit $x_{r+1-s}$ is index $r - s$. step is defined directly from the two-case formula of p. 465, not through $k/m$. The digit stream out is one-based: the seed digits for $n \le r$, then the last digit of $f^{\,n-r}(x)$. digit b m k j is the exact integer formula above, used for $j \ge 1$ only.
• Period. "The period" is Mathlib's Function.minimalPeriod. It is $0$ at non-periodic points, so the goal's equation with the positive $\operatorname{ord}_m(b)$ also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period $L$" is stated as "$p > 0$ is a period iff $L \mid p$".
• Quantifier readings. "With appropriately chosen base $b$, lags $r$ and $s$ and seed vector $x$" (p. 465) is read as: $m$ prime and $x$ not a trivial seed, following p. 468 ("Making $m$ a prime ensures this") and p. 472. "After a few iterations" is "after at most $r$", the paper's own bound (p. 472), so the goal is stated at $f^r(x)$. In milestone 5 the fraction $k$ depends on the length $C$ of the finite string, as in the paper's "arbitrarily long finite string". In milestone 8, "for any set of 21 seed digits" is stated at $f^{21}(x)$ for the same reason.
• Corrected misprints. p. 465 prints the second trivial seed as "(9, 9, 9)"; the last entry is the carry, so milestone 7 excludes $(9, 9, 1)$. p. 473, example (a), prints the Method 3 inequalities reversed; milestone 6 follows p. 472, which exhaustive checks on small parameters confirm. p. 478 repeats the die period with "− 1" for "− 2"; milestone 8 quotes p. 477.
• Ruled-out trivializations. The goal is not "some period divides $m - 1$" and not "every orbit is eventually periodic". Both hold for any self-map of a finite set or are vacuous. The trivial seeds are named states, not excluded by an assumption such as $f(x) \neq x$.
• Infrastructure and contributions. Needed: periods of base-$b$ expansions of rationals (milestones 1–2, reusable beyond this mission) and finite-dynamics facts about minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.

Selected references

• G. Marsaglia and A. Zaman, A new class of random number generators, Ann. Appl. Probab. 1(3) (1991), 462–480. https://doi.org/10.1214/aoap/1177005878
• S. Tezuka, P. L'Ecuyer and R. Couture, On the lattice structure of the add-with-carry and subtract-with-borrow random number generators, ACM Trans. Model. Comput. Simul. 3(4) (1993), 315–331. https://doi.org/10.1145/159737.159749
• R. Couture and P. L'Ecuyer, Distribution properties of multiply-with-carry random number generators, Math. Comp. 66 (1997), 591–607. https://doi.org/10.1090/S0025-5718-97-00827-2
• M. Lüscher, A portable high-quality random number generator for lattice field theory simulations, Comput. Phys. Commun. 79 (1994), 100–110. https://doi.org/10.1016/0010-4655(94)90232-1