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

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Primal-Dual Interior-Point Methods for Self-Scaled Cones I: After One Short Step from N(β), λ₂(x₊, s₊) ≤ (2 + δ − κ)(ϵ + κ)²/((1 − δ)²(1 − κ)³)Research Paper

Motivation

Linear programming, second-order cone programming and semidefinite programming are all instances of conic linear programming: minimize a linear function over the intersection of an affine subspace with a closed convex cone. Primal-dual interior-point methods solve these problems in polynomially many iterations and are the algorithms behind most conic solvers in practical use. Nesterov and Todd showed that the primal-dual path-following analysis known for linear programming extends verbatim to every cone that admits a self-scaled barrier, a class containing the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products (Nesterov & Todd 1997; Nesterov & Todd 1998).

Timeline. Kojima, Mizuno and Yoshise (1989) and Monteiro and Adler (1989) gave short-step primal-dual path-following methods for linear programming with an $O(\sqrt n \ln(1/\varepsilon))$ iteration bound. Mizuno, Todd and Ye (1993) added the predictor-corrector variant. Nesterov and Nemirovskii (1994) developed the general theory of self-concordant barriers. Nesterov and Todd (1997) introduced self-scaled barriers and scaling points; the 1998 paper analysed the short-step, adaptive-step and predictor-corrector methods for them. Güler (1996) identified self-scaled cones with symmetric (homogeneous self-dual) cones.

Setting

Let $E = \mathbb R^n$ with inner product $\langle\cdot,\cdot\rangle$ , and let $K \subseteq E$ be a closed convex cone that is pointed and has nonempty interior; $K^* = \{s : \langle s, x\rangle \ge 0\ \forall x \in K\}$ is its dual cone. A linear map $A : \mathbb R^n \to \mathbb R^m$ (surjective), $b \in \mathbb R^m$ and $c \in \mathbb R^n$ define the primal problem $\min\{\langle c, x\rangle : Ax = b,\ x \in K\}$ and its dual $\max\{\langle b, y\rangle : A^*y + s = c,\ s \in K^*\}$ . Strictly feasible points are $x \in S^0(P)$ ( $x \in \operatorname{int} K$ , $Ax = b$ ) and $(y, s) \in S^0(D)$ ( $s \in \operatorname{int}K^*$ , $A^*y + s = c$ ).

A $\nu$ -self-concordant logarithmically homogeneous barrier $F$ for $K$ is a self-concordant convex function on $\operatorname{int} K$ that tends to $+\infty$ at the boundary, satisfies $(\langle F'(x), h\rangle)^2 \le \nu\langle F''(x)h, h\rangle$ and $F(\tau x) = F(x) - \nu\ln\tau$ . Its conjugate is $F_*(s) = \sup_{x \in \operatorname{int}K}\{-\langle s, x\rangle - F(x)\}$ . The barrier is self-scaled if $F''(w)x \in \operatorname{int}K^*$ and $F_*(F''(w)x) = F(x) - 2F(w) - \nu$ for all $w, x \in \operatorname{int}K$ . For $x \in \operatorname{int}K$ and $s \in \operatorname{int}K^*$ the scaling point is the $w \in \operatorname{int}K$ with $F''(w)x = s$ .

Local norms at $x \in \operatorname{int}K$ are $\|v\|_x = \langle F''(x)v, v\rangle^{1/2}$ for primal vectors and $\|u\|_x = \langle [F''(x)]^{-1}u, u\rangle^{1/2}$ for dual vectors; $|u|_x$ is the cone-induced (max-type) norm. With $\mu(x, s) = \langle s, x\rangle/\nu$ the proximity measures are

\lambda_2(x, s) = \Big\|\frac{s}{\mu(x,s)} + F'(x)\Big\|_x,\qquad \lambda_\infty(x, s) = \Big|\frac{s}{\mu(x,s)} + F'(x)\Big|_x,

and $\bar\lambda_2(x, s, \mu) = \|s/\mu + F'(x)\|_x$ . The narrow neighbourhood is $N(\beta) = \{(x,y,s) \in S^0(P)\times S^0(D) : \lambda_2(x, s) \le \beta\}$ .

The short step from $(x, y, s) \in N(\beta)$ targets $\mu_+ = (1 - \kappa/\sqrt\nu)\mu(x,s)$ and solves

F''(w)q_x + q_s = s + \mu_+F'(x),\qquad Aq_x = 0,\qquad A^*q_y + q_s = 0,

then sets $(x_+, y_+, s_+) = (x - q_x, y - q_y, s - q_s)$ .

Formalization targets

Goal: Theorem 6.4

With $\delta = \lambda_\infty(x,s)$ , $\epsilon = \lambda_2(x,s)$ , $\epsilon_+ = \bar\lambda_2(x, s, \mu_+)$ and $\eta = \epsilon_+/(1-\delta) < 1$ :

x_+ \in \operatorname{int}K,\quad s_+ \in \operatorname{int}K^*,\quad \mu(x_+, s_+) = \mu_+,\quad \lambda_2(x_+, s_+) = \bar\lambda_2(x_+, s_+, \mu_+) \le \frac{(2 + \delta - \kappa)(\epsilon + \kappa)^2}{(1-\delta)^2(1-\kappa)^3}.

The constant $\kappa \in (0,1)$ and $\beta \in (0,1)$ are free; no numerical choice is hard-coded.

Milestones

Theorem 3.6 (norms at neighbouring points), Lemma 3.13 and Corollary 3.14 (scaling-point Hessian versus the Hessians at $x$ and $s$ ), Lemma 6.2 (effect of decreasing $\mu$ ), (6.10) (the gap after the step), and Lemma 6.3 (size of the step, feasibility, norms at $x_+$ ).

Companion results

The Algorithm 6.1 invariant ( $\beta = 1/10$ , $\kappa = 1/15$ : iterates stay in $N(1/10)$ while $\mu$ shrinks by $1 - (15\sqrt\nu)^{-1}$ ), Theorem 6.5 (the predictor step length $\alpha^* \ge (10\sqrt\nu)^{-1}$ ), and Lemma 6.1.

Significance

Theorem 6.4 is the one-step estimate behind the $O(\sqrt\nu\ln(\langle s_0, x_0\rangle/\zeta))$ iteration bound of the short-step method on every symmetric cone, and with it of the most widely used complexity bounds for semidefinite and second-order cone programming. The same estimate, with $\kappa = 0$ , certifies the corrector step of the predictor-corrector method (Algorithm 6.3).

The results are proved in the paper; none is formalized. A Lean development would provide a machine-checked core of conic interior-point theory: the local-norm calculus of self-scaled barriers (Theorem 3.6, Lemma 3.13), which is reused across all the methods of the paper, and a verified complexity statement for an algorithm family used in practice. The companion mission on the functional-proximity method (Theorem 7.1 of the same paper) shares the setting.

Difficulty

The obvious argument expands $s_+ + \mu_+F'(x_+)$ and bounds each term by self-concordance. Generic self-concordance controls norms at a new point only under $\|x_+ - x\|_x < 1$ and gives constants that do not close the recursion with $\beta = 1/10$ ; it also says nothing about the dual side. The proof needs properties special to self-scaled barriers: the scaling point $w$ and the two-sided comparison of $F''(w)/\mu$ with $F''(x)$ (Lemma 3.13), norm comparisons under the weaker hypothesis $|x_+ - x|_x < 1$ (Theorem 3.6), and a third-derivative bound from Nesterov–Todd 1997. In Lean, none of the self-scaled barrier theory, conjugate barriers on cones, or local norms exists in Mathlib.

Formalization scope

$E$ is EuclideanSpace ℝ (Fin n) and $E^*$ is identified with $E$ through the inner product. Because the paper distinguishes primal and dual norms by the space of the argument, the formalization names them: lnorm G v u (same space as $v$ ) and dnorm G v u (other space, through the inverse Hessian), for $G = F$ or $G = F_*$ ; sigma C c u and absn C c u take the cone and the centre explicitly. The conjugate is a real supremum over $\operatorname{int}K$ and is only evaluated in $\operatorname{int}K^*$ . $\lambda_2$ , $\lambda_\infty$ use the first of their two printed forms.

Standing assumptions carried by every statement: $K$ proper, $F$ a $\nu$ -self-scaled barrier, and $\nu \ge 1$ (a consequence of pointedness that the paper derives). The barrier definition adds positive definiteness of $F''$ on $\operatorname{int}K$ , implied by the other conditions for a pointed cone. Theorem 6.4 adds $0 < \kappa < 1$ (the paper's "some fixed constant", forced by its proof) and the conclusion $x_+ \in \operatorname{int}K$ , $s_+ \in \operatorname{int}K^*$ from Lemma 6.3. Assumptions (2.4)–(2.5) are implied by the strictly feasible starting point. In Theorem 3.6 the middle factors of (3.12) are corrected to $(1 - p_+)$ and $(1 + p_-)$ ; the printed ones fail for the half-line.

Search directions are any solution of their linear systems; their existence is not assumed. The goal assumes no bound from Lemmas 6.2–6.3 and no value of $\mu(x_+, s_+)$ , so it cannot be discharged by restating its hypotheses.

Needed infrastructure: derivatives of logarithmically homogeneous functions ((2.7)–(2.10)), properties of the conjugate barrier ((2.12)–(2.16)), the existence and properties of scaling points (Nesterov–Todd 1997), and the local norm inequalities of self-concordant functions. These are reusable for any interior-point formalization; contributions of such lemmas are welcome.

Selected references

Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Math. Oper. Res. 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
O. Güler, Barrier functions in interior point methods, Math. Oper. Res. 21 (1996) 860–885. https://doi.org/10.1287/moor.21.4.860
M. Kojima, S. Mizuno and A. Yoshise, A primal-dual interior point algorithm for linear programming, in Progress in Mathematical Programming, Springer, 1989, 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
S. Mizuno, M. J. Todd and Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Math. Oper. Res. 18 (1993) 964–981. https://doi.org/10.1287/moor.18.4.964

11 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 2: Wendel's Formula E[exp(−λ/V_n)] = e^{−λ} φ_α(λ)^{n−1} ψ_α(λ)^{−n} for PD(α, 0)Research Paper

Motivation

A random discrete distribution is a random sequence of nonnegative numbers summing to $1$ . Ranked in decreasing order, $V_1\ge V_2\ge\cdots$ , such sequences model the relative sizes of species in a population, of cycles of a random permutation, of excursion intervals of a Markov process, and of atoms of random measures used as priors in Bayesian nonparametrics. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ is the main family of such laws; Pitman and Yor (Ann. Probab. 1997) derived its properties from a stable subordinator.

The special case $\mathrm{PD}(\alpha,0)$ , $0<\alpha<1$ , describes the ranked lengths of the excursion intervals of a stable( $\alpha$ ) subordinator's range, or of a Bessel process away from zero, up to time $1$ . A basic question about it is the law of a single ranked term $V_n$ . The answer goes through the Laplace transform of $1/V_n$ :

Darling (1952) found the characteristic function of the limit of $S_n/X_{(n,1)}$ (sum over maximum of i.i.d. heavy-tailed variables), which is that of $1/V_1$ .
Lamperti (1961) derived the corresponding Laplace transform from renewal theory, for $n=1$ .
Wendel (1964) obtained the transform for every $n\ge2$ from the range of a stable subordinator.
Pitman and Yor (1997), Proposition 11, explained the formula through an exact decomposition of $1/V_n$ into independent, infinitely divisible pieces.

Setting

Fix $0<\alpha<1$ . Let $\tilde Y_1,\tilde Y_2,\dots$ be independent, with $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha,n\alpha)$ on $(0,1)$ . Form the stick-breaking sequence $\tilde V_1=\tilde Y_1$ and $\tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$ for $n\ge2$ , and let $V_1\ge V_2\ge\cdots$ be its terms in decreasing order. The law of $(V_n)$ is $\mathrm{PD}(\alpha,0)$ (Definition 1 of the paper, with $\theta=0$ ).

From $(V_n)$ define $R_n=V_{n+1}/V_n$ , $A_0=0$ and, for $n\ge1$ ,

A_n=\frac{V_1+\cdots+V_n}{V_{n+1}},\qquad \Sigma_n=\frac{V_{n+1}+V_{n+2}+\cdots}{V_n}.

For $\lambda\ge0$ the paper's two Laplace exponents are

\phi_\alpha(\lambda)=\alpha\int_1^\infty e^{-\lambda x}x^{-\alpha-1}\,dx,\qquad \psi_\alpha(\lambda)=1+\alpha\int_0^1\left(1-e^{-\lambda x}\right)x^{-\alpha-1}\,dx,

and $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

The proof represents $(V_n)$ through a Poisson random measure (PRM) $\Lambda_\alpha$ on $(0,\infty)$ with $\Lambda_\alpha(x,\infty)=Cx^{-\alpha}$ : its ranked points $\Delta_1>\Delta_2>\cdots$ satisfy $X_n:=C\Delta_n^{-\alpha}=\varepsilon_1+\cdots+\varepsilon_n$ with $\varepsilon_i$ i.i.d. standard exponential, and $V_n=\Delta_n/\sum_m\Delta_m$ .

Formalization targets

Goal: Proposition 11

For every $n\ge1$ ,

\frac1{V_n}=1+A_{n-1}+\Sigma_n\quad\text{a.s.},

where (i) $A_{n-1}$ is distributed as the sum of $n-1$ independent copies of $A_1$ , with $E[e^{-\lambda A_{n-1}}]=\phi_\alpha(\lambda)^{n-1}$ ; (ii) $\Sigma_n$ is distributed as the sum of $n$ independent copies of $\Sigma_1$ , with $E[e^{-\lambda\Sigma_n}]=\psi_\alpha(\lambda)^{-n}$ ; (iii) $A_{n-1}$ and $\Sigma_n$ are independent.

Milestones

Proposition 10 (iii): $X_n=LV_n^{-\alpha}$ , with $L=\lim nV_n^\alpha$ , are the arrival times of a unit Poisson process, and $V_n=X_n^{-1/\alpha}/\sum_mX_m^{-1/\alpha}$ .
Lemma 24 (i)–(ii): $C\Delta_n^{-\alpha}$ is gamma $(n)$ ; the ratios $\Delta_i/\Delta_n$ , $i<n$ , are the order statistics of $n-1$ i.i.d. variables of density $\alpha x^{-\alpha-1}$ on $(1,\infty)$ , independent of $(\Delta_n,\Delta_{n+1},\dots)$ .
(66): $P(A_1\in dx)=\alpha x^{-\alpha-1}dx\,1(x>1)$ .
(67): $E[e^{-\lambda\Sigma_n}\mid\Delta_1,\dots,\Delta_n]=\exp\left(-\Delta_n^{-\alpha}\int_0^1(1-e^{-\lambda u})\Lambda_\alpha(du)\right)$ .
Proposition 8: the $R_n$ are independent and $R_n\sim\mathrm{beta}(n\alpha,1)$ .
(34): $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

Consequence: Corollary 12 (Wendel's formula)

E\left[\exp(-\lambda/V_n)\right]=e^{-\lambda}\,\phi_\alpha(\lambda)^{n-1}\,\psi_\alpha(\lambda)^{-n}\qquad(\lambda\ge0).

Significance

The result. Proposition 11 turns $1/V_n$ into the sum of the constant $1$ and two independent variables, each a sum of i.i.d. pieces with explicit Laplace exponents. Wendel's formula (38) is a one-line consequence, and since $1/V_n>0$ it determines the law of $V_n$ . The same decomposition is reused later in the paper: Proposition 26 combines (35) and (67) into a conditional form of (38) given $R_1,\dots,R_{n-1}$ and $X_n$ , which the paper uses in later calculations.

Formalizing it. All results here are proved in the paper; none is machine-checked. A formal proof needs the Poisson representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10, itself resting on Perman–Pitman–Yor 1992), elementary but non-trivial facts about Poisson arrival times (gamma laws, order statistics, independence of ratios), and a conditional Laplace functional of a Poisson process. Each milestone is a self-contained target; Lemma 24 and (67) are statements about Poisson arrival times only and do not mention Poisson–Dirichlet laws.

Difficulty

The identity $1/V_n=1+A_{n-1}+\Sigma_n$ is algebra once $\sum_mV_m=1$ . The content is in the laws. On the stick-breaking side, the $V_n$ are the order statistics of a dependent sequence, and neither $A_{n-1}$ nor $\Sigma_n$ has an evident structure: the ranking destroys the independence of the $\tilde Y_n$ . The proof passes to the Poisson side, where the ranked points of a PRM have tractable conditional laws, and then must transport the conclusions back through a representation that holds only in distribution. Part (ii) requires a conditional computation (67) given $n$ points, followed by integration against a gamma law; part (iii) requires the mutual independence of all the ratios $R_n$ , an infinite family.

Formalization scope

The Lean development lives in namespace PoissonDirichlet.Wendel; its definitions file contains every object above.

Sequences are 0-based: V ω k is $V_{k+1}$ , Aseq (V ω) k is $A_k$ , Sigseq (V ω) k is $\Sigma_{k+1}$ , ratio (V ω) k is $R_{k+1}$ . Exponents $n-1$ and $n$ become k and k + 1.
$\mathrm{PD}(\alpha,0)$ is Definition 1 with $\theta=0$ . The law of $(\tilde Y_n)$ is a probability measure on sequences with independent coordinates of the stated beta laws. " $V$ has law $\mathrm{PD}(\alpha,0)$ " means $P(V\in s)$ equals the mass of the preimage of $s$ under the ranked stick-breaking map, for every measurable $s$ . Ranked values are defined with the extended cardinal Set.encard.
$A_n$ and $\Sigma_n$ are the $V$ -quotients of (31)–(32), not the $R$ -expressions; $\phi_\alpha,\psi_\alpha$ are the integrals (33)–(34), not Laplace transforms.
"Distributed as the sum of $m$ independent copies of $X$ " is equality with the $m$ -fold convolution power of the law of $X$ , the Dirac mass at $0$ when $m=0$ .
Every statement carries $0<\alpha<1$ except Lemma 24, which holds for all $\alpha>0$ .
The local time $L$ of (24) is a random variable with the hypothesis that $nV_n^\alpha\to L$ almost surely; this is its definition.
The PRM is used only through its ranked points, encoded by arrival times: $\Delta_n=(C/X_n)^{1/\alpha}$ with $X_n=\varepsilon_1+\cdots+\varepsilon_n$ , $\varepsilon_i$ i.i.d. standard exponential. This is the paper's own (27)–(28). In (67) the $\varepsilon_i$ are also assumed measurable, so that the conditioning $\sigma$ -algebra is a sub- $\sigma$ -algebra.
Lemma 24 (iii) is not stated; its only use is (67), which is stated. Corollary 12 states only the formula (38).

The formalization does not use Measure.map of a possibly non-measurable map in any definition: every equality of laws for such maps is stated through preimages. It does not use Set.ncard or limUnder. Every Laplace transform is the integral of a function with values in $(0,1]$ , and both exponent integrals are integrable under the stated parameter range, so no statement holds because an integral takes the junk value $0$ .

Useful infrastructure beyond this mission: arrival times of a Poisson process and their gamma and order-statistic laws; convolution powers of measures on $\mathbb R$ ; the Laplace functional of a Poisson random measure. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992.
J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964.
J. Lamperti, A contribution to renewal theory, Proc. Amer. Math. Soc. 12:724–731, 1961.
D. A. Darling, The influence of the maximum term in the addition of independent random variables, Trans. Amer. Math. Soc. 73:95–107, 1952.

9 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 1: Under PD(α, 0) the Ratios V_{n+1}/V_n Are Independent with beta(nα, 1) LawsResearch Paper

Motivation

Random partitions describe a population split into species, clusters, or types. If the species frequencies are put in decreasing order, the first frequency is the largest species, the second is the next largest, and so on. The Poisson–Dirichlet distribution gives a family of laws for these ranked frequencies. Its two parameters connect different random partition models, while the one-parameter case $\mathrm{PD}(\alpha,0)$ has a particularly direct description through ratios of neighboring frequencies. Pitman and Yor state that these ratios are independent and have explicit beta distributions, even though the ranked frequencies themselves have a complicated joint law (Pitman and Yor 1997, Proposition 8).

The result matters when a statistic of a random partition depends on the relative sizes of its largest components. A ratio $V_{n+1}/V_n$ describes the gap between two successive ranked species without requiring their total scale. An independent sequence of such ratios also gives a way to generate the entire ranked sequence. The paper records this converse immediately after Proposition 8 as Corollary 9 (Pitman and Yor 1997, p. 862).

Setting

Fix $0<\alpha<1$ . A beta $(a,b)$ distribution is a probability distribution on $(0,1)$ with density proportional to $x^{a-1}(1-x)^{b-1}$ . Let $\widetilde Y_n$ , for $n=1,2,\ldots$ , be independent beta $(1-\alpha,n\alpha)$ random variables. They break an initial mass of one into successive stick lengths

\widetilde V_n=\widetilde Y_n\prod_{i=1}^{n-1}(1-\widetilde Y_i).

Sort these lengths in decreasing order, counting repeated values separately, and write the resulting sequence as $V_1\geq V_2\geq\cdots$ . The law of this ranked sequence is $\mathrm{PD}(\alpha,0)$ , the $\theta=0$ case of Definition 1 in the paper (Pitman and Yor 1997, p. 857). The paper's broader definition takes $0\leq\alpha<1$ and $\theta>-\alpha$ , with beta $(1-\alpha,\theta+n\alpha)$ stick factors. This mission retains that general definition so later statements use the same object, but its theorems concern $\theta=0$ and $0<\alpha<1$ .

Define the adjacent ranked ratio $R_n=V_{n+1}/V_n$ . The source proves that the ranked masses are strictly positive almost surely under the Poisson–Dirichlet law, so these ratios have their ordinary probabilistic meaning (Pitman and Yor 1997, Proposition 2). The random sequence $R_1,R_2,\ldots$ is different from the independent stick factors $\widetilde Y_n$ : the latter are defined before ranking, whereas each $R_n$ compares consecutive masses after ranking.

Formalization targets

Goal: Proposition 8

For a sequence $(V_n)$ with $\mathrm{PD}(\alpha,0)$ law, the variables $R_n=V_{n+1}/V_n$ are mutually independent, and each has beta $(n\alpha,1)$ distribution. The equivalent cumulative distribution formula is part of the target:

\mathbb P(R_n\leq r)=r^{n\alpha}\qquad(n\geq1,\ 0\leq r\leq1).

The exponent and beta parameter use the paper's one-based $n$ . Independence concerns the full infinite family, rather than only pairs of ratios (Pitman and Yor 1997, Proposition 8, equations (21)–(22)).

Supporting targets

Proposition 10(i) establishes a local-time limit $L=\lim_{n\to\infty}nV_n^\alpha$ , both almost surely and in $L^p$ for every real $p\geq1$ . Proposition 10(iii) identifies the transformed sequence $X_n=LV_n^{-\alpha}$ with the arrival times of a unit-rate Poisson process: it has the joint law of partial sums of independent standard exponential variables. The proposition also recovers $V_n$ by normalizing $X_n^{-1/\alpha}$ . Finally, the proof of Proposition 8 states that consecutive Poisson arrival ratios $X_n/X_{n+1}$ are independent beta $(n,1)$ variables (Pitman and Yor 1997, pp. 862, 870). These are the three curated milestones. Corollary 9 is included as a companion: independent beta $(n\alpha,1)$ ratios, inserted into the paper's convergent series and finite products, produce a $\mathrm{PD}(\alpha,0)$ sequence.

Significance

Proposition 8 converts a statement about the order statistics of infinitely many dependent masses into an explicit product law for their ratios. It gives direct distributional information about every neighboring pair in a Poisson–Dirichlet partition. Together with Corollary 9, it specifies both how to read the ratios from a ranked partition and how to reconstruct a ranked partition from ratios. The formulas can therefore serve as a common interface for calculations and simulation involving $\mathrm{PD}(\alpha,0)$ (Pitman and Yor 1997, Propositions 8–10).

The mathematical results in this mission were proved in the 1997 paper; the open work here is a machine-checked Lean proof of their stated forms. Such a development would add reusable facts about infinite beta sequences, ranked stick lengths, Poisson arrival times, and their joint laws. The independent-arrival-ratio statement is useful beyond the Poisson–Dirichlet setting because its assumptions only concern standard exponential increments.

Difficulty

The stick factors are independent before their lengths are sorted, but sorting is a global operation: a particular ranked mass may have come from any stick index. Their independence therefore does not directly give independence of adjacent ranked ratios. Even a marginal calculation for one ratio does not establish mutual independence of the entire sequence. The local-time and arrival-time assertions in Proposition 10 encode the extra structure needed to state the joint result. The real technical burden is to relate the distribution obtained from ranked stick lengths to the distribution of an infinite Poisson arrival sequence, while retaining the almost-sure limits and normalization stated by the authors.

Formalization scope

Lean represents every sequence as a function $\mathbb N\to\mathbb R$ , with index $k=0$ denoting the paper's first index $n=1$ . stick implements equation (4); ranked defines the $(k+1)$ -st largest nonnegative length by upper-level-set cardinality, counted with multiplicity. It uses extended cardinality so an infinite upper-level set cannot be assigned cardinality zero. IsStickLaw records independence and the beta $(1-\alpha,\theta+(k+1)\alpha)$ coordinate laws. HasPD describes the distribution of the ranked stick sequence by probabilities of measurable preimages. This commits the mission to Definition 1 rather than a ratio construction of $\mathrm{PD}(\alpha,0)$ .

All mission theorems require $0<\alpha<1$ , and every source probability space is a probability measure. Ratios and negative real powers occur only as random quantities whose bases are positive almost surely under that law. Their exceptional values on null sets do not affect the distributional claims. The local time is identified by its almost-sure defining limit, rather than by a default value assigned when a limit fails. The $L^p$ clause uses the norm of the approximation error. The Poisson arrival law is stated jointly on measurable sets of infinite real sequences; it is not reduced to one-dimensional exponential marginals. These choices rule out vacuous interpretations through a nonmeasurable Measure.map, a finite-cardinality default on an infinite set, a junk integral, limUnder at a nonexistent limit, or a dropped parameter range.

The development needs Mathlib's beta and exponential measures, infinite product and independence APIs, measurable sequence spaces, real powers, infinite sums, and $L^p$ norms. Results about ranked values and arrival ratios would be reusable in later Poisson–Dirichlet missions. Contributions that establish these source statements at full strength, or their necessary measurable and summability infrastructure, fit the scope.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Annals of Probability 25(2):855–900, 1997. DOI: 10.1214/aop/1024404422.

5 thms2 active usersReviewed

Graph Theory Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms IV: A Uniform Flow of Size Ω(𝒮/log n) on Paths of Length O(C_max log n/(n𝒮))Research Paper

Motivation

Communication networks must route many source–destination demands through shared edges. A multicommodity flow describes how much of each demand can be carried simultaneously without exceeding an edge's capacity. In an undirected network, a cut bounds the traffic that can pass between two groups of vertices, but many commodities can interfere even when no single cut is obviously restrictive. Leighton and Rao showed that the uniform concurrent flow is within a logarithmic factor of the corresponding sparsest-cut bound Leighton and Rao, 1999.

For routing, flow value alone is incomplete: a feasible flow can use long detours. Section 2.5 of the same paper establishes that a flow of the guaranteed size can be carried on paths whose number of edges is also controlled. The result supports the paper's discussion of low-congestion, low-dilation routing in communication networks, where a long route can increase latency or complicate scheduling even if every edge has sufficient capacity Leighton and Rao, 1999, §2.5.

Setting

Let $V$ be a finite set of $n\ge2$ vertices. An undirected capacitated network has a symmetric capacity $C(u,v)\ge0$ for each pair, with $C(u,u)=0$ . A pair is an edge when its capacity is positive. Parallel physical edges can be combined by adding their capacities. The network is connected: every nonempty proper subset $U\subsetneq V$ has positive cut capacity $C(U,\bar U)=\sum_{u\in U,v\notin U}C(u,v)$ , where $\bar U=V\setminus U$ .

The uniform multicommodity flow problem gives one unit of demand to each unordered pair of distinct vertices. Equivalently, it gives demand $1/2$ to each ordered pair $(s,t)$ with $s\ne t$ Leighton and Rao, 1999, footnote 2. A concurrent flow of value $\lambda$ routes the fraction $\lambda$ of every demand. Traffic in both directions of an undirected edge shares that edge's capacity. The demand crossing $U$ is $|U|\,|\bar U|$ , so the uniform min-cut, also called the sparsest-cut value, is

\mathcal S=\min_{\varnothing\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.

For a flow path, length means its number of edges. A separate nonnegative symmetric distance function $d$ assigns lengths to edges; its total weight is $W=\sum_e C(e)d(e)$ . Given a hop budget $L$ , let $d_L(u,v)$ be the smallest $d$ -length of a walk from $u$ to $v$ using at most $L$ edges. The value is $\infty$ if no such walk exists. The maximum capacity incident to one vertex is $C_{\max}=\max_v\sum_u C(v,u)$ . The paper uses $\log n=\log_2n$ and $\ln n$ for the natural logarithm Leighton and Rao, 1999, footnote 3.

Formalization targets

A large uniform flow with short paths

Theorem 18 asserts the existence of absolute constants $c_1,c_2>0$ such that every network in the setting above admits a concurrent uniform flow of value $\lambda$ whose every route has at most $L$ edges, with

\lambda\ge c_1\frac{\mathcal S}{\log_2 n},\qquad L\le c_2\frac{C_{\max}\log_2 n}{n\mathcal S}.

The constants precede the choice of network: they cannot depend on its size or capacities. The goal gives an actual flow and integer hop limit, not only a lower bound on a supremum Leighton and Rao, 1999, Theorem 18.

The dual and geometric estimates

The short-path linear-programming dual uses $d_L$ in its distance constraint, $\frac12\sum_{u,v}d_L(u,v)\ge1$ , and minimizes $W$ . Lemma 19 partitions a network into components with both edge-radius at most $\Delta C/W$ and distance-radius at most $\Delta$ , while the capacity between components is at most $4W\log_2n/\Delta$ . Corollary 20 finds a component with at least $2n/3$ vertices when $0<W\le\mathcal S/(36\log_2n)$ . Lemma 21 bounds the sum of $L/4$ -restricted distances from any such large set to its complement by $6W/(n\mathcal S)$ , provided $L\ge12C_{\max}\ln n/(n\mathcal S)$ . These are the mission's milestones, in source order Leighton and Rao, 1999, pp. 808–809.

Significance

Theorem 18 places simultaneous lower and upper guarantees on a routing solution: it carries a substantial fraction of every uniform demand, while each route uses a bounded number of edges. Its hop guarantee is stronger than simply knowing that the unconstrained maximum flow is large. The result is one of the paper's inputs for reasoning about routing paths with low congestion and dilation; the paper also says analogous short-path results extend to product and directed flow problems, without presenting all their details Leighton and Rao, 1999, p. 811.

The known mathematical result has a published proof; this mission asks for machine-checked statements and proofs. A complete development would establish the hop-indexed flow model, the restricted shortest-path duality, and the two-radius partition estimates in Lean. The network, proper-cut, and extended-distance interfaces can be reused in later work on sparse cuts and length-constrained routing. No machine-checked proof of this exact theorem is claimed here.

Difficulty

The ordinary approximate max-flow/min-cut theorem controls the amount of concurrent traffic but does not bound the number of edges on each route. Restricting routes changes the dual: a shortest path that exceeds the hop budget is unavailable, and some vertex pairs have no allowed path at all. Assigning such a pair distance zero would alter the dual constraint. The geometric estimates must control both hop count and $d$ -length on the same connecting paths, since bounds witnessed by two unrelated paths cannot be combined into one short route Leighton and Rao, 1999, §2.5.

Formalization scope

The vertex type is finite and has at least two members. Capacities are real, symmetric and nonnegative; zero-capacity pairs are absent from the graph. Connectivity is the paper's standing cut assumption. The min-cut ranges over nonempty proper subsets, so no expression divides by a zero cardinality. Demands use the paper's ordered-pair $1/2$ convention. A short flow is a nonnegative commodity–hop–arc array whose equations inject, conserve and absorb traffic; the capacity constraint combines both directions and all hops. The maximum flow is a supremum over feasible values. Its use is confined to the positive-demand finite setting, where the feasible set is nonempty and bounded.

Restricted distances take values in extended nonnegative reals, so an empty family of allowed walks has value $\infty$ . The radius predicate requires one walk inside a component to meet both bounds. $\log_2$ appears in Theorem 18, Lemma 19 and Corollary 20; Lemma 21's threshold uses $\ln$ . For expressions dividing by $W$ , the formal statements require $W>0$ ; this makes the printed radius meaningful. The explicit companion theorem uses the hop limit $\lfloor L\rfloor$ for the paper's real $L$ , which is what "at most $L$ edges" means; Lemma 21 keeps $L$ real. The polynomial-time search claim is outside this existence formalization. A definition making every restricted distance zero, or quantifying its asymptotic constants after the network, would make the goal a different theorem.

Contributions may include finite-flow and linear-programming duality, path decomposition for the hop-indexed formulation, the partition estimate, the large-component corollary, or the restricted-distance estimate. The same finite graph and extended-distance definitions may serve subsequent missions.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, Journal of the ACM 46(6):787–832, 1999. DOI: 10.1145/331524.331526.

7 thms2 active usersReviewed

Dynamical Systems Operations Research Probability+1·Captain: mikedeng1

Subadditive Ergodic Theory 5: For a Stationary Sequence in a Banach Algebra with E(log‖Y₁‖)⁺ < ∞, n⁻¹ log‖Y₁⋯Y_n‖ Converges in [−∞, ∞)Research Paper

Motivation

Products of random linear operators appear wherever a system evolves by repeated application of randomly chosen linear maps: linear recursions with random coefficients, products of random matrices in statistical physics, the growth of random dynamical systems, and population models in random environments. The basic question is the exponential growth rate of the product $Y_1Y_2\cdots Y_n$ . For square matrices, Furstenberg and Kesten (Ann. Math. Statist. 31, 1960) proved that $n^{-1}\log\|Y_1\cdots Y_n\|$ converges for stationary sequences with a logarithmic moment condition.

Kingman (Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973) showed that this limit theorem is an instance of the subadditive ergodic theorem, and that the instance needs nothing of matrices beyond the norm inequality $\|AB\|\le\|A\|\,\|B\|$ . His Theorem 6 therefore holds in an arbitrary real or complex Banach algebra, including infinite-dimensional ones such as infinite matrices with finite $\ell_1$ norm. It is the source of what later became known as the top Lyapunov exponent of a stationary random operator product.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. A two-parameter family is a collection $x=(x_{st})$ of random variables indexed by nonnegative integers $s<t$ . Kingman's conditions (§1.1–1.2) are:

S₁: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ ;
S₂: the joint distributions of $(x_{s+1,t+1})$ are the same as those of $(x_{st})$ ;
S₃: $g_t=E(x_{0t})$ is finite for every $t\ge1$ and $g_t\ge -At$ for some constant $A$ ;
S₃′: $E(x_{01}^+)<\infty$ , where $x^+=\max(x,0)$ .

A family of real random variables satisfying S₁, S₂ and S₃ is a subadditive process. Kingman's Theorem 1 (the goal of the first mission of this series) says that for a subadditive process $x_{0t}/t$ converges almost surely and in mean to a finite random variable $\xi$ with $E(\xi)=\gamma=\inf_{t\ge1}g_t/t$ .

A Banach algebra $\mathfrak B$ is a complete normed algebra over $\mathbb R$ or $\mathbb C$ whose norm satisfies $\|AB\|\le\|A\|\,\|B\|$ . A sequence $(Y_n)_{n\ge1}$ of $\mathfrak B$ -valued random elements is stationary if $(Y_{n+1})_{n\ge1}$ and $(Y_n)_{n\ge1}$ have the same joint law. The log-norm process is

x_{st}=\log\|Y_{s+1}Y_{s+2}\cdots Y_t\|\in[-\infty,\infty),\qquad s<t,

with $\log 0=-\infty$ . Expectations of $[-\infty,\infty)$ -valued variables are extended expectations $E(f)=\int f^+\,dP-\int f^-\,dP$ , defined when $\int f^+\,dP<\infty$ and possibly equal to $-\infty$ .

Formalization targets

Goal: Theorem 6 (p. 893)

If $(Y_n)$ is a stationary sequence in a real or complex Banach algebra and $E\{(\log\|Y_1\|)^+\}<\infty$ , then

\xi=\lim_{n\to\infty}n^{-1}\log\|Y_1Y_2\cdots Y_n\|

exists in $-\infty\le\xi<\infty$ with probability one, and

E(\xi)=\lim_{n\to\infty}n^{-1}E\{\log\|Y_1Y_2\cdots Y_n\|\}.

The goal fixes no constant and no ergodicity assumption: $\xi$ is in general a non-degenerate random variable.

Milestones

(1.2.7), p. 885: under S₁, S₂ and S₃′, $E(x_{st}^+)<\infty$ for all $s<t$ .
Proof of Theorem 2, p. 886: the truncation $x^{(N)}_{st}=\max(x_{st},-N(t-s))$ is a subadditive process for every positive integer $N$ .
Theorem 2, p. 885: if $x$ satisfies S₁, S₂ and S₃′ but not S₃, then $\xi=\lim x_{0t}/t$ exists with probability one in $[-\infty,\infty)$ and $E(\xi)=-\infty$ .
Proof of Theorem 6, p. 893: the log-norm process satisfies S₁, S₂ and S₃′.

Significance

Theorem 6 defines a stochastic spectral radius: if every $Y_n$ equals a fixed element $y$ , then $e^\xi$ is the spectral radius of $y$ by Gelfand's formula, and for independent $Y_n$ with common law $\pi$ the limit is a constant $\rho(\pi)$ depending only on $\pi$ . For $k\times k$ matrices the theorem reduces to the Furstenberg–Kesten theorem. Theorem 2, the extension of the subadditive ergodic theorem from S₃ to S₃′, is the form needed whenever a process can have mean growth rate $-\infty$ , as happens for products that can vanish or contract superlinearly; it is used well beyond random products.

All results here are proved on paper (Kingman 1973, building on his 1968 paper). None of them is machine-checked: Mathlib has no subadditive ergodic theorem, no Furstenberg–Kesten theorem and no random-product limit in normed algebras. The platform poses an ergodic, constant-limit form of Kingman's theorem (PalmQueueing.Ergodic.kingman_subadditive, open); this mission's Theorem 2 is a different statement (non-ergodic, conclusion $E(\xi)=-\infty$ under failure of S₃). A complete development would give the first formal proof of the Furstenberg–Kesten limit, in the generality of Banach algebras.

Difficulty

Theorem 6 is short given Theorems 1 and 2, but the obvious one-line reduction to Theorem 1 fails in two places. First, the log-norm process can take the value $-\infty$ and its means $g_t$ can be $-\infty$ or decrease superlinearly, so condition S₃ fails and Theorem 1 does not apply; the case $E(\xi)=-\infty$ is a separate theorem (Theorem 2), whose proof must exchange a limit in $t$ with a limit in an auxiliary parameter. Second, stationarity of the log-norm process (S₂) is a statement about joint laws on a path space; in a non-separable Banach algebra, multiplication need not be measurable for the product $\sigma$ -algebra on $\mathfrak B\times\mathfrak B$ , so it is not automatic that the law of $(Y_n)$ determines the joint law of the products $Y_{s+1}\cdots Y_t$ . The main dependency, Theorem 1 itself, is the subject of a separate mission and is not restated here.

Formalization scope

The Lean development fixes these conventions:

Families are functions x : ℕ → ℕ → Ω → β; only pairs $s<t$ enter any condition. S₁ is required almost surely for each triple (the weaker hypothesis); the log-norm milestone proves it at every sample point.
S₂ and stationarity are equalities of laws of the whole path (Measure.map) on the product $\sigma$ -algebra, not equality of one-dimensional marginals.
S₃′ and all positive parts are lower Lebesgue integrals; expectations that may be $-\infty$ are computed as $\int f^+ - \int f^-$ in EReal, never as Bochner integrals (which return $0$ for non-integrable functions).
$\log\|\cdot\|$ is ENNReal.log of the norm, so $\log\|0\|=-\infty$ ; Real.log 0 = 0 would replace a vanishing product's growth rate $-\infty$ by $0$ , and is ruled out.
$\mathfrak B$ is a complete unital NormedRing with NormedAlgebra 𝕜 𝔅, RCLike 𝕜. Each $Y_n$ is strongly measurable; $\mathfrak B$ is not assumed separable.
Limits are Filter.atTop on ℕ in the topology of EReal; the conclusions assert $\xi<\infty$ almost surely, $E(\xi^+)<\infty$ , and, for (2.3.5), both the existence of the limit of means and its value.

A formalization that replaces the extended logarithm by Real.log, or the extended expectation by a Bochner integral, makes the statement false or trivially different, and is excluded.

Reusable infrastructure: extended expectations of EReal-valued random variables, joint-law stationarity of sequences and two-parameter families, and the truncation lemma for S₃′ processes. Contributions toward Theorem 1 (mission 1 of this series), toward measurability of products of strongly measurable random elements, and toward the milestones in any order are welcome.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30:499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31:457–469, 1960. https://doi.org/10.1214/aoms/1177705909

8 thms2 active usersReviewed

Dynamical Systems Operations Research Probability+1·Captain: mikedeng1

Subadditive Ergodic Theory 4: Furstenberg–Kesten — for Stationary Positive Random Matrices, n⁻¹ log [Y₁⋯Y_n]_ij Converges, Independently of i and jResearch Paper

Products of random matrices

Many systems evolve by repeated multiplication by a random linear map: the state of a linear system with randomly varying coefficients, population vectors in a random environment (Leslie models whose rates change from year to year), the transfer matrices of a disordered one-dimensional medium, and the transition operators of a Markov chain in a random environment. In each case the object of interest is the product $X_n = Y_1 Y_2 \cdots Y_n$ of random matrices and its growth as $n\to\infty$ .

The basic answer is due to Furstenberg and Kesten (Products of random matrices, Ann. Math. Statist. 31 (1960)): under a logarithmic moment condition and stationarity, $n^{-1}\log$ of the size of $X_n$ converges. Their proof was a substantial piece of analysis. In his 1973 IMS Special Invited Paper (Kingman, Subadditive ergodic theory, Ann. Probab. 1 (1973)), J. F. C. Kingman showed that for matrices with strictly positive entries the result is a short corollary of his subadditive ergodic theorem (Theorem 1 of that paper, 1968). This mission formalizes that application: Theorem 5 of the 1973 paper, §2.2, pp. 891–892.

Timeline:

1960: Furstenberg and Kesten prove convergence of $n^{-1}\log\|X_n\|$ and, for positive matrices, of $n^{-1}\log[X_n]_{ij}$ .
1968: Kingman proves the subadditive ergodic theorem (J. Roy. Statist. Soc. B 30).
1973: Kingman's survey deduces the positive-matrix theorem (Theorem 5) and the general Banach-algebra version (Theorem 6) from it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $k\ge1$ , and let $Y_1, Y_2,\dots$ be random $k\times k$ real matrices. Write $[A]_{ij}$ for the $(i,j)$ th entry of a matrix $A$ , and

X_n = Y_1 Y_2\cdots Y_n \qquad (2.2.1),

the product taken left to right. The sequence $(Y_n)$ is stationary if the joint law of $(Y_2, Y_3, \dots)$ equals the joint law of $(Y_1, Y_2, \dots)$ ; this is a statement about all finite-dimensional distributions at once, and it includes the case of independent identically distributed matrices.

The proof works with the diagonal process

z_{st} = [Y_{s+1}Y_{s+2}\cdots Y_t]_{11},\qquad x_{st} = -\log z_{st}\qquad (s<t),

and with the $\ell_1$ -norm $\|A\| = \max_i \sum_j |[A]_{ij}|$ . A family $(x_{st})_{s<t}$ is a subadditive process (§1.1) if S₁: $x_{su}\le x_{st}+x_{tu}$ for $s<t<u$ ; S₂: the joint distributions of $(x_{s+1,t+1})$ equal those of $(x_{st})$ ; S₃: $g_t=E(x_{0t})$ exists and $g_t\ge -At$ for some constant $A$ .

Formalization targets

Goal: Theorem 5

Suppose the elements of the matrices $Y_n$ are strictly positive, $E|\log[Y_n]_{ij}|<\infty$ for every $n$ and every $i,j$ , and $(Y_n)$ is stationary. Then there is one finite random variable $\lambda$ such that for every $(i,j)$

\lambda = \lim_{n\to\infty} n^{-1}\log [X_n]_{ij} \qquad (2.2.2)

with probability one and in mean. The limit is random in general (it is constant when $(Y_n)$ is ergodic); the theorem asserts its existence, its finiteness and its independence of $(i,j)$ , and nothing about its value.

Milestones, in the order of the paper's proof

(2.3.1): $[AB]_{11}\ge[A]_{11}[B]_{11}$ for matrices with strictly positive entries.
$x_{st}=-\log z_{st}$ satisfies S₁ and S₂, and each $x_{st}$ has finite expectation $g_{t-s}$ .
$E\{\log\|Y_1\|\}<\infty$ and $g_n/n\ge -E\{\log\|Y_1\|\}$ for all $n\ge1$ , so S₃ holds.
The limit (2.2.2) exists, with probability one and in mean, for $i=j=1$ .
(2.2.3): for every $(i,j)$ , $P\{\liminf n^{-1}\log[X_n]_{ij}\ge\lambda\}=1$ .
For every $(i,j)$ , $P\{\limsup n^{-1}\log[X_n]_{ij}\le\lambda\}=1$ .

Significance

The limit $\lambda$ is the top Lyapunov exponent of the random product: it is the almost-sure exponential growth rate of every entry, and hence of every norm, of $X_n$ . It governs the stability of random linear recursions $v_{n}=v_{n-1}Y_n$ , the long-run growth rate of populations in random environments, and localization in one-dimensional disordered systems. Theorem 5 is the existence statement on which all of these quantitative questions rest.

The theorem has been proved since 1960, and Kingman's derivation is a classical model application of subadditive ergodic theory. To our knowledge it has no machine-checked proof: Mathlib has neither Kingman's subadditive ergodic theorem nor any limit theorem for random matrix products. This mission produces a formal statement of the result together with the formal decomposition of the proof into the steps Kingman writes down; its milestone 4 is exactly where the subadditive ergodic theorem (the goal of the companion mission Subadditive Ergodic Theory 1) is applied.

Difficulty

Milestones 1–3 are deterministic matrix inequalities plus integrability bookkeeping; the substance is elsewhere. First, milestone 4 needs the full subadditive ergodic theorem, almost-sure and in mean, for a non-ergodic stationary process: the classical Birkhoff theorem does not apply, because $\log[X_n]_{11}$ is not a sum of stationary increments. Second, passing from the diagonal entry to all entries requires controlling $n^{-1}\log[Y_n]_{1j}$ along a stationary sequence with only a first-moment hypothesis, and transporting an almost-sure statement about $X_n'=Y_2\cdots Y_{n+1}$ back to $X_n$ by stationarity, where the limit $\lambda$ is itself random. The natural shortcut — treating $\lambda$ as a constant — is only valid under ergodicity, which is not assumed.

Formalization scope

Matrices are Matrix (Fin k) (Fin k) ℝ with NeZero k; the paper's index $1$ is 0 : Fin k. The sequence is Y : ℕ → Ω → Matrix …, read only for $n\ge1$ ; Y 0 plays no role.
Products are ordered: $Y_{s+1}\cdots Y_t$ is the List.prod of [Y (s+1), …, Y t]; $X_0$ is the identity.
Stationarity is equality of the laws of $(Y_{n+2})_{n\ge0}$ and $(Y_{n+1})_{n\ge0}$ on ℕ → Fin k → Fin k → ℝ with the product σ-algebra. Independence is not assumed.
Positivity holds for every outcome; "their logarithms have finite expectations" is integrability of every $\log[Y_n]_{ij}$ , $n\ge1$ .
"Finite limit" is a real-valued lam : Ω → ℝ; "in mean" is $E|n^{-1}\log[X_n]_{ij}-\lambda|\to0$ with $\lambda$ integrable; time is $n\in\mathbb N$ with Filter.atTop. One lam serves all $(i,j)$ .
Lim inf and lim sup inequalities are stated with $\varepsilon$ : almost surely, for every $\varepsilon>0$ , eventually $n^{-1}\log[X_n]_{ij}\ge\lambda-\varepsilon$ (respectively $\le\lambda+\varepsilon$ ), which avoids the junk value of a real liminf on unbounded sequences.
Real.log 0 = 0 in Lean; the statements apply log only to entries that are strictly positive under the hypotheses, so no junk value enters. Dropping the positivity hypothesis would change the theorem, and is not an acceptable shortcut.
The S₁/S₂ vocabulary of §1.1 comes from the group's shared process module; this mission defines $g_t$ locally. The general subadditive ergodic theorem is not restated here, and milestone 4 is the object-specific statement the paper writes.

Welcome contributions: proofs of the matrix inequalities, the integrability and stationarity transfer lemmas, a formal subadditive ergodic theorem (shared with the companion mission).

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31(2):457–469, 1960. https://doi.org/10.1214/aoms/1177705909
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

9 thms2 active usersReviewed

Dynamic Programming Linear Optimization Markov Chain+1·Captain: mikedeng1

Linear Programming and Markov Decision Chains 2: Representatives of Average Optimal Stationary Policies Are Optimal Dual Solutions, and Every Optimal Dual Solution Gives an Average Optimal PolicyResearch Paper

Motivation

A finite Markov decision process may have several recurrent classes under one policy. In that setting, its long-run reward depends on the initial state, and a single stationary distribution does not describe the whole decision problem. Hordijk and Kallenberg developed a linear program with two families of variables to handle this multichain case. Their Theorem 8 relates policies to feasible points of that program in both directions: optimal stationary policies give optimal dual solutions, and every optimal dual solution gives an average optimal stationary policy. This relationship explains why the dual program represents the original sequential decision problem rather than merely bounding its value. Hordijk and Kallenberg (1979)

An earlier frequency formulation associated stationary randomized policies with one family of occupation variables in a more restricted Markov-chain setting. The present theorem uses both $x$ and $y$ variables, and its policy comparison covers history-dependent randomized decisions. The corresponding formalization therefore addresses the finite multichain model of the 1979 paper, with its own dual equations and representative map. Hordijk and Kallenberg (1979), §§1 and 3.3

Setting

Let $E$ be a nonempty finite set of states. At state $i$ , an action $a$ is chosen from a nonempty finite set $A(i)$ . It earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}$ . The transition probabilities are nonnegative and sum to one over $j$ . A general policy $R$ may randomize and use the complete past history. Its average reward $\phi_i(R)$ is the liminf, as the horizon grows, of expected total reward divided by the horizon when the initial state is $i$ . The optimal value $\phi_i$ is the supremum of $\phi_i(R)$ over all such policies. A policy is average optimal when it attains that value at every state. These are the conventions of §2.1 of the paper. Hordijk and Kallenberg (1979), p. 353

A stationary randomized policy $\pi^\infty$ chooses each admissible action $a$ at state $i$ with a fixed probability $\pi_{ia}$ , independently of the epoch and history. Its transition matrix is $P(\pi)_{ij}=\sum_{a\in A(i)}\pi_{ia}p_{iaj}$ , and its reward vector is $r(\pi)_i=\sum_{a\in A(i)}\pi_{ia}r_{ia}$ . The Cesàro limit matrix $P^*(\pi)$ and deviation matrix $D(\pi)$ describe the recurrent and transient behavior of this finite chain. In particular, $\phi(\pi^\infty)=P^*(\pi)r(\pi)$ . Hordijk and Kallenberg (1979), p. 359

Fix positive state weights $\beta_j$ summing to one. The primal linear program minimizes $\sum_j\beta_j\widetilde\phi_j$ over pairs $(\widetilde\phi,\widetilde u)$ that are superharmonic: for every $i$ and $a\in A(i)$ , the first vector dominates its one-step expected continuation, and the sum of the two vectors dominates one-step reward plus the continuation of the second. The dual linear program maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative $x_{ia}$ and $y_{ia}$ satisfying the two flow equations (3) and (4). Variables are present only for admissible state-action pairs. The set $E_x$ consists of states where $\sum_a x_{ia}>0$ . Hordijk and Kallenberg (1979), pp. 356–357

For a feasible dual point $(x,y)$ , the associated policy $\pi(x,y)$ normalizes the $x$ row at states in $E_x$ and the $y$ row at other states. Conversely, equation (6) constructs a representative $(x(\pi),y(\pi))$ of a stationary randomized policy. Its $x$ coordinates use $\beta^TP^*(\pi)$ . Its $y$ coordinates use $\beta^TD(\pi)+\gamma^TP^*(\pi)$ , where $\gamma$ is zero at transient states and is chosen separately on each recurrent class by a maximum formula. The formalization restricts that formula's denominator to the recurrent class, as required by the subsequent nonnegativity calculation; the printed unrestricted denominator has a two-state counterexample. Hordijk and Kallenberg (1979), pp. 359–360

Formalization targets

Optimality correspondence

The goal is Theorem 8, with both directions in one statement:

\pi^\infty\text{ average optimal}\ \Longrightarrow\ (x(\pi),y(\pi))\text{ dual optimal}, \qquad (x,y)\text{ dual optimal}\ \Longrightarrow\ \pi^\infty(x,y)\text{ average optimal}.

The second implication applies to every optimal dual point. It produces the stationary randomized policy given by the printed normalization rule, including its existence as a valid policy. The first implication uses the particular representative defined by equation (6). Neither direction imposes an extreme-point condition. Hordijk and Kallenberg (1979), Theorem 8, p. 360

Supporting results

The milestones state the least-superharmonic characterization of $\phi$ ; the positivity that makes the dual-to-policy normalization meaningful; the stationary gain identity; feasibility and objective value of the representative; and Propositions 4 and 5, which describe tight actions and identify $E_x$ with the recurrent states of $P(\pi(x,y))$ . Each is a statement about the same finite model and the same primal–dual pair. Hordijk and Kallenberg (1979), pp. 356–361

Significance

The theorem establishes an exact relation between two ways of expressing average optimality. The LP direction turns an optimal stationary policy into a dual optimum with a concrete state-action representation. The converse says an arbitrary optimal dual point can be read as an average optimal policy, even when its $x$ coordinates vanish at some states. Proposition 5 specifies what those vanishing coordinates mean for the induced chain: those states are transient. These statements permit optimization over a finite LP while preserving the policy interpretation of its solutions. Hordijk and Kallenberg (1979), Theorem 8 and Proposition 5

The result was proved in 1979; this mission asks for a machine-checked proof of its precise finite-state statement. The shared MDP model and the limit and deviation matrix definitions already exist as published formal objects. The new work is the correspondence for Hordijk and Kallenberg's dual equations, with the representative, its class-wise correction, and the connection to liminf average reward. The definitions of stationary policy mixtures, admissible-pair LP coordinates, and finite-chain recurrence can support later results about average-reward optimization.

Difficulty

Normalizing $x$ alone does not define a policy at every state: its row sum can be zero. The dual program's second variable $y$ supplies the action weights there, and the feasibility equations must ensure its row sum is positive. In the other direction, the natural $\beta^TD(\pi)$ term in $y(\pi)$ need not be nonnegative. The correction $\gamma$ is chosen by a maximum over each recurrent class, while transient states require a different case. These issues remain in a multichain process even though the state and action sets are finite. Hordijk and Kallenberg (1979), pp. 359–361

Formalization scope

Lean uses finite types for states and actions, a nonempty state type, and a nonempty admissible action set at every state. The published StationaryMDP definition provides real rewards and stochastic transition rows. General policies are its history-dependent randomized AvgHRPolicy values; average reward is its liminf reward, and optimal gain is the supremum over that entire policy class. The mission defines its own average-optimality predicate because the published Puterman predicate uses a stronger limsup comparison. For finite rewards, the liminf gains and their supremum are bounded real numbers.

Stationary randomized weights are nonnegative, sum to one on each $A(i)$ , and vanish outside $A(i)$ . The dual variables are functions on the subtype of admissible state-action pairs. The primal and dual optima mean feasible points attaining the relevant objective against every other feasible point. The paper's positive, normalized $\beta$ remains explicit. The raw formula for $\pi(x,y)$ is used only with a feasible dual point, and the policy-well-definedness milestone supplies its nonzero denominators. The representative uses a maximum over the ergodic class of each recurrent state, with the class-restricted denominator needed by the paper's proof; replacing $\gamma$ by zero or by one global maximum would change the target.

The known matrix objects $P^*$ and $D$ are imported from the published Blackwell development. Their convergence and identities are theorem obligations, not assumptions hidden in definitions. Contributions proving the finite-chain identities, representative feasibility, complementary slackness, and the final policy comparison are within scope. A statement restricted to a unichain model, an extreme dual point, or a pure selected action would not establish this theorem.

Selected references

A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. DOI: 10.1287/mnsc.25.4.352.

13 thms2 active usersReviewed

Analysis Harmonic Analysis Probability+1·Captain: mikedeng1

Distribution Function Inequalities for Martingales 3: For Brownian Motion Stopped at Any Stopping Time τ, EΦ(X*(τ)) and EΦ(τ^{1/2}) Are ComparableResearch Paper

Motivation

The size of a martingale can be measured in two ways: by its maximal function, the largest absolute value it reaches, and by a quadratic quantity that records how much it has moved, the square function in discrete time or the elapsed time in the case of Brownian motion. The Burkholder–Davis–Gundy inequalities say that these two measurements are comparable in every $L^p$ norm and, more generally, under $E\Phi(\cdot)$ for every $\Phi$ of moderate growth. They are a basic tool of stochastic analysis, harmonic analysis and the theory of stochastic integration.

D. L. Burkholder's 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973)), organise these results around one device: a distribution function inequality ("good- $\lambda$ " inequality) between two random variables, which a single lemma then converts into integral inequalities for all $\Phi$ of moderate growth. The paper opens its second chapter with "a particularly easy but important special case": Brownian motion stopped at an arbitrary stopping time. This mission formalizes that case, §§6–8 of the paper.

Timeline. Burkholder proved the $L^p$ square-function inequalities for martingales, $1<p<\infty$ , in 1966 (Ann. Math. Statist. 37); B. Davis extended the comparison of the maximal and square functions to $p=1$ in 1970 (Israel J. Math. 8); Burkholder and R. F. Gundy introduced the extrapolation method for operators on martingales in 1970 (Acta Math. 124); Burkholder, Davis and Gundy proved two-sided $\Phi$ inequalities in 1972 (Proc. Sixth Berkeley Symp. 2, 223–240), the Brownian case being their Theorem 7.2, under the additional assumption that $\Phi$ is the integral of a function that itself satisfies a growth condition. The 1973 paper states Theorem 6.1 below as "Theorem 7.2 of [6] with $\Phi$ more general", that assumption removed.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $X=\{X(t),\,0\le t<\infty\}$ a one-dimensional Brownian motion: a real process with independent increments and continuous sample functions, with $X(t)$ normally distributed, $EX(t)=0$ , $EX^2(t)=t$ . Let $\mathcal B(t)$ be the $\sigma$ -field generated by $\{X(s),\,0\le s\le t\}$ . A stopping time of $X$ is a function $\tau:\Omega\to[0,\infty]$ with $\{\tau<t\}\in\mathcal B(t)$ for every $t>0$ . For $0\le b\le\infty$ put

X^*(b)=\sup_{t\ge0}|X(b\wedge t)| ,

so $X^*(\tau)$ is the maximal function of Brownian motion stopped at $\tau$ .

A function $\Phi:[0,\infty]\to[0,\infty]$ is of moderate growth if it is non-decreasing and continuous, $\Phi(0)=0$ , and

\Phi(2\lambda)\le c_{(6.1)}\,\Phi(\lambda),\qquad\lambda>0. \tag{6.1}

Examples are $\Phi(\lambda)=\lambda^p$ for $0<p<\infty$ . No convexity is assumed. In Lean these are IsBM X P, IsStoppingTimeOf X τ, maxStopped X b ω and IsPhi Φ c.

Formalization targets

Goal: Theorem 6.1

For every stopping time $\tau$ of $X$ ,

c\,E\Phi(\tau^{1/2})\le E\Phi(X^*(\tau))\le C\,E\Phi(\tau^{1/2}), \tag{6.2}

where $c,C>0$ depend only on $c_{(6.1)}$ . Neither $\tau$ nor any moment is assumed finite.

Milestones

(8.1) Wald's identity $EX^2(\tau)=E\tau$ for a bounded stopping time $\tau$ (cited in the paper from Doob).
Theorem 6.2. For $\beta>1$ , $\delta>0$ and every $\lambda>0$ ,

P(\tau^{1/2}>\beta\lambda,\ X^*(\tau)\le\delta\lambda)\le\frac{\delta^2}{\beta^2-1}P(\tau^{1/2}>\lambda), \tag{6.3}

P(X^*(\tau)>\beta\lambda,\ \tau^{1/2}\le\delta\lambda)\le\frac{\delta^2}{(\beta-1)^2}P(X^*(\tau)>\lambda). \tag{6.4}

Lemma 7.1. If nonnegative $f,g$ satisfy $P(g>\beta\lambda,f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ for all $\lambda>0$ , and $\Phi(\beta\lambda)\le\gamma\Phi(\lambda)$ , $\Phi(\delta^{-1}\lambda)\le\eta\Phi(\lambda)$ with $\gamma\varepsilon<1$ , then

E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f).

Significance

Theorem 6.1 is the Brownian case of the Burkholder–Davis–Gundy inequalities: for Brownian motion the stopping time $\tau$ plays the role of the square function, since $\tau$ is the quadratic variation of $X$ up to time $\tau$ . The result controls the stopped maximum through elapsed quadratic variation without a finite-time or integrability assumption. Lemma 7.1 is reusable: the paper applies it again in §§10–21 to discrete-time martingales.

The results are classical and proved; the mission's Lean statements remain open. Mathlib has Brownian motion as a predicate on processes (IsBrownianReal), while this development still needs optional sampling at the paper's stopping times and maximal inequalities for Brownian motion. A formal proof of this mission would provide Wald's identity at bounded optional times, a general good- $\lambda$ lemma, and the Brownian inequality with explicit dependence of the constants on $c_{(6.1)}$ .

Difficulty

The obvious route, integrating the tail bounds (6.3)–(6.4) against $d\Phi$ , does not close by itself: the right-hand side of each good- $\lambda$ inequality contains the same random variable as the left-hand side, and nothing in the hypotheses says that $E\Phi(\tau^{1/2})$ or $E\Phi(X^*(\tau))$ is finite, nor that $\tau$ is finite. The theorem has to hold in that generality, with constants that see only $c_{(6.1)}$ and not $\Phi$ itself. On the probabilistic side, the stopping times of the paper are defined by the strict events $\{\tau<t\}$ relative to the raw natural filtration $\mathcal B(t)$ , which is not right-continuous, while the one probabilistic input, Wald's identity (8.1), is a statement about optional sampling of the martingale $X^2(t)-t$ in continuous time, for which Mathlib has no theorem yet.

Formalization scope

Probability spaces are (Ω : Type) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]; time is ℝ≥0 and stopping times are valued in ℝ≥0∞.
Brownian motion IsBM X P is Mathlib's IsBrownianReal X P plus two explicit conjuncts the paper assumes: every sample function is continuous, and each $X(t)$ is measurable (so $\mathcal B(t)\subseteq\mathcal A$ ). $X(0)=0$ holds almost surely.
IsStoppingTimeOf X τ is exactly the paper's condition $\{\tau<t\}\in\mathcal B(t)$ , $t>0$ , with $\mathcal B(t)$ the raw generated $\sigma$ -field; it is weaker than Mathlib's IsStoppingTime, so the theorems are stronger than their Mathlib-stopping-time versions.
$\tau^{1/2}$ , $X^*(\tau)$ , $\Phi$ and all expectations take values in $[0,\infty]$ (ℝ≥0∞, lintegral), with $\infty^{1/2}=\infty$ ; both sides of (6.2) may be infinite. (8.1) is stated with lintegral on both sides.
The growth condition is required for all $\lambda\in[0,\infty]$ , equivalent to (6.1) by continuity. $\Phi\not\equiv0$ , which the paper assumes "to eliminate the trivial case", is dropped: all conclusions hold trivially for $\Phi\equiv0$ .
"The choice of $c$ and $C$ depends only on $c_{(6.1)}$ " is formalized with the quantifier order ∀ c, ∃ C₁ C₂ > 0, ∀ Ω P X τ Φ, IsPhi Φ c → …. A version in which the constants are chosen after $\Phi$ , $X$ or $\tau$ would be trivial whenever the right-hand side is positive and is ruled out by this order.
In Lemma 7.1, $f,g$ may take the value $\infty$ and $\gamma,\eta$ are nonnegative; both choices are harmless (see the item notes).

Contributions welcome: Wald's identity and optional sampling for Brownian motion at optional times, the Lebesgue–Stieltjes layer-cake formula $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ for continuous non-decreasing $\Phi$ (reusable for every $\Phi$ inequality of the series), and the good- $\lambda$ lemma, which the later missions of this series share.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, B. J. Davis, R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2 (1972), 223–240. https://digicoll.lib.berkeley.edu/record/113227
D. L. Burkholder, R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394576
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771562
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141

7 thms2 active usersReviewed

Control Theory Probability Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 2: The Coupled Backward-Forward System Has a Unique Adapted Solution When k Times the H∞ Norm of D Is Below OneResearch Paper

Motivation

A backward-forward stochastic differential equation couples two equations that run in opposite time directions: a forward equation for a state $U$ , started from a given input, and a backward equation for a quantity $V$ , pinned at a terminal time by a random variable $Y$ . Each equation's coefficients depend on both unknowns, so the solution at time $t$ depends on the past of $U$ and on the conditional future of $V$ . Such systems arise in stochastic control (the adjoint equation of the stochastic maximum principle runs backward while the state runs forward) and in mathematical finance (an asset's price is forward, a hedge or value process is backward).

Antonelli's 1993 paper (Ann. Appl. Probab. 3(3), 777–793) is one of the first treatments of the coupled problem. Pardoux and Peng (1990) had established existence and uniqueness for decoupled backward equations driven by Brownian motion. Antonelli proved existence and uniqueness for the coupled system under a smallness condition, and gave examples (§3) showing that without such a condition a solution may fail to exist. This mission formalizes the bounded-variation case of that result, Theorem 3.1.

Setting

Fix a horizon $T > 0$ and a probability space $(\Omega,\mathcal F,P)$ with a filtration $(\mathcal F_t)_{t\ge 0}$ satisfying the usual hypotheses: it is right-continuous, and $\mathcal F_0$ contains every $P$ -null set.

An integrator $A$ is an adapted process whose paths have bounded variation on $[0,T]$ , with $A_0 = 0$ . It is written $A = A^+ - A^-$ with $A^\pm$ adapted, nondecreasing and right-continuous, and $A^+_t + A^-_t = |A|_t$ , the total variation of $A$ on $[0,t]$ . It is bounded: $|A|_T \le \beta$ . The pathwise integral $\int_s^t h_r\,dA_r$ is the Lebesgue–Stieltjes integral over $(s,t]$ .

The system involves two integrators $A, C$ and the increasing process

D_t = \max(|A|_t, |C|_t),

whose pathwise Stieltjes measure is $dD$ . The Doléans measure $\mu$ of $D$ on $(0,T]\times\Omega$ gives the norm

\|V\|_{L^1(\mu)} = E\Big(\int_0^T |V_t|\,dD_t\Big),

and $L^1(\mu)$ is the space of jointly measurable processes with finite norm. The size of $D$ is $\|D\|_{\mathbf H^\infty} = \operatorname{ess\,sup} D_T$ .

The data are coefficients $f, g : [0,T]\times\Omega\times\mathbb R^2\to\mathbb R$ , a constant $k > 0$ , a terminal value $Y$ and a forward input $J$ . They satisfy:

$f, g$ are $k$ -Lipschitz in $(x,y)$ : $|\zeta_s(\omega,x,y) - \zeta_s(\omega,\bar x,\bar y)| \le k(|x-\bar x| + |y-\bar y|)$ for $\zeta = f, g$ ;
$f, g$ are adapted in $(s,\omega)$ ;
$f_s(0,0), g_s(0,0) \in L^1(\mu)$ .

In addition $Y \in L^1(P)$ is $\mathcal F_T$ -measurable and $J \in L^1(\mu)$ is adapted. The system is

U_t = J_t + \int_0^t f_s(U_s,V_s)\,dA_s, \qquad V_t = E\Big(\int_t^T g_s(U_s,V_s)\,dC_s + Y \;\Big|\; \mathcal F_t\Big), \tag{3.1–3.2}

and its right-hand side defines an operator $\Gamma(U,V) = (F(U,V), G(U,V))$ , (3.3). A solution in the $L^1(\mu)\otimes L^1(\mu)$ sense is a pair $(U,V)\in L^1(\mu)\otimes L^1(\mu)$ with $U = F(U,V)$ and $V = G(U,V)$ $\mu$ -a.e.

Formalization targets

Goal: Theorem 3.1

If $|dA|$ and $|dC|$ are dominated by $dD$ and

k\,\|D\|_{\mathbf H^\infty} < 1,

then there is a progressively measurable solution $(U,V)$ of (3.1)–(3.2) in the $L^1(\mu)\otimes L^1(\mu)$ sense, and any two progressively measurable solutions agree $\mu$ -a.e.:

\|U - U'\|_{L^1(\mu)} + \|V - V'\|_{L^1(\mu)} = 0.

Milestones

Remark 2.2, (2.6): $E(H\int_{[0,\infty)} a(s)\,dC_s) = E(\int_{[0,\infty)} H_s a(s)\,dC_s)$ for an adapted increasing càdlàg $C$ , a positive Borel $a$ , $H$ positive or in $L^1$ , and the càdlàg version $H_s$ of $E(H\mid\mathcal F_s)$ . The proof of Theorem 3.1 uses it with $C = D$ , $a \equiv 1$ .
$\Gamma$ maps $L^1(\mu)\otimes L^1(\mu)$ into itself (pp. 785–787).
The Lipschitz estimates (p. 787): $|F(U,V)_t - F(\tilde U,\tilde V)_t| \le k\int_0^t(|U_s-\tilde U_s| + |V_s-\tilde V_s|)\,dD_s$ , and the conditional analogue for $G$ on $(t,T]$ .
The contraction estimate (p. 788):

\|\Gamma(U,V) - \Gamma(\tilde U,\tilde V)\|_{L^1\otimes L^1} \le k\|D\|_{\mathbf H^\infty}\,\|(U,V) - (\tilde U,\tilde V)\|_{L^1\otimes L^1}.

Significance

The theorem identifies a regime in which a coupled forward-backward system is well posed. The integrability required is only $L^1$ , and the smallness condition $k\|D\|_{\mathbf H^\infty} < 1$ ties the Lipschitz constant to the total mass of the driving integrators. With $A_s = C_s = s$ it reads $kT < 1$ , a small-horizon condition. The paper's Example 1 (mission 3 of this series) shows that at $k = 1$ , $T \ge 1$ a solution may fail to exist, so some restriction of this type is necessary. Later work on forward-backward equations, for instance the four-step scheme of Ma, Protter and Yong (1994), replaced the smallness condition by other structural assumptions. Antonelli's small-horizon result remains the base case those methods extend.

The result is proved in the paper. No machine-checked version of it, or of any backward stochastic differential equation, exists in Mathlib or on the platform. The formalization adds three things on top of the paper. It makes the solution concept precise: versions, integrability, and $\mu$ -a.e. equality. It repairs a gap in the printed proof (see Formalization scope). And it builds pathwise Lebesgue–Stieltjes integration against adapted bounded-variation processes, together with the optional projection identity (2.6), as reusable infrastructure.

Difficulty

The Banach fixed point theorem does the final step once the contraction estimate holds. The difficulty lies in reaching that estimate. The $V$ -component is a conditional expectation, defined for each $t$ only up to a null set, and these null sets accumulate when the process is integrated against $dD$ , which may charge random times. The estimate has to be transported from "for each $t$ , almost surely" to " $\mu$ -almost everywhere". That needs càdlàg versions and the optional projection theorem, which Mathlib lacks. A second point: the naive bound treats the forward and backward differences separately and gives the constant $2k\|D\|_{\mathbf H^\infty}$ . Obtaining $k\|D\|_{\mathbf H^\infty}$ requires combining both differences inside one conditional expectation, and that uses the adaptedness of the forward difference.

Formalization scope

Time is $\mathbb R_{\ge 0}$ with horizon $T > 0$ ; integrators are frozen after $T$ . Each integrator carries its minimal Jordan decomposition as data, tied to Mathlib's eVariationOn. Pathwise measures are Mathlib's Stieltjes measures, and integrals are over $(s,t]$ . Norms are lower integrals in $[0,\infty]$ . Every conditional expectation is accompanied by the integrability of its argument, since Mathlib's condExp of a non-integrable function is $0$ . A version of $G(U,V)$ must be jointly measurable and have càdlàg paths on $[0,T]$ . Without the càdlàg requirement, two versions can differ on the graph of a random time charged by $dD$ , and the contraction estimate fails.

The formalization commits to these readings of the paper:

Domination. The paper asserts (p. 786) that $|A|\ll D$ and $|C|\ll D$ with densities at most $1$ . This is false for $D = \max(|A|,|C|)$ in general: take $|A|_t = t$ and $|C|_t = 2\cdot 1\{t\ge\varepsilon\}$ . It is assumed explicitly, as " $D - |A|$ and $D - |C|$ are nondecreasing on $[0,T]$ ". The paper's Example 1 ( $A = C$ ) satisfies it.
Adaptedness. "Adapted" solutions are progressively measurable. For each $(x,y)$ , $f(\cdot,\cdot,x,y)$ is required to be progressively measurable, since with a merely adapted integrand $\int_0^t f\,dA$ need not be adapted. The weaker printed hypothesis is kept for $g$ .
Norm of $D$ . $\|D\|_{\mathbf H^\infty}$ is $\operatorname{ess\,sup} D_T$ , not the bound $\beta$ . The hypothesis $k\|D\|_{\mathbf H^\infty} < 1$ is weaker than $k\beta < 1$ , and the theorem keeps it.
Small departures. The constant $k_1$ bounding $J$ becomes finiteness. " $|A|_T, |C|_T < \beta$ " becomes " $\le \beta$ ". In the positive case of Remark 2.2, the version of $E(H\mid\mathcal F_t)$ is $[0,\infty]$ -valued and characterized by its integrals over $\mathcal F_t$ -sets.

The solution concept rules out trivial solutions. It requires $U, V\in L^1(\mu)$ , the integrability of every argument of the conditional expectation, and a càdlàg version, and existence asserts a progressively measurable pair. A pair satisfying the equations only through Lean's junk values therefore does not count.

A complete development needs:

measurability of pathwise Stieltjes integrals in $\omega$ ;
the optional projection theorem for càdlàg processes (Dellacherie–Meyer VI.47, VI.57);
existence of càdlàg versions of martingales under the usual hypotheses;
completeness of $L^1$ over the progressive σ-algebra.

All four are reusable well beyond this mission. Contributions to any of them are welcome, as is a proof of any milestone in isolation.

Selected references

F. Antonelli, Backward-forward stochastic differential equations, Ann. Appl. Probab. 3(3) (1993) 777–793. https://doi.org/10.1214/aoap/1177005363
E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14 (1990) 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
C. Dellacherie, P.-A. Meyer, Probabilities and Potential B: Theory of Martingales, North-Holland Mathematics Studies 72, 1982. ISBN 0-444-86526-8
P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. https://doi.org/10.1007/978-3-662-02619-9
J. Ma, P. Protter, J. Yong, Solving forward-backward stochastic differential equations explicitly — a four step scheme, Probab. Theory Related Fields 98 (1994) 339–359. https://doi.org/10.1007/BF01192258

8 thms2 active usersReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Paths, Trees, and Flowers II: Invariance of the Dual — the Outer Vertices O(G) Are Exactly the Vertices Left Exposed by Some Maximum MatchingResearch Paper

Motivation

A maximum matching of a graph is a largest set of edges no two of which share a vertex. Maximum matchings are rarely unique, and a basic question is which features of them are forced by the graph. J. Edmonds' paper Paths, trees, and flowers (Canad. J. Math. 17 (1965), 449–467) gave the first polynomial-time algorithm for maximum matching in general graphs. Its Section 6, Invariance of the dual, uses the output of that algorithm to answer this question. The vertices that some maximum matching leaves uncovered, their neighbours, and the rest form a decomposition of the graph that does not depend on the matching chosen or on any choice made by the algorithm.

This decomposition is now called the Gallai–Edmonds structure theorem. T. Gallai obtained it independently (Gallai 1963, 1964; see Selected references). It is a standard tool in matching theory (Lovász–Plummer, Matching Theory, 1986): it determines the minimum odd-set cover of Section 5 of the same paper canonically (6.7), and it underlies the Tutte–Berge formula and the analysis of factor-critical graphs.

Timeline. Berge (1957) characterized maximum matchings by the absence of augmenting paths. Gallai (1963–1964) and Edmonds (1965, §6) proved the structure theorem; Edmonds' proof goes through the trees and shrunken blossoms of his algorithm. Witzgall's argument, reported in 6.6, simplifies the converse half.

Setting

A graph $G$ has a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices; parallel edges are allowed. A vertex is exposed for a set of edges $M$ if no edge of $M$ meets it.

An alternating tree $J$ is a tree (a connected graph with one more vertex than edges) whose vertices are split into inner and outer vertices, so that every edge joins an inner vertex to an outer one and every inner vertex meets exactly two edges of $J$ . A planted tree for $M$ with root $r$ is an alternating tree such that $M \cap J$ is a maximum matching of $J$ and $r$ , the vertex of $J$ left exposed by $M \cap J$ , is exposed for $M$ .

Shrinking a vertex set $U$ replaces $U$ by a single pseudovertex. Edges inside $U$ disappear; edges leaving $U$ keep their identity and now meet the pseudovertex. The set $U$ is the pseudovertex's complete expansion. A blossom for $M$ is an odd circuit $B$ for which $M \cap B$ is a maximum matching of $B$ . Shrinking blossoms repeatedly, inside graphs already shrunk, gives the graph $G^* = G/\mathcal P$ , where $\mathcal P$ is a partition of the vertices into blossom sets.

Construction 6.0. Let $M$ be a maximum matching. Run the matching algorithm on $(G, M)$ without augmenting. It grows planted trees $J_1, \dots, J_n$ in $G^*$ , one from each exposed vertex, and shrinks blossoms as they appear. The output satisfies:

the trees are disjoint and planted for $M^* = M/\mathcal P$ ;
every exposed vertex of $G^*$ lies in some tree;
$J_i$ is Hungarian in $G^* - J_1 - \dots - J_{i-1}$ : its outer vertices are joined only to its own inner vertices or to earlier trees;
every pseudovertex is an outer vertex of some $J_i$ .

The outer vertices $O(G)$ are the vertices whose part is a one-vertex outer vertex of some $J_i$ , together with all vertices of pseudovertex expansions. The inner vertices $I(G)$ are the vertices whose part is an inner vertex of some $J_i$ .

Formalization targets

Goal: Theorem 6.2 (a)–(c)

For every maximum matching $M$ and every output of construction 6.0:

\text{(a)}\quad v \in O(G) \iff \exists\, M' \text{ maximum matching of } G \text{ with } v \text{ exposed for } M',

\text{(b)}\quad v \in I(G) \iff v \notin O(G) \text{ and } v \text{ is adjacent to a vertex of } O(G),

\text{(c)}\quad u,v \text{ in the same part of } \mathcal P \iff u = v \text{ or } u, v \text{ in the same component of } O(G)^+,

where $O(G)^+$ is the subgraph induced on $O(G)$ .

Milestones

4.1–4.2: the maximum matchings of an alternating tree.
4.14: lifting a matching through the complete expansion of a pseudovertex, with a free choice of the exposed vertex.
4.15, extension, in the forest form of 4.20.
6.4: adjacency of outer and inner vertices.
6.2 (b) and 6.2 (c) separately.
6.5: every outer vertex is exposable.
6.6: for non-outer $v$ meeting $e \in M$ , $M - e$ is maximum in $G - v$ .
6.6: only outer vertices are ever exposed.

A companion item states that construction 6.0 succeeds for every maximum matching.

Significance

The result. Part (a) characterizes, without reference to any algorithm, the vertices that a maximum matching can miss. Parts (b) and (c) then make $I(G)$ and $G^*$ invariants of $G$ , as 6.1 announces: "the graph $G^*$ is uniquely determined by $G$ alone". Several consequences rest on this invariance: the unique preferred minimum odd-set cover (6.7), the Tutte–Berge deficiency formula read off from $|I(G)|$ and the components of $O(G)^+$ , and the classification of graphs into those with and without perfect matchings in terms of a canonical barrier.

Formalizing it. The theorem has been proved since 1964, but the proof in this paper has not been machine-checked. A formalization requires the paper's own objects: multigraphs with edge identity preserved under contraction, nested blossom shrinking, and alternating and planted trees. These are the objects of Edmonds' blossom algorithm, and they are reusable for any formal treatment of it. Mathlib contains Tutte's theorem for simple graphs but neither shrinking nor the Gallai–Edmonds decomposition.

Difficulty

The statement is about one particular output of a nondeterministic process. The partition into trees depends on the order in which they were grown, and the non-matching tree edges and the blossoms chosen are arbitrary (6.1). An outer vertex of a later tree may be joined to an inner vertex of an earlier one, so the individual trees are not Hungarian in $G^*$ . The tempting argument "each tree is Hungarian, so apply the tree lemma tree by tree" therefore fails. Only the ordered condition, applied in both directions as in 6.4, shows that the outer vertices of all trees together are adjacent only to inner vertices. Moving between $G$ and $G^*$ requires lifting matchings through nested blossoms, which means an induction over the nesting rather than over a single odd circuit.

Formalization scope

Graphs are the published EdmondsMatching65.Polyhedron.Graph V E: finite vertex and edge types, an unordered pair of distinct ends for each edge, parallel edges allowed. Matchings are its IsMatching, and "maximum" means maximum cardinality. A matching of a subgraph is a matching of $G$ contained in the subgraph's edges. Paths are not needed.

Shrinking is contraction along a Finpartition of the vertex set. The vertices of $G^*$ are the parts, and the edges of $G^*$ are the edges of $G$ joining different parts. Blossom sets are an inductive predicate recording the nested odd circuits directly; there is no tower of types.

The output of 6.0 is the structure Config60. It records exactly the invariants the construction establishes and nothing more, and the goal is stated for every such configuration. The configuration must not be weakened. Dropping density, the ordered Hungarian condition, the outerness of pseudovertices or the blossom condition on the parts makes (a) or (b) false. Taking the $J_i$ to be arbitrary trees, or $\mathcal P$ an arbitrary partition, would state a different and false theorem. The goal is not vacuous: exists_config_6_0 asserts that a configuration exists for every maximum matching. Shrinking is defined in 4.9 only for connected sets, so the forest form of 4.15 assumes connected parts.

Welcome contributions: the general theory of alternating trees and Hungarian forests (4.2, 4.17 and their forest forms), the lifting lemma 4.14 for nested odd circuits, and a proof of exists_config_6_0.

Selected references

J. Edmonds, Paths, trees, and flowers, Canadian Journal of Mathematics 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
C. Berge, Two theorems in graph theory, Proceedings of the National Academy of Sciences USA 43 (1957), 842–844. https://doi.org/10.1073/pnas.43.9.842
T. Gallai, Kritische Graphen II, Publ. Math. Inst. Hungar. Acad. Sci. 8 (1963), 373–395; Maximale Systeme unabhängiger Kanten, ibid. 9 (1964), 401–413.
L. Lovász and M. D. Plummer, Matching Theory, North-Holland, 1986 (reprinted AMS Chelsea, 2009). https://doi.org/10.1090/chel/367
A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 24.

16 thms2 active usersReviewed

Computational Geometry Discrete Geometry Theoretical Computer Science·Captain: mikedeng1

An Optimal Algorithm for Approximate Nearest Neighbor Searching in Fixed Dimensions: Priority Search in a BBD-Tree Visits at Most ⌈1 + 6d/ε⌉^d Leaf CellsResearch Paper

Motivation

Nearest neighbor searching asks for a data structure that stores $n$ points $S\subset\mathbb R^d$ and, given a query point $q$ , returns a point of $S$ closest to $q$ . It underlies classification, vector quantization, data compression, pattern recognition and similarity search in databases. In dimension $d\ge 3$ , exact methods either use space growing like $n^{\lceil d/2\rceil}$ or answer queries in time close to linear in $n$ , so practical systems settle for an approximate answer: a point whose distance to $q$ is within a factor $1+\varepsilon$ of the true nearest distance.

Arya, Mount, Netanyahu, Silverman and Wu (J. ACM 45 (1998), 891–923) gave the first structure for this problem that is simultaneously of linear size, built in $O(dn\log n)$ time, and answers $(1+\varepsilon)$ -approximate queries in $O(c_{d,\varepsilon}\log n)$ time for any fixed $d$ , with $c_{d,\varepsilon}\le d\lceil 1+6d/\varepsilon\rceil^d$ . The structure, the balanced box-decomposition tree (BBD-tree), and the priority search on it became the basis of the ANN library of Mount and Arya.

Timeline. Arya and Mount (SODA 1993) studied approximate nearest neighbor queries in fixed dimensions; the conference version of this paper (SODA 1994) gave an optimal algorithm; the journal version (1998), which the paper itself describes as differing from the conference version by a single balanced structure without auxiliary data structures (p. 897), is the one formalized here. Later work, for example by Har-Peled, Indyk and Motwani (2012), addressed the exponential dependence on $d$ .

Setting

Points are vectors in $\mathbb R^d$ . For an integer $m\ge1$ the $L_m$ distance is $\operatorname{dist}_m(x,y)=(\sum_i|x_i-y_i|^m)^{1/m}$ , and for $m=\infty$ it is $\max_i|x_i-y_i|$ . A rectangle is a product $\prod_i[\ell_i,h_i]$ of closed intervals; its size is the length of its longest side. A box is a rectangle with positive sides whose aspect ratio, longest over shortest side, is at most $3$ .

A cell consists of an outer box $b_O$ and an optional inner box $b_I$ ; as a point set it is $b_O$ , or the closure of $b_O\setminus b_I$ . Its size is the size of $b_O$ . The inner box must be sticky for the outer one: in every coordinate, each of the two gaps between the inner and the outer interval is either $0$ or at least the width of the inner interval.

A BBD-tree subdivides a root box by two operations. A fair split cuts a cell by a hyperplane $x_i=t$ into a low and a high child; a shrink cuts it by a shrinking box $b$ into an inner child (outer box $b$ ) and an outer child (outer box unchanged, inner box $b$ ). Throughout, every box has aspect ratio at most $3$ , a parent's inner box lies entirely within one child (within the inner child of a shrink), and inner boxes are sticky. The cells at the leaves are the leaf cells; they cover the root box and have disjoint interiors.

The distance from $q$ to a cell $c$ is $\operatorname{dist}_m(q,c)=\inf_{x\in c}\operatorname{dist}_m(q,x)$ . Each leaf cell $c_j$ carries an associated data point $p_j$ in its outer box. The search enumerates the leaf cells $c_0,c_1,\dots$ in nondecreasing order of distance from $q$ , processes each by comparing its point with the closest point $p$ seen so far, and terminates at the first cell whose distance from $q$ exceeds $\operatorname{dist}_m(q,p)/(1+\varepsilon)$ . The goal bounds $N$ , the number of cells that did not cause termination, which is the count the paper's proof bounds ("the number of cells visited up until termination", p. 912).

Formalization targets

Goal: Lemma 5 (p. 911)

For every valid BBD-tree, every Minkowski metric $1\le m\le\infty$ , every $\varepsilon>0$ , every query point and every sorted enumeration of the leaf cells,

N\le\Big\lceil 1+\frac{6d}{\varepsilon}\Big\rceil^d.

Milestones

The packing constraint (Lemma 4, p. 908): for $r,s>0$ , the number of leaf cells of size at least $s$ meeting an open $L_m$ ball of radius $r$ is at most

\Big\lceil 1+\frac{6r}{s}\Big\rceil^d.

Its proof has three stated steps, each a milestone: an $L_m$ ball of radius $r$ lies in an axis-parallel cube of side $2r$ ; at most $\lceil1+6r/s\rceil^d$ interior-disjoint boxes of side at least $s/3$ meet such a ball; and the leaf cells of size at least $s$ meeting the ball can be replaced by as many interior-disjoint boxes of size at least $s$ meeting it. The proof of Lemma 5 contributes two more: the $L_m$ diameter of a rectangle is at most $d$ (indeed $d^{1/m}$ ) times its longest side, and every visited cell has size at least $r\varepsilon/d$ , where $r$ is the distance to the last cell that did not cause termination.

A companion statement records the correctness of the termination rule: the closest point processed is a $(1+\varepsilon)$ -approximate nearest neighbor.

Significance

Lemma 5 is the explicit content of the query bound of Theorem 1(i): each visited cell costs $O(d\log n)$ time to enumerate and process, so the query takes $O(d\lceil1+6d/\varepsilon\rceil^d\log n)$ time, with no dependence on $n$ beyond the logarithm. Lemma 4 is the property of the subdivision on which this rests, and it is used again for the $k$ -nearest-neighbor variant (Lemma 6) and for approximate range searching with the same tree.

The results are proved on paper and widely cited; none has a machine-checked proof. The mission produces checked versions of the packing constraint and of the cell-count bound for an abstract BBD-tree, defined by its invariants rather than by a particular construction algorithm, so that any construction meeting the invariants inherits the bound. It also exposes two places where the printed argument needs care: the open versus closed ball in Lemma 4, and the step in Lemma 5 that applies Lemma 4 to cells within distance $r$ of $q$ , which touch the closed ball of radius $r$ .

Difficulty

The counting step of Lemma 4 is asserted on the page ("the densest packing of axis-aligned rectangles of side length at least $s/3$ is realized by a regular grid"), and a formal argument must replace that sentence with a genuine counting argument. The replacement step is the geometric core: the outer box of a leaf cell with an inner box overlaps every leaf cell inside that inner box, so outer boxes cannot be counted directly, and without stickiness many nested inner boxes could crowd against one face of a cell. Applying Lemma 4 inside Lemma 5 is not immediate either: the visited cells lie within distance $r$ of $q$ , so they meet the closed ball, while Lemma 4 concerns the open ball, and a naive enlargement of the radius changes the ceiling exactly when $6d/\varepsilon$ is an integer.

Formalization scope

Points are Fin d → ℝ, the metric index $m$ is an element of ℕ∞ with $1\le m$ , and the $L_m$ distance is defined explicitly by the formula above. Rectangles are pairs of corner vectors; boxes have positive sides and aspect ratio at most $3$ . A cell's point set is the closure of the outer box minus the inner box, as the paper's "cells are considered to be closed" requires; an inner box equal to its outer box is excluded. A BBD-tree is an inductive tree of splits and shrinks with a validity predicate expressing the §2.1 invariants relative to the root cell; the root may be any box rather than the paper's hypercube, and the construction algorithms of §2.2–§2.5 are not formalized.

The enumeration is a list of (leaf cell, associated point) pairs that is a permutation of the leaf cells, sorted by distance from $q$ , with each point in its cell's outer box. A cell is processed before its own termination test, and $N$ counts the cells processed before the cell whose test fires (all cells if none fires). Lemma 4 and its counting step use the open ball of property (d). Theorem 1's $O(\cdot)$ time and space claims, Lemmas 1–3 on the construction, and the $k$ -nearest-neighbor Lemma 6 are out of scope.

This convention follows the proof of Lemma 5, which takes $r$ to be the distance to "the last leaf cell that did not cause the algorithm to terminate" and bounds the cells up to that one. If the cell whose test fires is also counted, the printed bound can be exceeded by one: a valid one-dimensional tree with $\varepsilon=6$ needs three processed cells against $\lceil 1+6d/\varepsilon\rceil^d=2$ . The formal goal therefore states the bound for the cells that did not cause termination, which is what the proof establishes; consequently at most $\lceil 1+6d/\varepsilon\rceil^d+1$ cells are processed in total.

The goal must not be trivialized: the enumeration must contain every leaf cell (an empty enumeration would give $N=0$ ), it must be sorted, cells must be closed sets rather than outer boxes minus open inner boxes (which leaves isolated boundary points and makes the goal false), and no size bound or packing fact may be assumed in the goal.

Contributions welcome: proofs of the milestones in any order, general lemmas on $L_m$ distances and interior-disjoint boxes (reusable beyond this mission), and a construction of valid BBD-trees from the paper's midpoint or middle-interval rules.

Selected references

S. Arya, D. M. Mount, N. S. Netanyahu, R. Silverman, A. Y. Wu, An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, J. ACM 45(6):891–923, 1998. https://doi.org/10.1145/293347.293348
S. Arya, D. M. Mount, Approximate nearest neighbor queries in fixed dimensions, Proc. 4th ACM-SIAM SODA, 271–280, 1993 (reference [Arya and Mount 1993b] of the main paper, https://doi.org/10.1145/293347.293348).
S. Arya, D. M. Mount, N. S. Netanyahu, R. Silverman, A. Y. Wu, An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, Proc. 5th ACM-SIAM SODA, 573–582, 1994 (reference [Arya et al. 1994] of the main paper).
D. M. Mount, S. Arya, ANN: A library for approximate nearest neighbor searching. https://www.cs.umd.edu/~mount/ANN/
S. Har-Peled, P. Indyk, R. Motwani, Approximate nearest neighbor: towards removing the curse of dimensionality, Theory of Computing 8:321–350, 2012. https://doi.org/10.4086/toc.2012.v008a014

8 thms2 active usersReviewed

Graph Theory Markov Chain Probability·Captain: mikedeng1

The Evolution of Conventions II: The Stochastically Stable States of a Regular Perturbation of a Finite Markov Chain Are the Recurrent Classes of Minimum Stochastic PotentialResearch Paper

Motivation

Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.

H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in $2\times 2$ games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).

Setting

Let $X$ be a finite set and $P^0$ the transition matrix of a Markov chain on $X$ . A state $y$ is reachable from $x$ if $(P^0)^n_{xy} > 0$ for some $n \ge 0$ ; $x$ is recurrent if every state reachable from $x$ can reach $x$ back; the recurrent communication classes $X_1, \dots, X_J$ are the communication classes of recurrent states.

A family $(P^\varepsilon)_{\varepsilon \in (0,a]}$ of Markov chains on $X$ is a regular perturbation of $P^0$ if for all $x, y$ :

(6) $P^\varepsilon$ is aperiodic and irreducible for every $\varepsilon \in (0,a]$ ;
(7) $P^\varepsilon_{xy} \to P^0_{xy}$ as $\varepsilon \to 0$ ;
(8) if $P^\varepsilon_{xy} > 0$ for some $\varepsilon$ , there is $r \ge 0$ with $0 < \lim_{\varepsilon \to 0} \varepsilon^{-r} P^\varepsilon_{xy} < \infty$ .

The exponent $r = r(x,y)$ is the resistance of the transition $x \to y$ . The graph $G$ has vertex set $X$ and an edge $(x,y)$ when $P^\varepsilon_{xy} > 0$ for all small $\varepsilon$ , weighted by $r(x,y)$ .

For $z \in X$ , a $z$ -tree is a spanning tree of edges of $G$ in which every $x \ne z$ has a unique directed path to $z$ . The potential of $z$ is

\gamma(z) = \min_{T \in \mathcal T_z} \sum_{(x,y) \in T} r(x,y). \tag{9}

For classes $i \ne j$ , $r_{ij}$ is the least resistance of a path in $G$ from $X_i$ to $X_j$ . On the complete directed graph $\mathcal G$ with vertices $1, \dots, J$ and edge weights $r_{ij}$ , the stochastic potential $\gamma_j$ of $X_j$ is the least total weight of a $j$ -tree in $\mathcal G$ .

Formalization targets

Goal: Theorem 4 (p. 78)

If $\mu^\varepsilon$ is the stationary distribution of $P^\varepsilon$ for $\varepsilon \in (0,a]$ , then $\mu^\varepsilon \to \mu^0$ as $\varepsilon \to 0$ , where $\mu^0$ is a stationary distribution of $P^0$ , and

\mu^0_x > 0 \iff x \in X_j \text{ for some } j \text{ with } \gamma_j = \min_i \gamma_i .

Milestones, in the order of the paper's proof

Resistance (p. 77). The exponent in (8) is unique; a transition positive for some $\varepsilon$ is an edge of $G$ ; and the edges of zero resistance are exactly the transitions with $P^0_{xy} > 0$ .
Markov chain tree formula (p. 79). For an aperiodic irreducible chain $P'$ , $\mu'_z = p'_z / \sum_x p'_x$ with $p'_z = \sum_{T \in \mathcal T_z} \prod_{(x,y)\in T} P'_{xy}$ is the unique stationary distribution.
Lemma 1 (p. 78). $\mu^\varepsilon \to \mu^0$ , $\mu^0$ is stationary for $P^0$ , and $\mu^0_x > 0$ iff $\gamma(x) \le \gamma(y)$ for all $y$ .
(p. 80) A stationary distribution of a finite chain vanishes on non-recurrent states.
(p. 80) All states of a recurrent class of $P^0$ have the same potential.
Lemma 2 (p. 80). $\gamma(x) = \gamma_j$ for every $x \in X_j$ .

Significance

Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in $2\times 2$ coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.

The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.

Difficulty

The first idea is to take the limit in $\mu^\varepsilon P^\varepsilon = \mu^\varepsilon$ : compactness and (7) give that every limit point of $\mu^\varepsilon$ is stationary for $P^0$ , but $P^0$ has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes $\mu^\varepsilon_z$ a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal $x$ -tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a $j$ -tree on the class graph without increasing its resistance. The easy inequality $\gamma(x_j) \le \gamma_j$ glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.

Formalization scope

States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family $P^\varepsilon$ is a function ℝ → Matrix X X ℝ constrained only on $(0, a]$ ; all limits are one-sided ( $\varepsilon \to 0^+$ ), $\varepsilon^{-r}$ is the real power, and " $0 < \lim < \infty$ " is a real limit $c > 0$ . Distributions are row vectors and stationarity is $\mu A = \mu$ . Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is $+\infty$ ; under the hypotheses all of them are finite.

The goal quantifies over every regular perturbation, not a parametric family such as $(1-\varepsilon)P^0 + \varepsilon Q$ , and over every family of stationary distributions of the $P^\varepsilon$ (unique by (6)). The recurrent classes are computed from $P^0$ , not supplied as data, and $\gamma_j$ is computed on the class graph with weights $r_{ij}$ ; defining $\gamma_j$ as $\gamma(x)$ for some $x \in X_j$ would make Lemma 2 definitional and is ruled out.

Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.

Selected references

H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984 (Ch. 6, Lemma 3.1). https://doi.org/10.1007/978-1-4684-0176-9
M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
D. P. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988. https://mitpress.mit.edu/9780262582384/
Related missions on learning dynamics: StochFictPlay.* (Hofbauer and Sandholm 2002, stochastic fictitious play) and CalibratedCE.* (calibrated learning and correlated equilibrium).

11 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy: The Zheng–Federgruen Algorithm Terminates with an Optimal (s, S) Policy and c⁰ = c*Research Paper

Motivation

The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level $s$ , order enough to bring it up to the order-up-to level $S$ . Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.

Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal $s$ and $S$ and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the $(s,S)$ grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).

Setting

One-period demands $D$ are i.i.d. and integer valued, with $p_j=\Pr\{D=j\}$ , $j\ge0$ , and $p_0<1$ . An order costs $K>0$ . $G(y)$ is the one-period expected cost when a period starts at inventory position $y\in\mathbb Z$ . The paper assumes only:

$-G$ is unimodal: for some integer $m$ , $G$ is nonincreasing on $y\le m$ and nondecreasing on $y\ge m$ ;
$\lim_{|y|\to\infty}G(y)>\min_yG(y)+K$ .

Write $y_1^*$ and $y_2^*$ for the smallest and largest minimizers of $G$ . The renewal density $m$ and renewal function $M$ are

m(0)=(1-p_0)^{-1},\quad m(j)=\sum_{l=0}^{j}p_l\,m(j-l)\ (j\ge1),\qquad M(0)=0,\quad M(j)=M(j-1)+m(j-1).

For integers $s<S$ , the long-run average cost of the (s, S) policy is

c(s,S)=\frac{K+\sum_{j=0}^{S-s-1}m(j)\,G(S-j)}{M(S-s)}.

A pair $(s,S)$ is an optimal policy if $c(s,S)\le c(s',S')$ for all integers $s'<S'$ . The optimal cost $c^*$ is the value of any optimal policy. For fixed $S$ , $s$ is an optimal reorder level if $c(s,S)\le c(s',S)$ for all $s'<S$ .

The algorithm (§3, p. 659) starts at any minimizer $y^*$ of $G$ .

Step 0. Decrease $s$ from $y^*$ until $c(s,y^*)\le G(s)$ . Set $S^0:=y^*$ , $c^0:=c(s,S^0)$ and $S:=y^*+1$ .
Step 1. While $G(S)\le c^0$ : if $c(s,S)<c^0$ , set $S^0:=S$ , increase $s$ while $c(s,S^0)\le G(s+1)$ , and set $c^0:=c(s,S^0)$ . In either case, $S:=S+1$ .

Formalization targets

Goal: Theorem 1(a)

For every demand law with $p_0<1$ , every $K>0$ , every $G$ satisfying the two assumptions, and every minimizer $y^*$ of $G$ , the algorithm terminates. On termination, with final values $s,S^0,c^0$ ,

c(s,S^0)\le c(s',S')\ \text{ for all integers } s'<S',\qquad c^0=c(s,S^0)=c^*.

Milestones

The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:

the weighted-average identity (6), $c(s-1,S)=\alpha_nc(s,S)+(1-\alpha_n)G(s)$ with $\alpha_n=M(n)/M(n+1)$ and $n=S-s$ , and Lemma 0 on the comparisons it implies;
Lemma 1(a): a reorder level $s^0<y_1^*$ with $G(s^0)\ge c(s^0,S)\ge G(s^0+1)$ (condition (7)) is optimal for $S$ ;
Corollary 1, the stopping rule of Step 0;
Lemma 2(a)–(c), the bounds $y_2^*\le S^*$ and $S^*\le\bar S^*=\max\{y\ge y_2^*:G(y)\le c^*\}$ , which give the stopping rule of Step 1;
Lemma 3(a), the single-comparison test for improvement, and Corollary 2(b) with Lemma 3(b), which justify the inner loop.

Significance

The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any $G$ with $-G$ unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.

Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).

Difficulty

Optimality is claimed over all pairs $s'<S'$ , an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed $S$ , the skipped reorder levels are handled by the unimodality of $c(\cdot,S)$ (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of $c$ in $(s,S)$ is not available. The paper uses no structure of $c$ beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.

Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at $-\infty$ may be finite, so $\min_{s<S}c(s,S)$ need not be attained for every $S$ . Lattice demands, for which $m$ vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.

Formalization scope

Levels $s,S,y$ are integers. Demand values are natural numbers, and the demand law is the published VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis $p_0<1$ . All costs are real.
The cost is the ratio above. Equation (1) on p. 655 is misprinted as $M(S-s)K+\sum\cdots$ , and the ratio is the form fixed by (3) and (5). The Lean value $c(s,S)$ for $s\ge S$ is a junk $0$ , so every quantifier over reorder levels carries $s<S$ .
$m$ is defined by the solved recursion $m(j)=(1-p_0)^{-1}\sum_{l=1}^{j}p_l\,m(j-l)$ (p. 660), and $M(j)=\sum_{i<j}m(i)$ .
The growth assumption is encoded as: $G$ has a minimizer $y_0$ and $G(y)>G(y_0)+K$ for all but finitely many $y$ . Under unimodality this is equivalent to the page's limit condition. It is not strengthened to $G\to+\infty$ .
Optimality is among (s, S) policies. That an (s, S) policy is optimal among all policies is Veinott (1966) and is neither stated nor used. $c^*$ , $c^*(S)$ , $y_i^*$ , $\bar S^*$ , $\bar S_c$ and $s'$ are never real infima: they are the cost of a given optimal pair, $\exists$ -statements, or binders characterised as least or greatest elements.
The algorithm is a step function on the state $(s,S,S^0,c^0,\text{phase})$ that keeps the paper's order of tests and its weak and strict inequalities. The run with $n$ steps returns an output only if the algorithm has terminated.
Ruled out as trivializing: comparing only with the pairs the algorithm visits or with a bounded box; assuming termination, or a budget that returns the current state; assuming $G\to+\infty$ ; leaving $c(s,S)$ unguarded for $s\ge S$ .
Repaired statements. Lemma 3(a) is stated with condition (7) at $S^0$ as an extra hypothesis. With $s^0$ merely optimal it fails when $m$ has a zero: for $p=(1/5,0,1/5,3/5)$ , $m(1)=0$ and adjacent reorder levels tie. The algorithm always has (7). Lemma 1(b), "an optimal reorder level satisfying (7) exists for every $S$ ", is false when $\lim_{y\to-\infty}G(y)$ is finite. An example is $D\equiv2$ , $K=1$ , $G(0)=5$ , $G(y)=10-0.1\cdot2^{-|y|}$ ( $y\neq0$ ), $S=1$ , where no optimal reorder level exists. It is not posed here, and the goal does not depend on it.
Not formalized: Theorem 1(b)–(c), the operation counts, which depend on a bookkeeping model described in words; Corollary 3, which the paper notes is not needed for the algorithm; and the variant for a general starting level $S_0$ .
Welcome contributions: general facts about the discrete renewal density ( $m\ge0$ , $M>0$ ), the identity (6), and lemmas on $c(\cdot,S)$ that are reusable for related (s, S) and (r, Q) work.

Selected references

Y.-S. Zheng and A. Federgruen, Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy, Operations Research 39(4):654–665, 1991. https://doi.org/10.1287/opre.39.4.654
A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM J. Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
A. Federgruen and P. Zipkin, An Efficient Algorithm for Computing Optimal (s, S) Policies, Operations Research 32(6):1268–1285, 1984. https://doi.org/10.1287/opre.32.6.1268
A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

14 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.

A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.

Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.

Setting

A negative dynamic programming problem consists of non-empty Borel sets $S$ (states) and $A$ (actions), a law of motion $q(\cdot\mid s,a)$ , which is a probability kernel from $S\times A$ to $S$ , and a Borel return function $r(s,a,t)$ with

r\le 0,\qquad r>-\infty,\qquad \int r(s,a,t)\,dq(t\mid s,a)>-\infty\ \ \text{for all }(s,a).

There is no discounting. A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the action $a_n$ at stage $n$ from a probability kernel $\pi_n(\cdot\mid h_n)$ , where $h_n=(s_1,a_1,\dots,a_{n-1},s_n)$ is the history. A policy is Markov if $a_n=f_n(s_n)$ for Borel maps $f_n:S\to A$ , semi-Markov if $a_n=g_n(s_1,s_n)$ for Borel $g_n$ , and stationary, written $f^{(\infty)}$ , if $a_n=f(s_n)$ for one Borel rule $f$ . Random Markov and random semi-Markov policies draw $a_n$ from kernels in $s_n$ , respectively $(s_1,s_n)$ .

The expected total return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\mathbb E^{\pi}_{s}\,r(s_n,a_n,s_{n+1})\in[-\infty,0],

the optimal return is $v^*(s)=\sup_\pi I(\pi)(s)$ over all policies, and $\pi^*$ is optimal if $I(\pi^*)(s)\ge v^*(s)$ for every $s$ . For a Borel rule $f$ , the operator $T$ acts on non-positive Borel functions $u$ by

Tu(s)=\int r(s,f(s),t)+u(t)\,dq(t\mid s,f(s)).

The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

\big(\exists\,\pi^*\ \ I(\pi^*)\ge v^*\big)\ \Longrightarrow\ \exists\,f\ \text{Borel},\ \ I(f^{(\infty)})\ge v^* .

Milestones

Lemma 2.1: for a kernel $q(\cdot\mid x)$ and a Borel $u\le 0$ on $X\times Y$ there is a Borel $f$ with $u(x,f(x))\ge\int u(x,y)\,dq(y\mid x)$ .
Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$ .
Lemma 4.1 (a), (b): policies built from the conditional laws of $a_n$ given $(s_1,s_n)$ , respectively given $s_n$ under an initial law $p$ , reproduce the laws of $(s_1,s_n,a_n,s_{n+1})$ , respectively the $p$ -averaged laws of $(s_n,a_n,s_{n+1})$ .
Theorem 4.1: for every policy $\pi$ and initial law $p$ there are a random semi-Markov $\pi^*$ and a random Markov $\pi^{**}$ with $I(\pi)=I(\pi^*)$ and $pI(\pi)=pI(\pi^{**})$ for every return function.
Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$ , then $I(\pi)\ge I(\sigma)$ .
Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$ .
Theorem 5.1 (N), parts (a)–(g): the properties of $T$ , including $TI(\pi)=I(f,\pi)$ , $TI(f^{(\infty)})=I(f^{(\infty)})=\lim_n T^n0$ and $I_n(\pi,v)=T_1\cdots T_nv$ for Markov $\pi$ .

Significance

Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on $(p,\varepsilon)$ -optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.

All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.

Difficulty

The obvious argument starts from an optimal $\pi^*$ , takes its first decision rule $f$ , and shows that $f^{(\infty)}$ is optimal. That fails for a general $\pi^*$ , because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal $-\infty$ , and every limit exchange has to respect that.

Formalization scope

Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return $r$ is real-valued, non-positive and integrable under $q(\cdot\mid s,a)$ for every $(s,a)$ . Returns live in the extended reals. $I(\pi)$ , $I_n(\pi,v)$ , $T$ and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in $[0,\infty]$ , so a return of $-\infty$ is never collapsed to $0$ . $I(\pi)$ is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. $v^*$ is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case ( $r\le 0$ , $\beta=1$ ) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.

Explicit choices:

Lean numbers decisions from $0$ . Hist S A n is the paper's $H_{n+1}$ and the plan's kernel κ n is $\pi_{n+1}$ .
The objects $\pi^*$ and $\pi^{**}$ of Lemma 4.1 are defined in the paper's proof as conditional distributions. Here their defining property is a hypothesis: for every initial state, or after averaging over $p$ , the joint law of $(s_n,a_n)$ is the law of $s_n$ followed by the kernel.
In Theorem 4.1, "for any return function $r$ " is a quantifier over every negative problem with the same law of motion, placed after the choice of $\pi^*$ and $\pi^{**}$ .
In Theorem 5.1 (b), $u+c$ is required to lie in $M(S)$ . In (d), the increasing part holds only on $\{\sup_jTu_j>-\infty\}$ .
In Theorem 5.1 (f), $T$ is applied to $I(\pi)$ for a general plan with no measurability hypothesis. The lower integral is defined for every function.

Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell and C. Ryll-Nardzewski, Non-existence of everywhere proper conditional distributions, Ann. Math. Statist. 34(1) (1963) 223–225. https://doi.org/10.1214/aoms/1177704259

16 thms2 active usersReviewed

Dynamic Programming Machine Learning Probability+1·Captain: mikedeng1

Technical Note: Q-Learning: With Bounded Rewards and Learning Rates with Σα = ∞, Σα² < ∞ at Every State–Action Pair, Tabular Q-Learning Converges to Q* with Probability 1Research Paper

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$ , a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$ . Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$ . The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).

In the $n$ -th episode the agent observes a state $x_n$ , performs an action $a_n$ , observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$ , and updates its table with a learning rate $\alpha_n$ :

Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}

from given initial values $Q_0$ . Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$ -th visit to $(x,a)$ , the learning-rate condition is

\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$ ), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$ , emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$ .

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$ , learning rates $0\le\alpha_n<1$ and (3),

Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.

Milestones (the paper's appendix, in attack order)

Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$ .
Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$ .
Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$ , $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$ .
Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$ .

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$ .

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD( $\lambda$ ), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

$X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$ , rows nonnegative and summing to $1$ .
$Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
Lean index $n$ is the paper's episode $n\ge1$ ; index $0$ of the episode data is unused and qIter … 0 $=Q_0$ .
Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$ -measurable, $y_n,r_n$ are $\mathcal F_n$ -measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$ , $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$ , $|r_n|\le\mathcal R$ , $0\le\alpha_n<1$ , and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$ ; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$ : with the page's entrywise closeness the printed constant is false once $|X|\ge4$ . The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8

8 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Average Optimality in Dynamic Programming with General State Space: Under (W) or (S) and Bounded Relative Discounted Values, a Limit of Discount-Optimal Policies Is Average OptimalResearch Paper

Motivation

A Markov decision process with the average cost criterion asks for a policy that minimizes the long-run expected cost per unit time. The criterion is the natural one for inventory, queueing and maintenance systems that run indefinitely without a meaningful discount rate, and it is the standard benchmark in the theory of controlled Markov chains (Arapostathis et al. 1993, Hernández-Lerma and Lasserre 1996). Unlike the discounted criterion, it has no contraction to work with, and an average-optimal policy may fail to exist.

The classical route to average optimality is the vanishing discount approach: solve the $\beta$ -discounted problem, which is well behaved, and let $\beta \uparrow 1$ . Schäl's paper gives conditions on a model with a general (Borel) state space under which this limit produces an average-optimal stationary policy.

Timeline. Taylor (1965) and Ross (1968) used the vanishing discount approach with equicontinuity via Arzelà–Ascoli. Sennott (1989) proved, for countable state spaces, that pointwise bounded relative discounted values yield an average cost optimality inequality and an average-optimal stationary policy. Schäl (1993, this mission) extended this to standard Borel state spaces under two alternative compactness–continuity conditions, (W) and (S). Later work, e.g. Feinberg, Kasyanov and Zadoianchuk (2012) and Feinberg and Liang (2022), weakened the compactness assumptions and studied when the inequality becomes an equation.

Setting

The model $(S, A, A(\cdot), q, c)$ consists of standard Borel spaces $S$ (states) and $A$ (actions); nonempty action sets $A(x) \subseteq A$ whose graph $\{(x, a) : a \in A(x)\}$ is measurable; a transition law $q(\cdot \mid x, a)$ ; and a measurable one-step cost $c(x, a) \in [0, \infty]$ . A policy $\delta \in \Delta$ chooses, at each stage $n$ , a randomized action that may depend on the whole history and lies in $A(x_n)$ with probability one. A stationary policy $f \in \mathbb F$ is a measurable $f : S \to A$ with $f(x) \in A(x)$ .

For a policy $\delta$ and initial state $x$ , $J^n(\delta, x)$ is the expected total cost of the first $n$ stages, and

\Phi(\delta, x) = \limsup_{n\to\infty} \tfrac1n J^n(\delta, x), \qquad g = \inf_{x \in S}\inf_{\delta \in \Delta} \Phi(\delta, x).

A policy is average optimal if $\Phi(\delta, x) = g$ for every $x$ . The General Assumption is $g < \infty$ .

For $0 < \beta < 1$ , $J_\beta(\delta, x)$ is the expected total $\beta$ -discounted cost, $v_\beta(x) = \inf_\delta J_\beta(\delta, x)$ , $m_\beta = \inf_x v_\beta(x)$ , and $w_\beta = v_\beta - m_\beta \ge 0$ is the relative discounted value function. The quantities $\bar g$ and $\underline g$ are the upper and lower limits of $(1-\beta)m_\beta$ as $\beta \uparrow 1$ . Condition (B) requires $\sup_{\beta < 1} w_\beta(x) < \infty$ for each $x$ .

Condition (W): $S$ is locally compact with countable base, the $A(x)$ are compact and $x \mapsto A(x)$ is upper semicontinuous, $q$ is weakly continuous on the graph of $A$ , and $c$ is lower semicontinuous there. Condition (S): the $A(x)$ are compact, and for each fixed $x$ , $a \mapsto q(\cdot \mid x, a)$ is setwise continuous and $a \mapsto c(x, a)$ is lower semicontinuous on $A(x)$ .

Formalization targets

Goal: Theorem 3.8

Under the General Assumption, (B), and (W) or (S):

\exists f_1 \in \mathbb F:\ \Phi(f_1, x) = g \ \ \forall x \in S, \qquad g = \lim_{\beta\to1}(1-\beta)m_\beta = \lim_{\beta \to 1}(1-\beta)v_\beta(x)\ \ \forall x.

Moreover, for every sequence $\beta(k) \uparrow 1$ and every choice of $\beta(k)$ -discount-optimal stationary policies $f_{\beta(k)}$ , some average-optimal $f_1$ is a limit of them: under (W), $f_1(x) = \lim_m f_{\beta_m}(x_m)$ with $\beta_m$ from $\{\beta(k)\}$ , $\beta_m \to 1$ and $x_m \to x$ ; under (S), $f_1(x) = \lim_m f_{\beta_m}(x)$ .

Milestones

Lemma 1.2: $\limsup_{\beta\to1}(1-\beta)J_\beta(\delta, x) \le \Phi(\delta, x)$ , and $\underline g \le \bar g \le g$ .
Proposition 1.3: a finite measurable $\underline w \ge 0$ and $f_1 \in \mathbb F$ with $\underline w(x) + \underline g \ge c(x, f_1(x)) + \int \underline w\, dq(x, f_1(x))$ give $\Phi(f_1, \cdot) = g = \underline g = \bar g$ .
Proposition 2.1 and (2.2): existence of discount-optimal stationary policies, the discounted optimality equation and its relative form.
Lemma 2.3: Fatou's lemma for setwise and for weakly converging measures.
(3.2), Lemmas 3.3, 3.4: the lower limit $\underline w(x) = \liminf_{k\to\infty, y\to x} w_{\beta(k)}(y)$ is attained along measurable sequences.
Proposition 3.5 and its (S) version (3.7): $\underline w$ and some $f_1$ satisfy the optimality inequality with $\underline g$ .

Significance

The theorem gives existence of an average-optimal stationary policy on a general state space from checkable model conditions plus pointwise bounds on relative values, without assuming a solution of the average cost optimality equation. It also identifies the optimal average cost as the Abelian limit of discounted values, and says how to compute an optimal policy: as a limit of discount-optimal ones. §4 of the paper verifies (B) through entrance-time bounds and applies the theorem to Assaf's invariant problem and to a finite-capacity inventory model.

The result is a published theorem; none of it is machine-checked. Formalizing it requires the measure-theoretic layer of Borel dynamic programming (canonical path measures of history-dependent policies, discounted optimality equations, measurable selection of minimizers and of accumulation points) and Fatou lemmas for varying measures. These components are reusable for any Borel-space MDP. Related platform work: the Feinberg–Liang average-cost optimality equation under an additional equicontinuity assumption is posed separately (FeinbergLiang.ACOE.acoe_of_assumptionEC); it is a different theorem.

Difficulty

The naive argument takes a pointwise limit of $w_{\beta}$ as $\beta \to 1$ in the relative optimality equation (2.2). Under (B) the family $\{w_\beta(x)\}$ is only bounded pointwise, so no subsequence need converge, and even a pointwise lower limit loses the continuity needed to pass $\int w_\beta\, dq(x, f_\beta(x))$ to the limit when $q$ is only weakly continuous. The generalized lower limit $\underline w(x) = \liminf_{k, y\to x} w(k, y)$ repairs this, but then the limit has to be realized along measurably chosen states and indices, and the limiting actions must be selected measurably as accumulation points. The second obstacle is that only an inequality survives, with the constant $\underline g$ ; turning it into average optimality needs the Tauberian comparison of Lemma 1.2.

Formalization scope

The model reuses the published FeinbergLiang.ACOE.MDP (history-dependent randomized policies, the Ionescu-Tulcea path measure, $J^n$ , $J_\beta$ , $\Phi$ ) with its constant lower = 0, and a local definition file adds action sets, admissibility, $g$ , $v_\beta$ , $m_\beta$ , $\bar g$ , $\underline g$ , $w_\beta$ , $\underline w$ and Conditions (W), (S), (B). Committed conventions:

All costs and values lie in $[0, \infty]$ ; $(1-\beta)$ is a nonnegative extended real, and $\beta \to 1$ means $\beta \uparrow 1$ .
Every infimum defining $g$ and $v_\beta$ runs over admissible policies only (actions in $A(x)$ almost surely); $q$ and $c$ are defined on $S \times A$ , but only their values on the graph of $A$ enter.
$w_\beta$ is a truncated difference, which equals $v_\beta - m_\beta$ because the General Assumption gives $m_\beta < \infty$ . The General Assumption is an explicit hypothesis of every statement that involves $g$ , $\underline g$ , $\bar g$ , $m_\beta$ or $w_\beta$ .
Upper semicontinuity of $A(\cdot)$ is Berge's. Condition (W)(0) is part of CondW: the topology on $S$ generates its σ-algebra and is locally compact, second countable and Hausdorff, hence metrizable; the metric $\rho$ of §3 is a metric-space instance. Under (S) no topology on $S$ is used, and the lower limit is $\liminf_k w_{\beta(k)}(x)$ (the discrete metric).
(W)(1) prints " $A(x) \in \mathcal C(x)$ ", read as $\mathcal C(A)$ . (3.2) prints $\inf_{k\ge n}\underline w_k(k, x)$ , which is false in general; the subscript- $n$ version used in the proof of Lemma 3.4 is stated. " $\{\beta_m\} \subset \{\beta(k)\}$ , $\beta_m \to 1$ " is encoded as $\beta_m = \beta(k_m)$ with $k_m \to \infty$ .
Theorem 3.8's " $\{\beta(k)\}$ can be any sequence" is a universal quantifier over sequences and over choices of discount-optimal policies.

A formalization that assumes an average cost optimality inequality or equation, or that assumes the existence of the limit $\lim(1-\beta)m_\beta$ , proves Proposition 1.3 rather than the goal; the goal derives the inequality from (W) or (S), (B) and the General Assumption alone. Contributions to the shared infrastructure (Markov property of the canonical process, measurable selection theorems such as Brown–Purves, Fatou lemmas for varying measures) are welcome as separate theorems. §4 of the paper (entrance-time bounds for (B)) is outside this mission.

Selected references

M. Schäl, Average Optimality in Dynamic Programming with General State Space, Mathematics of Operations Research 18(1), 163–172, 1993. https://doi.org/10.1287/moor.18.1.163
M. Schäl, Conditions for optimality in dynamic programming and for the limit of n-stage optimal policies to be optimal, Z. Wahrscheinlichkeitstheorie verw. Gebiete 32, 179–196, 1975. https://doi.org/10.1007/BF00532612
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
R. F. Serfozo, Convergence of Lebesgue integrals with varying measures, Sankhyā Ser. A 44, 380–402, 1982.
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
E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 591–607, 2012. https://doi.org/10.1287/moor.1120.0555

14 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting 1: If G(f) ∪ H(f) Is Empty, f Maximizes the Gain and Then the Bias, and Each Improvement Step Raises (x, y, z)Research Paper

Motivation

A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector $z(f)$ guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the $n$ -discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.

Timeline:

1960: Howard, Dynamic Programming and Markov Processes: policy improvement for the discounted and the average-return problems.
1962: Blackwell, Discrete Dynamic Programming: existence of stationary policies optimal for all discount factors near one; the expansion $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+o(1)$ ; nearly optimal (1-optimal) policies characterized by lexicographic maximization of $(x,y)$ .
1966: Veinott, this paper: the extended policy improvement method that finds a 1-optimal stationary policy in finitely many steps (Theorem 6), and a finite-horizon characterization of the same policies (Theorem 7).
1969: Veinott, Discount optimality and sensitive optimality: the full hierarchy of $n$ -discount optimal policies and the corresponding nested improvement method.

Setting

There are finitely many states $s$ and a finite set of actions. Choosing action $a$ in state $s$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$ . A decision rule $f\in F$ picks an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$ and $Q(f)$ the stochastic matrix with entries $q(s'\mid s,f(s))$ . A policy is a sequence $(f_1,f_2,\dots)$ of decision rules, $f^\infty=(f,f,\dots)$ is a stationary policy, and for $0\le\beta<1$

V_\beta(\pi)=\sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\,r(f_{n+1})

is the vector of expected discounted returns. For vectors, $u\ge v$ is coordinatewise and $u>v$ means $u\ge v$ and $u\ne v$ .

Let $Q^*(f)$ be the Cesàro limit of the powers of $Q(f)$ . The gain $x(f)$ and the bias $y(f)$ are the unique solutions of

[I-Q(f)]x=0,\quad Q^*(f)x=Q^*(f)r(f);\qquad [I-Q(f)]y=r(f)-x(f),\quad Q^*(f)y=0,

and $z(f)$ is the unique solution of $[I-Q(f)]z=-y(f)$ , $Q^*(f)z=0$ . Write $F'$ for the decision rules of maximal gain and $F''\subset F'$ for those of maximal bias within $F'$ .

The two improvement sets compare $f$ with a decision rule $g$ through the state-by-state tests

\text{(i) } [Q(g)x(f)]_s\ge[x(f)]_s,\qquad \text{(ii) } [r(g)+Q(g)y(f)]_s\ge[x(f)+y(f)]_s .

$G(f)$ consists of the $g$ for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and $g(s)=f(s)$ wherever both are equalities. $E(f)$ consists of the $g$ for which (i) and (ii) are equalities at every state. For $g\in E(f)$ ,

\text{(iii) } [-y(f)+Q(g)z(f)]_s\ge[z(f)]_s,

and $H(f)$ consists of the $g\in E(f)$ for which (iii) holds everywhere, strictly somewhere, with $g(s)=f(s)$ wherever it is an equality.

Formalization targets

Goal: Theorem 6 (p. 1290)

For every $f\in F$ :

$G(f)=\varnothing\ \Rightarrow\ f\in F'$ ;
$G(f)\cup H(f)=\varnothing\ \Rightarrow\ f\in F''$ ;
$g\in G(f)\ \Rightarrow\ x(g)>x(f)$ , or $x(g)=x(f)$ and $y(g)>y(f)$ ;
$g\in H(f)\ \Rightarrow\ x(g)=x(f)$ , and $y(g)>y(f)$ , or $y(g)=y(f)$ and $z(g)>z(f)$ .

Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises $(x,y,z)$ lexicographically and stops at a decision rule in $F''$ .

Milestones

Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\epsilon(\beta,f)$ with $\epsilon(\beta,f)\to0$ as $\beta\to1^-$ , and the unique-solution characterizations of $x(f)$ , $y(f)$ (already posed on the platform, referenced).
Lemma 1 (Blackwell): $g\in E(f)\Rightarrow x(g)=x(f)$ , and $y(g)=y(f)$ if moreover $Q^*(g)Q^*(f)=Q^*(g)$ (referenced).
Theorem 1: for fixed $0\le\beta<1$ , exactly one of " $f^\infty$ has no one-step improvement and is $\beta$ -optimal" and "some $g$ gives $V_\beta(g,f^\infty)>V_\beta(f^\infty)$ and $V_\beta(g^\infty)>V_\beta(f^\infty)$ ".
Theorem 4: $F''$ is the nonempty set of $f$ with $f^\infty$ 1-optimal.
Theorem 5 and Corollary 1: $G(f)=\varnothing\Rightarrow f\in F'$ ; $g\in G(f)\Rightarrow V_\beta(g^\infty)>V_\beta(f^\infty)$ for $\beta$ near one, hence the lexicographic increase of $(x,y)$ .
Lemma 4: for $g\in E(f)$ , $y(g)=y(f)+w(g)$ , where $w(g)$ is the unique solution of $[I-Q(g)]w=0$ , $Q^*(g)w=Q^*(g)(-y(f))$ .
(12): $z(f)$ is the unique solution of its system.
Lemma 5: $G(f)=\varnothing$ and $y(f)\ge y(g)$ for all $g\in E(f)$ imply $f\in F''$ .
Two steps of the proof of Theorem 6: $H(f)=\varnothing\Rightarrow y(g)\le y(f)$ on $E(f)$ ; and $g\in H(f)\Rightarrow w(g)>w(f)=0$ , or $w(g)=w(f)=0$ and $z(g)>z(f)$ .

Significance

Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over $F'$ , a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set $E(f)$ suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the $n$ -discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.

The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and $z$ and the facts about the limit matrix $Q^*$ and the deviation matrix they rest on.

Difficulty

Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set $G(f)$ . The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of $g\in E(f)$ cannot be compared with the bias of $f$ by a state-by-state test in the original problem, because $E(f)$ is a product of action sets $E(s,f)$ different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is $-y(f)$ and the role of the gain is played by $w(g)$ . A second difficulty is Lemma 5: $E(f)$ may be a proper subset of $F'$ (Example 3 of the paper), so maximizing the bias over $E(f)$ does not obviously maximize it over $F'$ . The certificate does not follow from the gain and bias tests at $f$ alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).

Formalization scope

Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's $A_s$ are all equal to it), decision rules St → Act, policies indexed from $0$ (π 0 is $f_1$ ), real vectors St → ℝ with the pointwise order, and VecGt for the paper's $>$ (not coordinatewise strict). $Q^*(f)$ is the published Cesàro limit $\lim (N+1)^{-1}\sum_{i=0}^N Q(f)^i$ , the same limit as Veinott's $N^{-1}\sum_{i=0}^{N-1}$ . The gain and bias are the published closed forms $x(f)=Q^*(f)r(f)$ and $y(f)=H(f)r(f)$ with the deviation matrix $H(f)$ ; the new vectors are closed forms too: $w(g)=Q^*(g)(-y(f))$ and $z(f)=H(f)(-y(f))$ , and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set $H(f)$ is HSet, to keep it apart from the deviation matrix Hf.

$G(f)$ and $H(f)$ are defined literally from the paper's inequalities, including the clauses "at least one strict" and " $g(s)=f(s)$ where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a $g$ that only reshuffles ties would count as an improvement); replacing $F''$ or $G(f)$ by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.

The reduction "replace $A_s$ by $E(s,f)$ and $r(g)$ by $-y(f)$ " is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities $Q^*Q=QQ^*=Q^*Q^*=Q^*$ , $(I-Q)H=I-Q^*$ , $Q^*H=0$ , would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.

Selected references

D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
A. F. Veinott, Jr., Discount Optimality and Sensitive Optimality, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

16 thms2 active usersReviewed

Mathematical Physics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XIII: The Sherrington–Kirkpatrick Model at High Temperature — Deviations of log Z_N from β²N/4Textbook

Motivation

The Sherrington–Kirkpatrick model assigns random interactions to every pair of spins in a system. Its partition function aggregates the weights of all spin configurations, and the logarithm of that partition function is the free energy. For a finite system, the free energy is a random quantity because the interactions are random. A useful question is therefore how far it can move from a deterministic high-temperature scale. Aizenman, Lebowitz and Ruelle (1987), and Comets and Neveu (1995) for Gaussian couplings, proved that for $\beta<1$ the variable $\log Z_N-\beta^2N/4$ converges in law to a normal random variable ALR 1987; Talagrand asks instead for tail estimates valid for every $N$ . Talagrand's Chapter 12 gives a finite-size tail bound and a bound on the expected free energy per site under explicit moment conditions on the interaction law Talagrand 1995.

The chapter belongs to a larger study of concentration inequalities on product spaces. Its relevance to the spin model is concrete: each pair interaction is an independent coordinate, while every spin configuration uses all those coordinates. The number of coordinates grows quadratically with the number of spins. A uniform estimate must respect both this growing dimension and the normalization in the energy Talagrand 1995, pp. 191–195.

Setting

Fix an integer $N\ge1$ . A spin configuration is a vector $\varepsilon=(\varepsilon_i)_{1\le i\le N}$ with each $\varepsilon_i\in\{-1,1\}$ . Each unordered pair of sites $i<j$ has a real coupling $h_{ij}$ . For an inverse temperature $\beta>0$ , the normalized partition function is

Z_N(h)=2^{-N}\sum_{\varepsilon\in\{-1,1\}^N} \exp\left(\frac{\beta}{\sqrt N}\sum_{1\le i<j\le N} h_{ij}\varepsilon_i\varepsilon_j\right).

Write $F_N(h)=\log Z_N(h)$ . The factor $2^{-N}$ averages over configurations. Since every summand is positive, $Z_N(h)>0$ for every array $h$ , so this logarithm is defined without excluding any coupling array.

The couplings are independent with a common probability law $\nu$ on $\mathbb R$ ; their joint law is $P_N=\nu^{\otimes\binom N2}$ . Under $\nu$ , a single coupling $H$ satisfies $\mathbb EH=\mathbb EH^3=0$ and $\mathbb EH^2=1$ . The chapter also assumes $\mathbb E e^{\alpha|H|}<\infty$ for some $\alpha>0$ . Its main theorem adds $\mathbb Ee^H<2$ and $\mathbb Ee^{-H}<2$ . These inequalities describe a class of interaction laws rather than one chosen distribution. A median $M_N$ of $F_N$ means that both $P_N(F_N\le M_N)$ and $P_N(F_N\ge M_N)$ are at least $1/2$ Talagrand 1995, pp. 191–193.

Formalization targets

The goal is Theorem 12.1. There is one absolute constant $K>0$ such that, for $0<\beta<1$ and $0<t<N/K$ ,

P_N\left(\left|F_N-\frac{\beta^2N}{4}\right|\ge K\left(t+\sqrt{\log\frac K{1-\beta^2}}\right)\sqrt N\right) \le 2e^{-t^2},

and the same constant satisfies

-\frac K{\sqrt N}\sqrt{\log\frac2{1-\beta^2}} \le \frac1N\mathbb EF_N-\frac{\beta^2}{4} \le \frac KN.

The first formula controls deviations at finite $N$ ; the second locates the expected free energy per site. The theorem leaves the absolute value of $K$ unspecified, as the source does Talagrand 1995, Theorem 12.1.

Four numbered displays form the supporting targets. Equation (12.6) bounds the change in $F_N$ when all couplings are changed. Equation (12.5) bounds deviations about any median. Equations (12.7) and (12.8) give first- and second-moment estimates for $Z_N$ . Together these specify the deterministic regularity and probabilistic estimates used by the chapter Talagrand 1995, pp. 192–195.

Significance

The theorem gives a nonasymptotic probability estimate, valid for each finite size and each law meeting the stated conditions. It also bounds the difference between the mean free energy per site and $\beta^2/4$ as $N$ grows, for fixed $\beta<1$ . The moment estimates separately describe the scale of the partition function and limit its relative second moment. These conclusions keep the coupling law general within the stated moment class Talagrand 1995, Theorem 12.1 and Eqs. (12.7)–(12.8).

The result is proved in the cited paper; the open work here is its Lean formalization. A completed development would connect product-measure concentration, finite spin sums, exponential-moment bounds, and real-valued expectations in one reusable interface. The coupling product space and median conventions can also serve other finite random-interaction models. No machine-checked proof of this chapter's target is claimed by this proposal.

Difficulty

A direct bounded-differences estimate cannot be applied to this model as stated: the couplings are real and may be unbounded. An estimate that handles each coordinate must account for the law's exponential moments while still retaining the $N$ and $\beta$ factors in the chapter's explicit bounds. The normalization by $\sqrt N$ makes a single coupling's influence small, but there are $\binom N2$ couplings, so treating the total sensitivity as dimension-free would lose the scale of the theorem. The first moment alone also does not control the lower tail of $Z_N$ ; this is why the second-moment target is present Talagrand 1995, pp. 192–195.

Formalization scope

Lean indexes sites by Fin N and interactions by pairs with $i<j$ . A spin is a Boolean choice interpreted as $-1$ or $1$ , and the configuration sum is normalized by $2^N$ . The coupling array is a function on the pair type, carrying the finite product measure of the common law $\nu$ . The theorem uses $N\ge1$ , $0<\beta<1$ , and exactly the common-law moment assumptions above; the median deviation milestone uses $N\ge2$ because its denominator contains $N-1$ . The main theorem places its single universal $K$ before every size, temperature, law, and deviation level.

Expectations are Bochner integrals, so integrability is explicit in the law predicates or in each conclusion that needs it. Probability expressions are real values of measurable events under the product measure. This avoids relying on Lean's default value for a nonintegrable integral. The model retains the entire real coupling law and does not replace it with a finite alphabet or a Gaussian special case. The partition function is built from the couplings and spins, rather than supplied as an unconstrained variable.

The source's displayed (12.5) omits $\beta$ , whereas the derivation following (12.6) gives, for each tail separately, the range $0<t\le4\beta\sqrt N(N-1)$ and the exponent $-t^2/(32\beta^2(N-1))$ with the factor $2$ . The formal milestone states exactly these two one-sided bounds, while its milestone text preserves the printed display verbatim. The first- and second-moment displays are kept with an absolute constant; the second-moment target uses the proof's $N\ge8$ range, since for smaller sizes the chapter's interaction-law assumptions do not ensure that $Z_N^2$ is integrable. Integrability of $F_N$ is a conclusion of the main theorem, never a hypothesis, and the median is quantified universally, so neither the expectation in (12.4) nor the deviation bound can hold by a default value of an undefined integral or by an unsatisfiable hypothesis; the Rademacher law $\nu=\frac12(\delta_{-1}+\delta_1)$ satisfies every assumption. Reusable contributions include integrability and measurability of $Z_N$ and $F_N$ , product-law estimates, and the source's numbered inequalities.

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.
Michael Aizenman, Joel L. Lebowitz, David Ruelle, Some rigorous results on the Sherrington–Kirkpatrick spin glass model, Communications in Mathematical Physics 112 (1987), 3–20. DOI: 10.1007/BF01217677.
Francis Comets, Jacques Neveu, The Sherrington–Kirkpatrick model of spin glasses and stochastic calculus: the high temperature case, Communications in Mathematical Physics 166 (1995), 549–564. DOI: 10.1007/BF02099887.

6 thms2 active usersReviewed

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

Duality and Stability in Extremum Problems Involving Convex Functions 1: A Convex Program Is Stably Set If and Only If Its Infimum Equals the Attained Maximum of the Dual, inf (P) = max (P*)Research Paper

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

7 thms2 active usersReviewed

Combinatorics Graph Theory Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces X: The Chromatic Number of Random Graphs — χ(G(n,p), m) Lies in an Interval of Length k with High ProbabilityTextbook

Motivation

The chromatic number of the random graph $G(n,p)$ is one of the central random variables of probabilistic combinatorics. Its order of magnitude for constant $p$ , $\chi(G(n,p)) \sim n/(2\log_{1/(1-p)} n)$ , was settled by Bollobás ([B], 1988); the question that remains is how much $\chi$ fluctuates around its typical value. Shamir and Spencer ([S-S], 1987) used the edge- and vertex-exposure martingales to show that $\chi(G(n,p))$ lies, with high probability, in an interval of length about $\sqrt n$ , and for sparse graphs $p = n^{-\alpha}$ in an interval of bounded length.

Chapter 9 of Talagrand's 1995 memoir revisits this question as an application of his convex-hull inequality (Theorem 4.1.1 of the paper, posed in a separate mission of this series). The author states the aim plainly: martingale methods require ingenuity on this problem, and the chapter shows that Theorem 4.1.1 gives somewhat better results "in a completely straightforward manner". The chapter also derives, from the same inequality, an upper bound on the probability that $G(n,p)$ has no independent set of a given size — the quantity that drives the greedy colouring bound, previously obtained by Bollobás with martingales and by Janson's correlation inequality.

Timeline. 1987: Shamir–Spencer, concentration of $\chi(G(n,p))$ by martingales. 1988: Bollobás, the asymptotic value of $\chi(G(n,p))$ for constant $p$ , via a martingale bound on independent sets. 1990: Janson's inequality gives a simpler route to the same independent-set bound. 1995: Talagrand, Theorem 9.1 and Proposition 9.2, both from the convex-hull inequality.

Setting

A graph $G$ on the vertex set $V = \{1,\dots,n\}$ is a subset of $E_0 = \{(i,j);\ i<j\}$ . A set $I \subseteq V$ is independent if no two of its points are joined by an edge. For $A \subseteq V$ , the chromatic number $\chi(G,A)$ is the smallest number of independent sets that cover $A$ , that is, the chromatic number of the subgraph induced on $A$ ; $\chi(G,\emptyset) = 0$ . For an integer $m$ ,

\chi(G,m) = \inf\{\chi(G,A);\ \operatorname{card} A = m\}.

Given $0<p<1$ , the random graph $G(n,p)$ contains each possible edge $(i,j)$ with probability $p$ , independently. Concretely, $x = (x_e)_{e \in E_0} \in \{0,1\}^{E_0}$ carries the product of Bernoulli $(p)$ laws and $G(x)$ is the set of $e$ with $x_e = 1$ .

The vertex-exposure space is $\Omega' = \prod_{j} \Omega_j$ with $\Omega_j = \{0,1\}^{j-1}$ : the coordinate $\omega_j = (\omega_{i,j})_{i<j}$ lists the edges from $j$ to earlier vertices, and $G(\omega)$ contains $(i,j)$ iff $\omega_{i,j}=1$ . Changing one coordinate of $\omega$ changes only edges at one vertex.

For an integer $r$ and $e = (i,j) \in E_0$ , $N(G,e)$ denotes the number of independent sets of $G$ of size $r$ containing $i$ and $j$ .

Formalization targets

Goal: Theorem 9.1

For $k \in \mathbb N$ , $m \le n$ and $t>0$ there is an integer $a$ such that

P\big(\chi(G(n,p),m) \in [a-k,a]\big) \ \ge\ 1 - 2e^{-t^2/8} - P\big(\sup\{\chi(G(n,p),F);\ F\subset V,\ \operatorname{card}F \le t\sqrt m\} > k\big).

The integer $a$ depends on $n,p,m,k,t$ . The last term is zero when $k > t\sqrt m$ , so for such $k$ the chromatic number $\chi(G(n,p),m)$ sits in a window of $k+1$ values except on an event of probability $2e^{-t^2/8}$ .

The deterministic step of the proof, Eq. (9.3)

With $A \subseteq \Omega'$ the set of $\omega$ with $\chi(G(\omega),m) \ge a$ and $\sup\{\chi(G(\omega),F);\ \operatorname{card}F \le t\sqrt m\} \le k$ , and

B = \Big\{\omega;\ \forall (\alpha_j) \ge 0,\ \exists \omega' \in A;\ \sum_j \alpha_j 1_{\{\omega_j \ne \omega'_j\}} \le t\sqrt{\textstyle\sum_j \alpha_j^2}\Big\},

every $\omega \in B$ satisfies $\chi(G(\omega),m) \ge a-k$ .

Proposition 9.2 and Eq. (9.7)

The double count $N = \big(r(r-1)/2\big)^{-1}\sum_{e\in E_0} N(G,e)$ of independent $r$ -sets, and, for $u \ge 0$ and $r \ge 2$ , if with probability greater than $1/2$ the graph $G(n,p)$ has an independent $r$ -set and $u\sqrt{\sum_e N(G(n,p),e)^2} \le \sum_e N(G(n,p),e)$ , then

P\big(G(n,p)\ \text{contains no independent set of size } r\big) \le 2\exp\Big(-\frac{u^2}{r^2(r-1)^2}\Big).

Significance

The results. Theorem 9.1 is a two-sided concentration statement for $\chi(G(n,p),m)$ with an explicit Gaussian error $2e^{-t^2/8}$ and no loss in the exponent from a martingale difference bound; for sparse $p = n^{-\alpha}$ , where small vertex sets are sparse enough to be coloured with few colours, it localises $\chi$ to a bounded window. Proposition 9.2 is the independent-set estimate on which the greedy upper bound for $\chi(G(n,p))$ rests, obtained here with the same tool and constants $2$ and $r^2(r-1)^2$ stated on the page.

Formalizing them. All results are proved on paper; none of them, nor any concentration statement for $\chi(G(n,p))$ , is formalized in Lean or on the platform. A formal development gives a machine-checked model of $G(n,p)$ both as an edge product and as a vertex-exposure product, a statement-level check of how the convex-hull inequality transfers to graph functionals, and a corrected form of Proposition 9.2 (see the scope section): the printed hypothesis (9.4) is satisfied vacuously by graphs without independent $r$ -sets, and the formal statement records the hypothesis the proof uses.

Difficulty

The obvious encoding of $G(n,p)$ is the edge product $\{0,1\}^{E_0}$ , and it is the wrong one for Theorem 9.1: changing the edges at one vertex changes up to $n-1$ coordinates, so a Hamming-type control of $\chi(G,m)$ in the edge coordinates gives fluctuations of order $\sqrt{n^2}$ instead of order $\sqrt m$ . The statement is therefore tied to the vertex-exposure product $\Omega'$ , and transporting the law of $G(n,p)$ to $\Omega'$ and handling the "largest integer $a$ " with $P(\chi \ge a) \ge e^{-t^2/8} + b$ are further steps a formal proof must carry out. For Proposition 9.2 a plain Hamming-distance bound in the edge coordinates gives the wrong dependence on the number of independent sets: a graph with many independent $r$ -sets is turned into one with none by adding an edge inside each of them, and since these sets overlap heavily, the Hamming distance to the graphs without independent $r$ -sets is not determined by their number.

Formalization scope

Vertices are Fin n (0-based). $G(n,p)$ is graphOf x for $x : E_0 \to \mathrm{Bool}$ under gnp n p, the product (Measure.pi) of the law $p\,\delta_1 + (1-p)\,\delta_0$ on Bool, with $E_0$ the subtype $\{(i,j) : i<j\}$ ; all sets of this finite space are measurable. Probabilities are Measure.real, so right-hand sides may be negative, as on the page. $\chi(G,A)$ is Mathlib's chromaticNumber of the induced subgraph in ℕ∞; $\chi(G,m)$ is an infimum in ℕ∞, equal to $+\infty$ when $m>n$ , and Theorem 9.1 carries $m \le n$ , implicit on the page, without which it fails. Comparisons with integers are made in WithTop ℤ. The supremum over small sets $F$ is an ℕ∞ supremum over finsets with $\operatorname{card}F \le t\sqrt m$ . The vertex-exposure space has a coordinate $\{0,1\}^j$ for every 0-based vertex $j$ , the trivial one for $j=0$ included, as in the paper's $\prod_{j\le n}\Omega_j$ ; the weights in $B$ are nonnegative, the setting of Lemma 4.1.2.

Proposition 9.2 is stated with three explicit additions: $r \ge 2$ , $u \ge 0$ , and the event of (9.4) intersected with " $G(n,p)$ contains an independent set of size $r$ ". As printed, (9.4) holds for every $u$ whenever $G(n,p)$ almost surely has no independent $r$ -set (both sums are zero), and the conclusion then fails; the proof selects a graph with $N>0$ , which is exactly the added clause.

A formalization in which $\chi(G,m)$ is a real infimum (junk value $0$ on the empty family), in which the Bochner integral replaces probabilities, or in which the coloured set $A$ ranges over all vertices instead of $m$ -subsets would trivialise or change Theorem 9.1; these are ruled out by the definitions above.

Theorem 4.1.1 (the convex-hull inequality) and Lemma 4.1.2 are posed in their own mission and are not repeated here; a complete development needs them on the finite product $\Omega'$ , the identity in law between the edge and vertex-exposure models, and monotonicity and subadditivity of chromatic numbers of induced subgraphs. The vertex-exposure model and the independent-set counts are reusable for other random-graph functionals. Proofs of any milestone, and of the law identity between the two models, 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
E. Shamir, J. Spencer, Sharp concentration of the chromatic number on random graphs $G_{n,p}$ , Combinatorica 7 (1987), 121–129. https://doi.org/10.1007/BF02579208
B. Bollobás, The chromatic number of random graphs, Combinatorica 8 (1988), 49–55. https://doi.org/10.1007/BF02122551
S. Janson, Poisson approximation for large deviations, Random Structures & Algorithms 1 (1990), 221–229. https://doi.org/10.1002/rsa.3240010209
N. Alon, J. Spencer, The Probabilistic Method, Wiley, 1992 ([A-S] in the paper). https://doi.org/10.1002/0471722154

5 thms2 active usersReviewed

Analysis Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces V: The Convex Hull Distance — ∫ exp f_α(A,x) dP ≤ P(A)^{−α}Textbook

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.2.4

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

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

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

Milestones

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

Significance

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

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

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

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

Difficulty

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

Formalization scope

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

Selected references

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

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 1: The State Probabilities of an Aperiodic Equilibrium Process Converge to (1/μ₁)∫φ_A(v){1 − F(v)}dvResearch Paper

Motivation

Many stochastic systems studied in operations research "start afresh" at certain random instants: a single-server queue each time a customer arrives to find the server idle, an inventory system each time stock is replenished to its order level, a reliability system each time a failed unit is replaced. Between such instants the system may evolve in a complicated way, but its future after one of them does not depend on its past. W. L. Smith's 1955 paper Regenerative stochastic processes made this idea into a general theory. Its first main result, Theorem 2, says that the state probabilities of such a process converge as time grows, and gives the limit explicitly in terms of the behaviour of the process within one cycle and the law of the cycle length.

This limit theorem is the standard way of proving that a queue, an inventory or a reliability model has a limiting distribution and of computing it: one exhibits regeneration points and evaluates one cycle.

Timeline.

1948: Blackwell proves that the renewal function of a non-lattice renewal process has increments $H(t+h) - H(t) \to h/\mu_1$ (Duke Math. J. 15).
1949: Erdős, Feller and Pollard prove the discrete (lattice) renewal theorem.
1954: Smith proves the key renewal theorem for bounded, non-increasing, integrable kernels, and a version for kernels tending to zero when some convolution power of the cycle law has an absolutely continuous part (Proc. Roy. Soc. Edinburgh A 64).
1955: Smith introduces regenerative and equilibrium processes and proves Theorem 2 (this paper).

Setting

A general renewal process is a sequence $t_0, t_1, t_2, \dots$ of independent non-negative random variables in which $t_1, t_2, \dots$ have a common law $F$ , not concentrated at $0$ , with mean $\mu_1 = \int x\,dF(x) \in (0,\infty]$ , and the delay $t_0$ has a law $K$ . The regeneration epochs are $T_k = t_0 + \dots + t_k$ , and $n_t$ is the number of epochs in $[0,t]$ . The renewal measure is

H_K = \sum_{n \ge 0} K * F^{*n},

so that $H_K([0,t]) = \mathbb E\, n_t$ . The law $F$ is periodic with period $\varpi > 0$ if all its mass sits on $\{0, \varpi, 2\varpi, \dots\}$ ; otherwise $\varpi = 0$ and $F$ is aperiodic. $F$ belongs to the class $\mathfrak S$ if some convolution power $F^{*k}$ , $k \ge 1$ , has a non-zero absolutely continuous component.

An equilibrium process $\mathcal E(\mathfrak z, \mathcal A, \{t_i\})$ consists of a process $x_t$ on a measurable state space $\mathfrak X$ , a class $\mathcal A$ of measurable sets of states, a family of probability measures $P\{\cdot \mid z\}$ indexed by boundary conditions $z \in \mathfrak z$ , and under each of them a general renewal process whose cycle law $F$ does not depend on $z$ and whose delay has law $K_z$ . For each $A \in \mathcal A$ there is a measurable function $\varphi_A$ , depending on $A$ only, such that

P\{x_t \in A \mid z;\ n_t > 0;\ L_t\} = \varphi_A(t - L_t),

where $L_t$ is the epoch of the last regeneration at or before $t$ . In words: once a regeneration has occurred, the chance of being in $A$ at time $t$ depends only on the time elapsed since the last one.

Formalization targets

Goal: Theorem 2

If the process is aperiodic ( $\varpi = 0$ ) and the regeneration event is certain ( $K_z(+\infty) = 1$ ), then for every $z$ and every $A \in \mathcal A$ satisfying one of the regularity conditions (iv) $'$ ( $\varphi_A\{1-F\}$ integrable and monotonic), (iv) $''_a$ ( $\mu_1 < \infty$ and $\varphi_A\{1-F\}$ of locally bounded variation) or (iv) $''_b$ ( $\mu_1 < \infty$ and $F \in \mathfrak S$ ),

\lim_{t\to\infty} P\{x_t \in A \mid z\} = \frac{1}{\mu_1} \int_0^\infty \varphi_A(v)\{1 - F(v)\}\,dv,

the limit being $0$ when $\mu_1 = \infty$ .

Milestones

Theorem A(a), the key renewal theorem: for bounded, non-increasing, integrable $\Psi$ and aperiodic $F$ , $\int_0^t \Psi(t-t')\,dH_K(t') \to (K(+\infty)/\mu_1)\int_0^\infty \Psi$ .
Lemma A: for $F \in \mathfrak S$ , $(1 - G^*(s))/(1 - F^*(s))$ is the Laplace–Stieltjes transform of a function of bounded variation with net variation $\lambda_1/\mu_1$ .
Theorem 1: the same limit for bounded integrable $\Psi \to 0$ when $F \in \mathfrak S$ and $\mu_1 < \infty$ .
(3·4·3): $P\{x_t \in A \mid z\} = P\{x_t \in A, t_0 > t \mid z\} + \int_0^t \varphi_A(t-\tau)\{1-F(t-\tau)\}\,dH_{K_z}(\tau)$ .
(3·4·5): $\int_{t-\Delta}^t g(t-v)\,dH_K(v) \to \mu_1^{-1}\int_0^\Delta g$ for the page's kernel $g=\varphi_A(1-F)$ of locally bounded variation.
(3·4·7): $\int_0^{t-\Delta}\{1-F(t-v)\}\,dH(v) \to \mu_1^{-1}\int_\Delta^\infty\{1-F\}$ ; the limit is at most $\varepsilon$ for large enough $\Delta$ .

Significance

The result. Theorem 2 reduces the long-run behaviour of a regenerative system to a one-cycle computation: the limiting probability of $A$ is the expected time spent in $A$ during a cycle divided by the expected cycle length. It underlies the existence of limiting distributions for the waiting time in the GI/G/1 queue, the number in system in many queueing networks, inventory levels under $(s,S)$ policies and the availability of repairable systems, and it is the continuous-time counterpart of the ergodic theorem for positive recurrent Markov chains. The paper's later sections apply it to semi-Markov processes.

Formalizing it. The results here are classical and proved; none is machine-checked. Mathlib has measure convolution and the strong law of large numbers but no renewal measure, no Blackwell or key renewal theorem, and no regenerative process. On Prove2Me only the discrete Erdős–Feller–Pollard renewal theorem for renewal sequences is proved. A completed mission supplies the continuous-time key renewal theorem in two forms, a reusable renewal-measure interface, and a general limit theorem for regenerative processes on which queueing and inventory results can be built.

Difficulty

The decomposition (3·4·3) is a direct consequence of independence and the renewal structure. The difficulty is the key renewal theorem. Blackwell's theorem controls $H_K$ on intervals of fixed length; passing from intervals to a general kernel requires the kernel to be directly Riemann integrable, which is why Theorem A asks for monotonicity and Theorem 2 lists three alternative regularity conditions. A merely integrable kernel tending to zero is not enough for a general aperiodic $F$ : $H_K$ may concentrate on a set where the kernel has tall narrow spikes. Theorem 1 removes monotonicity only for $F \in \mathfrak S$ , through a Laplace-transform argument that needs Lemma A, the uniqueness theorem for Laplace transforms and the fact that the singular part of $H_K$ contributes nothing in the limit. Blackwell's theorem itself, for a non-lattice law with possibly infinite mean, is not in any library and is a substantial development of its own.

Formalization scope

Laws are measures on $\mathbb R$ carried by $[0,\infty)$ ; the distribution function is $F(t) = F((-\infty,t])$ and $1 - F(v) = F((v,\infty))$ . The mean $\mu_1$ is an extended non-negative real, so $\mu_1 = \infty$ is a value; every statement with a $1/\mu_1$ treats $\mu_1 = \infty$ and $\mu_1 < \infty$ as separate cases rather than relying on a default value of division. Stieltjes integrals $\int_0^t \cdots dH_K$ are integrals against the renewal measure over the closed interval $[0,t]$ . Aperiodicity is the lattice condition on $F$ , not a density condition. The delay law $K$ in Theorem A and Theorem 1 may have mass below one.

In the equilibrium process the conditional-probability representation is stated as the defining identity of conditional probability for every Borel set of last-regeneration epochs, every $t \ge 0$ , every $z$ and every $A \in \mathcal A$ . The paper writes $T_{n_t}$ for the last regeneration epoch, although under its own indexing that symbol is the first epoch after $t$ ; the formalization uses the last epoch at or before $t$ . The delay $t_0$ is real-valued, so the regeneration event is certain (hypothesis (iii)); improper delays and cycles, which §3 of the paper also allows, are outside this mission.

A trivializing formalization would condition only on $\{n_t > 0\}$ rather than on the epoch of the last regeneration, or fix $\mu_1 < \infty$ globally; both are ruled out, and hypothesis (iv) is imposed separately for the one set $A$ of the conclusion.

Infrastructure needed: Blackwell's renewal theorem (non-lattice, finite or infinite mean), direct Riemann integrability, Laplace–Stieltjes transforms of functions of bounded variation and their uniqueness. All of these are reusable well beyond this paper; contributions of any of them are welcome. The convolution power and the Laplace–Stieltjes transform are taken from the published definition QueueingFundamentals.MG1.transforms.

Selected references

W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232 (1955), 6–31. https://doi.org/10.1098/rspa.1955.0198
W. L. Smith, Asymptotic renewal theorems, Proc. Roy. Soc. Edinburgh A 64 (1954), 9–48. https://doi.org/10.1017/S0080454100007482
D. Blackwell, A renewal theorem, Duke Math. J. 15 (1948), 145–150. https://doi.org/10.1215/S0012-7094-48-01568-3
P. Erdős, W. Feller, H. Pollard, A property of power series with positive coefficients, Bull. Amer. Math. Soc. 55 (1949), 201–204. https://doi.org/10.1090/S0002-9904-1949-09203-0
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Ch. V–VI. https://doi.org/10.1007/b97236

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 3: A Cumulative Process Has Mean (κ₁/μ₁)t + o(t) and Variance (t/μ₁){σ₂² − 2ρσ₁σ₂κ₁/μ₁ + σ₁²(κ₁/μ₁)²} + o(t)Research Paper

Why cumulative-process moments matter

Many stochastic systems accumulate a real-valued quantity while repeatedly returning to a state at which a new cycle begins. A queue may accumulate work or cost, a component may accumulate wear, and a recurrent system may accumulate time in a state. The observations at a fixed clock time usually cut through a cycle. This makes the moments of the observed process different from the moments of a sum stopped exactly at a regeneration epoch. W. L. Smith introduced cumulative processes to state mean, variance, ergodic, and central limit results for this setting in a common language (Smith 1955, §5).

The mean growth rate describes the long-run reward per unit time. The variance growth rate also records the dependence between a cycle's length and its reward. That dependence matters in systems where unusually long cycles tend to accumulate unusually large rewards; assuming the two are independent would erase a term in Smith's formula (Smith 1955, Theorem 8). This mission targets the exact first-order mean and variance asymptotics, along with the source results Smith uses to pass from completed cycles to observations at ordinary times.

Renewal and cumulative-process setting

Work on one probability space $(\Omega,P)$ . The cycle lengths $t_1,t_2,\ldots$ are nonnegative, independent, identically distributed random variables whose common law is not concentrated at zero. Set $T_0=0$ and $T_n=t_1+\cdots+t_n$ for $n\geq1$ . Thus $T_n$ is the $n$ th renewal epoch after the initial renewal at time zero. For $t\geq0$ , $n_t$ counts the epochs $T_k\leq t$ , including $T_0$ . The corresponding renewal function is $H_U(t)=\mathbb E[n_t]$ , where $U=\delta_0$ is Smith's zero-delay law. These conventions come from §2·1 and §5·2 of the paper (Smith 1955, pp. 9 and 23).

A cumulative process $w_t$ is real valued, starts at $w_0=0$ , and has almost surely bounded variation on each finite nonnegative time interval. The cycle reward is $y_n=w_{T_n}-w_{T_{n-1}}$ . Write $\tilde w_t$ for the total variation of the path on $[0,t]$ and $\tilde y_n$ for its variation on $[T_{n-1},T_n]$ . For the moment results, the cycle vectors $(t_n,y_n,\tilde y_n)$ are independent and identically distributed across $n$ . Their coordinates within one cycle may be dependent. This joint-cycle interpretation is required by Smith's common joint distribution for $(t_i,y_i)$ in the proof of Lemma 5 (Smith 1955, pp. 23–24).

Let $\mu_r=\mathbb E[t_1^r]$ , $\kappa_r=\mathbb E[y_1^r]$ , and $\tilde\kappa_r=\mathbb E[\tilde y_1^r]$ when the moments exist. Put $\sigma_1^2=\operatorname{var}(t_1)$ , $\sigma_2^2=\operatorname{var}(y_1)$ , and $c=\operatorname{cov}(t_1,y_1)$ . Smith writes $c=\rho\sigma_1\sigma_2$ , with $\rho$ the cycle length–reward correlation. The covariance remains defined when either variance is zero. The auxiliary sum $Y_t=\sum_{i=1}^{n_t+1}y_i$ includes a reward beyond the cycles completed by time $t$ , exactly as in (5·2·1) (Smith 1955, p. 23).

Formalization targets

The first target is the mean part of Theorem 8. If $\mu_1$ and $\tilde\kappa_1$ are finite, then

\mathbb E w_t=\frac{\kappa_1}{\mu_1}t+o(t)\qquad(t\to\infty).

The goal includes the variance part under the additional assumptions $\mu_2<\infty$ and $\tilde\kappa_2<\infty$ :

\operatorname{var}(w_t)=\frac{t}{\mu_1} \left\{\sigma_2^2-2c\frac{\kappa_1}{\mu_1} +\sigma_1^2\left(\frac{\kappa_1}{\mu_1}\right)^2\right\}+o(t).

Both limits are along real time, and neither assumes that a cycle's length and reward are independent. The milestone list contains the mean and variance limits for $Y_t$ , the cycle-moment estimate used for the incomplete cycle, and Theorem 8(i) as the explicit mean target (Smith 1955, Lemmas 4, 5, 9 and Theorem 8).

What the result supplies

The theorem gives a linear approximation to the process's expected value and variance, with errors smaller than the observation horizon. The leading variance coefficient separates reward variability, cycle-length variability, and their covariance. It can therefore be used without a false independence assumption when the duration of a cycle affects the amount accumulated during it. The formulas are first-order statements; they do not claim a bounded error or a limiting distribution (Smith 1955, (5·3·6)–(5·3·7)).

Formalizing these statements requires reusable definitions of renewal counts, path variation, random-cycle rewards, and the moment conditions that make expectations and variances genuine. The statement is a draft target, not a claim that Smith's proof already has a machine-checked reconstruction. A completed development would also give formal tools for other regenerative reward models whose observations occur between renewal epochs.

Main mathematical difficulty

The auxiliary sum $Y_t$ is sampled at a random index, while $w_t$ is observed at a deterministic clock time. They differ by part of a cycle that crosses $t$ . Ordinary laws for sums of a fixed number of independent rewards do not directly control either this random index or the crossing-cycle contribution. At second order, a bound on the mean difference alone does not determine the variance difference. The length–reward covariance must also survive the passage from completed cycles to the continuous-time process (Smith 1955, pp. 24–28).

Formalization scope and conventions

Lean uses real time and real-valued paths. Cycle laws are represented by random variables on one probability space; the renewal at zero is explicit. The renewal count takes the value zero on a path with infinitely many renewals before a finite time, a null event under the nondegenerate i.i.d. length law. Variation is represented by Mathlib's extended nonnegative eVariationOn and converted to a real number only under the almost-sure bounded-variation condition. The theorem states integrability of $w_t$ and its square as consequences of the cycle-moment assumptions, avoiding default values for divergent real integrals or variance. A finite $r$ th moment is an integrability condition, not a comparison between a real number and infinity.

The paper's exact identity (5·2·2) is off by one under its own definitions of $n_t$ and $Y_t$ ; the mission targets its valid asymptotic consequence (5·2·3). The last variance in the printed Lemma 5 coefficient is $\sigma_2^2$ , while Theorem 8 and the calculation require $\sigma_1^2$ . Milestone provenance retains the printed text; the Lean statements use the corrected coefficient. Lemma 9 is formalized for the absolute $p$ th moment $\mathbb E|y_1|^p$ of the cycle increment, which is the printed statement for a nonnegative cycle quantity such as the variation $\tilde y_n$ to which Theorem 8 applies it. Solvers may contribute the renewal and random-index estimates needed for the listed targets. A definition that makes rewards independent of cycle lengths would remove the covariance term and would not represent this mission's model.

Selected references

W. L. Smith, Regenerative stochastic processes, Proceedings of the Royal Society of London, Series A 232(1188):6–31, 1955. DOI: 10.1098/rspa.1955.0198.

7 thms2 active usersReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Edge-Disjoint Spanning Trees of Finite Graphs: A Finite Multigraph Has k Edge-Disjoint Spanning Trees iff Every Partition P of Its Vertices Is Crossed by at Least k(|P| − 1) EdgesResearch Paper

Why edge-disjoint spanning trees

A connected network survives the failure of any single link exactly when it has no bridge, but a stronger and more useful property is to carry several edge-disjoint spanning trees: each tree can broadcast to every node on its own, so $k$ such trees give $k$ independent routing or broadcast structures, and the network stays connected after any $k-1$ link failures. The question of when a graph contains $k$ edge-disjoint spanning trees was answered in 1961, simultaneously and independently, by W. T. Tutte (On the problem of decomposing a graph into n connected factors) and C. St.J. A. Nash-Williams (Edge-disjoint spanning trees of finite graphs). The answer is a min-max condition over vertex partitions, now called the Tutte–Nash-Williams tree-packing theorem. It is a standard result in combinatorial optimization and the graphic case of Edmonds's matroid base-packing theorem (1965).

Timeline:

1961. Tutte proves the theorem in an equivalent form; Nash-Williams, unaware of Tutte's work, gives a different proof a few months later, the one formalized here.
1964. Nash-Williams proves the companion covering theorem: the edges can be covered by $k$ forests iff every vertex set $U$ spans at most $k(|U|-1)$ edges.
1965. Edmonds derives both results from matroid partition (Minimum partition of a matroid into independent subsets).

Setting

A graph $G$ here is a finite unoriented multigraph in which every edge joins two distinct vertices; two vertices may be joined by several edges. Write $V$ for its vertex set and $E$ for its edge set. A tree on a non-empty vertex set $W$ is an edge set $T$ , all of whose edges have both ends in $W$ , containing no cycle (two parallel edges count as a cycle), such that any two vertices of $W$ are joined by a path of $T$ -edges. A spanning tree of $G$ is a tree on all of $V$ using edges of $G$ . Spanning trees are edge-disjoint if no two share an edge.

A partition $P$ of $V$ is a set of non-empty, pairwise disjoint subsets of $V$ whose union is $V$ ; $|P|$ is the number of its members. The crossing edges $E_P(G)$ are the edges whose two ends lie in different members of $P$ , counted with multiplicity. Throughout, $k$ is a fixed positive integer. For $X \subseteq V$ , $E_X$ is the set of edges with both ends in $X$ , $e_X = |E_X|$ , and

\Delta_G(X) = k(|X|-1) - e_X .

Formalization targets

Goal: Theorem 1

G \text{ has } k \text{ edge-disjoint spanning trees} \iff |E_P(G)| \ge k(|P|-1) \text{ for every partition } P \text{ of } V. \tag{1}

Milestones, in the order of the proof

Lemma 1: a tree on $W$ has $|W|-1$ edges. Lemma 2: every connected graph has a spanning tree.
Necessity: $k$ edge-disjoint spanning trees imply (1) for every $P$ .
(*) On couples $[G,g]$ ( $g \ge 0$ on vertices, $\Delta_G \ge 0$ on non-empty sets): critical sets ( $\Delta_G = 0$ ) whose intersection is non-empty are closed under $\cap$ and $\cup$ . The same holds for crucial sets ( $\Gamma = 0$ , where $\Gamma(X) = \Delta_G(X) - s + g\,.\,\bar X$ ) when the couple is $s$ -good.
Lemma 3: for $s \ge 1$ , an $s$ -good couple has an $(s-1)$ -good supercouple with one added edge. Corollary 3A: an $s$ -good couple has an $s$ -supercouple, obtained by adding $s$ edges.
(†) and Lemma 4: a spanning tree of a graph produced by fusions at $\xi$ (replacing edges $\xi\eta$ , $\xi\zeta$ by a new edge $\eta\zeta$ ) pulls back to a spanning tree of the original graph.
Lemma 5: a graph with $|E| = k(|V|-1)$ satisfies (1) iff $\Delta_G(X) \ge 0$ for every non-empty $X$ .
Lemma 6: under the inductive hypothesis of the proof, a critical partition other than $\{V\}$ and the partition into singletons yields $k$ edge-disjoint spanning trees.

Significance

The theorem gives an exact, checkable certificate in both directions: a family of $k$ trees certifies the packing, and a single partition violating (1) certifies that no packing exists. Corollaries include that every $2k$ -edge-connected graph has $k$ edge-disjoint spanning trees, and that the maximum number of edge-disjoint spanning trees (the strength-type parameter used in network reliability and in Nagamochi–Ibaraki style connectivity algorithms) is the minimum of $\lfloor |E_P(G)|/(|P|-1) \rfloor$ over partitions with $|P| \ge 2$ . The partition condition is also the prototype of the rank condition in matroid base packing.

The result itself is classical and fully proved. What this mission adds is a machine-checked version in a multigraph setting. Mathlib has trees and spanning trees for simple graphs (SimpleGraph.IsTree, SimpleGraph.Connected.exists_isTree_le), but not edge-disjoint tree packing, and its simple graphs cannot express the parallel edges that the theorem and its proof need. Related items on the platform include the multigraph layer NagamochiIbaraki.EdgeConn.Multigraph (reused here), the Keller–Trotter spanning-forest count for simple graphs, and Edmonds's matroid partition theorem with Nash-Williams's covering corollary. Covering and packing are different statements, so none of these yields Theorem 1 directly. Formalizing Tutte's alternative proof, or deriving Theorem 1 from a formalized matroid union theorem, would also be welcome.

Difficulty

Necessity is a counting argument. The difficulty lies in sufficiency. The obvious induction deletes an edge or contracts a set of vertices, but deleting an edge can destroy (1), and contracting changes the vertex set, so neither reduction preserves the hypothesis on its own. The hardest case is a graph in which only the partition into singletons is critical. There a vertex of degree less than $2k$ has to be removed while (1) is preserved on the remaining graph, and the trees found there have to be converted back into trees of the original graph. Both steps need careful bookkeeping of edges incident with that vertex. A simple-graph development cannot carry the argument, because the edges that the reduction adds among the neighbours of the removed vertex may be parallel to existing ones.

Formalization scope

Graphs. A vertex type V, an edge type E (both finite, in Type), and ends : E → Sym2 V, the published encoding of NagamochiIbaraki.EdgeConn. Loops are excluded by the hypothesis ∀ e, ¬ (ends e).IsDiag. Parallel edges are allowed, and simplicity is never assumed. A subgraph is a pair (W : Finset V, F : Finset E).
Trees. "Tree" means non-empty vertex set, edges inside it, no cycle (IsForest: every edge is a bridge) and connected. $|T| = |W|-1$ is Lemma 1, not part of the definition. " $k$ edge-disjoint spanning trees" is a family Fin k → Finset E of pairwise disjoint spanning trees.
Partitions are Mathlib Finpartition (Finset.univ : Finset V). (1) is required for every partition, including the one-part partition and the singletons. All counts involving subtraction ( $\Delta_G$ , (1), criticality, $\Gamma$ ) are in $\mathbb Z$ .
Explicit readings. $V$ is non-empty in Theorem 1, since the paper's graphs have a vertex and on $V = \emptyset$ condition (1) holds while no tree exists. $k \ge 1$ in every statement. The paper's " $X \subset V(G)$ " includes $X = V(G)$ and is read as $\subseteq$ . "Exactly $g(\xi)-h(\xi)$ new edges" is written $\deg_{\text{new}}(\xi) + h(\xi) = g(\xi)$ , without natural-number subtraction. A supergraph with $s$ added edges has edge type E ⊕ Fin s, so the added edges always exist; none of them may be a loop. A fusion uses a given fresh edge ρ : E in an ambient edge type, and a sequence of fusions is a list, each valid on the graph produced by the later ones ( $L = \Phi_1\cdots\Phi_n G$ applies $\Phi_n$ first). In (†) and Lemma 4, "is a tree" means "is a spanning tree of $G$ ", since the vertex set is all of $V$ . Lemma 6 carries the paper's inductive hypothesis as an explicit hypothesis: Theorem 1 (admissible implies $k$ trees) for all loopless multigraphs with smaller $|V|+|E|$ .
Ruled out. Defining a spanning tree by an edge count alone, or by acyclicity alone, would make Lemma 1 or the goal trivial; the definitions require both acyclicity and connectivity on the stated vertex set. Taking added edges from a fixed ambient type would make Lemma 3 false. Dropping or globalizing Lemma 6's inductive hypothesis would turn it into the goal or a tautology.
Infrastructure. Multigraph trees, the tree edge count and spanning-tree existence, contraction $G_P$ of a partition, and splitting-off at a vertex. All of these are reusable beyond this mission. Contributions of general multigraph lemmas are welcome.

Selected references

C. St.J. A. Nash-Williams, Edge-disjoint spanning trees of finite graphs, J. London Math. Soc. 36 (1961), 445–450. https://doi.org/10.1112/jlms/s1-36.1.445
W. T. Tutte, On the problem of decomposing a graph into n connected factors, J. London Math. Soc. 36 (1961), 221–230. https://doi.org/10.1112/jlms/s1-36.1.221
C. St.J. A. Nash-Williams, Decomposition of finite graphs into forests, J. London Math. Soc. 39 (1964), 12. https://doi.org/10.1112/jlms/s1-39.1.12
J. Edmonds, Minimum partition of a matroid into independent subsets, J. Res. Nat. Bur. Standards 69B (1965), 67–72. https://doi.org/10.6028/jres.069B.004
C. Berge, Théorie des graphes et ses applications, Dunod, Paris, 1958.

15 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Random Walks in a Random Environment 1: Transience to +∞, to −∞, or Recurrence According to Σ n⁻¹P(ρ_n > 1) < ∞, Σ n⁻¹P(ρ_n < 1) < ∞, or Both Infinite (E ln σ < 0, > 0, = 0)Research Paper

Motivation

A random walk on the integers in which the probability of stepping right depends on the current site is the simplest model of motion through a disordered medium: a particle diffusing in a crystal with impurities, a molecule moving along a heterogeneous polymer, or a gene frequency drifting under fluctuating selection. When the site-dependent probabilities are themselves drawn at random, the result is a random walk in a random environment (RWRE). Fred Solomon's 1975 paper [Solomon 1975] gave the first rigorous analysis of this model on $\mathbb Z$ with independent, identically distributed site probabilities, and its recurrence criterion opened the subject now surveyed in [Zeitouni 2004].

Timeline. Chung [Chung 1960, pp. 65–71] gave the hitting probabilities and the recurrence/transience criterion for a nearest-neighbour chain on $\mathbb Z$ with fixed, site-dependent transition probabilities. Fluctuation theory, as presented in Chung's A Course in Probability Theory [Chung 1968, Ch. 8], characterises when a sum of i.i.d. random variables drifts to $-\infty$ , to $+\infty$ , or oscillates, through the series $\sum\frac1nP(S_n>0)$ and $\sum\frac1nP(S_n<0)$ . Solomon (1975) combined the two to classify the RWRE on $\mathbb Z$ , and also computed its speed and exhibited sub-ballistic and non-Gaussian behaviour. Kesten, Kozlov and Spitzer (1975) [KKS 1975] identified stable limit laws in the transient sub-ballistic regime, and Sinai (1982) [Sinai 1982] found the $(\log n)^2$ scaling of the recurrent case.

Setting

Let $\alpha=(\alpha_n)_{n\in\mathbb Z}$ be independent, identically distributed random variables with values in $[0,1]$ . Given a fixed sequence $a=(a_n)$ in $[0,1]$ (an environment), the chain $M_a$ on $\mathbb Z$ jumps from $n$ to $n+1$ with probability $a_n$ and to $n-1$ with probability $\beta_n=1-a_n$ . The random walk in a random environment $(X_n)_{n\ge0}$ is the process obtained by first drawing $\alpha$ and then running $M_\alpha$ from $X_0=0$ ; jointly,

P(\alpha\in A,\ X_0=x_0,\dots,X_n=x_n)=\int_{\{\alpha\in A\}}\mathbf 1\{x_0=0\}\prod_{k<n}M_\alpha(x_k,x_{k+1})\,dP .

The walk is a Markov chain given the environment, but not after averaging over it. Define

\sigma_n=\frac{\beta_n}{\alpha_n}\in[0,\infty],\qquad \rho_n=\sigma_1\cdots\sigma_n\ (n\ge1),\qquad \rho_{-n}=\sigma_{-1}\cdots\sigma_{-n}\ (n\ge1),

and, for a fixed environment, the hitting probability $f_{ij}=P(X_n=j\text{ for some }n>0\mid X_0=i)$ . The quantity $E(\ln\sigma)$ is defined when the expectation of the positive or of the negative part of $\ln\sigma\in[-\infty,\infty]$ is finite.

Formalization targets

Goal: Theorem (1.7)

Assume $\alpha_0$ is not almost surely constant and either $0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$ . Then

\sum_{n\ge1}\tfrac1nP(\rho_n>1)<\infty\Rightarrow X_n\to+\infty,\qquad \sum_{n\ge1}\tfrac1nP(\rho_n<1)<\infty\Rightarrow X_n\to-\infty,

and if both series diverge, $-\infty=\liminf X_n<\limsup X_n=+\infty$ , all almost surely. When $E(\ln\sigma)$ is defined, the three cases are exactly $E(\ln\sigma)<0$ , $>0$ , $=0$ .

Milestones

Theorem (0.1): almost-sure properties of the walk in almost every fixed environment transfer to the RWRE. Lemma (1.1)(i)–(ii): the hitting probabilities $f_{ij}$ in a fixed environment with $0<a_n<1$ , as ratios of series in $\sigma$ . Lemma (1.5): in a fixed environment, $\sum(\rho_{-n})^{-1}$ and $\sum\rho_n$ decide transience to $+\infty$ , to $-\infty$ , or recurrence. Lemma (1.6): fluctuation theory for i.i.d. sums, including the summability of $e^{S_n}$ . Two claims from the proof of (1.7) (p. 5): the boundary cases where $\alpha_n$ equals $1$ or $0$ with positive probability, and the equivalence $E(\ln\sigma)<0\iff S_n\to-\infty\iff\sum\frac1nP(\rho_n>1)<\infty$ for $S_n=\ln\sigma_1+\dots+\ln\sigma_n$ . A companion item asserts that the RWRE exists for every law of $\alpha_0$ on $[0,1]$ .

Significance

The theorem classifies the long-run behaviour of the RWRE on $\mathbb Z$ by a condition on the law of a single site variable, with no moment assumption. It shows that the averaged drift $E\alpha_0-E\beta_0$ is not the right quantity: a walk can be recurrent or transient to the left while its average step is positive, because the criterion involves $E\ln\sigma$ , a geometric rather than arithmetic mean. The criterion is the starting point for the speed law (Theorem (1.16) of the same paper), for the limit laws of Kesten–Kozlov–Spitzer and Sinai, and for the large-deviation theory of RWRE.

Solomon's results are proved; none of them, nor the fixed-environment criterion of Chung, is formalized in Lean. This mission produces machine-checked statements of the full trichotomy including the boundary cases $\sigma\in\{0,\infty\}$ , of the classical hitting-probability formulas for birth–death chains on $\mathbb Z$ , and of the fluctuation-theory criterion with infinite-valued expectations allowed.

Difficulty

The naive approach applies the law of large numbers to $X_n$ ; it fails because the increments $X_{j}-X_{j-1}$ are neither independent nor stationary once the environment is averaged out. The argument must instead pass through a fixed environment, where the criterion of Lemma (1.5) involves the full random series $\sum\rho_n$ and $\sum\rho_{-n}^{-1}$ , and then decide when these series converge almost surely. That step requires fluctuation theory for $\ln\rho_n=\sum_{k\le n}\ln\sigma_k$ , a random walk whose steps may be infinite and may have no mean. In Lean, the main missing infrastructure is the fluctuation-theory criterion $\sum\frac1nP(S_n>0)<\infty\iff S_n\to-\infty$ , which Mathlib does not have, and the transfer from quenched to annealed statements for a process defined only through its cylinder laws.

Formalization scope

Everything lives in the namespace SolomonRWRE.Recurrence. The fixed-environment chain is IsChainInEnv P a i X, specified by its cylinder probabilities. The RWRE is IsRWRE P α X on an arbitrary probability space: measurable $\alpha_n$ with values in $[0,1]$ at every outcome, iIndepFun α P, identically distributed, and the joint cylinder law above. $\sigma_n$ , $\rho_n$ , $f_{ij}$ and all series are in $[0,\infty]$ (ℝ≥0∞), so " $<\infty$ " and " $=\infty$ " are literal; series over $n\ge1$ are indexed by $n+1$ in Lean. $\ln\sigma$ and $S_n$ are extended reals, $E(\ln\sigma)$ is the difference of two lower Lebesgue integrals, and "defined" means one of them is finite. Recurrence is always stated in the paper's "in fact" form: $\liminf X_n=-\infty$ and $\limsup X_n=+\infty$ . "Correspond respectively" is formalized as three equivalences between the series conditions and the sign conditions.

Two trivializing formalizations are ruled out. Without nondegeneracy ( $\alpha\equiv\frac12$ ) both series vanish and (i), (ii) would contradict each other; the hypothesis is part of every statement that needs it. A cylinder law that cannot be met would make every theorem vacuous; a sorry-free check confirms that the environment $\alpha\equiv1$ with $X_n=n$ satisfies IsRWRE, and the companion item asserts existence for every law of $\alpha_0$ . The page's alternative " $0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$ " is kept, since a single range $[0,1]$ would let $0\cdot\infty=0$ change $\rho_n$ .

Needed infrastructure: hitting probabilities of birth–death chains (reusable for any nearest-neighbour chain), the fluctuation-theory criterion for i.i.d. sums with extended values (reusable throughout applied probability), and a quenched-to-annealed transfer lemma. Contributions to any of these are welcome.

Selected references

F. Solomon, Random walks in a random environment, The Annals of Probability 3(1):1–31, 1975. https://doi.org/10.1214/aop/1176996444
K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, Berlin, 1960 (pp. 65–71; reference [1] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
K. L. Chung, A Course in Probability Theory, Harcourt, Brace and World, New York, 1968 (Ch. 8; reference [2] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
H. Kesten, M. V. Kozlov, F. Spitzer, A limit law for random walk in a random environment, Compositio Mathematica 30(2):145–168, 1975. http://www.numdam.org/item/CM_1975__30_2_145_0/
Ya. G. Sinai, The limiting behavior of a one-dimensional random walk in a random medium, Theory of Probability and its Applications 27(2):256–268, 1982. https://doi.org/10.1137/1127028
O. Zeitouni, Random walks in random environment, Lectures on Probability Theory and Statistics (Saint-Flour 2001), Lecture Notes in Mathematics 1837, Springer, 2004. https://doi.org/10.1007/978-3-540-39874-5_2

9 thms2 active usersReviewed