Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Potential Games 2: Every Finite Potential Game Is Isomorphic to a Congestion GameResearch Paper

Motivation

Congestion games model situations in which agents choose sets of shared resources and the payoff of each resource depends only on how many agents use it: drivers choosing routes through road segments, jobs choosing machines, flows choosing links in a network. Rosenthal (A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2, 1973) showed that every such game has a pure-strategy Nash equilibrium, by exhibiting a single real function on strategy profiles whose changes track every player's unilateral payoff changes.

Monderer and Shapley (Potential Games, Games Econ. Behav. 14, 1996) isolated that property and called games having it potential games. Their Section 3 shows that the property characterizes congestion games: Rosenthal's argument gives Theorem 3.1 (every congestion game is a potential game), and Theorem 3.2 gives the converse up to a renaming of strategies. Potential games have since become a standard tool in algorithmic game theory (convergence of best-response dynamics, price of stability bounds, learning in games), and Theorem 3.2 is the reason that results proved for congestion games apply to all finite potential games.

Setting

A game in strategic form $\Gamma$ has a finite set of players $N = \{1, \dots, n\}$ , for each player $i$ a strategy set $Y^i$ , the profile set $Y = \times_{i\in N} Y^i$ , and payoff functions $u^i : Y \to \mathbb{R}$ . For a profile $y$ and $x \in Y^i$ , $(y^{-i}, x)$ is $y$ with player $i$ 's strategy replaced by $x$ . The game is finite if every $Y^i$ is finite.

A function $P : Y \to \mathbb{R}$ is a potential for $\Gamma$ (condition (2.2) with unit weights) if

u^i(y^{-i}, x) - u^i(y^{-i}, z) = P(y^{-i}, x) - P(y^{-i}, z) \qquad \text{for all } i,\ y^{-i},\ x, z \in Y^i,

and $\Gamma$ is a potential game if it has a potential (IsPotential, IsPotentialGame).

A congestion model $C(N, M, (\Sigma^i)_{i\in N}, (c_j)_{j\in M})$ has players $N$ , a finite set of facilities $M$ , for every player a set $\Sigma^i$ of strategies, each a nonempty subset of $M$ , and for every facility $j$ a vector $c_j$ , where $c_j(k)$ is the payoff to each user of $j$ when exactly $k$ players use it. The associated congestion game has strategy sets $\Sigma^i$ and payoffs

v^i(A) = \sum_{j\in A^i} c_j\big(\sigma_j(A)\big), \qquad \sigma_j(A) = \#\{i \in N : j \in A^i\}. \tag{3.1}

Two games with the same players are isomorphic (IsIsomorphic) if there are bijections $g^i : Y^i_1 \to Y^i_2$ with $u^i_1(y) = u^i_2(g^1(y^1), \dots, g^n(y^n))$ for every player $i$ and profile $y$ .

Formalization targets

Goal: Theorem 3.2

\text{Every finite potential game is isomorphic to a congestion game.}

Formally: for every finite set of players, finite strategy sets $Y^i$ and payoffs $u$ admitting a potential, there are $m \in \mathbb{N}$ and a congestion model on the facilities $\{1, \dots, m\}$ , all of whose strategies are nonempty facility sets, whose congestion game is isomorphic to $\Gamma$ .

Milestones

The milestones follow Appendix B of the paper.

Lemma B.1 (p. 139): with $x^r(j) = c_j(r)$ and $x(B) = \sum_{j\in B} x(j)$ , $v^i(A) = x^1(A(i)\cap A(-i)^c) + x^2\big(\bigcup_{k\neq i}[A(i)\cap A(k)\cap A(-\{i,k\})^c]\big) + \cdots + x^n\big(\bigcap_{k} A(k)\big)$ .
The invariance of $u^i - P$ (p. 141): $u^i(a^{-i}, a^i) - P(a^{-i}, a^i)$ does not depend on $a^i$ .
The $M_1$ identity and (B.2) (p. 141): on the facility set $M = \times_i \{0,1\}^{K(i)}$ , $A^1_{m_1}\cap\cdots\cap A^n_{m_n}\cap M_1 = \{\varepsilon(m)\}$ , so $x^n(A^1_{m_1}\cap\cdots\cap A^n_{m_n}) = P(a^1_{m_1}, \dots, a^n_{m_n})$ .
(B.6) (p. 141): $x^1(A^i_{m_i}\cap A(-i)^c) = x^1(\varepsilon(m^i)) = u^i(a) - P(a)$ .

Significance

Theorems 3.1 and 3.2 together say that, up to renaming strategies, the finite potential games and the congestion games are the same class. Consequently any statement about finite congestion games that is invariant under isomorphism (existence of pure equilibria, convergence of improvement dynamics, the structure of equilibrium sets) holds for all finite potential games, and conversely any potential game can be realized as a resource-sharing model. The representation is also the starting point of the later literature on the number of facilities needed to represent potential games, which the paper itself begins with a remark at the end of Appendix B.

Theorem 3.1 is already machine-checked on the platform, as Rosenthal's potential identity PriceOfStability.Harmonic.rosenthal_potential_change (Proved); it is included in this mission as a reference item. Theorem 3.2 is proved in the paper but has no machine-checked proof that we know of. The mission adds a formal statement of the theorem, of isomorphism of games, of congestion games as games in strategic form, and of the explicit construction of Appendix B; and, once proved, a verified converse to Rosenthal's theorem.

Difficulty

The theorem is an explicit construction, and its difficulty is bookkeeping rather than a single hard idea. The facility set is a product of Boolean cubes, one per player; each player's strategy is the set of facilities with a 1 in a given coordinate; and the facility payoffs are defined only at load $1$ and load $n$ , by two auxiliary vectors whose definitions involve a choice of representative. Showing that the resulting congestion game reproduces every payoff requires identifying, for every profile, exactly which facilities are used by one player and which by all players, and showing that the "load 1" facilities pick up precisely the part of $u^i$ that player $i$ cannot influence. The paper leaves the two key set identities as "it can be verified"; they are the milestones.

The construction as printed does not cover one player: with $n = 1$ the vectors $x^1$ and $x^n$ are the same vector, defined twice. The theorem is still true for one player, and the formal goal does not exclude it, so a complete proof must treat that case separately.

Formalization scope

Players form a finite type ι with decidable equality; strategy sets are types Y i, finite in the goal ([∀ i, Fintype (Y i)]). $(y^{-i}, x)$ is Function.update y i x. No nonemptiness of the strategy sets and no lower bound on the number of players is assumed.
The congestion model is the published CongestionPoA.AsymSum.CongestionGame ι M (reference item): strategies i is the finite family $\Sigma^i$ and latency j k is the paper's $c_j(k)$ , an arbitrary real number. No sign change is made; the published names "latency" and "cost" are only names. Values of latency at $0$ and above $n$ never enter (3.1).
The congestion game as a game in strategic form is congestionPayoff G, whose strategy set for player $i$ is the subtype of G.strategies i. Because the isomorphism maps onto that subtype, the strategies of a player are distinct facility sets.
In the goal the facility set is Fin m for an existentially quantified $m$ , and nonemptiness of every strategy, which is part of the definition of a congestion model on p. 133 but not of the published structure, is a separate conjunct. Dropping it, or replacing "congestion game" by an arbitrary game whose payoffs equal $u$ , would make the goal a different, weaker statement; the formal goal does neither.
The Appendix B construction (FacilityConstruction) indexes the coordinates of player $i$ by $Y^i$ itself instead of $K(i) = \{1, \dots, k(i)\}$ ; $m^i = (m_k)_{k\neq i}$ is passed as a full profile whose $i$ -th coordinate is ignored; $x^n$ and $x^1$ select a representative by choice, the chosen $i$ -th coordinate playing the role of the arbitrary $a^i$ in (B.4).
Misprints corrected: in Lemma B.1, $x^r(j) = c_j(m)$ is read $c_j(r)$ , and the " $\cdots$ " as the general term $x^r(\bigcup_{S\ni i, |S| = r}[\bigcap_{k\in S}A(k)\cap A(-S)^c])$ ; in (B.6), $A(-i)$ is read $A(-i)^c$ and $P^i(a)$ as $P(a)$ .

Contributions welcome: proofs of the milestones, a proof of the goal (by the paper's construction, with the one-player case handled separately, or by any other construction), and general lemmas about transporting potentials along isomorphisms.

Selected references

D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2 (1973), 65–67. https://doi.org/10.1007/BF01737559
E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler and T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38 (2008), 1602–1623. https://doi.org/10.1137/070680096 (source of the platform's Rosenthal potential identity)

13 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Monotone Comparative Statics II: f Is Quasisupermodular If and Only If a Strictly Increasing Transformation Makes It Supermodular on Every Sublattice {x₁, x₂, x₁ ∨ x₂, x₁ ∧ x₂}Research Paper

Motivation

Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.

Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). Examples are $\mathbb{R}^n$ and products of finite chains, ordered componentwise.

A function $f : X \to \mathbb{R}$ is supermodular on a set $S \subseteq X$ if

f(x) + f(y) \le f(x \vee y) + f(x \wedge y) \qquad \text{for all } x, y \in S.

It is quasisupermodular (p. 162) if for all $x, y \in X$

$f(x) \ge f(x \wedge y)$ implies $f(x \vee y) \ge f(y)$ , and
$f(x) > f(x \wedge y)$ implies $f(x \vee y) > f(y)$ .

A function $h : \mathbb{R} \to \mathbb{R}$ is strictly increasing if $r < s$ implies $h(r) < h(s)$ . A function $f$ is supermodularizable if $h \circ f$ is supermodular on $X$ for some strictly increasing $h$ .

For $x_1, x_2 \in X$ the set $\{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}$ is closed under $\vee$ and $\wedge$ ; it is the sublattice generated by $x_1$ and $x_2$ and has at most four points.

Quasisupermodularity depends only on the order of the values of $f$ , so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.

Formalization targets

Goal: Theorem 8 (p. 165)

$f : X \to \mathbb{R}$ is quasisupermodular if and only if there is $g : \mathbb{R} \times X \times X \to \mathbb{R}$ such that (i) $r \mapsto g(r, x_1, x_2)$ is strictly increasing for every $(x_1, x_2) \in X^2$ , and (ii) for every $x_1, x_2 \in X$ ,

x \mapsto g(f(x), x_1, x_2) \ \text{ is supermodular on } \{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}.

Milestones

Invariance (p. 164): if $f$ is quasisupermodular and $g$ strictly increasing, $g \circ f$ is quasisupermodular.
Supermodularizable implies quasisupermodular (pp. 164–165): if $h$ is strictly increasing and $h \circ f$ is supermodular on $X$ , then $f$ is quasisupermodular.
Lemma (p. 165): if $f$ is quasisupermodular on $L = \{x, x', x \vee x', x \wedge x'\}$ , then $h \circ f$ is supermodular on $L$ for some strictly increasing $h : \mathbb{R} \to \mathbb{R}$ .
Example 1 (p. 165): the function on $\{0,1\} \times \{0,1,2,3\}$ with rows $(1,2,2,1)$ and $(3,4,5,3)$ is quasisupermodular but not supermodularizable.

The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on $(x_1, x_2)$ .

Significance

Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.

On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of $\mathbb{R}$ that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.

Difficulty

The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values $a, b, c, d$ of $f$ at $x, x \vee x', x \wedge x', x'$ need not satisfy $a + d \le b + c$ , and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing $h$ of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which $x$ and $x'$ are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair $(x, x')$ .

Formalization scope

Lattices are Mathlib's Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.
Quasisupermodularity is a draft definition QuasiSupermodularOn g S, relativized to a set $S$ ; the paper's notion on $X$ is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of $S$ .
Supermodularity is the published definition Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.
"Strictly increasing" is StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.
The transformation $g : \mathbb{R} \times X \times X \to \mathbb{R}$ of Theorem 8 is curried, g : ℝ → X → X → ℝ; it may depend on $(x_1, x_2)$ but not on $x$ . Transformations are defined on all of $\mathbb{R}$ , as printed, not only on the values of $f$ .
The Lemma's four-point lattice is formalized as the subset $\{x, x', x \vee x', x \wedge x'\}$ of an ambient lattice, with both notions relativized to it; the subset is closed under join and meet, so this is the page's statement, including the degenerate cases.
Example 1's domain is Fin 2 × Fin 4 with the product order.

Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps $\mathbb{R} \to \mathbb{R}$ with prescribed values on finitely many points.

Selected references

P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
M. Li Calzi, Generalized Symmetric Supermodular Functions, Working Paper, Stanford University, 1990 (listed so in the paper's references; the text on p. 165 cites it as Li Calzi (1991)).

8 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 2: Kesten's Theorem for R = Q + MR — Unique Stationary Law, Power Tails with Explicit C±, and C₊ + C₋ > 0 iff Q ≢ (1 − M)cResearch Paper

Motivation

The random difference equation

R \overset{\mathcal L}{=} Q + MR,\qquad R \text{ independent of } (Q,M),

describes the stationary state of the affine recursion $R_n = Q_n + M_n R_{n-1}$ driven by independent copies of a random pair $(Q,M)$ . It appears wherever a quantity is multiplied by a random factor and then receives a random increment: the discounted value of a stream of random cash flows (a perpetuity), the stationary volatility of ARCH and GARCH models in financial econometrics (de Haan, Resnick, Rootzén and de Vries 1989), random walks in random environment, and the stationary laws of random coefficient autoregressions. In all of these, the question that matters for risk is the size of the tail $P(R>t)$ .

Timeline:

1973. Kesten proves, in a multivariate setting, that the stationary solution has power-law tails, $P(R>t)\sim C_+t^{-\kappa}$ , where $\kappa$ solves $\mathbf E|M|^\kappa=1$ ; the constants are not identified, and the proof of the key renewal step (his Theorem 4) runs to nine pages.
1979. Vervaat gives a full account of existence, uniqueness and moments of the solution in dimension one.
1980–1981. Grincevičius proves a maximal inequality of Lévy type for the partial sums of the recursion.
1986. Letac formulates a general principle for existence and uniqueness of solutions of random equations $R\overset{\mathcal L}{=}\Psi(R)$ .
1991. Goldie proves an implicit renewal theorem (Theorem 2.3, the subject of the first mission of this series) and deduces from it a new proof of Kesten's one-dimensional theorem, with explicit formulas for the constants $C_\pm$ and a necessary and sufficient condition for them not to vanish (Theorem 4.1).
2016. Buraczewski, Damek and Mikosch survey the theory, in which Kesten's theorem in Goldie's form is the central result.

Setting

Let $(Q,M)$ be a pair of real random variables with joint law $\mu$ on $\mathbb R^2$ . No independence between $Q$ and $M$ and no sign condition on either is assumed. A probability law $\rho$ on $\mathbb R$ is a law for $R$ satisfying (1.1) if the law of $Q+MR$ equals $\rho$ when $R$ has law $\rho$ and is independent of $(Q,M)$ .

A law on $\mathbb R$ is arithmetic if it is concentrated on a lattice $\{n\lambda:n\in\mathbb Z\}$ for some $\lambda>0$ , and nonarithmetic otherwise. For $\kappa>0$ , the conditions of Lemma 2.2 on $M$ are

\mathbf E|M|^\kappa = 1,\qquad \mathbf E|M|^\kappa\log^+|M|<\infty,

and that the conditional law of $\log|M|$ given $M\ne0$ is nonarithmetic. Under them

m := \mathbf E|M|^\kappa\log|M| \in (0,\infty).

With $x^+=x\vee0$ and $x^-=(-x)\vee0$ , the constants of Theorem 4.1 are, when $M\ge0$ a.s.,

C_\pm = \frac{\mathbf E\big(((Q+MR)^\pm)^\kappa-((MR)^\pm)^\kappa\big)}{\kappa m},

and otherwise $C_+=C_-=\frac{1}{2\kappa m}\mathbf E\big(|Q+MR|^\kappa-|MR|^\kappa\big)$ , where $R$ has the stationary law and is independent of $(Q,M)$ .

Formalization targets

Goal: Theorem 4.1

Assume the conditions of Lemma 2.2 and $\mathbf E|Q|^\kappa<\infty$ . Then there is a unique law $\rho$ for $R$ satisfying (1.1); the expectations defining $C_\pm$ are finite; and

\lim_{t\to\infty} t^\kappa P(R>t) = C_+,\qquad \lim_{t\to\infty} t^\kappa P(R<-t) = C_-,

with $C_\pm$ as above. Finally

C_++C_->0 \iff P\big(Q=(1-M)c\big)<1 \ \text{ for each fixed } c\in\mathbb R.

Milestones

In the order the proof uses them:

Corollary 2.4: the implicit renewal theorem with the moment conditions (2.16)–(2.17) and constants (2.18)–(2.20), for a general random function $\Psi$ in place of $t\mapsto Q+Mt$ .
Lemma 9.4: tail-difference integrals against $t^{\kappa-1}dt$ versus moment differences.
The elementary inequalities (9.26)–(9.27).
(4.8): for $\kappa>1$ , $\mathbf E|R|^{\kappa-1}<\infty$ with an explicit bound.
(2.16)–(2.17) for $\Psi(t)=Q+Mt$ : the moment differences are integrable.
Proposition 4.2 (Grincevičius's maximal inequality) and its consequence (4.6).
The lower bound $P(|\Pi_n|>e^t\text{ for some }n)\ge\delta e^{-\kappa t}$ for the products $\Pi_n=M_1\cdots M_n$ .
Under the condition $P(Q=(1-M)c)<1$ for each $c$ , $t^\kappa P(|R|>t)$ stays bounded away from $0$ .

Significance

The result. Theorem 4.1 identifies the tail exponent of the stationary solution as the root $\kappa$ of $\mathbf E|M|^\kappa=1$ , which depends on $M$ alone, and expresses the tail constants as expectations under the stationary law. The constants yield the bounds of Corollary 4.3 and closed forms when $\kappa$ is an integer (Corollaries 4.4, 4.5). The dichotomy between $M\ge0$ a.s. (different left and right constants) and $P(M<0)>0$ (equal constants) is visible only through these formulas. The positivity criterion tells when the power tail is really there: it fails exactly when the recursion has a deterministic fixed point $c$ . Tail estimates for GARCH processes, perpetuities in insurance mathematics and random walks in random environment are applications of this statement.

Formalizing it. The theorem has been proved since 1973 and in the present form since 1991; it is open only as a formalization. No machine-checked proof of Kesten's theorem, of the implicit renewal theorem, or of the underlying nonarithmetic key renewal theorem on the whole line is known to this mission. The work consists of formalizing Goldie's proof, which assembles the implicit renewal theorem with moment estimates, a maximal inequality and a Cramér–Lundberg-type lower bound for a random walk with negative drift.

Difficulty

The obvious argument is to write $R=\sum_{k\ge1}\Pi_{k-1}Q_k$ and estimate the tail of each term. It fails because $\mathbf E|M|^\kappa=1$ makes every term contribute tails of the same order $t^{-\kappa}$ , and the sum of infinitely many such contributions is exactly what has to be computed; termwise bounds give the right exponent at best, not the limit or the constant. A second natural idea, applying the renewal theorem directly to $P(R>t)$ , needs integrability of a tail difference that is not evident, because $\mathbf E|R|^\kappa$ is infinite whenever $C_++C_->0$ ; the moment differences $((Q+MR)^+)^\kappa-((MR)^+)^\kappa$ must be controlled without either term being integrable. The positivity half is a separate problem: the formula for $C_\pm$ is a difference of two infinite-looking quantities, and showing it is positive requires a lower bound on the tail that does not come from the formula.

Formalization scope

Everything is stated in terms of laws. The joint law of $(Q,M)$ is a probability measure $\mu$ on $\mathbb R\times\mathbb R$ (first coordinate $Q$ , second $M$ ); a law for $R$ satisfying (1.1) is a probability measure $\rho$ on $\mathbb R$ that equals the image of $\mu\otimes\rho$ under $((q,m),r)\mapsto q+mr$ , and uniqueness is among all probability measures on $\mathbb R$ , with no moment restriction. Expectations involving $R$ and $(Q,M)$ are integrals against $\mu\otimes\rho$ , which is what makes $R$ independent of $(Q,M)$ . The conditions of Lemma 2.2 are stated for the law of $M$ , with $\mathbf E|M|^\kappa$ and $\mathbf E|M|^\kappa\log^+|M|$ as lower Lebesgue integrals and the conditional law of $\log|M|$ taken given $M\neq0$ . " $P(R>t)\sim C_+t^{-\kappa}$ " is the limit statement $t^\kappa P(R>t)\to C_+$ , which the paper prescribes and which includes $C_+=0$ . Milestones on sequences use independent copies $(Q_n,M_n)$ on an arbitrary probability space carrying them, stored 0-based.

The statement does not reduce to a trivial one: the ratio form $P(R>t)/(C_+t^{-\kappa})\to1$ (undefined when $C_+=0$ ), existence of some fixed point without uniqueness, the positivity criterion as a one-way implication, and tail limits asserted for an arbitrary random variable rather than for the stationary law are all excluded. One correction to the source is built in: Lemma 9.4's (9.17) is printed as an equality, which fails for independent identically distributed non-degenerate $X$ , $Y$ ; the inequality the proof establishes is stated.

A complete development needs: convolution and image measures of products on $\mathbb R^2\times\mathbb R$ ; the key renewal theorem on the whole line for nonarithmetic laws with positive mean (the content of the first mission of this series); existence and uniqueness for contractive random affine maps; Lévy-type maximal inequalities; and ladder-height estimates for random walks with negative drift whose steps may equal $-\infty$ . The renewal-theoretic and random-walk components are reusable well beyond this mission. Contributions of any milestone, and of supporting lemmas such as the moment bounds for perpetuities, are welcome.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Annals of Applied Probability 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Mathematica 131:207–248, 1973. https://doi.org/10.1007/BF02392040
W. Vervaat, On a stochastic difference equation and a representation of non-negative infinitely divisible random variables, Advances in Applied Probability 11(4):750–783, 1979. https://doi.org/10.2307/1426858
L. de Haan, S. I. Resnick, H. Rootzén and C. G. de Vries, Extremal behaviour of solutions to a stochastic difference equation with applications to ARCH processes, Stochastic Processes and their Applications 32(2):213–224, 1989. https://doi.org/10.1016/0304-4149(89)90076-8
D. Buraczewski, E. Damek and T. Mikosch, Stochastic Models with Power-Law Tails: The Equation X = AX + B, Springer, 2016. https://doi.org/10.1007/978-3-319-29679-1

13 thms3 active usersReviewed

Completed

Graph Theory Markov Chain Probability·Captain: mikedeng1

Geometric Bounds for Eigenvalues of Markov Chains 2: Odd Closed Paths Bound the Smallest Eigenvalue, β_min ≥ −1 + 2/ιResearch Paper

Motivation

The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues $1=\beta_0>\beta_1\ge\dots\ge\beta_{m-1}\ge-1$ , the distance to stationarity after $n$ steps is governed by $\beta_*^{\,n}$ , where $\beta_*=\max(\beta_1,|\beta_{m-1}|)$ (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue $\beta_1$ are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue $\beta_{\min}=\beta_{m-1}$ : a chain whose smallest eigenvalue is close to $-1$ oscillates almost periodically and mixes slowly whatever $\beta_1$ is. A chain is aperiodic exactly when $\beta_{\min}>-1$ , but that qualitative fact gives no rate.

Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on $\beta_{\min}$ uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.

Timeline:

1988–1989, Jerrum and Sinclair: conductance (Cheeger-type) bounds on $\beta_1$ for chains on combinatorial structures.
1991, Diaconis and Stroock: path bounds for $\beta_1$ (Proposition 1, the Poincaré inequality $\beta_1\le1-1/\kappa$ ) and for $\beta_{\min}$ (Proposition 2, this mission), with the specializations to random walks on graphs (Corollaries 1 and 2).

Setting

Let $X$ be a finite set and $P(x,y)$ the transition matrix of an irreducible Markov chain on $X$ , reversible with respect to a probability distribution $\pi$ :

Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)\qquad(x,y\in X).

The operator $(P\varphi)(x)=\sum_yP(x,y)\varphi(y)$ is self-adjoint on $L^2(\pi)$ , with inner product $\langle\varphi,\psi\rangle_{L^2(\pi)}=\sum_x\varphi(x)\psi(x)\pi(x)$ , so its eigenvalues are real. Write $E(\varphi^2)=\sum_x\varphi(x)^2\pi(x)$ and let $\beta_{\min}$ be the smallest eigenvalue of $P$ .

The graph of the chain has vertex set $X$ , an edge from $x$ to $y$ when $Q(x,y)>0$ , and a self-loop at $x$ when $Q(x,x)>0$ . An odd closed path $\sigma_x$ at $x$ is a sequence of edges from $x$ back to $x$ , with an odd number of edges, in which no directed edge is traversed twice. Its length is

|\sigma_x|_Q=\sum_{e\in\sigma_x}Q(e)^{-1}.

A system of odd paths $\Sigma=(\sigma_x)_{x\in X}$ chooses one such path for every point, and its load is

\iota=\iota(\Sigma)=\max_e\sum_{\sigma_x\ni e}|\sigma_x|_Q\,\pi(x),

the maximum over directed edges $e$ of the weighted length of the paths through $e$ (display (1.7) of the paper).

For the random walk on a graph $G=(X,E)$ , $P(x,y)=1/d(x)$ when $\{x,y\}\in E$ , with $d(x)$ the degree, and $\pi(x)=d(x)/2|E|$ . There $d_*$ is the maximum degree, $\sigma_*$ the largest number of edges of a path in $\Sigma$ , and $b_*=\max_e\sharp\{\sigma\in\Sigma:e\in\sigma\}$ .

Formalization targets

Goal: Proposition 2

For an irreducible, aperiodic, reversible chain and every system $\Sigma$ of odd closed paths,

\beta_{\min}\ge-1+\frac{2}{\iota(\Sigma)}.

Milestones (the steps of the paper's proof)

The identity (1.8): $\tfrac12\sum_{x,y}(\varphi(x)+\varphi(y))^2Q(x,y)=E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}$ .
Along an odd closed path $x,y,w,\dots,z,x$ : $\varphi(x)=\tfrac12\{(\varphi(x)+\varphi(y))-(\varphi(y)+\varphi(w))+\dots+(\varphi(z)+\varphi(x))\}$ .
For every $\varphi$ : $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$ .
Every eigenvalue $\beta$ of $P$ satisfies $\beta\ge-1+2/\iota$ .

Companions

Corollary 2. For the random walk on a connected, non-bipartite graph and any system $\Sigma$ of odd paths, $\beta_{\min}\ge-1+\dfrac{2}{d_*\sigma_*b_*}$ .
Remark 1.3. With odd paths $\sigma_{xy}$ for every ordered pair and $\tilde\iota=\max_e\sum_{\sigma_{xy}\ni e}|\sigma_{xy}|_Q\pi(x)\pi(y)$ : $\beta_{\min}\ge-1+1/\tilde\iota$ .

Significance

Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds $\beta_1\le1-1/\kappa$ through paths between pairs of points, it bounds the absolute spectral gap $1-\beta_*$ entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.

Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the $L^2(\pi)$ inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that $-1$ is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.

Difficulty

Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while $\iota$ counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs $(x,y)$ , including $x=y$ , in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels $\varphi(x)$ instead of doubling it.

The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small $\iota$ , and the choice of $\Sigma$ is part of every application.

Formalization scope

The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that $\pi$ is a probability vector) and DetailedBalance. $Q$ is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). $\beta_{\min}$ is the infimum of the real eigenvalues of $P$ , a minimum for a stochastic matrix on a nonempty set.

Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with $Q>0$ . The paper defines $|\sigma_x|_Q$ "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. $\iota$ is a real supremum over the finite set of directed edges with $Q>0$ , and it is $0$ only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to $\beta_{\min}\ge-1$ by $2/0=0$ . The system $\Sigma$ is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption $|X|\ge2$ is made.

Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, $b_*$ counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.

Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.

Selected references

P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82(1):93–133, 1989. https://doi.org/10.1016/0890-5401(89)90067-9
D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (2nd ed. 2017). https://doi.org/10.1090/mbk/107

12 thms3 active usersReviewed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Learning Models with Uniform Performance via Distributionally Robust Optimization 2: A Minimax Lower Bound of Order n^(−1/2) ∨ n^(−1/k*) for Estimating the Cressie–Read Robust Risk (Theorem 3)Research Paper

Motivation

Distributionally robust optimization replaces the expected loss $\mathbb E_{P_0}[\ell(\theta; X)]$ of a statistical model by its worst case over all distributions $Q$ close to the data distribution $P_0$ . When closeness is measured by an $f$ -divergence ball $\{Q : D_f(Q\|P_0) \le \rho\}$ of fixed radius $\rho > 0$ , the robust risk upper-bounds the risk of every subpopulation of $P_0$ that has sufficiently large probability, so a model with small robust risk performs uniformly well across latent subgroups. This is the program of J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization (arXiv:1810.08750; Ann. Statist. 49 (2021), doi:10.1214/20-AOS2004).

The robust risk is itself a statistical functional. It is estimated by plugging in the empirical distribution, and the paper shows (its Theorem 2) that for the Cressie–Read family of divergences with parameter $k$ the plug-in estimate concentrates at rate $n^{-1/(k_* \vee 2)}$ , with $k_* = k/(k-1)$ . For small $k$ (heavy protection against distribution shift) $k_*$ is large and this rate is far slower than the parametric $n^{-1/2}$ . This mission formalizes the paper's answer to whether the slow rate is an artefact of the plug-in estimator or intrinsic: its Theorem 3, a minimax lower bound valid for every estimator.

Setting

Fix $k \in (1,\infty)$ and write $k_* = k/(k-1)$ . The Cressie–Read function is

f_k(t) = \frac{t^k - kt + k - 1}{k(k-1)} \quad (t \ge 0), \qquad f_k(t) = +\infty \quad (t < 0).

For a probability measure $P$ , a real random variable $Z$ and a radius $\rho > 0$ , the robust risk is

\mathcal R_k(Z) = \sup\Bigl\{ \mathbb E_P[LZ] : L \ge 0,\ \mathbb E_P[L] = 1,\ \mathbb E_P[f_k(L)] \le \rho \Bigr\},

the supremum of $\mathbb E_Q[Z]$ over distributions $Q \ll P$ with likelihood ratio $L = dQ/dP$ and Cressie–Read divergence $D_{f_k}(Q\|P) = \mathbb E_P[f_k(L)]$ at most $\rho$ .

Write

c_k(\rho) = (1 + k(k-1)\rho)^{1/k}, \qquad p_k = (1 + k(k-1)\rho)^{-1/(k-1)}, \qquad \beta_k = \frac{k(k-1)\rho}{2(1+k(k-1)\rho)} .

Fix $M > 0$ and let $\mathcal P$ be the set of all distributions on the two points $\{0, M\}$ ; each is determined by its mass $p \in [0,1]$ at $M$ . An estimator is any function $\widehat R : \{0, M\}^n \to \mathbb R$ of a sample $Z_1^n = (Z_1, \dots, Z_n)$ drawn i.i.d. from $P_0 \in \mathcal P$ . The minimax risk of estimating the robust risk is

\mathfrak M_n(\mathcal P, f_k) = \inf_{\widehat R}\ \sup_{P_0 \in \mathcal P}\ \mathbb E_{P_0^n}\bigl|\widehat R(Z_1^n) - \mathcal R_k(Z)\bigr|, \qquad Z \sim P_0. \qquad (16)

The total variation distance between two product laws $P^n, P'^n$ on the finite set $\{0,M\}^n$ is $\|P^n - P'^n\|_{\mathrm{TV}} = \tfrac12\sum_z |P^n\{z\} - P'^n\{z\}|$ , and $D_{\mathrm{kl}}$ denotes the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 3

For every $n \ge 1$ ,

\mathfrak M_n(\mathcal P, f_k) \ge M \max\Biggl\{ \frac{1}{8 k_* p_k}\Bigl( \sqrt{\frac{p_k(1-p_k)}{16 n}} \wedge \tfrac12(1-p_k) \wedge p_k \Bigr),\ \ \frac18 \beta_k^{1/k} c_k(\rho) \Bigl( \frac{1}{4n} \wedge p_k \wedge \bigl(1 - (1-\beta_k)^{1-k_*} p_k\bigr) \Bigr)^{1/k_*} \Biggr\}.

The first branch is of order $n^{-1/2}$ , the second of order $n^{-1/k_*}$ . The page prints $8n$ in the first branch; the target uses $16n$ (see Formalization scope).

Milestones

Lemma 12 (three claims): for $Z$ equal to $z_0 \le z_1$ with probabilities $1-p$ , $p$ : if $p \ge p_k$ then $\mathcal R_k(Z) = z_1$ ; if $p \le p_k$ then $\mathcal R_k(Z) \le c_k p^{1/k_*} z_1 + (1 - c_k p^{1/k_*}) z_0$ ; and if $p \le p_k \wedge (1 - (1-\beta)^{1-k_*} p_k)$ for some $\beta \in (0,1)$ then $\mathcal R_k(Z) \ge \beta^{1/k} c_k p^{1/k_*} z_1 + (1 - \beta^{1/k} c_k p^{1/k_*}) z_0$ .
The primal two-point formula (p. 47): for $p \in (0,1)$ ,

\mathcal R_k(Z) = z_0 + (z_1 - z_0)\sup\{q \in [0,1] : (1-p)^{1-k}(1-q)^k + p^{1-k}q^k \le c_k^k\}.

Le Cam's reduction (37): if $|\mathcal R_k(P_0) - \mathcal R_k(P_1)| \ge 2\delta > 0$ then $\mathfrak M_n \ge \frac\delta2(1 - \|P_0^n - P_1^n\|_{\mathrm{TV}})$ .
The Taylor display $c_k(p_k - \delta)^{1/k_*} \le 1 - \frac{1}{k_*}c_k^{k_*}\delta$ for $0 < \delta \le p_k$ .
The KL display $D_{\mathrm{kl}}(P_2\|P_1) \le 8\delta^2/(p_k(1-p_k))$ for the laws with masses $p_k \mp \delta$ at $M$ .
Pinsker for products $\|P_1^n - P_2^n\|_{\mathrm{TV}}^2 \le \frac n2 D_{\mathrm{kl}}(P_2\|P_1)$ .
The second-branch KL display $-\log(1-\delta) \le \delta/(1-\delta) \le 2\delta$ for $\delta \le \frac12$ .

Significance

Theorem 3 shows that the rate $n^{-1/(k_* \vee 2)}$ of the paper's concentration bound for the plug-in robust risk cannot be improved by any estimator, even when the data take only two values. For $k < 2$ the robust risk is therefore intrinsically harder to estimate than a mean: its value depends on how much mass $P_0$ puts on rare large values, and rare events are observed rarely. The same phenomenon drives the paper's lower bounds for minimizing the robust risk (its Section 5.2), which are not part of this mission.

The result is proved in the paper; no machine-checked version of it or of Lemma 12 is known. Formalizing it produces a verified two-point analysis of the Cressie–Read robust risk (Lemma 12 and its primal formula), which is reusable for any lower bound or worked example involving $f$ -divergence balls, and a verified finite-sample Le Cam two-point bound for estimating a functional of a distribution on two points. It also corrects a constant in the first branch of the printed statement.

Difficulty

The lower bound needs two distributions on $\{0,M\}$ that are statistically close yet have well-separated robust risks. Both requirements must be quantitative and must hold simultaneously at the stated constants. The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so the separation needs exact control of that supremum for two-point laws: an exact value above the threshold $p_k$ , and matching upper and lower bounds below it. For mass near $p_k$ the separation is linear in $\delta$ , while for small mass it is of order $\delta^{1/k_*}$ , which is where the slow rate comes from. Closeness requires the KL divergence of each pair to be at most $1/(2n)$ , and the two branches need different perturbations. A naive bound on the robust risk by $\max(z_0, z_1)$ or by the mean gives no separation at all.

Formalization scope

The Lean development lives in the namespace UniformDRO.LowerBound. Its conventions are:

$k > 1$ , $\rho > 0$ , $M > 0$ (all on the page); $n \ge 1$ in the goal (implicit on the page, since the bound contains $1/n$ ).
The robust risk is the real supremum in the likelihood-ratio form above, with the divergence constraint written as a lower Lebesgue integral of $f_k(L) \ge 0$ . Absolute continuity $Q \ll P$ is built in. For a two-point law the feasible values lie between the two points, so the supremum is genuine.
Laws on $\{0,M\}$ are $(1-p)\delta_0 + p\,\delta_M$ , $p \in [0,1]$ . Expectations under $P_0^n$ are finite sums over $\{0,M\}^n$ . The minimax risk takes values in $[0,\infty]$ , with the infimum over all real functions of the sample taken outside the supremum over $p$ . For these laws it agrees with the platform's general HighDimStat.Minimax.minimaxRisk.
$D_{\mathrm{kl}}$ between two-point laws is the platform's BanditAlgorithm.bernoulliRelativeEntropy, always evaluated with a second argument in $(0,1)$ , where it is the true divergence.
Real powers are Real.rpow. The primal formula is stated for $p \in (0,1)$ , where its negative powers are finite.
Correction of the print. In Theorem 3 the page has $\sqrt{p_k(1-p_k)/(8n)}$ . The paper's argument with that choice gives $D_{\mathrm{kl}} \le 1/n$ and, by Pinsker, total variation at most $1/\sqrt2$ , which does not yield the printed constant $1/(8k_*p_k)$ . The target uses $16n$ , for which the same argument gives total variation at most $\tfrac12$ and exactly the printed constant. The second branch is as printed. The milestone quotes keep the page's text.

The goal is the lower bound on the minimax risk (16) over all estimators and all laws on $\{0,M\}$ . It does not mention the two hypotheses, $\delta$ , total variation or KL divergence, so it cannot be satisfied by a statement about a particular pair of laws or a particular estimator.

Contributions are welcome at every level: proofs of Lemma 12 through the primal formula or through the dual representation of the robust risk, a general finite-space Le Cam lemma, and tensorization of KL and Pinsker for finite products, which are reusable beyond this mission.

Selected references

J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization, Ann. Statist. 49(3), 2021; arXiv:1810.08750v6. https://arxiv.org/abs/1810.08750, https://doi.org/10.1214/20-AOS2004
L. Le Cam, Asymptotic Methods in Statistical Decision Theory, Springer, 1986. https://doi.org/10.1007/978-1-4612-4946-7
B. Yu, Assouad, Fano, and Le Cam, in Festschrift for Lucien Le Cam, Springer, 1997, 423–435. https://doi.org/10.1007/978-1-4612-1880-7_29
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
N. Cressie and T. R. C. Read, Multinomial goodness-of-fit tests, J. R. Stat. Soc. B 46(3), 1984, 440–464. https://doi.org/10.1111/j.2517-6161.1984.tb01318.x

13 thms3 active usersReviewed

Completed

Functional Analysis Markov Chain Probability·Captain: mikedeng1

Logarithmic Sobolev Inequalities for Finite Markov Chains 2: Entropy Decay Ent_π(μH_t) ≤ e^{−2αt} Ent_π(μ), Improved to e^{−4αt} for Reversible ChainsResearch Paper

Motivation

How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap $\lambda$ , which controls convergence in $\ell^2(\pi)$ but loses a factor $1/\pi(x)$ when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant $\alpha$ , introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.

The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate $2\alpha$ , and at rate $4\alpha$ for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$ . Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$ , with $\pi(x)>0$ for every $x$ . Functions act on the right, $Kf(x)=\sum_yK(x,y)f(y)$ , and $\langle f,g\rangle=\sum_xf(x)g(x)\pi(x)$ is the inner product of $\ell^2(\pi)$ , with norms $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$ . The chain is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all $x,y$ .

The continuous-time heat semigroup is

H_t=e^{-t(I-K)}=e^{-t}\sum_{n\ge0}\frac{t^n}{n!}K^n,

acting on functions by $H_tf(x)=\sum_yH_t(x,y)f(y)$ and on probability measures by $\mu H_t(y)=\sum_xH_t(x,y)\mu(x)$ . The row $H_t^x=H_t(x,\cdot)$ is the law at time $t$ of the chain started at $x$ .

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$ ; it is bilinear but not symmetric unless the chain is reversible. With

\mathcal L(f)=\sum_x|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),

the log-Sobolev constant is

\alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.

The relative entropy of a probability $\mu$ is $\mathrm{Ent}_\pi(\mu)=\sum_x\mu(x)\log\frac{\mu(x)}{\pi(x)}$ , and the total variation distance is $\|\mu-\pi\|_{TV}=\sup_{A\subset\mathcal X}|\mu(A)-\pi(A)|$ .

Formalization targets

Goal: Theorem 3.6 (p. 722)

For every probability measure $\mu$ on $\mathcal X$ ,

\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-2\alpha t},\qquad t>0,

and, if $(K,\pi)$ is reversible,

\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-4\alpha t},\qquad t>0.

Milestones

§2.1, Remarks (ii), p. 702: if $\mu=f\pi$ then $\mu H_t$ has density $H_t^*f$ , where $H_t^*$ is the semigroup of the adjoint kernel $K^*(x,y)=K(y,x)\pi(y)/\pi(x)$ .
Lemma 2.5, second part, p. 707: $\partial_t\,\mathrm{Ent}_\pi(H_tf)|_{t=0}=-\mathcal E(f,\log f)$ .
Lemma 2.7, p. 708: $\mathcal E(\log f,f)\ge2\,\mathcal E(\sqrt f,\sqrt f)$ , and $\ge4\,\mathcal E(\sqrt f,\sqrt f)$ for reversible chains.
§3.3, p. 722: for $f\ge0$ with $\|f\|_2=1$ and $\mu=f^2\pi$ , $\mathcal L(f)=\mathrm{Ent}_\pi(\mu)$ .
(2.8), p. 710: $2\|\mu-\pi\|_{TV}^2\le\mathrm{Ent}_\pi(\mu)\le\|\mu-\pi\|_{TV}+\tfrac12\|\mu/\pi-1\|_{\pi,2}^2$ .

Companion: (3.3) (p. 723)

For an irreducible chain, every $x$ and $t>0$ ,

2\|H_t^x-\pi\|_{TV}^2\le\Big(\log\frac1{\pi(x)}\Big)e^{-2\alpha t},

with $2\alpha$ replaced by $4\alpha$ for reversible chains.

Significance

Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor $\log(1/\pi(x))$ replaces the factor $1/\pi(x)$ of the spectral bound $4\|H_t^x-\pi\|_{TV}^2\le\pi(x)^{-1}e^{-2\lambda t}$ . When $\pi(x)$ is exponentially small in the size of the problem, as for random walks on large groups or product spaces, $\log(1/\pi(x))$ is polynomial where $1/\pi(x)$ is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from $\alpha$ .

The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of $\mathcal E(\log f,f)$ with $\mathcal E(\sqrt f,\sqrt f)$ , and Pinsker's inequality in the encoding used by the mixing-time library.

Difficulty

The statement is about measures, while the natural quantities to differentiate are densities with respect to $\pi$ , and for a nonreversible chain the density of $\mu H_t$ evolves under the adjoint semigroup, not under $H_t$ . The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from $2\alpha$ to $4\alpha$ holds only under reversibility.

The obvious first idea, differentiating $\mathrm{Ent}_\pi(\mu H_t)$ term by term, meets $\log 0$ wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary $t=0$ and the degenerate laws separately from the smooth interior. The constant $\alpha$ is defined as an infimum over all functions, with no claim that it is attained or positive.

Formalization scope

The state space is a Fintype with decidable equality, $K$ is a real matrix with the published predicate MarkovMixing.IsStochastic, $\pi$ satisfies MarkovMixing.IsStationary K π and $\pi(x)>0$ for all $x$ , and reversibility is MarkovMixing.DetailedBalance K π. $H_t$ is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for $t>0$ .

The local definitions are $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$ , the norms $\|f\|_p$ , $\mathcal L$ , $\alpha$ as a real infimum over the ratios with $\mathcal L(f)\ne0$ , $\mathrm{Ent}_\pi(\mu)$ , and $\mu H_t$ as the row vector $\mu\,H_t$ . Lean's Real.log 0 = 0 implements $0\log0=0$ . The goal does not assume irreducibility: it is true for every stochastic $K$ with a positive invariant probability, and a reducible chain has $\alpha=0$ . The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's $f\ge0$ is strengthened to $f>0$ , because $\log f$ is $-\infty$ at a zero of $f$ on the page and $0$ in Lean.

Several encodings would make the goal trivially true and are ruled out. $\alpha$ is not assumed positive. $\mu$ is a probability, since for $\mu=2\pi$ the entropy is a positive constant in $t$ . $\pi$ is invariant and positive, so $\mu/\pi$ is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying $H_t$ to $\mu$ as a function, $H_t\mu$ , is not the same as $\mu H_t$ for a nonreversible chain.

A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property $\partial_tH_t=(K-I)H_t$ ; the adjoint identity for $H_t$ ; elementary convexity inequalities for $\log$ and $\sqrt{\cdot}$ ; the symmetric form of $\mathcal E$ for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.

Selected references

P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6 (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97 (1975), 1061–1083. https://doi.org/10.2307/2373688
D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. https://doi.org/10.1090/mbk/107

14 thms3 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Fast Rates for Support Vector Machines Using Gaussian Kernels 1: Under Tsybakov and Geometric Noise, Gaussian-Kernel SVMs Reach Excess Risk Cx²n^{−β+ε} with Probability 1 − e^{−x}Research Paper

Motivation

Support vector machines classify observations by choosing a real-valued function from a reproducing kernel Hilbert space and using its sign as the predicted label. The Gaussian kernel is widely used because it gives a flexible class of functions, but that flexibility alone does not explain how quickly classification error approaches the best possible error as the training sample grows. Steinwart and Scovel's 2007 paper identifies distributional conditions under which a Gaussian-kernel SVM achieves a polynomial, and sometimes nearly linear, excess-risk rate. The conditions describe both ambiguity in the labels and the location of data relative to the decision boundary.

The article's result is already proved mathematically. This mission asks for machine-checked statements and proofs of its finite-geometric-exponent, no-offset rate and selected supporting results. It uses arXiv:0708.1838v1, the electronic reprint of the Annals of Statistics article. Its printed page number equals its PDF page number throughout; all page references below use those numbers.

Setting

Let $X$ be the closed unit ball of $\mathbb R^d$ , where $d>0$ , and let the label set be $Y=\{-1,1\}$ . A distribution $P$ on $X\times Y$ has input marginal $\mu=P_X$ and a measurable regression function $\eta(x)=P(y=1\mid x)$ . In the Lean representation, $\mu$ and one version of $\eta$ are carried explicitly; the joint law gives conditional masses $\eta(x)$ and $1-\eta(x)$ to the two labels. Classification predicts $\operatorname{sign}f(x)$ , with $\operatorname{sign}(0)=1$ . Write $R_P(f)$ for its error probability and $R_P$ for the smallest such risk over measurable decision functions.

The hinge loss is $\ell(y,t)=\max\{0,1-yt\}$ . The Gaussian kernel with parameter $\sigma>0$ is $k_\sigma(x,x')=\exp(-\sigma^2\|x-x'\|^2)$ , and $H_\sigma(X)$ is its restricted RKHS. Given a sample $T$ of size $n$ , an SVM without offset minimizes $\lambda\|f\|^2_{H_\sigma(X)}+R_{\ell,T}(f)$ over that space. The approximation error $a_\sigma(\lambda)$ is the infimum of the corresponding population objective minus the unrestricted Bayes hinge risk; equation (6) uses that unrestricted baseline.

Two assumptions describe the distribution. It has Tsybakov noise exponent $q\in[0,\infty]$ if, for sufficiently small $t>0$ , $\mu\{|2\eta-1|\le t\}\le C t^q$ for some $C>0$ . To define geometric noise exponent $\alpha>0$ , partition $X$ according to whether $\eta$ is below, above, or equal to $1/2$ . The distance $\tau_x$ goes from a point in either strict class to the opposite strict class together with the equal-probability class. The geometric condition is

\int_X |2\eta(x)-1|\exp(-\tau_x^2/t)\,d\mu(x) \le C t^{\alpha d/2}\qquad(t>0).

These are Definitions 2.2 and 2.3 and equation (7) of the paper.

Formalization targets

The goal is the finite- $\alpha$ , no-offset clause of Theorem 2.8. With the paper's two-case exponent $\beta=\beta(\alpha,q)$ , set $\lambda_n=n^{-(\alpha+1)\beta/\alpha}$ and $\sigma_n=n^{\beta/(\alpha d)}$ . For every $\varepsilon>0$ , one constant $C>0$ works uniformly for $x\ge1$ and $n\ge1$ :

\Pr^*\!\left\{T:R_P(f_{T,\lambda_n}) \le R_P+C x^2n^{-\beta+\varepsilon}\right\}\ge1-e^{-x}.

Here $\Pr^*$ is outer probability, and the statement applies to every empirical minimizer. The formula for $\beta$ is $\alpha/(2\alpha+1)$ in the first case, $\alpha\le(q+2)/(2q)$ , and $2\alpha(q+1)/(2\alpha(q+2)+3q+4)$ otherwise; the paper's limiting convention specifies $q=\infty$ .

Three milestones record results used on this path. Theorem 2.1 bounds empirical covering numbers of Gaussian RKHS balls, uniformly in $\sigma$ and the sample. Lemma 4.1 locates balls of radius $\tau_x$ inside the corresponding enlarged decision class. Theorem 2.7 bounds the approximation error by

a_\sigma(\lambda)\le c_d\bigl(\sigma^d\lambda+C(2d)^{\alpha d/2}\sigma^{-\alpha d}\bigr),

where $c_d$ depends only on dimension. Their exact source text and page positions appear in the milestone list.

Significance

Theorem 2.8 gives a quantitative guarantee for classification risk, rather than only convergence of the regularized hinge objective. The rate responds to both the label-noise exponent and the concentration of input mass near the decision boundary. In the regimes discussed after the theorem, the exponent can approach one; the paper's Remark 2.9 compares it with the $n^{-1/2}$ benchmark.

Formalizing this result adds a concrete Gaussian RKHS norm compatible with a kernel parameter that changes with $n$ , an explicit binary-law model, extended-valued risks and covering numbers, and source-indexed bounds on approximation and complexity. Those objects can be reused in later SVM and kernel-learning statements. The paper's argument is a published proof; the Lean theorem files here are open proof obligations, while the definition files have compiled bodies. No claim of a machine-checked proof of the rate is made.

Difficulty

It is not enough to combine a general consistency theorem with the noise assumptions. The kernel parameter grows with sample size, so the relevant hypothesis class changes with $n$ ; a complexity estimate for one fixed class gives no uniform rate. Geometric noise controls approximation error, while Tsybakov noise controls a different fluctuation quantity, and neither by itself supplies the stated exponent. The probability statement also concerns an event defined by empirical minimizers, whose measurability the source deliberately avoids by using outer probability. These are the points at which a direct fixed-class or ordinary-probability statement would fail to match Theorem 2.8.

Formalization scope

Lean represents functions on all of $\mathbb R^d$ but uses only their restrictions to $X$ . The joint distribution is built from a probability marginal and a fixed measurable $\eta:\mathbb R^d\to[0,1]$ . This makes the paper's choice of regression-function version explicit. The Gaussian RKHS squared norm is the supremum over finite normalized kernel-section combinations; it is $+\infty$ outside the RKHS. A covering number is the least positive finite cardinality of a cover with centers in the ambient empirical function space, or $+\infty$ if there is no such cover. Hinge and classification risks are extended nonnegative integrals, and Bayes risks range over measurable functions.

The assumptions $d>0$ and $n\ge1$ give the divisions and powers their intended domains. For $q=\infty$ , the small- $t$ noise bound uses zero on the right, as in the source convention. The paper leaves distance to an empty set unstated; this mission pins $d(x,\varnothing)=0$ . With the infinite-distance convention, Lemma 4.1 and Theorem 2.7 fail for a one-class regression function. The proof display (25) has a volume-factor slip in high dimension; Theorem 2.7 is stated with its printed conclusion, and the issue is recorded in the moderation notes. The goal event includes existence of an empirical minimizer, a fact stated in the paper's setup, and quantifies over every minimizer. This excludes a vacuous SVM predicate. The constant $C$ is chosen before $x$ and $n$ .

The clauses for $\alpha=\infty$ and an SVM with offset are outside this mission. The separate series mission addresses the implication from an envelope assumption to geometric noise. Further contributions toward the §5 empirical-process estimates, §6 variance estimates, and §7 shrinking and general-rate theorems are welcome; they are not asserted as milestones in this draft.

Selected references

Ingo Steinwart and Clint Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 2007, 575–607. arXiv:0708.1838v1, DOI:10.1214/009053606000001226.

11 thms3 active usersReviewed

Bandit Algorithms Operations Research Stochastic Systems·Captain: mikedeng1

On the Gittins Index for Multiarmed Bandits 2: A Policy Falls Short of the Gittins Policy by at Most Its Expected Discounted Gap Between the Greatest Gittins Index and That of the Bandit It PlaysResearch Paper

Motivation

The multiarmed bandit problem asks how to allocate a single resource, one play at a time, among several alternative projects whose states evolve only when they are worked on. It models the scheduling of jobs on a single machine, the design of sequential clinical trials and many problems of research planning. Gittins and Jones showed that it is optimal to play, at each time, a project of greatest Gittins index, a number computed from that project alone (Gittins and Jones 1974; Gittins 1979).

In practice the Gittins index policy is often replaced by a heuristic: indices are computed approximately, or a policy is constrained by operational rules. A practitioner then needs to know how much value is lost. R. Weber's paper On the Gittins index for multiarmed bandits (Ann. Appl. Probab. 1992) gives a short proof of the index theorem through prevailing charges, and in its Section 5 derives from it two suboptimality bounds. This mission formalizes the second of them, Theorem 3, which bounds the loss of an arbitrary policy using Gittins indices only.

Timeline. Gittins and Jones (1974) and Gittins (1979) prove optimality of the index policy by an interchange argument; Whittle (1980) gives a proof by retirement options; Glazebrook (1982) bounds the suboptimality of policies in terms of Gittins indices, the bound Weber calls "usually weaker than (6)"; Glazebrook (1990) gives the prevailing-charge bound that is Weber's Theorem 2; Weber (1992) proves the index theorem by prevailing charges and states Theorems 2–4.

Setting

There are $k$ bandit processes. Bandit $i$ has a state $x_i(t)$ in a state space $S$ ; at each epoch $t = 0, 1, 2, \dots$ the gambler plays one bandit $j(t)$ , receives a reward with mean $r(x_{j(t)}(t))$ , the state of bandit $j(t)$ moves according to a Markov transition kernel $P$ , and the states of all other bandits are unchanged. Rewards are nonnegative and uniformly bounded, and $0 < \beta < 1$ is a discount factor. A policy $\pi$ chooses $j(t)$ , possibly at random, as a function of everything observed so far. Its value from the initial state vector $x$ is the expected total-discounted reward

V_\pi(x) = E_\pi\Big[\sum_{t=0}^\infty \beta^t r\big(x_{j(t)}(t)\big) \,\Big|\, x(0) = x\Big]. \tag{1}

The fair charge $\gamma(y)$ of a state $y$ is the largest ratio of expected discounted reward to expected discounted time that a stopping time $\tau \ge 1$ of a single bandit started at $y$ can achieve,

\gamma(y) = \sup_{\tau \ge 1} \frac{E\big[\sum_{t=0}^{\tau-1}\beta^t r(x(t)) \mid x(0)=y\big]}{E\big[\sum_{t=0}^{\tau-1}\beta^t \mid x(0)=y\big]},

and Weber's Gittins index is $G(y) = \gamma(y)/(1-\beta)$ . A Gittins index policy $\pi^*$ plays, at every epoch, a bandit with the greatest index, ties broken arbitrarily. Theorem 1 of the paper, already formalized on Prove2Me as BanditAlgorithm.gittins_index_theorem, states that every Gittins index policy maximizes $V_\pi(x)$ .

The model, the fair charge and the Gittins index policy are the published GittinsIndex definitions of Shuze Chen, and the history truncation used to write round expectations is from Harry_Xu's GittinsTerminalPotential.

Formalization targets

Goal: Theorem 3

For a Gittins index policy $\pi^*$ , every policy $\pi$ and every initial state vector $x$ ,

V_{\pi^*}(x) - V_\pi(x) \le E_\pi\left[\sum_{t=0}^\infty \beta^t\Big(\max_i G_i\big(x_i(t)\big) - G_{j(t)}\big(x_{j(t)}(t)\big)\Big) \,\middle|\, x(0)=x\right]. \tag{7}

The right-hand side is computed along the trajectory of $\pi$ alone: in each epoch it charges the gap between the greatest index and the index of the bandit $\pi$ actually plays.

Milestones

The proof compares, for each $t$ , two policies built from $\pi$ : $\pi^*(t)$ , identical to $\pi$ before time $t$ and a Gittins index policy from $t$ on, and $\pi(t)$ , identical to $\pi$ up to and including time $t$ , which then continues playing $j(t)$ until its fair charge drops below its value at time $t$ and is a Gittins index policy thereafter.

Switching to Gittins later never hurts. If $\sigma'$ is identical to $\sigma$ through time $t$ and a Gittins index policy from $t+1$ on, then $V_\sigma(x) \le V_{\sigma'}(x)$ ; in particular $V_{\pi(t)}(x) \le V_{\pi^*(t+1)}(x)$ .
Equation (8).

V_{\pi^*(t)}(x) - V_{\pi(t)}(x) \le \beta^t E_\pi\left[\frac{\max_i \gamma_i(x_i(t)) - \gamma_{j(t)}(x_{j(t)}(t))}{1-\beta} \,\middle|\, x(0)=x\right].

Significance

The result. Theorem 3 turns any per-epoch guarantee about the index of the bandit played into a guarantee on value. If a policy always plays a bandit whose Gittins index is within $\varepsilon$ of the greatest, it loses at most $\varepsilon/(1-\beta)$ ; this is the form in which index heuristics, approximate index computations and constrained index policies are analysed. The open Prove2Me goal AllocationIndices.eps_index_policy_near_optimal (Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices, Theorem 4.18, after Glazebrook 1982) is a bound of this kind for $\varepsilon$ -index policies and follows from (7); it is a separate item and is not part of this mission. Unlike Theorem 2 of the same paper, the bound (7) involves only Gittins indices, not prevailing charges or rewards.

Formalizing it. Theorem 3 is proved in the paper; no machine-checked proof exists. The mission produces a formal statement of the bound on top of the published Markov bandit model and Theorem 1, together with the two intermediate statements of Weber's proof, which have uses of their own: optimality of switching to the index policy after any finite prefix of play is the dynamic-programming form of the index theorem.

Difficulty

The informal proof is half a page, and its key sentence is that the difference of the charges paid by $\pi^*(t)$ and $\pi(t)$ at any later time is never more than the gap at time $t$ . Making it rigorous requires the value-to-go of a history-dependent randomized policy after a fixed time, the fact that both policies from time $t$ on are fair games in which expected discounted reward equals expected discounted charge, and a pathwise comparison of two interleavings of charge sequences. The naive reading, that $\pi(t)$ loses only the single epoch $t$ , is wrong: playing $j(t)$ at time $t$ commits the policy to a whole run of $j(t)$ , and the bound accounts for the entire run through the factor $1/(1-\beta)$ . Telescoping (8) over $t$ also needs $V_{\pi^*(t)}(x) \to V_\pi(x)$ as $t \to \infty$ , which rests on bounded rewards and $\beta < 1$ .

Formalization scope

The Lean development uses the published BanditAlgorithm model, in which all bandits share one state space $S$ (a standard Borel space), one kernel $P$ and one reward $r$ ; Weber's bandits with different state spaces are encoded by taking the disjoint union. Time is 0-indexed in both. The committed readings of the paper's phrases are:

" $\pi^*$ is the optimal (Gittins) policy" is any policy satisfying IsGittinsIndexPolicy; it is not assumed to be built from $\pi$ .
$R_j(x_j(t))$ is represented by its conditional mean $r(x_j(t))$ , and " $E_\pi[\sum_t \beta^t \cdots]$ " by the series of per-epoch expectations $\sum_t \beta^t E_\pi[\cdots]$ , the published value convention.
The index in (7) is $G = \gamma/(1-\beta)$ (weberIndex), and (8) is written with $\gamma$ (gittinsIndex) divided by $1-\beta$ , as on the page.
$\pi^*(t)$ and $\pi(t)$ are predicates on a policy (IsSwitchToGittinsAt, IsRunThenGittinsAt), and (8) is stated for every pair of policies satisfying them. "Identical to $\pi$ for times less than $t$ " is rounds $n < t$ ; "plays $j(t)$ at time $t$ " and "identical through time $t$ " are rounds $n \le t$ . "Drops below" is strict.
The standing assumptions of Section 1 (nonnegative, uniformly bounded rewards and $0<\beta<1$ ) are hypotheses of every theorem, as are measurability of $r$ and of $y \mapsto \gamma(y)$ , which the paper takes for granted.

Using the fair charge $\gamma$ in place of $G$ in (7) would make the bound false by the factor $1-\beta$ ; dropping the measurability of $\gamma$ would let the expectation degenerate to $0$ and make the bound claim that every policy is optimal. Neither is the statement posed here, and a constant-index or one-armed instance, where both sides vanish, only checks that the hypotheses are satisfiable.

Theorem 1 is referenced, not posed. Theorem 2 (the prevailing-charge bound) and Theorem 4 (submodularity of the optimal value in the set of bandits) are missions 1 and 3 of this series; this mission does not depend on them. Weber's definition of an index consistent policy (p. 1028) is not formalized here: the proof of (8) needs the fair-game property in the form of Remark 2 (continue while the fair charge exceeds the prevailing charge), which differs from the definition's "initial value" after an interruption. Contributions welcome: a measurable greatest-index selection, value-to-go decompositions for history-dependent policies, and the fair-game identity for index-consistent play are reusable beyond this mission.

Selected references

R. Weber, On the Gittins index for multiarmed bandits, The Annals of Applied Probability 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
K. D. Glazebrook, Procedures for the evaluation of strategies for resource allocation in a stochastic environment, Journal of Applied Probability 27, 215–220, 1990.
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 241–266, 1974.
P. Whittle, Multi-armed bandits and the Gittins index, Journal of the Royal Statistical Society B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19, 716–722, 1982.
J. C. Gittins, K. D. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

8 thms3 active usersReviewed

Completed

Bandit Algorithms Dynamic Programming Operations Research+1·Captain: mikedeng1

A Short Proof of the Gittins Index Theorem: For Finite-State Semi-Markov Bandits, Every Priority Policy Ordering States by the Index Algorithm's Indices Is OptimalResearch Paper

Motivation

The multi-armed bandit problem with discounted rewards asks how to allocate effort among $n$ independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an $n$ -dimensional dynamic program into $n$ one-dimensional computations.

Several proofs followed, each with its own model and its own definition of the index:

Gittins and Jones (1974) and Gittins (1979): the original interchange proofs, with the index as a supremum over stopping times of a reward-to-time ratio.
Whittle (1980): a proof through the retirement option and the dynamic-programming equation of the multi-armed problem.
Varaiya, Walrand and Buyukkoc (1985): the largest-remaining-index algorithm for finite-state Markov bandits, which computes the indices by removing states one at a time.
Weber (1992): the "prevailing charge" proof.
Tsitsiklis (1994): the short proof formalized here, for semi-Markov bandits with finite state spaces, by induction on the total number of states, with the indices produced by an index algorithm of the largest-remaining-index type.

Setting

There are $n\ge1$ bandit processes. Bandit $i$ has a finite nonempty state space $\mathcal X_i$ , and $\mathcal X=\mathcal X_1\cup\cdots\cup\mathcal X_n$ is their disjoint union. When bandit $i$ at state $x\in\mathcal X_i$ is played, a random reward $R(x)$ is received, the bandit is busy for a random time $T(x)\ge0$ , and it then moves to a random state $Y(x)\in\mathcal X_i$ ; the other bandits do not move. The joint law of $(T(x),R(x),Y(x))$ depends only on $x$ , and different plays are independent.

A policy is a map $\pi:\mathcal X_1\times\cdots\times\mathcal X_n\to\{1,\dots,n\}$ : at time zero and at every play completion time it chooses the bandit to play from the current states. With $t_i$ the start time and $R_i$ the reward of the $i$ -th play and a discount rate $\beta>0$ , the expected discounted reward from the initial joint state $z$ is

J_\pi(z)=\mathbb E\Big[\sum_{i=1}^{\infty}R_i e^{-\beta t_i}\Big].

A policy is optimal if it maximizes $J_\pi(z)$ for every initial state $z$ . A priority rule is a policy for which some ordering of $\mathcal X$ makes it always play the bandit whose current state is ordered highest.

The reward rate of a state is

r(x)=\frac{\mathbb E[R(x)]}{\mathbb E\big[\int_0^{T(x)}e^{-\beta t}\,dt\big]}. \tag{2.1}

Reducing bandit $i^*$ by removing a state $s^*$ merges every play that ends in $s^*$ with the following run of plays at $s^*$ into one composite play, whose reward rate is $\hat r(x)$ of (2.3). The index algorithm repeatedly picks a state $s^*$ of maximal current rate, sets its index $\gamma(s^*)$ to that rate, and reduces its bandit by removing $s^*$ (or removes the bandit if $s^*$ was its last state).

Formalization targets

Goal: Theorem 2.2

Let $\gamma$ be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies

\gamma(y)<\gamma(x)\ \Longrightarrow\ y \text{ is ordered below } x

is optimal. Ties in $\gamma$ may be ordered either way, and the run may break ties in its own choices arbitrarily.

Milestones, in the order the proof uses them

(2.2), the interchange inequality $\mathbb E\big[(1-e^{-\beta\tau})\int_0^{T(s^*)}r(s^*)e^{-\beta t}dt\big]\ge\mathbb E\big[(1-e^{-\beta T(s^*)})\int_0^{\tau}\bar r(t)e^{-\beta t}dt\big]$ when $\bar r\le r(s^*)$ .
Lemma 2.1: if $r(s^*)=\max_{x}r(x)$ , some optimal policy always plays bandit $i^*$ when it is at $s^*$ .
Reduction step: optimizing within the policies giving $s^*$ top priority is a bandit problem with one state fewer, the reduced bandit with rates (2.3).
Theorem 2.1: some priority rule is optimal.
Pick-order optimality: a priority rule that orders the states as a run of the index algorithm picks them is optimal.
Index monotonicity: along a run, $\gamma(s^*)\ge\gamma(q^*)$ for consecutive picks $s^*,q^*$ .
Picked-before characterization: $x$ can be picked before $y$ (in a run with the same indices) if and only if $\gamma(x)\ge\gamma(y)$ .

Significance

The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the $c\mu$ rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.

The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.

Difficulty

Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.

Formalization scope

Bandits are indexed by Fin n ( $0,\dots,n-1$ ), with $n\ge1$ and each state type finite and nonempty. $\mathcal X$ is the sigma type Σ i, X i, disjoint by construction.
The law of $(T(x),R(x),Y(x))$ is a probability measure on $\mathbb R\times\mathbb R\times\mathcal X_i$ with $T\ge0$ almost surely and $R$ integrable. The model also assumes $\mathbb P(T(x)>0)>0$ , which the page leaves implicit: it makes the denominator of (2.1) nonzero.
$J_\pi$ is computed from the moments $\mathbb E[R(x)]$ and $D(x,y)=\mathbb E[e^{-\beta T(x)};Y(x)=y]$ : it is the limit of the expected discounted reward of the first $k$ plays, given by the first-step recursion. No path space is constructed. The row sums of $D$ are below $1$ , so the limit exists; it never mentions rates, indices or reductions.
Policies are the paper's stationary deterministic maps of the current joint state, and optimality is within that class, for every initial state. An ordering of $\mathcal X$ is an injective ranking into $\mathbb N$ .
The reduced bandit is given by explicit formulas for its expected discounted reward, discounted duration and discounted transition data. These make the page's "transition probabilities are suitably modified" concrete, and the reduced rate is (2.3). Removing a bandit is the reduction of its last state.
The index is that of any run of the index algorithm, with arbitrary tie choices.

A formalization in which the value of a policy is defined through rates or indices, or in which $\gamma$ is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.

Needed infrastructure: the convergence of the $k$ -play values and the first-step (Bellman) equation for $J_\pi$ ; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.

Selected references

J. N. Tsitsiklis, A Short Proof of the Gittins Index Theorem, Annals of Applied Probability 4(1) (1994), 194–199.
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 1974, 241–266.
J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
P. Whittle, Multi-armed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42 (1980), 143–149. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
P. P. Varaiya, J. C. Walrand and C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30 (1985), 426–439. https://doi.org/10.1109/TAC.1985.1103989
R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4) (1992), 1024–1033. https://doi.org/10.1214/aoap/1177005588

11 thms3 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes IV: Critical-Level Ordering at Nondecreasing Myopic Levels ȳₘ Is OptimalResearch Paper

Motivation

A firm with one product may face several customer classes in each selling interval. When stock is scarce, it must decide which outstanding demands to satisfy and how much inventory to carry into later intervals. When new stock can be bought at several dates, the rationing choice also changes the value of future purchasing opportunities. Topkis studied these linked decisions in a nonstationary model with class-dependent shortage penalties and a finite number of ordering periods. His Theorem 4 identifies conditions under which a policy computed from each period's myopic cost is optimal in the full multiperiod problem Topkis 1968.

The result belongs to a line of work on critical-level policies: choose a stock target and order up to it if current stock is lower. Here the target can be computed one period at a time despite the possibility of future purchases and the separate question of how to ration stock among demand classes. The paper attributes a related myopic policy result to Veinott and explains that its own setting allows a more general rationing policy than the special zero-rationing-level case discussed there Topkis 1968, pp. 175–176. This mission formalizes Topkis's multiperiod statement, including its ordering and rationing conclusions.

Setting

There are $N$ ordering periods, numbered $1$ through $N$ . Period $m$ has a unit purchase cost $c_m$ . It contains $k_m$ selling intervals, numbered backward: interval $k_m$ is first and interval $1$ is last. Within an interval, a random nonnegative demand vector has one component for each of $n$ customer classes. The vectors in distinct intervals and periods are independent and each class has a finite mean. At the start of an interval the demand is observed. A decision then selects how much of each class's outstanding demand to leave unsatisfied. The remaining physical stock incurs a holding cost, and each unsatisfied unit incurs a class-specific penalty. Unsatisfied demand is either carried entirely to the next interval or lost entirely, according to the interval. Penalties are nonnegative and rise with class index, so class $n$ has the highest shortage penalty Topkis 1968, pp. 162–163, 174.

Let $w$ be net stock before ordering at the start of period $m$ : physical stock minus outstanding backlogs. The order must clear the backlog, so the post-order stock $z$ satisfies $z\ge w^+=\max(w,0)$ . After period $N$ , a further unit can be purchased for $c_{N+1}\ge0$ , while unused stock can be salvaged for revenue $v\le c_{N+1}$ . The terminal cost is $C_{N+1}(w)=(c_{N+1}-v)w^+$ . Working backward, $C_m(w)$ is the optimal continuation cost, including the period- $m$ ordering decision. The actual period cost $\widetilde g^m(z)$ includes the later continuation value $C_{m+1}$ , and equation (19) reads

C_m(w)=\inf_{z\ge w^+}\widetilde g^m(z).

The single-period cost $g^m(z)$ uses the same demand, holding costs and rationing choices in period $m$ , but replaces the later continuation value by the linear terminal charge $-c_{m+1}y$ . A myopic level $\bar y_m$ is any minimum of $g^m$ on $[0,\infty)$ ; it is $+\infty$ if no such minimum exists. Thus the level need not be the smallest minimum when several stock levels tie Topkis 1968, pp. 174–175.

Formalization targets

Theorem 4: myopic ordering and rationing

Suppose $v=c_{N+1}$ and the selected myopic levels are nondecreasing from period $m$ onward:

\bar y_m\le\bar y_{m+1}\le\cdots\le\bar y_N.

Then $\bar y_m<+\infty$ , and ordering to $w\vee\bar y_m$ minimizes $\widetilde g^m$ over all feasible post-order levels $z\ge w^+$ . If $m<N$ and the stock at the start of period $m$ is at most $\bar y_{m+1}$ , the optimal rationing policy during that period is the optimal policy for its single-period problem, calculated with terminal costs $v_1\equiv0$ and $v_2(y)=-c_{m+1}y$ Topkis 1968, Theorem 4.

The milestones are the paper's regularity claim for $C_m$ and $\widetilde g^m$ , existence of an actual optimal order-up-to level, finiteness of $\bar y_N$ , the shape of $C_m$ around an optimal level, and the comparison in equation (20). Together these specify the route from the general dynamic program to the myopic target.

Significance

Theorem 4 gives a checkable sufficient condition for replacing a multiperiod ordering computation with a sequence of single-period cost minimizations. It also identifies when the rationing decisions can be obtained from the same single-period model. The stock bound in its rationing clause matters: outside that range, future costs may alter which class demands should be filled now. The result therefore describes both the simplification and its operational domain Topkis 1968, pp. 175–176.

Topkis proved the theorem in 1968; the task here is to produce machine-checked definitions and proofs of that known result. The definitions of feasible rationing, backward value functions, myopic costs and order-up-to levels will also support comparisons with other finite-horizon inventory models. The §1 model is duplicated locally while the four missions for this paper are drafted in parallel, then intended for consolidation into a shared interface.

Difficulty

Convexity alone gives an order-up-to form for the actual cost $\widetilde g^m$ , but it does not identify its minimizing level with a minimum of the simpler cost $g^m$ . The continuation value $C_{m+1}$ depends on all later ordering and rationing decisions. When some unsatisfied demand is lost, the end-of-period net stock can depend on the within-period rationing choice as well. The core issue is therefore to control the difference between the actual and myopic objectives in the stock range relevant to period $m$ Topkis 1968, pp. 174–176. A statement restricted to a preselected rationing rule would miss the theorem's claim about optimality among all feasible decisions.

Formalization scope

Classes are indexed by Fin n; the largest index is the highest penalty class. Intervals and ordering periods use natural numbers with explicit bounds, and intervals retain the paper's backward numbering. Stock, penalties and costs are real. A period's demand vector has a probability law on real vectors supported on the nonnegative orthant, with every coordinate integrable. The §1 dynamic program uses real infima for feasible rationing choices and Bochner integrals for demand expectations. The multiperiod value $C_m$ uses the nonnegative post-order domain $z\ge w^+$ in (19). Its defining infimum is intended to be finite under the paper's assumptions; the regularity and attainment milestones expose the facts that rule out Lean's default value for an unbounded infimum. These functions are used only at $1\le m\le N+1$ , with period costs at $1\le m\le N$ .

The multiperiod standing assumptions require $n>0$ , $N>0$ , and at least one interval per period, matching the paper’s positive counts.

Holding costs and the appropriate terminal costs satisfy the convexity and continuity assumptions of §1. Within each period, backlog multipliers equal $0$ or $1$ . The terminal procurement cost is nonnegative and salvage revenue does not exceed it. Assumption (D′) is encoded as an eventually positive lower bound on the extended-real right derivative of $c_mw+\sum_{i=m}^N\sum_t h_{t,i}(w)-vw$ . The §1 terminal functions used in the period assumptions are the linear functions required by the single-period comparison; their regularity adds no independent restriction. Independence across intervals and periods is built into successive expectations. The goal separately assumes $v=c_{N+1}$ and monotonicity of the selected myopic levels only from $m$ through $N$ .

The formal target compares the actual and single-period sets of optimal rationing decisions at every interval and at every nonnegative state with stock at most $\bar y_{m+1}$ . The stock bound and the full feasible set prevent the claim from becoming a result about a handpicked policy. Contributions to the backward recursion, convexity and attainment facts, and the comparison of these two decision sets are all part of this mission.

Selected references

Donald M. Topkis, Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes, Management Science 15(3), 160–176, 1968. DOI: 10.1287/mnsc.15.3.160.

9 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Primal-dual subgradient methods for convex problems 2: Stochastic Simple Averages Reach E[φ(x̄ₖ)] − φ* ≤ β̂ₖ₊₁(γd(x*) + L²/(2σγ))/(k+1)Research Paper

Motivation

Many decision problems under uncertainty take the form of minimizing an expected cost $\varphi(x) = \mathbb E_\xi f(x, \xi)$ over a convex feasible set, where $\xi$ is a random parameter whose distribution can be sampled but not integrated in closed form. Evaluating $\varphi$ even approximately can cost exponentially many evaluations of $f$ in the dimension of $\xi$ , so the classical deterministic notion of an approximate solution is unusable. A practical alternative, going back to Nemirovski and Yudin, asks for a random output $x$ whose expected objective value is close to the optimum: $\mathbb E\,\varphi(x) - \varphi^* \le \epsilon$ . Stochastic subgradient methods achieve this; Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009)) shows that the same guarantee holds for a stochastic version of his method of simple dual averages, a scheme that aggregates all past subgradients in the dual space instead of taking projected steps with decreasing step sizes.

Dual averaging has since become a standard tool in stochastic and online convex optimization (regularized dual averaging, AdaGrad's primal-dual variant, distributed dual averaging). Section 6 of Nesterov's paper is the original statement of its expected-accuracy guarantee.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ and dual space $E^*$ with dual norm $\|s\|_* = \max\{\langle s, x\rangle : \|x\| \le 1\}$ . Let $Q \subseteq E$ be closed and convex, and let $d$ be a prox-function of $Q$ : continuous on $Q$ and strongly convex on $Q$ with convexity parameter $\sigma > 0$ ,

d(\alpha x + (1-\alpha)y) \le \alpha d(x) + (1-\alpha) d(y) - \tfrac12\sigma\alpha(1-\alpha)\|x-y\|^2,

with prox-center $x_0 = \arg\min_{x\in Q} d(x)$ and $d(x_0) = 0$ . For $\beta > 0$ and $s \in E^*$ the point $\pi_\beta(s) = \arg\min_{x \in Q}\{-\langle s, x\rangle + \beta d(x)\}$ is well defined. The scalar sequence $\hat\beta$ is given by $\hat\beta_0 = \hat\beta_1 = 1$ and $\hat\beta_{i+1} = \hat\beta_i + 1/\hat\beta_i$ for $i \ge 1$ .

The stochastic problem is given by a probability space $(\Xi, \mu)$ and a cost $f : Q \times \Xi \to \mathbb R$ with $\varphi(x) = \mathbb E_\xi f(x,\xi)$ well defined on $Q$ , and a minimizer $x^*$ of $\varphi$ over $Q$ with $\varphi^* = \varphi(x^*)$ . Assumption 1: each $f(\cdot, \xi)$ is convex on $Q$ . Assumption 2: a stochastic oracle returns a subgradient $f'(x, \xi)$ of $f(\cdot, \xi)$ at $x$ , and $\|f'(x,\xi)\|_* \le L$ for all $x \in Q$ , $\xi \in \Xi$ .

The method of stochastic simple averages (SSA, (6.3)) fixes $\gamma > 0$ , starts from $x_0$ and $s_0 = 0$ , and for $k \ge 0$ draws a fresh independent sample $\xi_k \sim \mu$ and sets

s_{k+1} = s_k + f'(x_k, \xi_k), \qquad x_{k+1} = \pi_{\gamma\hat\beta_{k+1}}(-s_{k+1}).

Its deterministic counterpart, the method of simple dual averages (SDA, (2.21)), is the same recursion with arbitrary answers $g_k$ in place of $f'(x_k, \xi_k)$ . The quality of the points $x_0,\dots,x_k$ is measured by the gap $\delta_k(D) = \max\{\sum_{i=0}^k\langle g_i, x_i - x\rangle : x \in Q,\ d(x)\le D\}$ . Write $\boldsymbol\xi_k = (\xi_0, \dots, \xi_k)$ and $\mathbb E_{\boldsymbol\xi_k}$ for the expectation over these $k+1$ independent samples.

Formalization targets

Goal: Theorem 7 (p. 27)

For every $k \ge 0$ ,

\mathbb E_{\boldsymbol\xi_k}\Big(\varphi\Big(\frac{1}{k+1}\sum_{i=0}^k x_i\Big)\Big) - \varphi^* \le \frac{\hat\beta_{k+1}}{k+1}\Big(\gamma\, d(x^*) + \frac{L^2}{2\sigma\gamma}\Big).

Milestones

Theorem 2 (p. 11): for SDA with any answers $g_i$ and $L_k = \max_{i\le k}\|g_i\|_*$ , $\delta_k(D) \le \hat\beta_{k+1}(\gamma D + L_k^2/(2\sigma\gamma))$ for $D \ge 0$ , and, if some $x^* \in Q$ satisfies $\langle g_i, x_i - x^*\rangle \ge 0$ for all $i$ , $\|x_k - x^*\|^2 \le \frac2\sigma d(x^*) + L_k^2/(\sigma^2\gamma^2)$ .
(6.5) (p. 26): along every sample path, $\frac{1}{k+1}\tilde\delta_k(D) \le \frac{\hat\beta_{k+1}}{k+1}(\gamma D + \frac{L^2}{2\sigma\gamma})$ .
Display after (6.5) (p. 26): for $D \ge d(x^*)$ , the gap of a run dominates $\frac1{k+1}\sum_i\langle f'(x_i,\xi_i), x_i - x^*\rangle$ , which dominates $\frac1{k+1}\sum_i[f(x_i,\xi_i) - f(x^*,\xi_i)]$ .
(6.6) (p. 26): $\mathbb E_{\boldsymbol\xi_k}(\frac1{k+1}\delta_k(D)) \ge \frac1{k+1}\sum_i\mathbb E_{\boldsymbol\xi_k} f(x_i,\xi_i) - \varphi^*$ .
p. 27, first display: $\mathbb E_{\boldsymbol\xi_k} f(x_i,\xi_i) = \mathbb E_{\boldsymbol\xi_k}\varphi(x_i)$ for $i \le k$ .
p. 27, display before Theorem 7: $\frac1{k+1}\sum_i\mathbb E\varphi(x_i) \ge \mathbb E\varphi(\frac1{k+1}\sum_i x_i)$ , together with the averaged identity.

Significance

Theorem 7 gives an explicit, non-asymptotic bound on the expected optimality gap of the averaged SSA point. Since $\hat\beta_{k+1} \approx \sqrt{2k}$ , the bound is $O(1/\sqrt k)$ , the optimal rate for nonsmooth stochastic convex optimization with bounded subgradients. Two features distinguish it from the classical stochastic subgradient bound: it holds in an arbitrary norm with a non-Euclidean prox-function (for example the entropy on the simplex with the $\ell_1$ norm), and the feasible set $Q$ need not be bounded, since only $d(x^*)$ enters. The constant is explicit and $\gamma$ can be tuned to $\gamma = L/\sqrt{2\sigma d(x^*)}$ .

The result is proved in the paper; to our knowledge no machine-checked proof of Theorem 7 or of the dual averaging bounds of the paper exists. A formalization yields a reusable verified analysis of dual averaging in a general normed space, a template for expectation bounds over i.i.d. sample paths of an adaptive algorithm, and checked constants.

Difficulty

The pathwise part is a consequence of the deterministic Theorem 2, which itself rests on the general Dual Averaging bound (the companion mission's Theorem 1) and on the strong convexity estimates for $\pi_\beta$ . The probabilistic part looks routine on paper but is where formal arguments break: the iterate $x_i$ is a function of $\xi_0, \dots, \xi_{i-1}$ , and the identity $\mathbb E f(x_i, \xi_i) = \mathbb E\varphi(x_i)$ requires measurability of the whole run and a Fubini argument on the product space. Measurability of the run in turn depends on continuity of the argmin map $\pi_\beta$ , and integrability of $\varphi(\bar x_k)$ and of the gap is not assumed but must be derived from the uniform bound $L$ and the boundedness of the iterates. Pathwise bounds alone do not suffice: (6.5) controls the gap on each sample, not $\varphi(\bar x_k)$ .

Formalization scope

Theorem numbers and page numbers refer to source.pdf, the author's revised CORE discussion-paper version (September 2005) of the Math. Program. article; printed pages equal PDF pages.

$E$ is a finite-dimensional real normed space with an arbitrary norm; $E^*$ is StrongDual ℝ E with the operator norm, and $\langle s, x\rangle$ is s x. Strong convexity is Mathlib's StrongConvexOn Q σ d, which is exactly (1.8); $\sigma > 0$ .
$\pi$ is a map ℝ → StrongDual ℝ E → E with the hypothesis that $\pi_\beta(s)$ lies in $Q$ and minimizes $-\langle s, x\rangle + \beta d(x)$ for every $\beta > 0$ ; no choice function is used.
$\hat\beta$ is defined by recursion with $\hat\beta_0 = \hat\beta_1 = 1$ . The gap is a real supremum over $\mathcal F_D = \{x\in Q : d(x)\le D\}$ , used only for $D \ge 0$ , where the set is nonempty and bounded.
Indices start at 0; $x_0$ is the prox-center. The run is a function of a sample path $\omega : \mathbb N \to \Xi$ ; $\mathbb E_{\boldsymbol\xi_k}$ is the integral against the product measure $\mu^{\otimes(k+1)}$ on $\Xi^{k+1}$ (the law of $k+1$ i.i.d. copies of $\xi$ ), with the finite sample padded to a sequence that the iterates never read.
$f$ and $f'$ are functions on $E \times \Xi$ whose values off $Q$ are irrelevant; the subgradient inequality is relative to $Q$ . Integrability of $f(x, \cdot)$ for $x \in Q$ , and joint measurability of $f$ and $f'$ , are explicit hypotheses. The paper uses measurability tacitly; without it a Lean integral of a non-measurable function is $0$ and the goal could become false.
A statement for a fixed sample path, or with $\mathbb E\varphi(\bar x_k)$ replaced by a pathwise quantity, is a different and weaker theorem and does not count. Integrability of the run is not assumed: it is part of what must be proved.

A complete development needs the deterministic dual averaging analysis (Lemma 1, Lemma 2, Theorem 1 of the paper, restated here only through Theorem 2), measurability and continuity of $\pi_\beta$ , and Fubini on finite products of probability spaces. The dual averaging lemmas and the product-measure lemmas for adaptive sample paths are reusable beyond this mission. Proofs of any milestone, and supporting lemmas on measurability of the SSA run, are welcome.

Selected references

Yu. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009), 221–259. https://doi.org/10.1007/s10107-007-0149-x
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19 (2009), 1574–1609. https://doi.org/10.1137/070704277
L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, J. Mach. Learn. Res. 11 (2010), 2543–2596. https://jmlr.org/papers/v11/xiao10a.html

10 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes II: Without Backlogging, the Critical Rationing Levels Are Nondecreasing in tResearch Paper

Motivation

A firm that holds a single stock of one product often faces demand from several classes of customers that differ in importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority users of a military supply system. When stock runs low it can pay to refuse a less important demand now in order to keep stock for a more important demand that may arrive later. Veinott (Operations Research 13 (1965), 761–778) studied a dynamic inventory model with several demand classes but required the specific policy that serves every class whenever stock is available. Topkis (Management Science 15 (1968), 160–176) treated the dynamic version, in which demands arrive over the intervals of a period between two procurements, and showed that the optimal rationing policy has a simple form described by one critical rationing level per class and interval.

This mission concerns how those critical levels move over time. The paper's Theorem 2 gives a condition under which, without backlogging, the levels are monotone in the interval index, so that rationing is at least as strict early in the period as late in it. It is the second of four missions on the paper; the first establishes the critical-level policy itself (Theorem 1).

Setting

A period is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so interval $k$ is the first and interval 1 the last. There are $n$ demand classes, class $n$ the most important. At the start of interval $t$ the demand vector $d_t = (d_t^1,\dots,d_t^n)$ is observed; demands of different intervals are independent, and each class has a finite mean. With backlog $b$ and stock $z$ , one decides the vector $u$ of outstanding demand left unsatisfied, $0 \le u \le B = b + d_t$ , using $\mathbf 1\cdot(B-u)$ units of stock, so the stock at the end of the interval is $w = z - \mathbf 1\cdot(B-u) \ge 0$ . A fraction $a_t \ge 0$ of the unsatisfied demand is carried as backlog $a_t u$ into the next interval: $a_t = 1$ is complete backlogging, $a_t = 0$ none.

The costs are a penalty $p_t\cdot u$ with $0 \le p_t^1 \le \dots \le p_t^n$ (Assumption (C)), a holding cost $h_t(w)$ continuous and convex on $[0,\infty)$ (Assumption (A)), and a salvage cost $v_1(z) + v_2(z - \mathbf 1\cdot b)$ at the end of the period, with $v_1$ , $v_2$ convex and continuous and $D^+v_2$ bounded below (Assumption (B)). Here $D^+$ denotes the right derivative. The optimal costs satisfy the recursion (1)

f_t(z,B) = \inf_{0\le u\le B,\ w = z-\mathbf 1\cdot(B-u)\ge 0}\bigl[p_t\cdot u + h_t(w) + g_{t-1}(w, a_t u)\bigr],\qquad g_t(z,b) = \mathbb E f_t(z, b+d_t),

with $g_0(z,b) = v_1(z) + v_2(z-\mathbf 1\cdot b)$ .

With $\delta_j$ the $j$ -th unit vector, the critical rationing level $\bar z_t^j\in[0,\infty]$ is $+\infty$ if $\varphi_t^j(w) = p_t^j w + h_t(w) + g_{t-1}(w, a_t w\delta_j)$ is strictly decreasing on $[0,\infty)$ , and the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. Under the paper's Theorem 1 the rationing level policy $u^j = (B^{(j)} - z + \bar z_t^j)^+\wedge B^j$ , with $B^{(j)} = \sum_{i\ge j}B^i$ , is optimal: class $j$ is served from stock only while the stock stays at or above $\bar z_t^j$ .

Formalization targets

Goal: Theorem 2 (p. 170)

Let $1\le t$ , $t+1\le k$ , $a_{t+1} = a_t = 0$ , and $a_i\in\{0,1\}$ for $i\le t$ . If

p_{t+1}^j + \lim_{z\to\infty}D^+h_{t+1}(z) \le p_t^j, \qquad\text{then}\qquad \bar z_t^j \le \bar z_{t+1}^j .

Milestones

Lemma 5 (p. 168). For $b\le\bar b$ : $D_z^+g_t(z,\bar b)\le D_z^+g_t(z,b)$ .
Lemma 6 (p. 168). For $z\le\bar z$ and $y\ge 0$ : $g_t(\bar z,b)-g_t(z,b)\le g_t(\bar z+\mathbf 1\cdot y,b+y)-g_t(z+\mathbf 1\cdot y,b+y)$ .
(12) (p. 170). If $b=0$ or $a_t=1$ , for small $\varepsilon>0$ and every $d\ge0$ , the difference quotients of $f_t(\cdot,b+d)$ , $f_t(\cdot,b)$ and $h_t+g_{t-1}(\cdot,b)$ at $z$ are ordered.
Lemma 7 (p. 169). If $a_t = 1$ or $b = 0$ : $D_z^+g_t(z,b)\le D^+h_t(z)+D_z^+g_{t-1}(z,b)$ .

Significance

The result says that, in intervals without backlogging, the stock reserved against a class is never larger late in the period than early in it, provided the class's penalty in the earlier interval plus the eventual marginal holding cost does not exceed its penalty in the later interval. Together with Theorem 1 it reduces the dynamic rationing problem to a family of one-dimensional critical numbers with a known order in both the class and the time index. The paper's example on p. 170 shows that the analogous monotonicity fails with backlogging, so the hypothesis $a_{t+1} = a_t = 0$ is essential.

The paper's proofs are complete but informal: they interchange expectation and right-derivative limits, and rest on Lemma 2 (convexity and attainment) and Theorem 1 (c). No part of this paper has been machine-checked. This mission produces formal statements of Theorem 2 and the three lemmas it rests on; contributions that formalize the known proofs, or that settle whether the extra hypothesis on earlier backlogging fractions (below) can be dropped, are equally in scope.

Difficulty

The central difficulty is Lemma 7, the comparison of the marginal value of stock in two consecutive intervals. The value functions are defined through an infimum and an expectation, so they are convex but not differentiable, and the minimizer in (1) changes regime each time the stock crosses a critical level; differentiating (1) directly is not available. Right derivatives may also be $-\infty$ at $z = 0$ , and statements about them have to survive an interchange of expectation and a one-sided limit. The lemma depends on the optimal policy of Theorem 1, which is the subject of the first mission of this series. The claim of Lemma 7 is false when $a_t = 0$ and $b\ne0$ (p. 168), so no argument can ignore the case split.

Formalization scope

Classes are Fin n (paper class $j$ is index $j-1$ ); intervals are natural numbers counted backwards; vectors are Fin n → ℝ with the pointwise order.
$f_t$ and $g_t$ are defined by the recursion (1) with sInf and the Bochner integral, and every statement restricts to $z\ge0$ , $b\ge0$ , where the paper's Lemma 2 (proved in the first mission of the series) makes the infimum finite and attained and the integrand integrable.
$D^+$ is an extended-real liminf of right difference quotients, never a real derivWithin, which would return $0$ where the right derivative is $-\infty$ . Sums of right derivatives are taken in EReal.
The standing assumptions (A), (B), (C), $a_t\ge0$ , and probability laws on $[0,\infty)^n$ with finite means are bundled in Model.Standing; (B)'s limit condition is read as " $D^+v_2$ is bounded below".
Critical levels are values in WithTop ℝ satisfying the defining predicate (strictly decreasing ⇒ $+\infty$ , otherwise the smallest minimizer); the theorem holds for any such choice. Their existence is a milestone of the first mission; a sanity check exhibits a model in which all hypotheses of Theorem 2 hold with $\bar z_t^j = \bar z_{t+1}^j = 0$ .
The penalty hypothesis is stated for all $z\ge0$ instead of as a limit; these agree because $D^+h_{t+1}$ is nondecreasing.
Disclosed addition: Theorem 2 is stated with $a_i\in\{0,1\}$ for all $i\le t$ , the hypothesis of Lemma 7 that its proof uses; the printed statement names only $a_{t+1}=a_t=0$ . The hypothesis on $a_i$ in Lemmas 5–7 is required only for $i\le t$ .
A formalization in which the goal assumes Lemma 7's inequality, or any property of $D^+g_t$ , would be trivial and is excluded: those facts appear only as milestones.

Selected references

D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761

8 thms3 active usersReviewed

Combinatorics Operations Research Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XI: The Random Assignment Problem — Fluctuations of the Optimal Cost of Order (log N)²/(√N log log N)Textbook

Motivation

The assignment problem asks for a one-to-one matching of $N$ agents to $N$ tasks that minimizes the total cost. It is one of the basic problems of combinatorial optimization and is solved in polynomial time by the Hungarian method. Its random version, in which the $N^2$ costs are independent random variables, is a standard model for the typical behavior of optimization problems on random inputs, and it has been studied in probability, operations research and statistical physics.

Timeline:

Walkup (1979) showed that the expected optimal cost $E(L_N)$ of the random assignment problem with independent uniform $[0,1]$ costs stays bounded as $N \to \infty$ (doi:10.1137/0208036).
Karp (1987) proved $E(L_N) \le 2$ .
Talagrand (1995), in the article this mission formalizes, bounded the fluctuations of $L_N$ around its median by $K(\log N)^2/(\sqrt N \log\log N)$ , as a showcase of his concentration inequality for product measures (doi:10.1007/BF02699376).
Aldous (2001) proved the limit $E(L_N) \to \pi^2/6$ , the value predicted by Mézard and Parisi (doi:10.1002/rsa.1015).

This mission is Chapter 10 of Talagrand's article.

Setting

Fix $N$ and two sets $I$ and $J$ of cardinal $N$ . An assignment is a one-to-one map $\tau$ from $I$ onto $J$ . Given a cost matrix $a = (a_{i,j})_{i \in I, j \in J}$ , the cost of $\tau$ is $\sum_{i \in I} a_{i,\tau(i)}$ . In the random problem the costs are $X_{i,j}$ , independent and uniformly distributed on $[0,1]$ , and the optimal cost is the random variable

L_N = \min\Big\{ \sum_{i \in I} X_{i,\tau(i)} \;;\; \tau \text{ assignment} \Big\}.

A median of $L_N$ is any real $M$ with $P(L_N \le M) \ge 1/2$ and $P(L_N \ge M) \ge 1/2$ .

The argument uses digraphs. A digraph is a subset $D \subseteq I \times J$ , and for $S \subseteq I$ the set of neighbors is $D(S) = \{ j \in J ;\ \exists i \in S,\ (i,j) \in D \}$ . For $\alpha \ge 2$ , $D$ is $\alpha$ -expanding if for every $S \subseteq I$

\operatorname{card} S \le \tfrac N2 \Rightarrow \operatorname{card} D(S) \ge \min\big(\alpha \operatorname{card} S, \tfrac N2\big), \qquad \operatorname{card} S \ge \tfrac N2 \Rightarrow \operatorname{card} D(S) \ge N - \tfrac 1\alpha (N - \operatorname{card} S).

For $u > 0$ the threshold digraph is $D_u = \{(i,j) ;\ X_{i,j} \le 2uN^{-1}\log N\}$ : it keeps only the cheap edges.

Formalization targets

Goal: Theorem 10.5

There is a universal constant $K$ such that for $N \ge 3$ , every median $M$ of $L_N$ and every $t \ge 0$ ,

t \le \sqrt{\log N} \Rightarrow P\Big(|L_N - M| \ge \frac{K t (\log N)^2}{\sqrt N \log\log N}\Big) \le 2 e^{-t^2},

t \ge \sqrt{\log N} \Rightarrow P\Big(|L_N - M| \ge \frac{K t^3 \log N}{\sqrt N \log t^2}\Big) \le 2 e^{-t^2}.

The constant $K$ is left unspecified, as in the paper.

Milestones, in attack order

Lemma 10.1 (deterministic): in an $\alpha$ -expanding digraph with $\alpha^m \ge N/2$ , every $i \in I$ lies on a cycle $i = i_1, \dots, i_{n+1} = i$ of distinct points, $n \le 2m$ , with $(i_\ell, \tau(i_{\ell+1})) \in D$ .
Corollary 10.2 (deterministic in the costs): if $D_u$ is $\alpha$ -expanding and $\alpha^m \ge N/2$ , every optimal assignment satisfies $X_{i,\tau(i)} \le 4muN^{-1}\log N$ .
Lemma 10.4: for independent events of probability $p$ , fewer than $\delta p N$ occur with probability at most $\exp(-Np/K(\delta))$ .
Proposition 10.3: for a universal $K$ and $u > K$ with $u \log N \le N$ , $D_u$ is $u\log N$ -expanding with probability at least $1 - N^{-u/K}$ .

Significance

The expected value of $L_N$ is of the same order as a single cost, yet $L_N$ is a function of $N^2$ independent variables. A generic bounded-difference bound in all $N^2$ coordinates gives no useful concentration at this scale. Theorem 10.5 shows that the fluctuations are at most of order $(\log N)^2/(\sqrt N \log\log N)$ , and by the remark after the theorem, so is the standard deviation of $L_N$ . The chapter is a worked example of how a concentration inequality in product spaces is combined with a combinatorial localization argument, the reduction to small costs, and that pattern recurs in the study of random combinatorial optimization problems.

Status: the theorem and its lemmas are proved in the paper. As far as a search of the platform shows, none of them has a machine-checked proof. The two posed statements of Theorem 4.1.1 on the platform (finite-alphabet form) are the concentration inequality the proof calls on; formalizing this chapter adds the combinatorics of expanding digraphs, the random-graph estimate Proposition 10.3 and the final assembly.

Difficulty

The naive approach applies a concentration inequality directly to $L_N$ as a function of the $N^2$ costs, each of which can change $L_N$ by up to $1$ . That loses all control, because the variance proxy grows with the number of coordinates. The central step is to show that, with high probability, an optimal assignment only uses costs of order $N^{-1}(\log N)^2$ . This requires the cycle structure of Lemma 10.1, and it requires showing that the sparse random digraph $D_u$ has expansion uniformly over all subsets $S$ of $I$ , whose number is exponential in $N$ . Proposition 10.3 has to beat that union bound, and its proof covers only one of the two expansion conditions in detail; the condition (10.2) for large sets is "left to the reader". The final step combines the truncation with Theorem 4.1.1 and a careful choice of parameters for the two ranges of $t$ .

Formalization scope

The Lean development lives in the namespace TalagrandConc.Assignment and commits to the following conventions:

$I = J =$ Fin N, assignments are Equiv.Perm (Fin N), and $L_N$ is optCost, a Finset.inf' over all permutations (no junk value).
The probability space is the cost matrices Fin N × Fin N → ℝ with costLaw N, the product of Lebesgue measure restricted to $[0,1]$ . The coordinates are the $X_{i,j}$ .
Cardinalities of subsets are Set.ncard on the finite type Fin N. $\alpha$ -expansion includes $\alpha \ge 2$ as part of the definition.
Probabilities are in ℝ≥0∞, and $1 - N^{-u/K}$ is truncated subtraction there.
Universal constants are existentially quantified before every object they are uniform over. $K(\delta)$ in Lemma 10.4 is chosen after $\delta$ and before everything else.
Implicit side conditions of the paper are stated: $m \ge 1$ in Lemma 10.1 and Corollary 10.2, $n \ge 1$ for the cycle, $N \ge 1$ in Proposition 10.3, $t \ge 0$ in Theorem 10.5.

A cycle of length $n = 0$ would satisfy Lemma 10.1 vacuously. The formal statement therefore requires $n \ge 1$ , which rules out that trivializing reading. Similarly, Theorem 10.5 fixes one constant $K$ for all $N$ ; a $K$ depending on $N$ would make the bound empty.

Infrastructure: the product of uniform laws on a finite index set, iterated expansion arguments for bipartite digraphs, a lower-tail Chernoff bound for independent events, and the union bound over subsets are reusable beyond this mission. Theorem 4.1.1 of the paper is posed elsewhere on the platform and is not restated here. The bound (8.1.1) used in Step 2 of the proof belongs to another chapter of the series. Contributions of proofs of any milestone, or of intermediate displayed estimates such as (10.5), (10.6) and (10.9), are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. doi:10.1007/BF02699376
D. W. Walkup, On the expected value of a random assignment problem, SIAM J. Comput. 8 (1979), 440–442. doi:10.1137/0208036
R. M. Karp, An upper bound on the expected cost of an optimal assignment, in Discrete Algorithms and Complexity, Academic Press (1987), 1–4.
J. M. Steele, Probability Theory and Combinatorial Optimization, SIAM (1997). doi:10.1137/1.9781611970029
D. J. Aldous, The ζ(2) limit in the random assignment problem, Random Structures Algorithms 18 (2001), 381–418. doi:10.1002/rsa.1015

7 thms3 active usersReviewed

Completed

Functional Analysis Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces IX: Suprema of Linear Forms in Bounded Independent Variables — P(|Z − M| ≥ u) ≤ 4 exp(−u²/(4σ²))Textbook

Why linear suprema arise

A family of linear forms turns independent observations into a single random maximum. Examples include the largest value of a collection of statistical scores and the norm of a random vector sum, which can itself be expressed through the continuous dual of a normed space. A bound for each form separately does not automatically control the supremum over an infinite family. Talagrand's 1995 paper gives a concentration inequality in which the coefficient scale, rather than the number of forms, controls the deviation Talagrand 1995, §8.1. The Banach-space consequence in Chapter 13 applies the same principle to norms of vector sums Talagrand 1995, Theorem 13.2.

The two results have a direct relationship: the norm of a vector is the supremum of its evaluations by continuous linear functionals of norm at most one. The formalization therefore gives a setting in which a general real-valued supremum theorem and a vector-valued corollary can be audited together. It also tests whether the concentration statement remains faithful when the family of forms is infinite and the coordinate laws differ.

The random supremum and its scale

Fix a finite number $N$ of coordinates and a nonempty family $\mathcal F\subseteq\mathbb R^N$ of coefficient vectors $\alpha=(\alpha_i)_{i=1}^N$ . The coefficients may have either sign. Write $\|\alpha\|_2=(\sum_i\alpha_i^2)^{1/2}$ , and let $\sigma=\sup_{\alpha\in\mathcal F}\|\alpha\|_2$ . The mission treats the case in which this coefficient scale is finite and positive. Let $X_i$ be independent real random variables, with an individual interval $[r_i,r_i+1]$ containing each $X_i$ almost surely. The center $r_i$ and the law of $X_i$ may vary with $i$ . The object of interest is

Z=\sup_{\alpha\in\mathcal F}\sum_{i=1}^N\alpha_iX_i.

A median $M$ of $Z$ means that both $P(Z\le M)$ and $P(Z\ge M)$ are at least $1/2$ . This definition permits more than one median and makes no choice among them. With a bounded coefficient family and bounded coordinates, the supremum is finite for each input. The mission also assumes that $Z$ is measurable, because an uncountable supremum of measurable functions need not be measurable automatically. These are the mathematical conditions needed to give the displayed probability its ordinary meaning.

The supporting observation uses Talagrand's convex-hull distance. For a set $A$ of coordinate tuples and a point $x$ , form the binary vectors $s$ for which there is some $y\in A$ such that every coordinate with $s_i=0$ agrees between $x$ and $y$ . Let $V_A(x)$ be their convex hull in $\mathbb R^N$ . The distance $f_c(A,x)$ is the Euclidean distance from zero to $V_A(x)$ . If $A$ is empty, this distance is $+\infty$ . This convention preserves the intended meaning of a distance to an empty target Talagrand 1995, §4.1.

Formalization targets

For $x\in[0,1]^N$ , put $Z_r(x)=\sup_{\alpha\in\mathcal F}\sum_i\alpha_i(r_i+x_i)$ and $A(a)=\{y\in[0,1]^N:Z_r(y)\le a\}$ . The first milestone is Eq. (8.1.3): if $A(a)$ is nonempty, then for every $\alpha\in\mathcal F$ some $y\in A(a)$ has disagreement set $I=\{i:y_i\ne x_i\}$ with

\sum_{i\in I}|\alpha_i|\le\|\alpha\|_2\,f_c(A(a),x)\le\sigma f_c(A(a),x).

The second milestone is the deterministic observation in Eq. (8.1.2):

Z_r(x)\le a+\sigma f_c(A(a),x).

The goal, Theorem 8.1.1, asserts that every median $M$ of $Z$ and every $u>0$ satisfy

P(|Z-M|\ge u)\le 4\exp\!\left(-\frac{u^2}{4\sigma^2}\right).

The third milestone is Theorem 13.2. For vectors $v_i$ in a real Banach space $W$ , define the weak variance scale $\sigma_W=(\sup_{w^*\in W^*,\,\|w^*\|\le1}\sum_i w^*(v_i)^2)^{1/2}$ . If the independent real variables $Y_i$ satisfy $|Y_i|\le1$ , the theorem bounds deviations of $S=\|\sum_iY_iv_i\|$ from any median $M$ :

P(|S-M|\ge t\sigma_W)\le4\exp(-t^2/16),\qquad t>0.

The statement is made for $\sigma_W>0$ . With $\sigma_W=0$ , the displayed event has threshold zero and probability one, while the right side falls below one for large $t$ ; the printed inequality therefore needs that qualification Talagrand 1995, p. 198.

What the results provide

Theorem 8.1.1 controls a supremum using only the largest Euclidean norm of its coefficient vectors. Its statement does not charge a factor for the cardinality of $\mathcal F$ , so it applies equally to a finite collection and to an infinite measurable supremum. The coordinatewise interval condition allows different distributions and different centers. Theorem 13.2 converts the same concentration scale into a statement about Banach-space vector sums, where the dual unit ball supplies the coefficient family Talagrand 1995, pp. 156, 198.

Both results are proved in the paper. The work here is to formalize their exact statements and the distance interface used between them. The reusable pieces are the median convention, an extended-valued convex distance on arbitrary product spaces, a measurable supremum over a general set of coefficient vectors, and the weak variance scale for Banach-space vectors. None of the two claimed concentration inequalities is treated as already machine checked by this mission.

The difficult point

For a single fixed vector $\alpha$ , bounded-coordinate concentration gives information about $\sum_i\alpha_iX_i$ . Applying that estimate to every member of $\mathcal F$ and taking a union would introduce a dependence on the number of vectors. It would also give no useful bound for a genuinely infinite family without additional covering information. Talagrand's target avoids a cardinality term, so a direct collection of fixed-form estimates does not establish the stated result Talagrand 1995, §8.1.

The deterministic distance statement presents a second issue for formalization. Its set $A(a)$ can be empty, and the paper's distance then has value $+\infty$ . A real-valued infimum with a default value at the empty set would erase that distinction. The exact Euclidean norm also matters: the usual norm on a Lean function space need not be the paper's $\ell^2$ norm. These choices affect the mathematical meaning of the milestone before any concentration argument begins.

Formalization scope

Coordinates are indexed by Fin N, corresponding to the paper's indices $1,\ldots,N$ . The independent observations live on the canonical product of their individual real-valued laws. Each law gives probability one to its own interval $[r_i,r_i+1]$ ; identical distribution is not assumed. The coefficient family is a set, not a finite list. Its nonemptiness, finite norm supremum and positive scale are explicit. Measurability of the real supremum is also explicit, following the paper's convention of ignoring measurability questions Talagrand 1995, pp. 81–82.

The mismatch vectors and their convex hull are defined over the whole underlying product type. The distance is an extended nonnegative real infimum of Euclidean lengths, so an empty target has distance $+\infty$ . Eq. (8.1.2) uses extended arithmetic for the positive part of $Z_r(x)-a$ , which keeps the empty-sublevel case meaningful. The probability bounds retain the paper's constants $4$ , $4\sigma^2$ , and $16$ . A zero coefficient scale cannot be used to make the goal a vacuous division-by-zero statement; the Banach result likewise requires a positive weak variance scale.

The mission welcomes proofs of the two concentration statements, the deterministic distance observation, and supporting facts about the supremum's finiteness and measurability. General lemmas about product measures, medians, extended distances, and dual norms would be useful beyond this chapter. The statements do not restrict $\mathcal F$ to a finite or countable subset, so a proof must address the general family under the explicit measurability assumption.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.

7 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Primal-dual subgradient methods for convex problems 1: Dual Averaging Keeps the Gap Below β_{k+1}D + (1/2σ)Σλᵢ²‖gᵢ‖²_*/βᵢ and Its Iterates BoundedResearch Paper

Motivation

Subgradient methods are the basic tool for minimizing a nonsmooth convex function when only a black-box oracle returning one subgradient per query is available. In the classical method the new subgradient enters the iterate with a weight that decreases over time, so information collected late is counted less than information collected early, and the method has no natural certificate of its own accuracy.

Yu. Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009) 221–259; first circulated as a CORE discussion paper, March 2002, revised September 2005) introduces Dual Averaging (DA): the method accumulates all past subgradients with nondecreasing weights in the dual space and maps the aggregate back to the feasible set through a strongly convex prox-function. One analysis, Theorem 1 of the paper, gives at once an upper bound on a primal-dual gap, a bound on the iterates that holds even on unbounded feasible sets, and a bound on the averaged subgradients. From it the paper derives rates for minimization over simple sets, problems with functional constraints, saddle points, variational inequalities, and stochastic optimization. Dual Averaging later became a standard method in online learning and regularized stochastic optimization (e.g. L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, JMLR 11 (2010)).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ , and $E^*$ its dual. The value of $s \in E^*$ at $x \in E$ is $\langle s, x\rangle$ , and the dual norm is $\|s\|_* = \max\{\langle s, x\rangle : \|x\| \le 1\}$ . Balls are $B_r(x) = \{y : \|y - x\| \le r\}$ .

Let $Q \subseteq E$ be closed and convex. A prox-function of $Q$ is a function $d$ , continuous on $Q$ , that is strongly convex on $Q$ with convexity parameter $\sigma > 0$ :

d(\alpha x + (1-\alpha)y) \le \alpha d(x) + (1-\alpha) d(y) - \tfrac12\sigma\alpha(1-\alpha)\|x - y\|^2, \qquad x, y \in Q,\ \alpha\in[0,1].

The prox-center $x_0 \in Q$ minimizes $d$ on $Q$ , and $d(x_0) = 0$ . Two examples: the Euclidean norm with $d(x) = \frac12\|x - x_0\|_2^2$ , and the $\ell_1$ norm on the simplex with the entropy $d(x) = \ln n + \sum_i x^{(i)}\ln x^{(i)}$ .

For $D \ge 0$ and $\beta > 0$ set $F_D = \{x \in Q : d(x) \le D\}$ and

\xi_D(s) = \max_{x\in F_D}\langle s, x - x_0\rangle, \qquad V_\beta(s) = \max_{x\in Q}\{\langle s, x - x_0\rangle - \beta d(x)\},

and let $\pi_\beta(s) = \arg\min_{x\in Q}\{-\langle s, x\rangle + \beta d(x)\}$ .

Given sequences $x_i \in E$ , $g_i \in E^*$ , $\lambda_i$ , write $S_k = \sum_{i=0}^k \lambda_i$ , $s_{k+1} = \sum_{i=0}^k \lambda_i g_i$ ( $s_0 = 0$ ), $\hat s_{k+1} = s_{k+1}/S_k$ , the gap function

\delta_k(D) = \max_{x\in F_D}\sum_{i=0}^k \lambda_i\langle g_i, x_i - x\rangle,

and the upper gap function $\Delta_k(\beta, D) = \beta D + \sum_{i=0}^k \lambda_i\langle g_i, x_i - x_0\rangle + V_\beta(-s_{k+1})$ .

The DA-scheme (2.14) starts at $x_0$ with $s_0 = 0$ and $\beta_0 > 0$ ; at step $k \ge 0$ it receives $g_k$ (the oracle answer at $x_k$ ), chooses $\lambda_k > 0$ and $\beta_{k+1} \ge \beta_k$ , and sets

s_{k+1} = s_k + \lambda_k g_k, \qquad x_{k+1} = \pi_{\beta_{k+1}}(-s_{k+1}).

A point $x^* \in Q$ is a solution in the sense (2.8) if $\langle g_i, x_i - x^*\rangle \ge 0$ for all $i$ .

Formalization targets

Goal: Theorem 1 (p. 9)

For every run of the DA-scheme, every $k \ge 0$ and every $D \ge 0$ ,

\delta_k(D) \le \Delta_k(\beta_{k+1}, D) \le \beta_{k+1} D + \frac{1}{2\sigma}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2;

if $x^*$ is a solution in the sense (2.8), then

\tfrac12\sigma\|x_{k+1} - x^*\|^2 \le d(x^*) + \frac{1}{2\sigma\beta_{k+1}}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2;

and if moreover $B_r(x^*) \subseteq F_D$ for some $r, D > 0$ , then

\|\hat s_{k+1}\|_* \le \frac{1}{r S_k}\Big[\beta_{k+1}D + \frac{1}{2\sigma}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2\Big].

The theorem leaves the step sizes $\lambda_k$ and the parameters $\beta_k$ free; every rate in the paper is obtained by choosing them.

Milestones

In the order the proof uses them: Lemma 6 (unique minimizer of a strongly convex function, quadratic growth (9.5), p. 36); Lemma 1 (convexity, differentiability, $\nabla V_\beta(s) = \pi_\beta(s) - x_0$ and its $1/(\beta\sigma)$ -Lipschitz continuity, p. 7); (2.5) $V_\beta(s+\delta) \le V_\beta(s) + \langle\delta, \nabla V_\beta(s)\rangle + \frac{1}{2\sigma\beta}\|\delta\|_*^2$ ; (2.6) $V_\beta(\delta) \le \frac{1}{2\sigma\beta}\|\delta\|_*^2$ ; (2.2) monotonicity of $V_\beta$ in $\beta$ ; Lemma 2 $\xi_D(s) \le \beta D + V_\beta(s)$ (p. 8); (2.11) the representation $\delta_k(D) = \sum_i\lambda_i\langle g_i, x_i - x_0\rangle + \xi_D(-s_{k+1})$ ; (2.13) $\delta_k(D) \le \Delta_k(\beta, D)$ ; and (2.18), the telescoped estimate along the scheme (p. 10).

Significance

Theorem 1 is the single estimate behind the whole paper. With $\beta_k$ growing like $\sqrt k$ it gives the $O(1/\sqrt k)$ rate of Dual Averaging for nonsmooth convex minimization with simple or weighted averages (Theorems 2 and 3), and through the gap $\delta_k(D)$ it gives primal-dual certificates for saddle-point problems and variational inequalities (§§3–5) and the stochastic version (§6, the companion mission). Part 2 is the reason the method can run on unbounded feasible sets: the iterates stay in a ball around any solution. Part 3 bounds the averaged subgradients, which yields approximate dual solutions.

The result is proved in the paper. As far as a search of Mathlib and the Prove2Me catalog shows (October 2026), none of its statements is machine-checked: Mathlib has strong convexity (StrongConvexOn) and Fréchet derivatives, but no prox-functions in an arbitrary norm, no Danskin-type differentiability of a maximum, and no analysis of Dual Averaging. A formalization produces these as reusable pieces: Lemma 6 in an arbitrary finite-dimensional norm, the smoothness of $V_\beta$ (a form of the duality between strong convexity and Lipschitz gradients of the conjugate), and the definitions of the scheme and its gap functions, on which the paper's §§3–6 can then be built.

Difficulty

The bookkeeping of the proof is short; the analytic content sits in Lemma 1 and Lemma 6. Lemma 1 asserts differentiability of a function defined as a maximum over a possibly unbounded set, in an arbitrary norm, where the gradient lives in $E^{**}$ and no inner product is available to identify it with a vector. The prox-function is only continuous and strongly convex, never assumed differentiable (footnote 2, p. 5), so first-order optimality conditions for $\pi_\beta$ are not available. Lemma 6's existence claim needs boundedness of the level sets of $d$ in finite dimension; the printed argument ends with "this contradicts continuity of $d$ ", which does not by itself close the argument, so a complete proof has to supply the missing step. Finally, (2.18) pairs a sum from $i = 0$ with a sum from $i = 1$ and depends on $x_0$ being the prox-center, so an off-by-one in the indices of the scheme changes the statement.

Formalization scope

$E$ is a finite-dimensional real normed space with an arbitrary norm; $E^*$ is StrongDual ℝ E with the operator norm, which is $\|\cdot\|_*$ , and $\langle s, x\rangle$ is s x. No inner product is used, so the $\ell_1$ /entropy example remains an instance. The prox-function is a real function on $E$ of which only its values on $Q$ are used, strongly convex in Mathlib's sense StrongConvexOn Q σ d (exactly (1.8)), with $\sigma > 0$ (the paper's " $\sigma \ge 0$ " at (1.8) is corrected by its Definition 1). The maxima $\xi_D$ , $V_\beta$ , $\delta_k$ are real suprema, finite for $D \ge 0$ , $\beta > 0$ ; every statement assumes these ranges, including Lemma 2 and (2.13), where the page writes $\beta \ge 0$ but $V_0$ is not defined. The argmin map $\pi$ is a hypothesis on a given map, not a construction, and the run of (2.14) starts at the prox-center and takes the oracle answers $g_k$ as free data. Indices start at $0$ . Pages and equation numbers are those of the CORE discussion-paper version (September 2005) used as source, not the journal's pp. 221–259.

A trivializing formalization is ruled out: the run must set $x_{k+1}$ to the argmin point $\pi_{\beta_{k+1}}(-s_{k+1})$ and $\pi$ must carry its argmin property, without which the statements would be false, and the setting is satisfiable (E = ℝ, $Q = ℝ$ , $d(x) = x^2/2$ , $\sigma = 1$ , $\pi_\beta(s) = s/\beta$ ), so the theorem is not vacuous.

Needed infrastructure: Lemma 6 in an arbitrary norm; a Danskin-type differentiability lemma for $V_\beta$ ; Lipschitz continuity of the argmin map; suprema manipulations for $\xi_D$ , $V_\beta$ , $\delta_k$ under boundedness. Contributions of any of the milestones, of general lemmas on strongly convex functions in normed spaces, and of the remaining parts of Theorem 1 are welcome.

Selected references

Yu. Nesterov, Primal-dual subgradient methods for convex problems, Math. Program. 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, J. Mach. Learn. Res. 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
Yu. Nesterov, Smooth minimization of non-smooth functions, Math. Program. 103 (2005) 127–152. https://doi.org/10.1007/s10107-004-0552-5

12 thms3 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VIII: The Longest Increasing Subsequence — Gaussian Concentration of L_N around Its Median MTextbook

Why the longest increasing subsequence

Pick $N$ independent points $X_1, \dots, X_N$ uniformly in $[0,1]$ and let $L_N$ be the length of the longest increasing subsequence. Because the points are almost surely distinct, $L_N$ has the law of the longest increasing subsequence of a uniform random permutation of $\{1, \dots, N\}$ . This is Ulam's problem, one of the most studied random combinatorial quantities. Hammersley (1972) showed $\mathbb E L_N / \sqrt N$ converges, and Vershik–Kerov and Logan–Shepp (1977) identified the limit as $2$ . That leaves the size of the fluctuations of $L_N$ around its typical value.

Timeline.

Frieze (1991, [F] in the paper) and Bollobás–Brightwell (1992, [B-B]) proved concentration of $L_N$ around its mean with martingale methods, on deviation scales larger than $N^{1/4}$ .
Talagrand (1995), Section 7.1, derived from his convex hull inequality a two-sided Gaussian-type bound around the median on the scale $\sqrt{M_N} \asymp N^{1/4}$ , with explicit constants and no logarithmic loss. This is the target of the mission.
Baik, Deift and Johansson (1999) showed that the true fluctuations are of order $N^{1/6}$ , with Tracy–Widom limit law, so Talagrand's scale is not sharp. Its value is that it comes from a short, general principle.

Section 7.2 of the same paper applies the same idea to the longest common subsequence of two random words, a quantity tied to the edit distance used in genetics and speech recognition.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$ . For $x = (x_1, \dots, x_N) \in \Omega^N$ , $L_N(x)$ is the largest integer $p$ for which there are indices $i_1 < \dots < i_p$ with $x_{i_1} \le \dots \le x_{i_p}$ . For $a > 0$ , the level set is $A(a) = \{x \in \Omega^N ;\ L_N(x) \le a\}$ .

Fix a probability $\mu$ on $[0,1]$ without atoms (Lebesgue measure, for instance) and let $P = \mu^{\otimes N}$ be the product probability on $\Omega^N$ ; the coordinates are the random points $X_i$ . A median of $L_N$ is a number $M$ with $P(L_N \le M) \ge 1/2$ and $P(L_N \ge M) \ge 1/2$ .

The tool is Talagrand's convex hull distance. For $A \subseteq \Omega^N$ and $x \in \Omega^N$ , let $U_A(x)$ be the set of $s \in \{0,1\}^N$ for which some $y \in A$ agrees with $x$ at every coordinate $i$ with $s_i = 0$ ; let $V_A(x)$ be its convex hull in $\mathbb R^N$ ; and let $f_c(A,x)$ be the Euclidean distance from $0$ to $V_A(x)$ (with $f_c(A,x) = +\infty$ if $A = \emptyset$ ).

A function $L_N : \Omega^N \to \mathbb N$ on an arbitrary probability space $(\Omega, \mu)$ is a configuration function if, for every $x$ , some set $J$ of exactly $L_N(x)$ coordinates satisfies $L_N(y) \ge \operatorname{card}\{i \in J ;\ y_i = x_i\}$ for all $y$ .

For two sequences $x = (x_1, \dots, x_N)$ and $y = (y_1, \dots, y_{N'})$ , $L_{N,N'}(x;y)$ is the largest $p$ with $i_1 < \dots < i_p$ , $j_1 < \dots < j_p$ and $x_{i_\ell} = y_{j_\ell}$ for all $\ell \le p$ .

Formalization targets

Goal: Theorem 7.1.2 (p. 153)

For every median $M$ of $L_N$ and every $u > 0$ ,

P(L_N \ge M + u) \le 2\exp\Big(-\frac{u^2}{4(M+u)}\Big), \qquad P(L_N \le M - u) \le 2\exp\Big(-\frac{u^2}{4M}\Big).

Milestones

Lemma 7.1.1 (p. 153). For $a > 0$ and every $x$ , $a \ge L_N(x) - f_c(A(a),x)\sqrt{L_N(x)}$ ; in particular $L_N(x) \ge a + v$ implies $f_c(A(a),x) \ge v/\sqrt{a+v}$ .
Theorem 7.1.3 (p. 154). The two bounds of the goal hold for every configuration function on any product probability space.
Eq. (7.2.3) (p. 155). For the longest common subsequence $L(x)$ of the two halves of $x \in [0,1]^{N+N'}$ : $a \ge L(x) - 2\sqrt2\, f_c(A(a),x)\sqrt{L(x)}$ .
Theorem 7.2.1 (p. 154). For two independent i.i.d. sequences with common real law and a median $M$ of $L_{N,N'}$ :

P(L_{N,N'} \ge M + u) \le 2\exp\Big(-\frac{u^2}{32(M+u)}\Big), \qquad P(L_{N,N'} \le M - u) \le 2\exp\Big(-\frac{u^2}{32M}\Big).

Significance

The result. Since $M_N$ is of order $\sqrt N$ , the goal confines $L_N$ to a window of width of order $N^{1/4}$ around its median with Gaussian-type tails. For $u$ much larger than $M$ the upper bound becomes exponential in $u$ , the natural tail of a quantity bounded by the size of a witnessing configuration. Theorem 7.1.3 isolates what is used: every integer quantity certified by a configuration of exactly its own size has the same concentration. This abstraction became the notion of certifiable functions used widely in random graph theory and probabilistic combinatorics (see the treatment of Talagrand's inequality in Alon–Spencer, The Probabilistic Method). For the longest common subsequence, the bound is useful when the alphabet is large and $M \ll N$ , where it improves on Azuma's inequality.

Formalizing it. All four results are proved in the paper; none is formalized in Lean as far as a search of the Prove2Me corpus shows. A finite-alphabet certifiable-function inequality (Talagrand.certifiable_concentration) has been posed on the platform as an open statement; it uses a Lipschitz hypothesis and no median, so it is a relative of Theorem 7.1.3, not the same statement. The mission produces a general- $\Omega$ formalization of the configuration-function principle, its application to the continuous Ulam problem, and the common-subsequence variant.

Difficulty

The deterministic inequalities (Lemma 7.1.1, Eq. (7.2.3)) relate the Euclidean distance $f_c$ , defined through a convex hull in $\mathbb R^N$ , to purely combinatorial counts of disagreeing coordinates; this needs the infimum defining $f_c$ to be attained and a duality between the convex hull and its extreme points. The probabilistic step rests on Talagrand's convex hull inequality (Theorem 4.1.1, Eq. (4.1.2)), $\int \exp(f_c^2(A,x)/4)\, dP(x) \le 1/P(A)$ , for a general product probability; that inequality is not in Mathlib. A bounded-difference (Azuma or McDiarmid) argument does not suffice: changing one point changes $L_N$ by at most $1$ , which gives deviations of order $\sqrt N$ , not $\sqrt M$ . The point of the configuration property is that only the $L_N(x)$ coordinates of a witness matter.

Formalization scope

Product space. $\Omega^N$ is Fin N → Ω (0-based), and $P$ is Measure.pi (fun _ => μ). For the goal, $\Omega$ is unitInterval and $\mu$ is any probability measure on it with $\mu\{t\} = 0$ for all $t$ . Theorem 7.2.1 uses the product of Measure.pi measures on (Fin N → ℝ) × (Fin N' → ℝ) for a probability $\mu$ on $\mathbb R$ . Eq. (7.2.3) lives on Fin (N + N') → unitInterval, with the first $N$ coordinates forming the first sequence.
Increasing means weakly increasing ( $\le$ ), as printed. Index sequences are strictly increasing maps Fin p → Fin N. $L_N$ and $L_{N,N'}$ take values in ℕ.
Convex hull distance. $f_c$ takes values in ℝ≥0∞, with the Euclidean norm written out as $\sqrt{\sum_i s_i^2}$ . Mathlib's default norm on Fin N → ℝ is the sup norm and would give a different, much weaker statement. The deterministic inequalities are stated in the rearranged form $L \le a + c\, f_c \sqrt L$ in $[0, +\infty]$ .
Median: $P(Z \le M) \ge 1/2$ and $P(Z \ge M) \ge 1/2$ ; the statements hold for every median.
Measurability. The paper treats all functions as measurable. In Theorem 7.1.3 this convention is the explicit hypothesis that the configuration function is measurable. The concrete $L_N$ and $L_{N,N'}$ carry no hypothesis.
Degenerate corner. When $M = 0$ , Lean's division gives $u^2/(4M) = 0$ , so the lower-tail bound reads " $\le 2$ ". The event $\{L \le -u\}$ is then empty, so no content is lost.
No trivialization. Using the sup norm in $f_c$ , using a real-valued infimum (which is $0$ on an empty $A(a)$ ), or putting the conclusion of Theorem 4.1.1 among the hypotheses would each make a statement trivial or empty. None of these is done.

The mission uses the shared definition of the convex hull distance from Section 4.1. A general- $\Omega$ proof of Eq. (4.1.2) and of the attainment of $f_c$ would be reusable for every Part II chapter of the paper. Contributions are welcome in particular for the deterministic Lemma 7.1.1 and Eq. (7.2.3), the measurability of $L_N$ and $L_{N,N'}$ , and the reduction of Theorem 7.1.2 to Theorem 7.1.3.

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
A. Frieze, On the length of the longest monotone subsequence in a random permutation, Ann. Appl. Probab. 1 (1991), 301–305. https://doi.org/10.1214/aoap/1177005939
B. Bollobás, G. Brightwell, The height of a random partial order: concentration of measure, Ann. Appl. Probab. 2 (1992), 1009–1018. https://projecteuclid.org/journals/annals-of-applied-probability/volume-2/issue-4
A. M. Vershik, S. V. Kerov, Asymptotics of the Plancherel measure of the symmetric group and the limiting form of Young tables, Soviet Math. Dokl. 18 (1977), 527–531.
J. Baik, P. Deift, K. Johansson, On the distribution of the length of the longest increasing subsequence of random permutations, J. Amer. Math. Soc. 12 (1999), 1119–1178. https://doi.org/10.1090/S0894-0347-99-00307-0
N. Alon, J. H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016. https://doi.org/10.1002/9781119062042

8 thms3 active usersReviewed

Completed

Complexity Theory Linear Optimization Operations Research+1·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 2: The Adaptive-Step Algorithm in N∞(β) or N∞⁻(β) with γ ≤ 2(1 − β) Attains Precision t in O(nt) IterationsResearch Paper

Why wide neighbourhoods

Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products $x_js_j$ are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood $\{x_js_j \ge \tfrac12\,x^Ts/n\}$ and attained precision $t$ in $O(nt)$ iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood $\mathcal N_2(\beta)$ and improved the bound to $O(\sqrt n\,t)$ . Practical codes nevertheless favour wide neighbourhoods, which allow long steps.

Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods $\mathcal N_\infty(\beta)$ and $\mathcal N_\infty^-(\beta)$ attains precision $t$ in $O(nt)$ iterations. With $\beta$ close to $1$ , $\mathcal N_\infty^-(\beta)$ contains almost all of the strictly feasible set.

Setting

Fix $n\ge1$ , $m\ge0$ , $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider

\text{(P)}\ \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad \text{(D)}\ \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .

The strictly feasible pairs $\mathcal F^0$ are the $(x,s)$ with $x>0$ , $s>0$ , $Ax=b$ , and $A^Ty+s=c$ for some $y$ . For such a pair the duality gap is $x^Ts$ , and the duality measure is $\mu=x^Ts/n$ . Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ and $e=(1,\dots,1)^T$ .

Norms: $\|\cdot\|$ is the Euclidean norm, $\|\cdot\|_\infty$ the maximum norm, and $\|z\|^-_\infty:=\|z^-\|_\infty$ , $\|z\|^+_\infty:=\|z^+\|_\infty$ with $(z^-)_j=\min\{z_j,0\}$ and $(z^+)_j=\max\{z_j,0\}$ . For $\beta\in(0,1)$ the wide neighbourhoods are

\mathcal N_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|_\infty\le\beta\mu\},\qquad \mathcal N^-_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|^-_\infty\le\beta\mu\}.

The second says only that $x_js_j\ge(1-\beta)\mu$ for every $j$ .

The search direction $d=(d_x,d_s)$ with centering parameter $\gamma$ solves, for some $d_y$ ,

Sd_x+Xd_s=\gamma\mu e-Xs,\qquad Ad_x=0,\qquad A^Td_y+d_s=0, \tag{2}

and the step is $x(\theta)=x+\theta d_x$ , $s(\theta)=s+\theta d_s$ . The scaled quantities $p=X^{-1/2}S^{1/2}d_x$ , $q=X^{1/2}S^{-1/2}d_s$ , $r=(XS)^{-1/2}(\gamma\mu e-Xs)$ satisfy $p+q=r$ and $p^Tq=0$ . The componentwise product $Pq=(p_jq_j)_j$ is the second-order term $D_xd_s$ .

Algorithm 2 with neighbourhood $\mathcal N$ and $\gamma\in(0,1)$ starts at $(x^0,s^0)\in\mathcal N$ with $(x^0)^Ts^0\le2^t$ . While $(x^k)^Ts^k>2^{-t}$ , it computes $d$ from (2), takes the largest $\bar\theta$ such that $(x(\theta),s(\theta))\in\mathcal N$ for all $\theta\in[0,\bar\theta]$ , and sets $(x^{k+1},s^{k+1})=(x(\bar\theta),s(\bar\theta))$ .

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Let $\beta,\gamma\in(0,1)$ with $\gamma\le2(1-\beta)$ , and let $\mathcal N$ be $\mathcal N_\infty(\beta)$ or $\mathcal N_\infty^-(\beta)$ . Every run of Algorithm 2 reaches $(x^k)^Ts^k\le 2^{-t}$ for some

k\ \le\ \Big\lceil\frac{\ln2\cdot n\,t}{2\beta\gamma(1-\gamma)}\Big\rceil .

The paper states " $O(nt)$ iterations"; the count above is the one its inequality (15) yields.

Milestones, in the order the proof uses them

Lemma 1(b): $-\|r\|^2/4\le p_jq_j\le r_j^2/4$ for each $j$ .
Lemma 1(c): $\|Pq\|^-_\infty\le\|r\|^2/4\le n\|r\|^2_\infty/4$ , $\|Pq\|^+_\infty\le\|r\|^2_\infty/4$ , $\|Pq\|_\infty\le\|r\|^2/4$ .
Lemma 2(c): if $\gamma\le2(1-\beta)$ and $(x,s)\in\mathcal N_\infty^-(\beta)$ then $\|r\|^2\le n\mu$ ; in $\mathcal N_\infty(\beta)$ , $\|r\|_\infty^2\le(1+\beta)\mu$ .
Lemma 5: $\bar\theta\ge\theta_2=\min\{1,\beta\gamma\mu/\|Pq\|_\infty\}$ in $\mathcal N_\infty(\beta)$ , and $\bar\theta\ge\theta_2^-=\min\{1,\beta\gamma\mu/\|Pq\|^-_\infty\}$ in $\mathcal N_\infty^-(\beta)$ .
Proof of Theorem 2: $\theta_2^-\ge\theta_2\ge4\beta\gamma/n$ (for $n\ge2$ ).
(15): $\mu^{k+1}\le\big(1-4\beta\gamma(1-\gamma)/n\big)\mu^k$ .

Significance

Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of $\mathcal F^0$ keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.

The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods $\mathcal N_\infty$ , $\mathcal N_\infty^-$ , of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.

Difficulty

Most of the steps are finite-dimensional inequalities. The sticking points are the following.

The bound $p_jq_j\ge-\|r\|^2/4$ uses the orthogonality $p^Tq=0$ , which comes from $Ad_x=0$ and $d_s=-A^Td_y$ . Those relations hold only for a solution of the full system (2), not for the first equation alone.
Lemma 5 needs every point of the segment $[0,\theta_2]$ to lie in the neighbourhood, including strict positivity of $x(\theta)$ and $s(\theta)$ and dual feasibility. Positivity of the products alone does not give positivity of the factors without a continuity argument along the segment.
"The largest $\bar\theta$ " is a maximum over a set defined by infinitely many conditions. The theorem needs only that $\bar\theta$ dominates $\theta_2$ , but the formal run must say what $\bar\theta$ is.
Converting the per-iteration contraction (15) into the explicit count needs $(1-\delta)^k\le e^{-k\delta}$ , real powers of $2$ , and a ceiling.

Formalization scope

Vectors are Fin n → ℝ, with coordinates indexed $0,\dots,n-1$ , and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. $\mu$ divides by $n$ as a real number. Here $\log$ is the natural logarithm and $2^t$ is a real power with $t\in\mathbb R$ .

Committed conventions and repairs:

The direction is "any $(d_x,d_y,d_s)$ solving (2)". No rank assumption on $A$ is made.
"The largest $\bar\theta$ " is IsGreatest of the set of admissible step lengths, and $\bar\theta$ is not capped at $1$ . When no maximum exists (always the case for $n=1$ , where $Pq=0$ ), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for $n=2$ .
A run is a pair of sequences that starts as required and makes one iteration from every iterate with $(x^k)^Ts^k>2^{-t}$ . Its behaviour after the stopping test is unconstrained.
In $\theta_2$ and $\theta_2^-$ , a zero norm makes the quotient $+\infty$ and the minimum $1$ . Since Lean's real division by zero is $0$ , this case is defined explicitly.
The bound $\theta_2\ge4\beta\gamma/n$ is stated for $n\ge2$ . At $n=1$ it can fail (e.g. $\beta=1/2$ , $\gamma=0.9$ ), and Algorithm 2 makes no iterations there.
The goal covers both neighbourhoods. A goal for $\mathcal N^-_\infty$ alone would be weaker than the paper.
Lemma 1 assumes only $x,s>0$ and $\gamma\in[0,1]$ of the pair, which is all its statement uses.

The goal is not to be read with a hidden constant. A statement of the form "there is $C$ with at most $Cnt$ iterations", with $C$ allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.

Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.

Selected references

S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944 (1990, rev. 1991); Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
M. Kojima, S. Mizuno, A. Yoshise, A primal-dual interior point algorithm for linear programming, in N. Megiddo (ed.), Progress in Mathematical Programming, Springer, 1989, pp. 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
R. D. C. Monteiro, I. Adler, Interior path following primal-dual algorithms. Part I: Linear programming, Mathematical Programming 44:27–41, 1989. https://doi.org/10.1007/BF01587075
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

11 thms3 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces II: The Two-Point Space — an N-Free Exponential Bound for the One-Sided Hamming Distance under a Second MeasureTextbook

Motivation

The concentration of measure phenomenon says that in a product probability space a set of probability not too small is "large" in the sense that most points lie within a small distance of it. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces develops this phenomenon through exponential moment bounds for distances to sets. Its Section 2.1 treats the Hamming distance on an arbitrary product space and recovers the bounds obtainable by martingale methods (McDiarmid, On the method of bounded differences, 1989).

Section 2.3, the subject of this mission, specialises to the two-point space $\{0,1\}^N$ with biased coordinates. This is the setting of the binomial law, of random subsets of a finite set, and of monotone properties of random graphs. Two things happen there that do not happen in general. First, the bias $p$ of the coordinates enters the bound through the variance $p(1-p)$ , which gives sharper tails when $p$ is close to $0$ or $1$ . Second, when one counts only the coordinates where $x$ has a $1$ and the point of $A$ has a $0$ , and measures $A$ under a second, more heavily biased product measure, the exponential moment bound becomes independent of the dimension $N$ . The paper calls this the first of its results that "apparently cannot be obtained via martingales". Bounds of this one-sided kind are the natural tool for upper tails of increasing functions on the biased cube, the regime of the binomial law near $Np_1$ when samples are drawn at rate $p<p_1$ .

Setting

Let $\Omega=\{0,1\}$ . For $p\in[0,1]$ let $\mu$ be the probability on $\Omega$ with $\mu(\{1\})=p$ , $\mu(\{0\})=1-p$ , and let $P=\mu^N$ be the product probability on $\Omega^N$ , whose points are written $x=(x_1,\dots,x_N)$ . For a set $A\subseteq\Omega^N$ and a point $x\in\Omega^N$ , the Hamming distance from $x$ to $A$ is

f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\neq y_i\}:\ y\in A\big\},

the least number of coordinates of $x$ that must be changed to land in $A$ . The one-sided distance counts only changes from $1$ to $0$ :

f^{+}(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i=1,\ y_i=0\}:\ y\in A\big\}.

Both are $+\infty$ when $A$ is empty. A second probability $\mu_1$ on $\Omega$ has $p_1=\mu_1(\{1\})$ , and $P_1=\mu_1^N$ . For $\alpha>0$ and $t\ge 0$ the paper uses two constants,

b(\alpha,t,p)=((1-p)e^{t}+p)(p+(1-p)e^{-t/\alpha})^{\alpha}\quad(p\ge \tfrac12),\qquad b(\alpha,t,p)=b(\alpha,t,1-p)\quad(p\le\tfrac12),

a(\alpha,t)=\max\Big(1,\ (1-p+pe^{t})(p_1e^{-t/\alpha}+1-p_1)^{\alpha}\Big).

In the Lean development these are hammingDistToSet, oneSidedDistToSet, bConst, aConst, the measure productMeasure N p, and the integrand expMul t z $=e^{tz}$ .

Formalization targets

Goal: Theorem 2.3.4

If $p_1>p$ , then for every $N$ , every $A\subseteq\Omega^N$ , every $\alpha>0$ and every $t\ge 0$ ,

\int e^{t f^{+}(A,x)}\,dP(x)\le\frac{a(\alpha,t)^N}{P_1(A)^{\alpha}}.

For small $t$ one has $a(\alpha,t)=1$ . When $0<p<p_1<1$ and $\alpha=1$ , the paper's explicit threshold is $e^{t}\le p_1(1-p)/(p(1-p_1))$ . At equality, the bound becomes $\int (p_1(1-p)/(p(1-p_1)))^{f^{+}(A,x)}dP\le 1/P_1(A)$ , with no dependence on $N$ . The main theorem also includes the endpoint cases $p=0$ and $p_1=1$ without using this ratio.

Milestones

Proposition 2.3.1. For $t\ge0$ , $\alpha\ge1$ : $\displaystyle\int e^{tf(A,x)}\,dP(x)\le \frac{b(\alpha,t,p)^N}{P(A)^\alpha}$ .
Corollary 2.3.2, Eq. (2.3.4). There is a universal $K$ such that for $\alpha\ge1$ , $0\le t\le1$ :

\int e^{tf(A,x)}\,dP(x)\le\frac{1}{P(A)^\alpha}\exp N\Big[p(1-p)\Big(1+\frac1\alpha\Big)\frac{t^2}{2}+Kt^3\Big].

Corollary 2.3.2, Eq. (2.3.5). There is a universal $K$ such that for $(4p(1-p)N\log\frac1{P(A)})^{1/2}\le k\le p(1-p)N$ :

P(\{f(A,x)\ge k\})\le\exp\Big(-\frac{1}{2p(1-p)N}\Big(k-\sqrt{2p(1-p)N\log\tfrac{1}{P(A)}}\Big)^2+\frac{Kk^3}{(p(1-p))^3N^2}\Big).

Lemma 2.3.5. If $a\le b\le 1$ , then

\frac{1-p}{b^{\alpha}}+p\min\Big(\frac{1}{a^{\alpha}},\frac{e^{t}}{b^{\alpha}}\Big)\le\frac{a(\alpha,t)}{(ap_1+b(1-p_1))^{\alpha}}.

Milestones 1–3 concern the two-sided Hamming distance; milestone 4 is the one-coordinate inequality behind the goal.

Significance

The results. Proposition 2.3.1 and Corollary 2.3.2 give, for every set $A$ in the biased cube, a tail bound for the Hamming distance whose Gaussian part has the variance $p(1-p)N$ of the binomial law, not the worst case $N/4$ . The paper notes that this matches the quality of the optimal isoperimetric inequalities that are known only for hereditary (monotone) sets. Theorem 2.3.4 is a statement with no dimension in it: it controls how many $1$ s of a $\mu^N$ -sample must be switched off to reach a set $A$ that is not small under the more biased $\mu_1^N$ .

Formalizing it. These results are proved in the paper; the local Prove2Me index contains no machine-checked proof of these statements. Mathlib has the Bernoulli measure, finite products of measures and lower Lebesgue integrals, but no exponential moment bound for these distances to sets. A complete development would add reusable facts about biased Boolean products, their distance functions and exponential moments, and the uniform cubic error term in Corollary 2.3.2.

Difficulty

The obvious route to a Hamming-distance tail bound is a martingale (bounded differences) argument. It yields $e^{-2k^2/N}$ -type bounds that do not see the bias $p$ , and its variance proxy grows with $N$ , so it gives no bound independent of $N$ ; the paper states that Theorem 2.3.4 apparently cannot be obtained this way. Theorem 2.3.4 measures $A$ under $P_1$ while the integral is under $P$ , so a one-coordinate estimate must account for two different probabilities and keep the factor $a(\alpha,t)$ exactly equal to $1$ for small $t$ . Lemma 2.3.5 must handle $a=0$ as well as interior values. Corollary 2.3.2 requires a cubic error bound uniform in $p\in[0,1]$ and $\alpha\ge1$ .

Formalization scope

$\Omega$ is Bool with $1$ = true; $P$ reuses the published TalagrandCore.bernPi Bernoulli product measure with p : unitInterval converted to a nonnegative real, over Fin N (0-based coordinates). Every subset of $\{0,1\}^N$ is measurable, so the paper's convention of ignoring measurability costs nothing here.
Distances take values in ℝ≥0∞, with $f(\emptyset,x)=+\infty$ ; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$ ; $P(A)^{-\alpha}$ is computed in $[0,\infty]$ , so $P(A)=0$ gives $+\infty$ .
Theorem 2.3.4 and Lemma 2.3.5 are stated for $\alpha>0$ , the range under which Section 2.2 introduces the exponent $\alpha$ (the theorem's page does not restate it). Proposition 2.3.1 and Corollary 2.3.2 keep the page's $\alpha\ge 1$ . The standing hypothesis $p_1>p$ appears as a binder.
The universal constants of Corollary 2.3.2 are quantified before $p$ , $N$ , $A$ , $\alpha$ , $t$ , $k$ . In Eq. (2.3.5), $0<p<1$ , $N\ge1$ and $P(A)>0$ are assumed, which is where the displayed formula is defined.
A trivializing formalization is ruled out: the integrals are not Bochner integrals (which vanish on non-integrable functions), the empty set and $P_1(A)=0$ are handled through $+\infty$ , not junk zeros, and the two different distances of the section carry different names.

The mission also imports the published TalagrandCore.bernPi definition for the Boolean product law. Reusable pieces include evaluation of $\int$ over $\{0,1\}$ under a Bernoulli measure and facts about product measures over Fin N. Contributions to any of the four milestones or the goal are welcome.

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
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89 (2001). https://doi.org/10.1090/surv/089

8 thms3 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$ , but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.

Let $\mu$ be a probability distribution on a set $\mathcal X$ , and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$ . For $f\in\mathcal F$ , its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$ , with $X\sim\mu$ . For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$ , $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$ .

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$ , and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$ -balls centred in $A$ that cover $A$ . Then

\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).

For $\lambda\ge0$ , sample variance penalization selects

SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$ , $n\ge2$ , $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$ . With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$ ,

P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$ , so it covers an optimal one when one exists.

Milestones

In the order of the proof:

the fourth-moment inequality (Lemma 8, Corollary 9);
the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
the comparison $W\le\mathbb EV_n$ of (7)–(9);
Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
the uniform bound, Theorem 6:

\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$ ; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$ . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$ -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$ , and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
Indices $i=1,\dots,n$ are i : Fin n.
A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$ " have laws giving zero mass outside $[0,1]$ .
"With probability at least $1-\delta$ , $A$ " is written as $\mu^n\{\neg A\}\le\delta$ . For a set that is not measurable this is the outer measure.
$P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$ ).
$\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
$SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
- Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
- Lemma 13: the function is measurable.
- Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$ . With an infinite value the printed bound is vacuous.
Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$ . Theorem 3 and Bennett's display add $n\ge1$ . Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$ .
Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

SVP is not defined as the comparator $f^*$ .
$\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$ .
$V_n$ is the sample variance, not the true variance.
No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

the entropy method for self-bounding functions (Theorem 7);
Bennett's inequality for independent non-identical bounded variables;
product-measure symmetrization;
covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

21 thms3 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs: A Variable-Rate Queue Has an Average Cost Optimal Stationary Policy Whenever λ < max aβResearch Paper

Motivation

Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).

Timeline:

1962–1970. Derman and Ross obtain average cost optimal stationary policies from the vanishing discount approach when the relative values $h_\alpha$ are bounded.
1986. Sennott treats the queue with variable service rates under bounded costs and gives a first discrete-time Tauberian argument (Operations Research 34, 1986a; 1986b).
1989. This paper: Assumptions 1–3, the Theorem, the Markov chain test of Propositions 4–5, and applications to a packet system and to the queue with variable service rates (Proposition 8).

Setting

A Markov decision chain has states $i=0,1,2,\dots$ ; in state $i$ a finite nonempty set $A_i$ of actions; a cost $0\le C(i,a)<\infty$ ; and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may depend on the whole history and may randomize; a stationary policy $f$ chooses $f(i)\in A_i$ in state $i$ . For $0<\alpha<1$ , $V_{\theta,\alpha}(i)$ is the expected total $\alpha$ -discounted cost from $i$ and $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$ , possibly infinite. The average cost of $\theta$ is

g_\theta(i)=\limsup_{N\to\infty}\frac1N\,E_\theta\Big[\sum_{t=0}^{N-1}C(X_t,a_t)\,\Big|\,X_0=i\Big].

A stationary policy $f$ is average cost optimal if there is a finite constant $g$ with $g=g_f(i)\le g_\theta(i)$ for every policy $\theta$ and every state $i$ .

The queue with variable service rates (Example 2). Time is slotted; $p_i$ is the probability of $i$ arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables $a$ and serves at rate $a\beta\in(0,1)$ , so that the customer in service leaves during the slot with probability $a\beta$ ; there is no decision in state $0$ . From state $i\ge1$ the next state is $i-1+k$ with probability $a\beta p_k+(1-a\beta)p_{k-1}$ ( $p_{-1}=0$ ), and from $0$ it is $j$ with probability $p_j$ . The cost structure: $B(a)>0$ ; $Q$ a polynomial of degree $n\ge0$ , nonnegative and increasing on $i\ge0$ ; $C(0)=Q(0)$ and $C(i,a)=Q(i)+B(a)$ for $i\ge1$ . The arrival moments are $\lambda^{(k)}=\sum_i i^kp_i$ and $\lambda=\lambda^{(1)}$ .

Formalization targets

Goal: Proposition 8

If $\lambda^{(n+1)}<\infty$ , then

\lambda<\max_a(a\beta)\ \Longrightarrow\ \text{there is an average cost optimal stationary policy},

and

\lambda<\min_a(a\beta)\ \Longrightarrow\ g+h(i)=\min_a\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\quad i\ge0,

with $g$ the optimal average cost, $g=\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)$ , and $h$ bounded below.

Milestones

Propositions 1–3 (p. 627): $V_\alpha$ solves the discount optimality equation, is its minimal nonnegative solution, and is the limit of value iteration (already proved on the platform, referenced).
The Lemma (p. 628): discount optimal stationary policies along $\alpha_n\to1$ have a stationary limit point.
Lemmas A1 and A2 (p. 632): the comparison between solutions of the optimality inequality and average costs, and $\limsup_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)\le g_\theta(i)$ .
The Theorem (p. 628): under Assumptions 1–3, any limit point $f$ from the Lemma is average cost optimal, with the optimality inequalities (5); under Assumption 3*, the optimality equation (6).
Propositions 4, 5 and the Corollary (pp. 629–630): the Markov chain criteria that yield Assumptions 1, 3 and 3* from one well-behaved stationary policy.
Two steps of the proof of Proposition 8 (p. 631): $V_\alpha(i)$ is increasing in $i$ (hence Assumption 2), and the drift of $r(i)=Ai^{n+1}$ is a polynomial of degree at most $n$ with leading coefficient $A(n+1)(\lambda-a\beta)$ , display (14).

Significance

Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.

All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.

Difficulty

The obvious route takes a limit of $h_\alpha=V_\alpha-V_\alpha(0)$ along a sequence $\alpha_n\to1$ and passes to the limit in the discount optimality equation. With unbounded costs and unbounded $h_\alpha$ the sum $\sum_jP_{ij}(a)h_\alpha(j)$ is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of $V_\alpha$ and a Lyapunov drift computation whose leading term, $A(n+1)(\lambda-a\beta)i^n$ , has to dominate a cost polynomial of the same degree.

Formalization scope

The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:

costs, discounted values and average costs lie in $[0,\infty]$ ; $V_\alpha$ may be infinite unless Assumption 1 is assumed;
$h_\alpha$ is a real number, used only together with Assumption 1;
the constants $N$ and $M_i$ of Assumptions 2–3 are explicit and chosen before $i$ and $\alpha$ ; Assumption 3* uses the same $M$ ;
"average cost optimal" always carries a finite constant $g\ge0$ and compares with all policies, not only stationary ones;
sums $\sum_jP_{ij}(a)h(j)$ against a real function are extended reals (positive part minus negative part);
"ergodic" means positive recurrent (no aperiodicity);
in the queue, every decision is formally available in state $0$ with identical cost $Q(0)$ and identical transitions, which represents "no decision in state 0"; $\lambda<\max_a(a\beta)$ is "for some $a$ " and $\lambda<\min_a(a\beta)$ "for every $a$ ".

The second half of the goal is not "there exist $g$ and $h$ satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties $g$ to the optimal average cost and $\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha$ and requires $h$ bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals $p_0=3/4$ , $p_1=1/4$ , one rate $a\beta=1/2$ , $Q(i)=i+1$ , $B=1$ ), so the goal is not vacuous.

A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on $\prod_iA_i$ , first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

L. I. Sennott, Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs, Operations Research 37(4):626–633, 1989. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970.
A. G. Pakes, Some Conditions for Ergodicity and Recurrence of Markov Chains, Operations Research 17(6):1058–1061, 1969. https://doi.org/10.1287/opre.17.6.1058
A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey, SIAM J. Control Optim. 31(2):282–344, 1993. https://doi.org/10.1137/0331018

22 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis Numerical Analysis+2·Captain: mikedeng1

Régularisation d'inéquations variationnelles par approximations successives II: The Proximal Regularization of a Convex Minimization Problem Is a Minimizing SequenceResearch Paper

Motivation

The proximal point algorithm replaces a hard optimization or equilibrium problem by a sequence of better-conditioned ones: from the current point $x^n$ it solves the original problem with a quadratic penalty $\|x-x^n\|^2$ added, and takes the solution as $x^{n+1}$ . The method is a building block of modern convex optimization. Augmented Lagrangian methods, Douglas–Rachford and ADMM splitting, and many bundle methods are proximal point iterations applied to suitable problems (Rockafellar 1976; Eckstein–Bertsekas 1992).

The algorithm was introduced by B. Martinet in a five-page note in the Revue française d'informatique et de recherche opérationnelle in 1970 (Martinet 1970). The note treats three cases: monotone variational inequalities on a bounded convex set (§II), convex–concave min–max problems (§III), and convex minimization (§IV). This mission formalizes §IV.

Timeline.

1970, Martinet: the regularization (13) for convex minimization over a closed convex set in a Hilbert space; Théorème 3 (weak cluster points are minimizers, the sequence is minimizing), stated without proof.
1976, Rockafellar (SIAM J. Control Optim. 14): the proximal point algorithm for maximal monotone operators, with inexact steps and weak convergence of the whole sequence when a zero exists.
1991, Güler (SIAM J. Control Optim. 29): the rate $f(x^n)-\inf f = O(1/n)$ for convex minimization, and an example in which the iterates converge weakly but not strongly.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $C\subseteq H$ be a nonempty, closed, convex set, and let $f:H\to\mathbb R$ be a convex, lower semicontinuous function such that, for every $a\in\mathbb R$ , the sublevel set $\{x\in C \mid f(x)\le a\}$ is bounded. These are the standing hypotheses of §4.1 (Lean: Standing f C). The problem is

(12)\qquad \min\,\{\,f(x)\mid x\in C\,\},

and its solution set (solSet f C) is the set of $\bar x\in C$ with $f(\bar x)\le f(x)$ for all $x\in C$ .

The regularization algorithm (13) starts from $x^0\in C$ and, given $x^n$ , takes

(13)\qquad x^{n+1}\in C\ \text{ the minimizer of } \ f(x)+\|x-x^n\|^2\ \text{ over } x\in C .

Lean encodes one step as IsProxStep f C xn y ( $y\in C$ and $f(y)+\|y-x^n\|^2\le f(x)+\|x-x^n\|^2$ for all $x\in C$ ) and a run as IsProxSeq f C x.

A point $\tilde x$ is a weak cluster point of $(x^n)$ (IsWeakClusterPt) if every neighbourhood of $\tilde x$ in the weak topology of $H$ contains $x^n$ for infinitely many $n$ . A sequence is minimizing if $f(x^n)\to\inf_{x\in C} f(x)$ .

Formalization targets

Existence for (12) and well-posedness of (13)

\exists\,\bar x\in C\ \ \forall x\in C:\ f(\bar x)\le f(x), \qquad \forall x^n\in C\ \ \exists!\,y\in C:\ y \text{ minimizes } f(x)+\|x-x^n\|^2 \text{ over } C .

These are the paper's claims in §4.1 ("Ces hypothèses assurent l'existence d'une solution pour (12)") and §4.2 ("solution unique").

Goal: Théorème 3

For every sequence generated by (13),

\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in \operatorname{sol}(12), \qquad \lim_{n\to\infty} f(x^n)=\inf_{x\in C} f(x)\in\mathbb R .

The goal asserts no rate and no constant. It is the statement the paper makes, with both conclusions in one theorem.

Stronger: Remarque 1

If in addition $f$ is uniformly convex, i.e. $f(ax+by)\le af(x)+bf(y)-ab\,\varphi(\|x-y\|)$ for $a,b\ge0$ , $a+b=1$ , with $\varphi(t)>0$ for $t>0$ , then (12) has a unique solution $\bar x$ and $\|x^n-\bar x\|\to0$ .

Significance

The result. Théorème 3 says that the proximal iterates make progress on the objective, not only on the distance to the solution set. A user of the method can stop on a value criterion. The convergence also needs no step-size tuning, no smoothness of $f$ , and no bound on $f$ beyond the boundedness of the sublevel sets. The well-posedness of (13) is what makes the method an algorithm. Each step is a strongly convex subproblem with a unique solution, and later inexact and splitting variants rely on that.

Formalizing it. The note gives no proof of Théorème 3 ("On peut faire une démonstration directe de ce théorème") and none of Remarque 1. The mission asks for a complete machine-checked proof of the convex minimization case of the original proximal point paper. To our knowledge, none of these statements has a machine-checked proof. Mathlib has convexity, lower semicontinuity, the weak topology of a normed space and uniform convexity of functions, but no proximal point algorithm.

Difficulty

Each iterate $x^{n+1}$ is defined only implicitly, as the minimizer of a problem that changes with $n$ . Monotonicity of $f(x^n)$ follows at once from comparing $x^{n+1}$ with $x^n$ . Monotonicity alone gives convergence of $f(x^n)$ to some limit, but not to $\inf_C f$ . Closing that gap needs information about the minimizers of (12) and their distance to the iterates.

The cluster-point statement is about the weak topology. A norm-continuity argument does not apply: $f$ is only lower semicontinuous in norm, and passing to weak limits requires the weak lower semicontinuity of convex lower semicontinuous functions. The boundedness that makes weak cluster points exist comes from the sublevel-set hypothesis, not from $C$ , which may be unbounded.

Formalization scope

All statements live in MartinetReg.ConvexMin. The conventions the formalization commits to:

$H$ is a real complete inner product space (InnerProductSpace ℝ H, CompleteSpace H). The paper says "espace de Hilbert", and its inequalities make it real.
$C\neq\emptyset$ is a standing hypothesis. The paper leaves it implicit, but its existence claim for (12) is false for $C=\emptyset$ .
$f$ is real-valued, convex and lower semicontinuous on all of $H$ , as printed. The constraint $x\in C$ stays explicit in (12) and (13). It is not absorbed into an extended-valued indicator.
The penalty in (13) has weight $1$ , as printed, not $\tfrac12$ .
The algorithm is a relation on sequences: IsProxSeq accepts any sequence with $x^0\in C$ satisfying (13) at every step. Existence and uniqueness of the step are a separate milestone, not built into a definition by choice.
"Minimisante" is stated as: some real $m$ is the greatest lower bound of $f(C)$ and $f(x^n)\to m$ . This avoids the junk value sInf takes on sets unbounded below. As a side effect, the theorem asserts that $f$ is bounded below on $C$ .
Weak cluster points are cluster points in WeakSpace ℝ H. A norm cluster point would weaken the conclusion and is not used.
Remarque 1 uses Mathlib's UniformConvexOn Set.univ φ f with $\varphi(t)>0$ for $t>0$ . It keeps every hypothesis of §4.1.

The goal does not assume that (12) has a solution, that $f$ is bounded below on $C$ , or that the iterates are bounded. Each of these would remove part of the content of Théorème 3, and the first two are consequences proved as milestones.

Not formalized here: Remarque 2 (p. 158), a comment that convexity seems indispensable; and the Exemple (p. 158). The Exemple's linear system $(A^*A+2I)x^{n+1}=A^*b+2x^n$ corresponds to $f=\tfrac12\|Ax-b\|^2$ . For the printed $f=\|Ax-b\|^2$ , (13) gives $(A^*A+I)x^{n+1}=A^*b+x^n$ . The variational inequality case (§II) is the companion mission I of this series.

Reusable beyond this mission: the existence of minimizers of convex lower semicontinuous functions with bounded sublevel sets on closed convex subsets of a Hilbert space, and the weak lower semicontinuity it rests on. Contributions of these general lemmas, and of strong-convexity facts for $x\mapsto f(x)+\|x-x^n\|^2$ , are welcome.

Selected references

B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3), 154–158, 1970. https://doi.org/10.1051/m2an/197004R301541
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14(5), 877–898, 1976. https://doi.org/10.1137/0314056
O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29(2), 403–419, 1991. https://doi.org/10.1137/0329022
J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Mathematical Programming 55, 293–318, 1992. https://doi.org/10.1007/BF01581204
J. L. Lions and G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20, 493–519, 1967. https://doi.org/10.1002/cpa.3160200302

6 thms3 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

A 2-Approximation Algorithm for Stochastic Inventory Control Models with Lost Sales: The Dual-Balancing Policy Costs at Most Twice Any Nonanticipatory Policy under Independent DemandsResearch Paper

Motivation

Inventory systems in which unmet demand is lost, not backlogged, are the norm in retail: a customer who finds an empty shelf buys elsewhere. With a positive lead time $L$ between ordering and delivery, the optimal policy for such a system depends on the entire pipeline of outstanding orders, so dynamic programming is intractable beyond small $L$ . Optimal policies are not of base-stock type, and for decades no policy with a provable guarantee on its expected cost was known for this model.

Levi, Janakiraman and Nagarajan (Math. Oper. Res. 33(2), 2008) gave the first such guarantee. Their dual-balancing policy balances, in every period, the expected holding cost against the expected lost-sales penalty of the units ordered now, and it costs at most twice as much as an optimal policy.

Timeline.

2007. Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2)) introduce marginal cost accounting and the dual-balancing policy for the backlogging model, with a worst-case guarantee of 2.
2008. Levi, Janakiraman and Nagarajan extend the guarantee to lost sales (this mission). In their model the truncated inventory positions of the two policies can cross back and forth inside a lead time, which the backlogging argument never meets.
2009. Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science, 2009) prove that order-up-to policies are asymptotically optimal in the lost-sales model as the penalty cost grows.
2021 onward. Xin (Oper. Res., 2021; SSRN 7134538) analyses capped base-stock policies for i.i.d. lost-sales demand, culminating in a 2.33-approximation guarantee for that policy class, whose main theorem is proved on Prove2Me.

Page and display numbers in this mission refer to the authors' accepted manuscript (28 pages, pp. 1–28), not to the journal's pages 351–374.

Setting

Periods are $t=1,\dots,T$ . An order $Q_s\ge0$ placed in period $s$ arrives at the start of period $s+L$ , where $L\ge1$ is an integer. Before the horizon there are $x_0\ge0$ units on hand and pipeline orders $Q_j=q_j\ge0$ for $1-L\le j\le0$ . Demands $D_1,\dots,D_T\ge0$ have finite means. The information $\mathcal F_s$ available at the start of period $s$ contains $D_1,\dots,D_{s-1}$ and possibly more. A feasible policy chooses $Q_s$ as an $\mathcal F_s$ -measurable quantity.

The on-hand inventory $I_t$ at the start of period $t$ , after the arrival, satisfies $I_1=x_0+Q_{1-L}$ and

I_{t+1}=(I_t-D_t)^+ + Q_{t+1-L}.

Demand $(D_t-I_t)^+$ is lost. Costs are a holding rate $h_t\ge0$ , a lost-sales penalty $p_t\ge0$ and an ordering cost $c_t\ge0$ per unit, where $p_t$ and $c_t$ are non-increasing in $t$ .

Marginal cost accounting. Under first-ordered-first-consumed bookkeeping, $H_s$ is the ordering cost $c_sQ_s$ plus the holding cost that the $Q_s$ units incur until the end of the horizon, and $\Pi_s=p_{s+L}(D_{s+L}-I_{s+L})^+$ is the lost-sales penalty in the period in which they arrive. The cost of a policy $P$ is

\mathcal C(P)=\sum_{s=1}^{T-L}\bigl(H^P_s+\Pi^P_s\bigr).

It omits only costs that are the same for every policy.

The truncated inventory position of period $s$ with respect to $t\le s$ is $Y_{st}=I_s+\sum_{j=s+1-L}^{t}Q_j$ . For two policies $B$ and $P$ , the set $\mathcal T_H$ holds the periods $t\le T-L$ with $Y^B_{st}<Y^P_{st}$ for every $s\in[t,t+L]$ , and $\mathcal T_\Pi$ holds the remaining periods $t\le T-L$ .

A dual-balancing policy $B$ orders, in each period $t\le T-L$ , the amount that equalises the two conditional expectations

E[H^B_t\mid\mathcal F_t]=E[\Pi^B_t\mid\mathcal F_t]=:Z_t.

Formalization targets

Goal: Theorem 3.1

If demands are independent, then for every feasible policy $P$

E[\mathcal C(B)]\le 2\,E[\mathcal C(P)].

Comparing with every feasible $P$ , rather than with an optimal policy, gives the guarantee without assuming that an optimum is attained.

Milestones, in attack order

(11) For $t\le s\le t+L$ , $I_{t+L}=Y_{st}-D_{[s,t+L)}+\sum_{r=s}^{t+L-1}(D_r-I_r)^+$ .
Lemma 3.2. On every sample path, $\sum_{t\in\mathcal T_H}H^B_t\le\sum_{t}H^P_t$ .
Lemma 3.3. On every sample path, $\sum_{t\in\mathcal T_\Pi}\Pi^B_t\le\sum_{t}\Pi^P_t$ .
(14) $E[\mathcal C(P)]\ge E\bigl[\sum_t(\mathbb 1_{t\in\mathcal T_H}H^B_t+\mathbb 1_{t\in\mathcal T_\Pi}\Pi^B_t)\bigr]$ .
Lemma 3.1. $E[\mathcal C(B)]=2\sum_{t=1}^{T-L}E[Z_t]$ .
Lemma 3.4. This lemma characterises the crossing events $A_{st}=[Y^B_{st}<Y^P_{st}]\cap[Y^B_{s+1,t}\ge Y^P_{s+1,t}]$ .
Lemmas 3.5 and 3.6. Under independence, conditioning on $t\in\mathcal T_H$ (respectively $t\in\mathcal T_\Pi$ ) does not lower the conditional expected holding (respectively lost-sales) cost of $B$ below $Z_t$ .

Significance

The result. The theorem gives a constant-factor guarantee for a lost-sales system with lead times, for arbitrary independent and non-identical demand distributions. The policy is computed online, one period at a time, from one-dimensional conditional expectations, which an optimal policy cannot be. The guarantee holds with time-dependent holding costs and with non-increasing ordering and penalty costs. Section 5 of the paper extends it to correlated demand structures, which are out of this mission's scope.

Formalizing it. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The mission produces the lost-sales dynamics, the truncated inventory position, marginal cost accounting and the sample-path amortization lemmas as reusable Lean objects. It also produces a formal treatment of the conditional-expectation step under independence, which the backlogging analysis does not need. The sibling mission on the backlogging model, LeviBalancing.DualBalancing, provides the shared instance and policy definitions that are reused here.

Difficulty

In the backlogging model, $t\in\mathcal T_H$ is decided by information available at time $t$ , so the cost comparison can be made period by period after conditioning on $\mathcal F_t$ . With lost sales this fails: the truncated positions of $B$ and of the benchmark can cross from below to above and back inside the window $[t,t+L]$ . Whether $t\in\mathcal T_H$ is therefore not known at time $t$ , and conditioning on that event moves the conditional expectations of $H^B_t$ and $\Pi^B_t$ away from $Z_t$ . A newcomer's first idea, to reuse the backlogging argument with $\mathcal F_t$ -measurable indicators, does not apply. The lost-sales penalty also cannot be charged period by period: Lemma 3.3 is a global amortization over intervals. The non-increasing penalties are what make that amortization possible when $p_t$ varies.

Formalization scope

Periods are integers. The pipeline $Q_j$ , $j\le0$ , is shared by every policy through the published order. Instance, cumDemand, order, DemandProcess and IsFeasiblePolicy are reused from LeviBalancing.DualBalancing. The new layer is one definition file, LostSalesBalancing.DualBalancing.Model.
Orders and demands are real (fractional orders, as in §3.1). The randomized integral-order variant is out of scope.
Cost generality is that of Theorem 3.1. Rates are only required to be $\ge0$ , which strengthens the paper's stationary $h,p>0$ . Accordingly (11) is stated in lost units, and Lemma 3.4(iv) is stated as positive lost demand, not positive penalty.
Independence. The paper assumes independent demands but lets $\mathcal F_s$ hold more than past demands. The formalization requires $\mathcal F_t$ to be independent of $(D_t,\dots,D_T)$ for every $t$ , which for the natural filtration is exactly mutual independence. Finite means are integrability.
"OPT" becomes every feasible policy in Theorem 3.1, (14) and Lemmas 3.5–3.6. In the sample-path statements, (11) and Lemmas 3.2–3.4, it becomes every nonnegative order sequence.
Conditional events. $\Pr(A\mid\mathcal F)\,E[X\mid\mathcal F,A]$ is written $E[\mathbb 1_AX\mid\mathcal F]$ , which never divides by a zero probability.
Expected costs are lower Lebesgue integrals in $[0,\infty]$ . The dual-balancing predicate requires $H^B_t$ and $\Pi^B_t$ to be integrable, so no conditional expectation takes Mathlib's default value $0$ .
Lemma 3.4(iii) is stated with $D_s\ge I^P_s-\Delta Q_s$ . The printed strict inequality excludes a tie at which the event $A_{st}$ does occur.
A trivializing formalization is ruled out: the dual-balancing predicate and the independence hypothesis are jointly satisfiable with $T>L$ (checked locally on an explicit instance), and no statement is meaningful only when $T\le L$ , the case in which every cost is zero.

Contributions welcome: proofs of the sample-path lemmas, which need only finite sums and the recursion; the conditional-expectation lemmas, which need a Harris-type argument for independent coordinates; and the existence of a measurable balancing order, which this mission does not pose.

Selected references

R. Levi, G. Janakiraman, M. Nagarajan, A 2-Approximation Algorithm for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research 33(2), 351–374, 2008. https://doi.org/10.1287/moor.1070.0285
R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2), 284–302, 2007. https://doi.org/10.1287/moor.1060.0205
W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science, 2009. https://doi.org/10.1287/mnsc.1080.0945
L. Xin, capped base-stock policies in lost-sales inventory models, Operations Research, 2021. https://doi.org/10.1287/opre.2020.2019
L. Xin, Capped Base-Stock Policies: A 2.33-Approximation, SSRN working paper 7134538, 2026. https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538

12 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Fixed Point and Bregman Iterative Methods for Matrix Rank Minimization: The Matrix Shrinkage Fixed Point Iteration Converges to an Optimal Solution of the Nuclear Norm Regularized ProblemResearch Paper

Motivation

Many estimation problems ask for a matrix of low rank that is consistent with a small number of linear measurements: completing a partially observed ratings matrix, identifying a low-order linear system, or embedding points from a few pairwise distances. Rank minimization under linear constraints is NP-hard, and the standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values (Recht, Fazel and Parrilo, 2010). Under incoherence assumptions the surrogate recovers the low-rank matrix exactly (Candès and Recht, 2009).

The surrogate is a semidefinite program, and interior point methods for it do not scale past matrices of a few hundred rows. Ma, Goldfarb and Chen (2009) proposed a first-order method for the regularized form of the problem: a gradient step on the data-fit term followed by singular value shrinkage. Their algorithms FPC and FPCA are built on this two-line iteration, and the paper's one convergence theorem says that the iteration, run with a fixed step size, converges to a minimizer. This mission formalizes that theorem and the lemmas used to prove it.

Timeline of the closest results:

2005: Combettes and Wajs prove convergence of forward–backward splitting for the sum of a convex function and a convex function with Lipschitz gradient in a Hilbert space.
2008: Hale, Yin and Zhang analyse the fixed point continuation (FPC) method for $\ell_1$ -regularized least squares, with vector shrinkage in place of matrix shrinkage.
2008–2010: Cai, Candès and Shen introduce singular value thresholding (SVT) for matrix completion, prove that the shrinkage is the proximal map of the nuclear norm, and prove convergence of a different iteration (Uzawa's method on a strongly convex problem with equality constraints).
2009: Ma, Goldfarb and Chen state and prove convergence of the matrix shrinkage fixed point iteration for the nuclear norm regularized least squares problem (1.8), following Hale, Yin and Zhang's argument.

Setting

Fix natural numbers $m,n,p$ . Matrices $X\in\mathbb R^{m\times n}$ carry the Frobenius norm $\|X\|_F=(\sum_{ij}X_{ij}^2)^{1/2}$ and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$ . A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by matrices $A_0,\dots,A_{p-1}$ through $\mathcal A(X)_i=\langle A_i,X\rangle$ ; equivalently $\mathcal AX=A\,\mathrm{vec}(X)$ for a matrix $A\in\mathbb R^{p\times mn}$ . Its adjoint is $\mathcal A^*$ , and $\lambda_{\max}(A^\top A)=\|\mathcal A\|_2^2$ , the square of its spectral norm. Fix $b\in\mathbb R^p$ and $\mu>0$ .

Problem (1.8) is

\min_{X\in\mathbb R^{m\times n}}\ \mu\|X\|_*+\tfrac12\|\mathcal A(X)-b\|_2^2 ,

and $\mathcal X^*$ denotes its set of optimal solutions. Write $g(X)=\mathcal A^*(\mathcal A(X)-b)$ for the gradient of the data-fit term and $h(X)=X-\tau g(X)$ for a gradient step of size $\tau>0$ .

For $\nu>0$ , the matrix shrinkage operator $S_\nu$ takes a singular value decomposition $Y=U\,\mathrm{Diag}(\sigma)V^\top$ to $S_\nu(Y)=U\,\mathrm{Diag}(\bar\sigma)V^\top$ , where $\bar\sigma_i=\max(\sigma_i-\nu,0)$ . The fixed point iterations (2.1) start from an arbitrary $X^0$ and repeat

Y^k=X^k-\tau g(X^k),\qquad X^{k+1}=S_{\tau\mu}(Y^k).

Formalization targets

Goal: Theorem 4

For $\tau\in(0,2/\lambda_{\max}(A^\top A))$ and every starting point, there is $X^*\in\mathcal X^*$ with

\lim_{k\to\infty}\|X^k-X^*\|_F=0 .

The goal fixes no rate and no particular limit: it asserts convergence of the whole sequence to some minimizer.

Milestones, in attack order

Theorem 3. $S_\nu(Y)$ is an optimal solution of $\min_X\nu\|X\|_*+\tfrac12\|X-Y\|_F^2$ . This is already posed on the platform as Cai, Candès and Shen's Theorem 2.1 (which adds uniqueness) and is referenced, not restated.
Corollary 1. For every $\tau>0$ : $X^*\in\mathcal X^*$ if and only if $X^*=S_{\tau\mu}(h(X^*))$ .
Lemma 1. $\|S_\nu(Y_1)-S_\nu(Y_2)\|_F\le\|Y_1-Y_2\|_F$ , with equality if and only if $Y_1-Y_2=S_\nu(Y_1)-S_\nu(Y_2)$ .
Lemma 2. For $\tau$ in the step range, $\|h(X)-h(X')\|_F\le\|X-X'\|_F$ , and $h(X)-h(X')=X-X'$ if and only if equality holds.
Lemma 3. If $X^*\in\mathcal X^*$ , then $X\in\mathcal X^*$ if and only if $\|S_{\tau\mu}(h(X))-X^*\|_F=\|X-X^*\|_F$ .

The mission also contains the paper's Theorem 2, the optimality condition for (1.8) written with a reduced singular value decomposition $X=U\,\mathrm{Diag}(\sigma)V^\top$ : $X\in\mathcal X^*$ if and only if some $W$ satisfies $\mu(UV^\top+W)+g(X)=0$ , $U^\top W=0$ , $WV=0$ and $\|W\|_2\le1$ . The chain to Theorem 4 does not use it.

Significance

Theorem 4 is the correctness guarantee for FPC and FPCA, which were among the first algorithms to solve nuclear norm regularized problems with matrices in the thousands of rows. It certifies that the output of the plain iteration is an exact minimizer in the limit, for every starting point and every step below $2/\lambda_{\max}(A^\top A)$ . Lemmas 1–3 are the reusable part: non-expansiveness of the matrix shrinkage with a precise equality case, and the fixed point characterization of the optimal set, are the ingredients of every proximal gradient analysis with nuclear norm regularization.

Status: the theorem is proved on paper, and it is also a special case of the general convergence of forward–backward splitting. No machine-checked proof of it is known. The platform holds general forward–backward and inertial forward–backward convergence statements in Hilbert space (for example NesterovFB.Weak.theorem_3, InertialFB.IFB.theorem1_convergence) and the nonexpansiveness of abstract proximal maps (MoreauProx.Characterization.prox_nonexpansive). None is stated for the nuclear norm, for matrix shrinkage defined through the SVD, or with Ma, Goldfarb and Chen's equality cases. Formalizing this mission connects Mathlib's singular values to these operator-theoretic statements.

Difficulty

The obvious route goes through Fejér monotonicity: every step brings the iterate no farther from any minimizer, so the iterates are bounded and have a limit point. Two steps of this route do not come for free. First, the argument presupposes a minimizer; nothing in the hypotheses provides one, so the existence of an optimal solution of (1.8) has to be established from the data. Second, a limit point must be shown to be optimal, which requires the equality cases of Lemmas 1 and 2, not just the inequalities. Lemma 1's equality case concerns the singular value decompositions of two unrelated matrices whose singular vectors need not be aligned; non-expansiveness alone does not deliver it. Nonexpansive maps in general need not have convergent iterates (a rotation is nonexpansive), so continuity plus boundedness is not enough.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ. The Frobenius norm, the nuclear norm (the sum of Mathlib's LinearMap.singularValues), the linear map $\mathcal A$ as $p$ matrices Aop, its adjoint and spectral norm, and the shrinkage relation IsShrink are reused from the published Cai–Candès–Shen definitions.
$S_\nu$ is a relation, IsShrink ν Y X: $X$ is the shrinkage of $Y$ for some reduced SVD (orthonormal columns, positive singular values). Every statement takes the shrinkage output as a variable with an IsShrink hypothesis. The paper's Definition 4 also allows zero singular values, which shrink to zero and change nothing.
The step range $\tau\in(0,2/\lambda_{\max}(A^\top A))$ is written $0<\tau$ and $\tau\|\mathcal A\|_2^2<2$ , without division. For $\mathcal A=0$ this is the range $(0,\infty)$ , as on paper, rather than the empty range that Lean's $2/0=0$ would give.
$\mu>0$ is an explicit hypothesis, and so is $\nu>0$ in Lemma 1; in Corollary 1, $\tau>0$ is the only condition on the step, as on the page ("for any $\tau>0$ "). $\nu=\tau\mu$ is built into the statements.
The run of (2.1) is a predicate on the whole sequence with an arbitrary $X^0$ ; it is not the continuation scheme FPC and does not fix $X^0=0$ .
Convergence is in the Frobenius norm to some minimizer chosen after the run. Neither $\mathcal X^*\neq\emptyset$ nor boundedness of the iterates is a hypothesis; a statement that assumes either is a different, weaker theorem and is ruled out.
No statement assumes $m\le n$ ; the paper's "without loss of generality" belongs to its proofs.

A complete development needs the SVD of real matrices in terms of Mathlib's singular values, the subdifferential of the nuclear norm, and a Fejér-monotone convergence argument in finite dimension. The first two are reusable for any nuclear norm or spectral function result, and contributions of general lemmas about singular value shrinkage (functionality of IsShrink, its proximal characterization) are welcome.

Selected references

S. Ma, D. Goldfarb, L. Chen, Fixed point and Bregman iterative methods for matrix rank minimization, Math. Program. 128 (2011); preprint arXiv:0905.1643v2, 2009. https://arxiv.org/abs/0905.1643
J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://arxiv.org/abs/0810.3286
E. T. Hale, W. Yin, Y. Zhang, Fixed-point continuation for ℓ1-minimization: methodology and convergence, SIAM J. Optim. 19(3), 2008. https://doi.org/10.1137/070698920
P. L. Combettes, V. R. Wajs, Signal recovery by proximal forward-backward splitting, Multiscale Model. Simul. 4(4), 2005. https://doi.org/10.1137/050626090
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://arxiv.org/abs/0706.4138
E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://arxiv.org/abs/0805.4471

10 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Quality Control under Markovian Deterioration 3: Sufficient Conditions for a Three-Region Optimal Policy and for an Optimal Policy That Never InspectsResearch Paper

Motivation

Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)

The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593

Setting

The belief $P\in[0,1]$ is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability $\pi\in[0,1]$ if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to $T(P)=P+\pi-\pi P$ . The discount factor is $\beta\in(0,1)$ . Producing without inspection has cost $0$ in the good state and cost $C$ in the bad state, so its expected current cost is $CP$ . Inspection costs $I$ in either state, and revision costs $R$ in either state. The standing order is $0<C<I<R$ . The explicit $C>0$ records that $C$ is a cost and makes the quotient in Theorem 3.7 meaningful.

Write $V_\beta(P)$ for the discounted value starting from belief $P$ . Inspection reveals the current state: the next belief is $\pi$ after observing a good process and $1$ after observing a bad one. Revision resets the next belief to $\pi$ . The three current-plus-continuation costs are

\begin{aligned} q_{\mathrm P}(P)&=CP+\beta V_\beta(T(P)),\\ q_{\mathrm I}(P)&=I+\beta P V_\beta(1)+\beta(1-P)V_\beta(\pi),\\ q_{\mathrm R}(P)&=R+\beta V_\beta(\pi). \end{aligned}

The Bellman equation is $V_\beta(P)=\min\{q_{\mathrm P}(P),q_{\mathrm I}(P),q_{\mathrm R}(P)\}$ . A stationary rule is $\beta$ -optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)

Formalization targets

The first target is the sufficient condition for an optimal three-region rule. Set $\Delta=V_\beta(1)-V_\beta(\pi)$ . If

\frac{(1-\beta)(R+\beta V_\beta(\pi))}{C}\le\frac{R-I}{\beta\Delta},

there are thresholds $\pi\le P_1\le P_2$ such that an optimal rule produces for $P<P_1$ , inspects for $P_1\le P<P_2$ , and revises for $P\ge P_2$ . The revise interval may be empty: if no admissible belief has revision as an optimal action, $P_2$ may exceed $1$ . If revision is optimal somewhere, the conclusion includes $P_2\le1$ . This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)

The second target gives an optimal no-inspection rule. If

I+\beta\Delta\ge\frac{C}{1-\beta(1-\pi)} \quad\text{or}\quad \frac{R-I}{\beta\Delta}\le\frac{R}{C}\bigl(1-\beta(1-\pi)\bigr),

then some $P_1\ge\pi$ gives an optimal rule that produces below $P_1$ and revises from $P_1$ onward. A threshold above $1$ is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)

Significance

The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum $P\in[0,1]$ . Ross (1971), Theorem 3.7

The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.

Difficulty

The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.

Formalization scope

Lean represents a belief as a real number and restricts all claims to $[0,1]$ . It defines $V^0=0$ and obtains $V^{n+1}$ by taking the minimum of the three action costs with continuation $V^n$ , exactly as in equation (4). The value $V_\beta$ is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including $P=1$ and both thresholds.

The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use $P_1,P_2\in[0,1]$ . The last quotient in Corollary 3.6 divides by $\pi$ , so that second inequality is stated under $\pi>0$ ; the first inequality, and the main theorem, cover $\pi=0$ . If $\pi=1$ , then $\Delta=0$ . Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.

Selected references

Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587

8 thms3 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Potential Games 2: Every Finite Potential Game Is Isomorphic to a Congestion GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Monotone Comparative Statics II: f Is Quasisupermodular If and Only If a Strictly Increasing Transformation Makes It Supermodular on Every Sublattice {x₁, x₂, x₁ ∨ x₂, x₁ ∧ x₂}Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 165)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Implicit Renewal Theory and Tails of Solutions of Random Equations 2: Kesten's Theorem for R = Q + MR — Unique Stationary Law, Power Tails with Explicit C±, and C₊ + C₋ > 0 iff Q ≢ (1 − M)cResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Geometric Bounds for Eigenvalues of Markov Chains 2: Odd Closed Paths Bound the Smallest Eigenvalue, β_min ≥ −1 + 2/ιResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2

Milestones (the steps of the paper's proof)

Companions

Significance

Difficulty

Formalization scope

Selected references

Learning Models with Uniform Performance via Distributionally Robust Optimization 2: A Minimax Lower Bound of Order n^(−1/2) ∨ n^(−1/k*) for Estimating the Cressie–Read Robust Risk (Theorem 3)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Logarithmic Sobolev Inequalities for Finite Markov Chains 2: Entropy Decay Ent_π(μH_t) ≤ e^{−2αt} Ent_π(μ), Improved to e^{−4αt} for Reversible ChainsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.6 (p. 722)

Milestones

Companion: (3.3) (p. 723)

Significance

Difficulty

Formalization scope

Selected references

3SUM in O(n^1.999074) Time on a Word RAMOpen Problem

Fast Rates for Support Vector Machines Using Gaussian Kernels 1: Under Tsybakov and Geometric Noise, Gaussian-Kernel SVMs Reach Excess Risk Cx²n^{−β+ε} with Probability 1 − e^{−x}Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

On the Gittins Index for Multiarmed Bandits 2: A Policy Falls Short of the Gittins Policy by at Most Its Expected Discounted Gap Between the Greatest Gittins Index and That of the Bandit It PlaysResearch Paper

Motivation

Setting