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.

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.

NoneFormalized record≥ 0.00003666565558019Open frontier

3 provers on it0 of 4 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.999074Formalized record

3 provers on it4 of 4 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.103205334138Formalized record≤ 2Open frontier

9 provers on it7 of 8 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.

≤ 70Formalized record

3 provers on it8 of 8 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

35 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)

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.

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).

NoneFormalized record≥ 0.00003666565558019Open frontier

3 provers on it0 of 4 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.999074Formalized record

3 provers on it4 of 4 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.103205334138Formalized record≤ 2Open frontier

9 provers on it7 of 8 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.

≤ 70Formalized record

3 provers on it8 of 8 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

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems II: High-Probability and Expected Regret of Exp3.PTextbook

Motivation

In the adversarial (non-stochastic) multi-armed bandit problem a forecaster repeatedly chooses one of $K$ actions while an opponent sets the rewards, and only the reward of the chosen action is revealed. The model was proposed as a way of playing an unknown repeated game: Baños (1968) studied the repeated game in which the player observes only its own payoff, which is exactly the bandit problem against an opponent who reacts to the player's past moves. It is the basic model of online decision making under partial feedback without statistical assumptions, and it underlies regret minimization in games, adversarial routing and online advertising. Chapter 3 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) collects its fundamental results: the Exp3 forecaster of Auer, Cesa-Bianchi, Freund and Schapire (SIAM J. Comput. 2002), its high-probability variant Exp3.P, and the $\sqrt{nK}$ minimax lower bound.

Setting

There are $K \ge 2$ arms and rounds $t = 1, 2, \dots, n$ . At each round an adversary assigns a gain $g_{i,t} \in [0,1]$ to every arm $i$ ; the forecaster picks an arm $I_t$ , possibly at random, and observes only $g_{I_t,t}$ . The adversary may be non-oblivious (adaptive): $g_{i,t} = g_{i,t}(I_1,\dots,I_{t-1})$ may depend on the forecaster's past actions. A forecaster rule maps the past actions to a probability vector $p_t$ on the arms, and a run is a sequence of random arms with $I_t \sim p_t$ given the past. The regret is the random variable

R_n = \max_{i=1,\dots,K}\sum_{t=1}^n g_{i,t} - \sum_{t=1}^n g_{I_t,t},

and, in the loss version $\ell_{i,t} \in [0,1]$ , the pseudo-regret is $\overline R_n = \mathbb E\sum_t \ell_{I_t,t} - \min_i \mathbb E\sum_t \ell_{i,t}$ . Since the maximum sits inside the expectation, $\overline R_n \le \mathbb E R_n$ in the gain version, and against an adaptive adversary the two can differ.

Exp3 draws $I_t$ from exponential weights $p_{i,t+1} \propto \exp(-\eta_t \tilde L_{i,t})$ of importance-weighted cumulative loss estimates $\tilde L_{i,t} = \sum_{s \le t} \ell_{i,s}\mathbb 1_{I_s = i}/p_{i,s}$ . Exp3.P uses biased gain estimates $\tilde g_{i,t} = (g_{i,t}\mathbb 1_{I_t=i} + \beta)/p_{i,t}$ and mixes in the uniform distribution:

p_{i,t+1} = (1-\gamma)\frac{\exp(\eta\tilde G_{i,t})}{\sum_k \exp(\eta \tilde G_{k,t})} + \frac{\gamma}{K}, \qquad \tilde G_{i,t} = \sum_{s=1}^t \tilde g_{i,s}.

Formalization targets

Goal: Theorem 3.3 (expected regret of Exp3.P)

With $\beta = \sqrt{\ln K/(nK)}$ , $\eta = 0.95\sqrt{\ln K/(nK)}$ , $\gamma = 1.05\sqrt{K\ln K/n}$ , against every adaptive adversary,

\mathbb E R_n \le 5.15\sqrt{nK\ln K} + \sqrt{\frac{nK}{\ln K}}.

Milestones

Lemma 3.1: for $\beta \in (0,1]$ and a fixed arm $i$ , with probability at least $1-\delta$ , $\sum_t g_{i,t} \le \sum_t \tilde g_{i,t} + \ln(\delta^{-1})/\beta$ .
Eq. (3.12): if $\gamma \le 1/2$ and $(1+\beta)K\eta \le \gamma$ , then with probability at least $1-\delta$ ,

R_n \le \beta nK + \gamma n + (1+\beta)\eta Kn + \frac{\ln(K\delta^{-1})}{\beta} + \frac{\ln K}{\eta}.

Theorem 3.2: with $\beta = \sqrt{\ln(K\delta^{-1})/(nK)}$ , $R_n \le 5.15\sqrt{nK\ln(K\delta^{-1})}$ (3.10); with $\beta = \sqrt{\ln K/(nK)}$ , $R_n \le \sqrt{nK/\ln K}\,\ln(\delta^{-1}) + 5.15\sqrt{nK\ln K}$ (3.11), each with probability at least $1-\delta$ .
Theorem 3.1: Exp3 with $\eta = \sqrt{2\ln K/(nK)}$ has $\overline R_n \le \sqrt{2nK\ln K}$ (3.2); with $\eta_t = \sqrt{\ln K/(tK)}$ , $\overline R_n \le 2\sqrt{nK\ln K}$ (3.3).
Lemma 3.2 and Theorem 3.4: for $n \ge K \ge 2$ and every forecaster there is a Bernoulli instance with $\max_i \mathbb E\sum_t Y_{i,t} - \mathbb E\sum_t Y_{I_t,t} \ge \sqrt{nK}/20$ .

Significance

The goal bounds the expected regret, not the pseudo-regret, against an opponent that adapts to the forecaster's randomized past choices. A pseudo-regret bound says nothing about $\mathbb E R_n$ in that setting, and the book obtains the expected-regret bound by first proving a high-probability bound valid at every confidence level, (3.11), and integrating its tail. Together with Theorem 3.4 the chapter shows that $\sqrt{nK}$ is the minimax rate of adversarial bandits up to a $\sqrt{\ln K}$ factor. Lemma 3.1, the concentration of biased importance-weighted estimates, holds for any forecaster rule and is the step that turns exponential weights into a high-probability guarantee.

All results are proved in the book. On the formal side, the platform has the pseudo-regret bound of Exp3 against an oblivious adversary (a fixed reward table, Bandit Algorithms V) and an Exp3-IX high-probability bound; it has no Exp3.P, no regret bound against adaptive adversaries and no Bernoulli $\sqrt{nK}/20$ lower bound. This mission adds an explicit model of adaptive adversaries and randomized forecaster runs, and the chapter's statements with the book's exact constants.

Difficulty

Against an adaptive adversary the gains are random and depend on the forecaster's own past draws, so the argument used for a fixed reward table (take expectations of an inequality that holds for every fixed sequence) does not control $\mathbb E R_n$ : the maximum over arms does not commute with the expectation. Unbiased estimates do not help either, because the variance of $\ell_{i,t}/p_{i,t}$ is of order $1/p_{i,t}$ , which can be arbitrarily large; even with uniform mixing at rate $n^{-1/2}$ the cumulative variance is of order $n^{3/2}$ . The bias $\beta$ and the mixing $\gamma$ have to be tuned jointly so that the estimate concentrates while the exponential-weights analysis survives, and the constants $0.95$ , $1.05$ and $5.15$ come out of that tuning. The lower bound needs an information-theoretic comparison of a forecaster's behaviour on $K+1$ Bernoulli instances, against forecasters that may be randomized.

Formalization scope

Arms are Fin K with $K \ge 2$ ; rounds are numbered $1,\dots,n$ ; logarithms are natural. Action sequences are functions $\mathbb N \to$ Fin K whose entry $0$ is ignored. An adversary is a structure holding values in $[0,1]$ that may depend on the past actions only (gains for Exp3.P, losses for Exp3); a randomized adversary with independent external randomness reduces to this case by conditioning. A run of a forecaster rule $p$ on a probability space is pinned down by the cylinder identity $\mathbb P(I_1 = h_1,\dots,I_t = h_t) = \mathbb P(I_1=h_1,\dots,I_{t-1}=h_{t-1})\,p_t(h)(h_t)$ , which determines the law of $(I_1,\dots,I_n)$ . "With probability at least $1-\delta$ " is $\mathbb P(\text{event}) \ge 1-\delta$ for $\delta \in (0,1)$ , and $\mathbb E R_n$ is the Bochner integral of the bounded, measurable regret. The lower bounds use a stochastic model in which the forecaster sees past actions and the rewards of the played arms, and rewards are i.i.d. product Bernoulli.

Constants and conventions:

Every constant is the book's exact one: $0.95$ , $1.05$ , $5.15$ , $1/20$ . No $O(\cdot)$ is involved.
Exp3.P with $1.05\sqrt{K\ln K/n} > 1$ is outside the box's range $\gamma \in [0,1]$ ; its vector can then have negative entries, and if it does on a history of positive probability no run exists. This happens only when $n < 1.11\,K\ln K$ , where the printed bounds already follow from $R_n \le n$ , so the statements are true there whether or not a run exists.
Corrected misprints: the Exp3 box's $\tilde\ell_{i,s}$ is $\tilde\ell_{i,t}$ ; the sign in (3.16) is the box's $\exp(+\eta\tilde G)$ ; the proof of (3.10) says the bound is trivial "if $n \ge 5.15\sqrt{\cdots}$ ", which should be $n \le$ . The statements carry no lower bound on $n$ .
Added standing hypotheses: $K \ge 2$ everywhere, $n \ge K$ in Theorem 3.4 (from the protocol box, p. 6; Theorem 3.4 is false without it), $\beta > 0$ and $p_{i,t} > 0$ in Lemma 3.1.
Theorem 3.4 is stated as "for every forecaster there is a Bernoulli instance with regret at least $\sqrt{nK}/20$ ", which implies the book's $\inf\sup$ (3.18).

A trivializing formalization is ruled out: the forecasters are fixed rules of the observed history drawn with fresh randomness, the adversary is not restricted to a fixed sequence, and the lower bounds quantify over all forecasters and exhibit the instance.

Welcome contributions: a reusable construction of runs (existence of a probability space carrying a run for every rule), the supermartingale form of Lemma 3.1, the exponential-weights potential argument, a tail-integration lemma $\mathbb E W \le \int_0^1 \delta^{-1}\mathbb P(W > \ln\delta^{-1})\,d\delta$ , and a KL/Pinsker comparison for bandit runs.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. doi:10.1137/S0097539701398375
J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. jmlr.org/papers/v11/audibert10a
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. doi:10.1017/CBO9780511546921

13 thms1 active userReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Stability and Generalization 1: Polynomial Generalization Bounds from Hypothesis Stability for the Empirical and Leave-One-Out ErrorsResearch Paper

Why stability bounds

A learning algorithm is judged by its generalization error, its expected loss on a fresh example, which cannot be computed because the data distribution is unknown. Practitioners estimate it either by the empirical error on the training set or by the leave-one-out error, which retrains the algorithm once per example. Classical learning theory justifies these estimates through uniform convergence over the whole hypothesis space (VC dimension, covering numbers). That route says nothing useful about algorithms such as nearest-neighbour rules or regularized kernel methods, whose effective hypothesis space is huge or unknown.

An alternative is to bound the deviation through a property of the algorithm itself: how much its output changes when one training example is removed. This idea goes back to Rogers and Wagner (1978) and Devroye and Wagner (1979) for local rules, and Kearns and Ron (1999) gave it a name. Bousquet and Elisseeff (JMLR 2002) systematized it with several stability notions and corresponding bounds; their paper is the standard reference for algorithmic stability in learning theory. This mission formalizes its first family of results, the polynomial bounds of §4.1.

Setting

Let $Z = X \times Y$ and let $D$ be a probability distribution on $Z$ . A training set $S = \{z_1, \dots, z_m\}$ consists of $m$ examples drawn i.i.d. from $D$ . A learning algorithm $A$ maps a training set $S$ to a hypothesis $A_S : X \to Y'$ ; it is deterministic and symmetric, meaning it does not depend on the order of the examples. A cost $c$ with $0 \le c(y', y) \le M$ defines the loss $\ell(f, z) = c(f(x), y)$ of a hypothesis $f$ at $z = (x, y)$ .

For each index $i$ , $S^{\setminus i}$ is $S$ with $z_i$ removed, and $S^i$ is $S$ with $z_i$ replaced by an independent fresh draw $z'_i \sim D$ . The three error quantities are

R(A,S) = \mathbb E_z[\ell(A_S, z)], \qquad R_{\mathrm{emp}}(A,S) = \frac1m \sum_{i=1}^m \ell(A_S, z_i), \qquad R_{\mathrm{loo}}(A,S) = \frac1m \sum_{i=1}^m \ell(A_{S^{\setminus i}}, z_i).

Two stability notions (Definitions 3 and 4) control them. $A$ has hypothesis stability $\beta_1$ if $\mathbb E_{S,z}[|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|] \le \beta_1$ for every $i$ , and pointwise hypothesis stability $\beta_2$ if $\mathbb E_{S}[|\ell(A_S,z_i) - \ell(A_{S^{\setminus i}},z_i)|] \le \beta_2$ for every $i$ .

Formalization targets

Goal: Theorem 11

For $m \ge 1$ , under hypothesis stability $\beta_1$ and pointwise hypothesis stability $\beta_2$ , for every $\delta > 0$ , each of the following holds with probability at least $1 - \delta$ over $S \sim D^m$ :

R(A,S) \le R_{\mathrm{emp}}(A,S) + \sqrt{\frac{M^2 + 6Mm(\beta_1+\beta_2)}{2m\delta}}, \qquad R(A,S) \le R_{\mathrm{loo}}(A,S) + \sqrt{\frac{M^2 + 6Mm\beta_1}{2m\delta}} .

Milestones

Lemma 25 (p. 520), a generalized Rogers–Wagner identity: upper bounds on $\mathbb E_S[(R - R_{\mathrm{emp}})^2]$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2]$ by correlations of the loss.
Lemma 9, (8) and (9) (p. 505): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le \frac{M^2}{2m} + 3M\,\mathbb E_{S,z'_i}[|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|]$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le \frac{M^2}{2m} + 3M\,\mathbb E_{S,z}[|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|]$ .
The replace-one term (proof of Theorem 11): $\mathbb E_{S,z'_i}[|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|] \le \beta_1 + \beta_2$ .
The second-moment bounds (proof of Theorem 11): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le \frac{M^2}{2m} + 3M(\beta_1+\beta_2)$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le \frac{M^2}{2m} + 3M\beta_1$ .

Significance

Theorem 11 is the weakest-assumption bound in the paper: it requires only average-case stability, not the uniform (worst-case) stability behind the exponential bounds of §4.2. It shows that both the resubstitution and the deleted estimate are within $O(1/\sqrt{m\delta})$ of the risk whenever the stability parameters decay like $1/m$ , with no reference to the size of the hypothesis class. It also extends Devroye and Wagner's leave-one-out analysis for classification to bounded regression losses and to the empirical estimator. Later work on average stability and on generalization of stochastic gradient methods (for example Hardt, Recht and Singer, 2016) starts from these notions.

The result is proved in the paper; as far as is known it has no machine-checked proof. A formal development has two concrete payoffs. First, it fixes the constants: in checking the argument, two printed slips were found (the empirical constant in Theorem 11 and the third term of Lemma 25's first inequality), and the formal statements record the versions that the paper's proof actually establishes. Second, the Lemma 25 and Lemma 9 machinery — exchangeability of i.i.d. samples under renaming, and second-moment control through stability — is reusable for any later stability result.

Difficulty

The obvious route is the Efron–Stein (Steele) variance inequality, Theorem 1 of the paper. It bounds the variance of $R - R_{\mathrm{emp}}$ , not its second moment, and leaves the bias to be handled separately; the paper notes that it gives worse constants. The direct route of Appendix A instead expands $\mathbb E_S[(R - R_{\mathrm{emp}})^2]$ and rewrites each correlation term by renaming i.i.d. variables: training points, fresh test points and replacement points are exchanged with one another, and the algorithm is retrained on sets $T \cup \{z, z'\}$ with $T = S^{\setminus \{i,j\}}$ . Every renaming is a measure-preserving map on a product of $m + 2$ copies of $D$ , and each must be justified by the symmetry of $A$ . Doing this rigorously, rather than as "a matter of renaming", is the core of the work. The leave-one-out case is only sketched in the paper ("it is easy to see"), so its formal proof has to be reconstructed.

Formalization scope

An algorithm is a function Multiset (X × Y) → (X → Y'). Symmetry in the training set is built into the type, and the same algorithm acts on sets of every size, as $S$ and $S^{\setminus i}$ require. A sample is S : Fin m → X × Y with law $D^m$ (Measure.pi); fresh points $z$ , $z'$ , $z'_i$ are further independent coordinates, via product measures $D^m \otimes D$ and $(D^m \otimes D) \otimes D$ .
The loss, empirical error and generalization error are the published FoundationsML.Stability definitions (Loss, EmpiricalError, GeneralizationError).
The cost satisfies $0 \le c \le M$ everywhere. The paper's assumption that "all functions are measurable" becomes one hypothesis: for every $n$ , $(S, z) \mapsto \ell(A_S, z)$ is measurable on $(X \times Y)^n \times (X \times Y)$ . Both stability definitions also require their integrands to be integrable. Together these rule out the trivializing reading in which a non-integrable expectation equals Lean's default value $0$ and the stability hypotheses hold vacuously.
"With probability $1 - \delta$ " is stated as a bound on the failure event: $D^m\{S : R > R_{\mathrm{emp}} + \cdots\} \le \delta$ for every $\delta > 0$ , separately for each estimator.
$m \ge 2$ is assumed in Lemmas 9 and 25 and in the two second-moment steps of the proof, because the lemmas refer to two distinct indices. Theorem 11 itself is stated for every $m \ge 1$ , as printed.
Corrected statements. (i) Theorem 11's empirical bound is stated with $6Mm(\beta_1+\beta_2)$ , not the printed $12Mm\beta_2$ : the proof bounds a hypothesis-stability term by $\beta_2$ when it is bounded by $\beta_1$ . The two coincide when $\beta_1 = \beta_2$ . Accordingly the replace-one milestone is stated as $\le \beta_1 + \beta_2$ (printed $2\beta_2$ ), and the empirical second-moment bound as $\frac{M^2}{2m} + 3M(\beta_1+\beta_2)$ (printed $6M\beta_2$ ). (ii) Lemma 25's empirical inequality has $\mathbb E_S[\ell(A_S,z_i)\ell(A_S,z_j)]$ as its third term, as its proof gives, not the printed leave-one-out term. (iii) The leave-one-out second-moment bound follows from (9), not from (10) as printed.

Contributions are welcome at every level: proofs of the milestones, a general exchangeability lemma for symmetric algorithms on product measures, and Markov/Chebyshev glue for the final step.

Selected references

O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
W. H. Rogers and T. J. Wagner, A finite sample distribution-free performance bound for local discrimination rules, Annals of Statistics 6(3) (1978), 506–514. https://doi.org/10.1214/aos/1176344196
L. Devroye and T. J. Wagner, Distribution-free performance bounds for potential function rules, IEEE Transactions on Information Theory 25(5) (1979), 601–604. https://doi.org/10.1109/TIT.1979.1056087
M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11(6) (1999), 1427–1453. https://doi.org/10.1162/089976699300016304
M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240

13 thms1 active userReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

Dynamic Scheduling of a System with Two Parallel Servers in Heavy Traffic with Resource Pooling: The Threshold Policy Is Asymptotically OptimalResearch Paper

Motivation

Many service systems route several classes of work to servers with overlapping skills: call centers with cross-trained agents, manufacturing cells with flexible machines, computing clusters with heterogeneous processors. Choosing which server works on which class at each moment is a dynamic scheduling problem. Exact optimal policies are out of reach except in toy cases, so heavy-traffic theory replaces the queueing system by a Brownian control problem, solves that limit problem, and then asks for a policy in the original system whose performance converges to the Brownian optimum. This programme was proposed by Harrison (Harrison 1988), and the parallel server system studied here is the example Harrison used (Harrison, Ann. Appl. Probab. 1998) to show that the greedy static priority rule can be very inefficient.

Bell and Williams (2001) gave the first proof of asymptotic optimality of a continuous-review policy for this system, with renewal arrivals and general service times. Harrison (1998) had treated Poisson arrivals and deterministic service times with a discrete-review policy and a pathwise criterion. Harrison and López (Queueing Systems, 1999) identified the complete resource pooling condition for general parallel server systems. The threshold policy and the proof method of Bell and Williams were later extended to multiserver systems (Bell and Williams, Electron. J. Probab., 2005).

Setting

There are two job classes and two servers. Server 1 serves class 1 (activity 1); server 2 serves class 1 (activity 2) and class 2 (activity 3). A sequence of such systems is indexed by $r\to\infty$ . On a probability space, i.i.d. sequences $\check u_k(i)$ ( $k=1,2$ ) and $\check v_j(i)$ ( $j=1,2,3$ ), $i\ge1$ , are fixed: strictly positive, mutually independent, with mean one and finite variances $\alpha_k^2,\beta_j^2$ . In system $r$ the interarrival times are $u_k^r(i)=\check u_k(i)/\lambda_k^r$ and the service times are $v_j^r(i)=\check v_j(i)/\mu_j^r$ . The renewal processes $A_k^r(t)$ and $S_j^r(t)$ count arrivals and potential service completions.

A scheduling control policy is an allocation $T=(T_1,T_2,T_3)$ , where $T_j(t)$ is the time devoted to activity $j$ in $[0,t]$ . Each $T_j(t)$ is a random variable, each $T_j$ is continuous and nondecreasing from $0$ , and so are the idle times $I_1=t-T_1$ and $I_2=t-T_2-T_3$ . The queue lengths

Q_1(t)=A_1(t)-S_1(T_1(t))-S_2(T_2(t)),\qquad Q_2(t)=A_2(t)-S_3(T_3(t))

must be nonnegative. Policies may anticipate the future. The rates satisfy Assumption 3.1: $\lambda_1>\mu_1$ , $1-(\lambda_1-\mu_1)/\mu_2=\lambda_2/\mu_3$ , and the rates converge at rate $1/r$ to limits with second-order parameters $\theta_1,\theta_2$ . Assumption 3.2 is $h_1\mu_2\ge h_2\mu_3$ , and Assumption 3.3 gives finite exponential moments near $0$ . With $\hat Q^r(t)=r^{-1}Q^r(r^2t)$ the cost is

\hat J^r(T^r)=\mathbf E\Big(\int_0^\infty e^{-\gamma t}\,h\cdot\hat Q^r(t)\,dt\Big).

The threshold policy with $L^r=[c\log r]$ works as follows. Server 1 works whenever it has a class 1 job available. Server 2 serves class 1 with preemptive-resume priority when more than $L^r$ class 1 jobs are present, and otherwise serves class 2. The Brownian benchmark is built from a two-dimensional Brownian motion $\tilde X$ with drift $\theta$ and diagonal covariance, from $y=(1,\mu_2/\mu_3)$ , and from the reflected process $\tilde W^*=y\cdot\tilde X+\tilde V^*$ with $\tilde V^*(t)=-\inf_{s\le t}y\cdot\tilde X(s)$ . Its cost is $J^*=\mathbf E\int_0^\infty e^{-\gamma t}h_2\,\tilde W^*(t)/y_2\,dt$ .

Formalization targets

Goal: Theorem 5.3

For $c$ larger than a constant $c_0$ that depends only on the model data, and for every sequence $\{T^r\}$ of scheduling control policies,

\liminf_{r\to\infty}\hat J^r(T^r)\ \ge\ J^*\ =\ \lim_{r\to\infty}\hat J^r(T^{r,*}),\qquad J^*<\infty .

Milestones

Proposition B.1: the one-dimensional Skorokhod problem, its explicit solution and its minimality.
Appendix A, (181) and (184): Cramér-type deviation bounds for delayed renewal processes.
Theorem 7.2: after first reaching $L^r$ , the class 1 queue stays within $L^r-1$ of the threshold, with probability tending to one.
Theorem 7.1: $(\hat Q_1^r,\hat I_1^r)\Rightarrow(0,0)$ under the threshold policy.
Lemma 8.1: the fluid-scaled threshold allocations converge to $\bar T^*(t)=(t,\frac{\lambda_1-\mu_1}{\mu_2}t,\frac{\lambda_2}{\mu_3}t)$ .
Theorem 5.2 (state-space collapse): $(\hat Q_1^r,\hat Q_2^r,\hat I_1^r,\hat I_2^r)\Rightarrow(0,\tilde Q_2^*,0,\tilde I_2^*)$ .
Lemma 9.3: along a subsequence achieving a finite $\liminf$ cost, the fluid-scaled processes converge to $(0,\lambda t,\mu t,\bar T^*,0)$ .

A further draft theorem states that Definition 5.1 determines an admissible allocation, unique pathwise, whenever $L^r\ge1$ .

Significance

The theorem proves that a simple state-dependent rule, which sends server 2 to class 1 only when the class 1 queue exceeds a logarithmic safety stock, is asymptotically optimal among all policies, including those that anticipate the future. The limiting cost is the explicit optimum of the Brownian control problem. The proof gives a template for heavy-traffic asymptotic optimality under complete resource pooling: a lower bound valid for every policy, and state-space collapse under the proposed policy. The residual process analysis of Section 7 shows how a threshold of order $\log r$ makes starvation of server 1 negligible on the diffusion time scale.

The paper's results are proved but not machine-checked; no formal proof exists in any proof assistant. The mission asks for formal statements of the paper's main theorem and its supporting lemmas, followed by formal proofs. Parts of the development are independent of the paper: the one-dimensional Skorokhod map, renewal large deviation bounds, and convergence encodings on path space.

Difficulty

The lower bound must hold for arbitrary, possibly anticipating, policies, so no Markov structure is available. The argument has to pass through fluid limits of an arbitrary cost-minimizing subsequence and a pathwise minimality property, and Fatou's lemma for the limit needs uniform control. For the upper bound, the obvious approach, a static priority rule, is known to fail: it starves server 1 and produces a large class 1 queue. With a threshold policy, the hard step is to show that the class 1 queue, once at the threshold, rarely moves $L^r-1$ away from it over a time interval of length $r^2t$ . That requires large deviation estimates for renewal processes started at random, multiparameter stopping times. Showing that $\hat J^r(T^{r,*})$ converges to $J^*$ , rather than only that the processes converge in distribution, also requires uniform integrability of the scaled queue lengths.

Formalization scope

Classes and activities are indexed by Fin 2 and Fin 3. The i.i.d. sequences keep the paper's index base $i\ge1$ , and the systems are indexed by $n\in\mathbb N$ with $r=r_n\in[1,\infty)$ , $r_n\to\infty$ . Time is real, and every condition is imposed for $t\ge0$ . Admissibility is exactly (11)–(14). Measurability in (11) is with respect to the completion of $\mathbf P$ , since the paper's space is complete. Finiteness of the renewal processes everywhere on $\Omega$ , which the paper obtains by discarding a null set, is a hypothesis. Queue lengths are real, costs are lower Lebesgue integrals in $[0,\infty]$ , counting processes take values in $\mathbb N\cup\{\infty\}$ , and $\Lambda$ , $\Lambda^*$ take values in the extended reals.

The constant $c_0$ is existential and is chosen after the model data and before $c$ , the policies and the Brownian motions. The threshold relations are required only for the systems with $L^r\ge1$ , which are all but finitely many. Each convergence to a deterministic limit (Theorem 7.1, Lemmas 8.1 and 9.3) is stated as u.o.c. convergence in probability, the paper's own equivalence (p. 633). Theorem 5.2 is stated in coupling form: there are copies of the processes on one probability space, with Skorokhod paths and the same laws, that converge almost surely uniformly on compacts. This is equivalent to weak convergence in $\mathbf D^4$ to a limit with continuous paths. $J^*$ is defined by (44) from an arbitrary pair of independent standard Brownian motions (Mathlib's IsBrownianReal), not by a closed form.

Two formalizations would make the goal trivial, and both are excluded. Leaving out the requirement that $T^{r,*}$ actually follow the policy would make the goal false or empty. Narrowing the class of competing policies, for example to non-anticipating ones, would weaken the theorem. A draft theorem also states that the threshold allocation exists and is unique pathwise, so the hypothesis on $T^{r,*}$ can be satisfied.

The development needs renewal theory (functional central limit theorems, Cramér bounds), multiparameter stopping times, tightness in $\mathbf D$ , the Skorokhod representation theorem, the reflection map, and properties of reflected Brownian motion. Contributions are welcome at every level: proofs of milestones, reusable lemmas on renewal processes and the Skorokhod map, and further lemmas of the paper (Lemmas 7.5, 7.6 and 9.2 are not yet stated).

Selected references

S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11 (2001) 608–649. https://doi.org/10.1214/aoap/1015345343
J. M. Harrison, Heavy traffic analysis of a system with parallel servers: asymptotic optimality of discrete-review policies, Ann. Appl. Probab. 8 (1998) 822–848.
J. M. Harrison and M. J. López, Heavy traffic resource pooling in parallel-server systems, Queueing Systems 33 (1999) 339–368.
J. M. Harrison, Brownian models of queueing networks with heterogeneous customer populations, in Stochastic Differential Systems, Stochastic Control Theory and Their Applications, Springer (1988) 147–186.
S. L. Bell and R. J. Williams, Dynamic scheduling of a parallel server system in heavy traffic with complete resource pooling: asymptotic optimality of a threshold policy, Electron. J. Probab. 10 (2005) 1044–1115.
J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley (1985).

14 thms1 active userReviewed

Dynamical Systems Operations Research Probability+1·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 7: Weak Limit Points of the Occupation Measures of a Weak Asymptotic Pseudotrajectory Are InvariantResearch Paper

Motivation

Stochastic approximation algorithms are recursions $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ driven by small steps $\gamma_n$ and noise $U_{n+1}$ ; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.

The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically $\gamma_n=o(1/\log n)$ or $\gamma_n=O(n^{-\alpha})$ . When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order $1/\log n$ the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.

Setting

A semiflow on a metric space $(M,d)$ is a continuous map $\Phi:\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ for $t,s\ge0$ . Throughout, $M$ is a separable metric space with its Borel $\sigma$ -algebra.

Let $(\Omega,\mathcal F,P)$ be a probability space and $\{\mathcal F_t\}_{t\ge0}$ a nondecreasing family of sub- $\sigma$ -algebras. A process $X:\mathbb R_+\times\Omega\to M$ is a weak asymptotic pseudotrajectory of $\Phi$ if

it is progressively measurable: for every $T>0$ the restriction of $X$ to $[0,T]\times\Omega$ is measurable for the product of the Borel $\sigma$ -field of $[0,T]$ and $\mathcal F_T$ ;
for each $\alpha>0$ and $T>0$ , almost surely

\lim_{t\to\infty}P\Big\{\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)\ge\alpha\ \Big|\ \mathcal F_t\Big\}=0 .

Let $\mathcal P(M)$ be the space of Borel probability measures on $M$ with the topology of weak convergence. A measure $\mu\in\mathcal P(M)$ is $\Phi$ -invariant if $(\Phi_t)_*\mu=\mu$ for every $t\ge0$ ; the set of invariant measures is $\mathcal M(\Phi)$ . The occupation measure of the process at time $t>0$ is the random probability measure

\mu_t(\omega)=\frac1t\int_0^t\delta_{X(s,\omega)}\,ds ,

and $\mathcal M(X,\omega)\subset\mathcal P(M)$ is the set of its weak limit points as $t\to\infty$ .

Formalization targets

Goal: Theorem 10.1

If $X$ is a weak asymptotic pseudotrajectory of $\Phi$ , there is a set $\tilde\Omega\subset\Omega$ with $P(\tilde\Omega)=1$ such that for all $\omega\in\tilde\Omega$

\mathcal M(X,\omega)\subset\mathcal M(\Phi).

No tightness is assumed, so $\mathcal M(X,\omega)$ may be empty; the statement asserts the inclusion, not nonemptiness.

Milestones

Fix a uniformly continuous $f:M\to[0,1]$ and $T>0$ , and set $U_n(f,T)=\int_{(n-1)T}^{nT}f(X(s))\,ds$ for $n\ge1$ . The milestones are the numbered displays of the proof on pp. 62–63:

Eq. (47): $\frac1n\sum_{i=1}^n[U_i(f,T)-E(U_i(f,T)\mid\mathcal F_{(i-1)T})]\to0$ almost surely (stated for every continuous $f$ with values in $[0,1]$ , since the proof also applies it to $f\circ\Phi_T$ );
Eq. (50): the same with $U_{i+1}(f,T)$ conditioned on $\mathcal F_{(i-1)T}$ ;
Eq. (51): $E(U_{i+1}(f,T)-U_i(f\circ\Phi_T,T)\mid\mathcal F_{(i-1)T})\to0$ almost surely;
Eq. (52): $\frac1n\sum_{i=1}^nU_{i+1}(f,T)-\frac1n\sum_{i=1}^nU_i(f\circ\Phi_T,T)\to0$ almost surely;
Eq. (53): for a single measurable path whose occupation measures converge weakly to $\mu$ along $t_j\to\infty$ , the averages $\frac1{n_jT}\sum_{i=0}^{n_j-1}\int_{iT}^{(i+1)T}f(x_s)\,ds$ with $n_j=\lfloor t_j/T\rfloor$ converge to $\int f\,d\mu$ for every bounded continuous $f$ .

Significance

The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, $\mathcal M(X,\omega)$ is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in $\mathcal M(X,\omega)$ ; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.

Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in $\mathcal P(M)$ .

Difficulty

The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space $M$ , and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.

Formalization scope

Time is $\mathbb R_{\ge0}$ ; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; $\mathcal P(M)$ is ProbabilityMeasure M with its topology of weak convergence. $M$ is a separable metric space with its Borel $\sigma$ -algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every $T>0$ . The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's $P\{\cdot\mid\mathcal F_t\}$ presupposes an event); the supremum over $h\in[0,T]$ is taken in $[0,\infty]$ . Invariance for the semiflow is $(\Phi_t)_*\mu=\mu$ for all $t\ge0$ , the form the proof establishes; for a flow it agrees with the definition $\mu(A)=\mu(\Phi_t(A))$ of Section 8.3. Weak limit points are cluster points of $t\mapsto\mu_t(\omega)$ as $t\to\infty$ ; the occupation measure is a genuine probability measure for every measurable path and $t>0$ .

The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to $0$ and which would make condition 2 vacuous; invariance defined through images $\Phi_t(A)$ , which need not be Borel for a semiflow; and a compactness or Polish assumption on $M$ , which the theorem does not make.

A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. Section 10, Theorem 10.1, pp. 60–63. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617

10 thms1 active userReviewed

Dynamical Systems Operations Research Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 1: Limit Sets of Precompact Asymptotic Pseudotrajectories Are Internally Chain TransitiveResearch Paper

Motivation

A stochastic approximation algorithm updates an estimate by small noisy steps, $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ , with step sizes $\gamma_n\to0$ and noise $U_n$ . Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation $\dot x=F(x)$ . Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.

Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of $F$ , and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).

Timeline. Bowen (1975) and Conley (1978) introduced $(\delta,T)$ -pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.

Setting

Let $(M,d)$ be a metric space. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ . A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$ ; then $\Phi|A$ denotes the restricted semiflow on $A$ .

A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory of $\Phi$ if

\lim_{t\to\infty}\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)=0\quad\text{for every }T>0,

and it is precompact if $X(\mathbb R_+)$ has compact closure. Its limit set is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$ .

For $\delta>0$ , $T>0$ , a $(\delta,T)$ -pseudo-orbit from $a$ to $b$ consists of $k\ge1$ partial trajectories, given by points $y_0,\dots,y_{k-1}$ (and an endpoint $y_k$ ) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$ , $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$ , and $y_k=b$ . One writes $a\hookrightarrow b$ if such pseudo-orbits exist for all $\delta,T>0$ . A nonempty compact invariant set $\Lambda$ is internally chain transitive if $a\hookrightarrow b$ for the restricted semiflow $\Phi|\Lambda$ for all $a,b\in\Lambda$ , so that all $y_i$ lie in $\Lambda$ ; it is internally chain recurrent if $a\hookrightarrow a$ for $\Phi|\Lambda$ for every $a\in\Lambda$ . An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ such that $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly in $x\in W$ .

Formalization targets

Goal: Theorem 5.7 (i)

For every semiflow $\Phi$ on a metric space $M$ and every precompact asymptotic pseudotrajectory $X$ of $\Phi$ ,

L(X)\ \text{is internally chain transitive.}

Milestones (in the order of the proof)

Lemma 3.1. $X$ is an asymptotic pseudotrajectory iff $d(\Theta^t(X),\hat\Phi\circ\Theta^t(X))\to0$ , where $\Theta$ is the translation semiflow on $C^0(\mathbb R_+,M)$ and $\hat\Phi(Y)=\Phi^{Y(0)}$ .
Theorem 3.2. For precompact continuous $X$ : $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of $\Theta^{t}(X)$ , $t\to\infty$ , is a trajectory of $\Phi$ ; and then $\{\Theta^t(X)\}_{t\ge0}$ is relatively compact.
Lemma 5.2. A nonempty open $U$ with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$ contains an attractor whose basin contains $\overline U$ .
Proposition 5.3. For nonempty $\Lambda$ : internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact, invariant and $\Phi|\Lambda$ has no proper attractor.
Theorem 5.5. On a nonempty compact $M$ , the chain recurrent set $R(\Phi)$ is internally chain recurrent.
Corollary 5.6. If $\overline{\gamma^+(x)}$ is compact, then $\omega(x)$ is internally chain transitive.

Significance

The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).

Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.

Difficulty

The obvious approach follows $X$ from a point $a\in L(X)$ to a point $b\in L(X)$ : $X$ returns near $a$ and near $b$ infinitely often, and on windows of length $T$ it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve $X$ , not in $L(X)$ ; this only shows that $L(X)$ is chain transitive for $\Phi$ on $M$ , a strictly weaker property. Producing pseudo-orbits whose points lie in $L(X)$ itself is the central difficulty, and it is where precompactness of $X$ is used. Invariance $\Phi_t(L(X))=L(X)$ , with equality, also needs a compactness argument, since a semiflow is not invertible.

Formalization scope

A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; $M$ is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality $\Phi_t(A)=A$ . Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype $\Lambda$ , so every point of the pseudo-orbit lies in $\Lambda$ . Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on $C^0(\mathbb R_+,M)$ (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write $C^0(\mathbb R,M)$ , but with the convention $\Phi^p(t)=p$ for $t<0$ that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of $C^0(\mathbb R_+,M)$ .

Ruled out: pseudo-orbits with no trajectory piece ( $k=0$ ), pseudo-orbits allowed to leave $L(X)$ , invariance as mere inclusion $\Phi_t(A)\subset A$ , and any compactness assumption on $M$ . Each of these makes the goal weaker than the theorem of the notes.

A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between $\Phi$ and the translation semiflow on $S_\Phi$ . Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

12 thms1 active userReviewed

Dynamical Systems Operations Research Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 2: Under A1 and A2 the Interpolated Process Is an Asymptotic Pseudotrajectory of the Flow of FResearch Paper

Motivation

A stochastic approximation algorithm is a recursion

x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)

in $\mathbb R^d$ , driven by a vector field $F$ , decreasing step sizes $\gamma_n$ and perturbations $U_n$ . Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation $\dot x=F(x)$ .

Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of $\{x_n\}$ is an asymptotic pseudotrajectory of the flow of $F$ . Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.

Setting

Let $F:\mathbb R^d\to\mathbb R^d$ be continuous. It is globally integrable if through every point there is exactly one integral curve $y:\mathbb R\to\mathbb R^d$ , $\dot y=F(y)$ ; the flow $\Phi_t(p)$ is the value at time $t$ of the integral curve through $p$ .

The step sizes satisfy $\gamma_n\ge0$ , $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ . Set $\tau_0=0$ , $\tau_n=\sum_{i=1}^n\gamma_i$ , and $m(t)=\sup\{k\ge0:\tau_k\le t\}$ . The affine interpolated process $X:\mathbb R_+\to\mathbb R^d$ and the piecewise constant processes $\overline X,\overline U,\bar\gamma$ are, for $0\le s<\gamma_{n+1}$ ,

X(\tau_n+s)=x_n+s\,\frac{x_{n+1}-x_n}{\gamma_{n+1}},\qquad \overline X(\tau_n+s)=x_n,\quad \overline U(\tau_n+s)=U_{n+1},\quad \bar\gamma(\tau_n+s)=\gamma_{n+1}.

The noise enters through

\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\overline U(s)\,ds\Big\| .

A1: for every $T>0$ , $\sup\{\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\|:n<k\le m(\tau_n+T)\}\to0$ as $n\to\infty$ ; equivalently $\Delta(t,T)\to0$ as $t\to\infty$ .
A2: $\sup_n\|x_n\|<\infty$ .
A2′: $F$ is Lipschitz and bounded on a neighbourhood of $\{x_n\}$ .

A continuous $X:\mathbb R_+\to\mathbb R^d$ is an asymptotic pseudotrajectory of $\Phi$ if for every $T>0$

\lim_{t\to\infty}\sup_{0\le h\le T}\big\|X(t+h)-\Phi_h(X(t))\big\|=0 .

Formalization targets

Goal: Proposition 4.1

F\ \text{continuous, globally integrable},\quad \text{A1},\quad \text{A2 or A2}'\quad\Longrightarrow\quad X\ \text{is an asymptotic pseudotrajectory of}\ \Phi .

No rate and no constant appear; the statement holds under either alternative.

Milestones

Eq. (9): $X(t)-X(0)=\int_0^t[F(\overline X(s))+\overline U(s)]\,ds$ .
A1: the discrete and the continuous forms of A1 are equivalent, for each $T>0$ .
Theorem 3.2: for a flow on a metric space and a continuous $X$ with relatively compact image, $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of the translates $\Theta^t(X)$ in $C^0(\mathbb R,M)$ is a trajectory of the flow; both imply that $\{\Theta^t(X)\}$ is relatively compact.
Comparison of $X$ and $\overline X$ (p. 13): if $\|F(x_n)\|\le K$ , then for $t$ large, $\sup_{t\le u\le t+T}\|X(u)-\overline X(u)\|\le2\Delta(t-1,T+1)+\sup_{t\le u\le t+T}K\bar\gamma(u)$ .
Estimate (11): under A1 and A2′, for $t$ large,

\sup_{0\le h\le T}\|X(t+h)-\Phi_h(X(t))\|\le C(T)\Big[\Delta(t-1,T+1)+\sup_{t\le s\le t+T}\bar\gamma(s)\Big],

with $C(T)$ depending only on $T$ and on $F$ (through its Lipschitz constant and bound on the neighbourhood).

Significance

Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for $L^q$ -bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of $\dot x=F(x)$ . The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.

The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.

Difficulty

The obvious argument compares $X$ directly with the flow by Gronwall's inequality. It needs $F$ Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where $F$ is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.

Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where $F$ is controlled for the whole window $[t,t+T]$ .

Formalization scope

Space $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; $\gamma_0$ and $U_0$ are unused.
$m(t)$ is the largest $k$ with $\tau_k\le t$ , so the divisor $\gamma_{m(t)+1}$ is positive even when some steps vanish.
Limits are written with $\varepsilon$ ; the suprema that remain ( $\Delta$ , $\sup\bar\gamma$ ) are over bounded nonempty sets, and $\overline U$ is a step function with finitely many pieces on bounded intervals, so no integral or supremum takes a default value.
The flow of $F$ is a function satisfying the integral-curve property, together with global integrability (existence and uniqueness of integral curves on $\mathbb R$ ); continuity of the flow is not assumed.
A2′ is read with a uniform neighbourhood: $F$ is Lipschitz and bounded on $\{y:\operatorname{dist}(y,\{x_n\})<r\}$ for some $r>0$ . Under the reading "some open set containing $\{x_n\}$ " the proposition fails for unbounded iterates.
Theorem 3.2 is stated for flows on $C^0(\mathbb R,M)$ (compact-open topology); for semiflows with the convention $\Phi^p(t)=p$ for $t<0$ , the implication (i)⇒(ii) is false as printed.

Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), $X$ is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.

A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on $C^0(\mathbb R,M)$ , continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of $X$ and $\overline X$ are the natural entry points.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probab. Theory Related Fields 74 (1987), 403–428. https://doi.org/10.1007/BF00699098
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
L. Ljung, Analysis of recursive stochastic algorithms, IEEE Trans. Automat. Control 22 (1977), 551–575. https://doi.org/10.1109/TAC.1977.1101561

9 thms1 active userReviewed

Probability Statistics·Captain: mikedeng1

Weighted Sums of Certain Dependent Random Variables 2: An Iterated-Logarithm Upper Bound for Weighted Conditionally Sub-Gaussian Martingale DifferencesResearch Paper

Motivation

The law of the iterated logarithm (LIL) gives the exact almost-sure size of the fluctuations of a sum of random variables. For independent fair $\pm1$ increments $x_1,x_2,\dots$ with partial sums $S_n$ , Khinchin (1924) showed that $\limsup_n |S_n|/\sqrt{2n\log\log n}=1$ almost surely; Kolmogorov (1929) extended this to bounded independent increments, and Hartman and Wintner (1941) to independent, identically distributed increments with variance $1$ . Weighted sums $a_1x_1+\dots+a_nx_n$ appear in summability theory, in stochastic approximation and in the analysis of orthogonal series, and there the natural normalisation replaces $n$ by the sum of squared weights.

Independence is often not available. In martingale settings (sequential estimation, online learning, adaptive algorithms) the increments are only conditionally centred given the past. In 1967 Kazuoki Azuma (Azuma 1967) introduced a conditional sub-Gaussian condition on martingale differences, called property [G], and proved for it an iterated-logarithm upper bound for weighted sums. The moment-generating-function bound that drives his proof, display (2.4), is the inequality now known as the Azuma–Hoeffding inequality. This mission formalizes Theorem 2 of that paper and the lemmas its proof rests on.

Timeline.

1924: Khinchin proves the LIL for fair coin tossing.
1929: Kolmogorov proves it for bounded independent increments under a growth condition.
1941: Hartman and Wintner prove it for i.i.d. increments with finite variance.
1963: Hoeffding proves the exponential tail bound for sums of bounded independent variables.
1965: Gaposhkin proves a LIL for weighted (Cesàro and Abel) means of independent variables.
1967: Azuma proves the conditional mgf bound (2.4), its maximal version (Lemma 2) and the upper-half LIL for weighted sums of class [G] martingale differences (Theorem 2).

Setting

Let $(\Omega,\mathfrak A,P)$ be a probability space and $(\mathfrak A_n)_{n\ge0}$ an increasing family of sub- $\sigma$ -fields of $\mathfrak A$ (a filtration). A sequence of real random variables $(x_n)_{n\ge1}$ is a martingale-difference sequence if each $x_n$ is $\mathfrak A_n$ -measurable and integrable and $E\{x_n\mid\mathfrak A_{n-1}\}=0$ almost surely.

The sequence satisfies [G] with $\tau(x_n)\le1$ if, in addition, for every $n\ge1$ and every real $t$ ,

E\{\exp(tx_n)\mid\mathfrak A_{n-1}\}\le\exp(t^2/2)\quad\text{a.s.}

Every martingale-difference sequence with $|x_n|\le1$ almost surely has this property, but the class also contains unbounded increments, for instance conditionally standard Gaussian ones.

Fix real weights $(a_n)_{n\ge1}$ of arbitrary sign and write

D_n^2=\sum_{j=1}^n a_j^2,\qquad S_n=a_1x_1+\dots+a_nx_n .

For the lemmas the weights are called $(b_k)$ , and the maximal partial sum is $S_n^*(\omega)=\max_{1\le m\le n}\big|\sum_{k=1}^m b_kx_k(\omega)\big|$ .

In Lean these objects are IsMartingaleDiff, IsCondSubgaussianOne, weightedSum ( $S_n$ ), sqWeightSum ( $D_n^2$ ) and maxAbsWeightedSum ( $S_n^*$ ), all in the namespace AzumaWeightedSums.IteratedLog.

Formalization targets

Goal: Theorem 2, display (4.2)

If $(x_n)$ satisfies [G] with $\tau(x_n)\le1$ and the weights satisfy

a_n^2/D_n^2\to0,\qquad D_n^2\to\infty,

then

\limsup_{n\to\infty}\frac{|S_n|}{\sqrt{2D_n^2\log\log D_n^2}}\le1\quad\text{a.s.}

The constant $1$ is sharp, as Gaussian increments show, so the goal is stated with the paper's constant and in no weaker form.

Milestones

Display (2.4). For every $n$ , every real $(b_k)$ and every real $t$ ,

E\Big\{\exp\Big(t\sum_{k=1}^n b_kx_k\Big)\Big\}\le\exp\Big(\frac{t^2}{2}\sum_{k=1}^n b_k^2\Big).

Doob's $L^\alpha$ maximal inequality, cited on p. 359: for a nonnegative submartingale $(f_m)$ and $\alpha>1$ , $E\{(\max_{m\le n}f_m)^\alpha\}\le(\alpha/(\alpha-1))^\alpha E\{f_n^\alpha\}$ .
Lemma 2, display (2.3). $E\{\exp(tS_n^*)\}\le8\exp\big(\frac{t^2}{2}\sum_{k=1}^n b_k^2\big)$ for every real $t$ .
Maximal tail bound. If $V_n=\sum_{k=1}^n b_k^2>0$ and $\lambda\ge0$ , then $P\{S_n^*>\lambda\}\le8\exp(-\lambda^2/(2V_n))$ .

Significance

The result. Theorem 2 controls weighted sums of dependent increments almost surely, uniformly in $n$ , at the iterated-logarithm scale. It needs no independence and no boundedness: a conditional sub-Gaussian bound is enough. Bounded martingale differences are a special case, so the theorem covers martingale noise in stochastic approximation and the error terms of adaptive estimators. Milestones 1, 3 and 4 are reusable concentration inequalities: the conditional-expectation form of the Azuma–Hoeffding bound, and its maximal version with an explicit constant.

Formalizing it. The theorem is proved in the literature; nothing here is open. Mathlib has the sub-Gaussian mgf bound for sums in kernel form (HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF, under a standard Borel assumption that this mission does not make), and Doob's weak-type maximal inequality (Submartingale.maximal_ineq). It has no $L^p$ form of Doob's inequality and no law of the iterated logarithm of any kind. Prove2Me has an Azuma–Hoeffding tail bound without the maximum, and nothing at the iterated-logarithm scale. A complete development would therefore add Doob's $L^\alpha$ inequality and the first machine-checked iterated-logarithm upper bound, for a dependent class.

Difficulty

The tail bound (milestone 4) is not enough on its own: applied at each fixed $n$ and summed over $n$ , it gives a divergent series at the $\sqrt{2D_n^2\log\log D_n^2}$ scale. The proof has to pass to a subsequence of times and control the maximum over each block, and the blocks have to be fine enough that no constant is lost. The paper's printed proof chooses blocks along which $D_n^2$ roughly doubles. Its third displayed estimate uses the increment $D_{n_{k+1}}^2-D_{n_k}^2$ where the maximal inequality actually delivers the full $D_{n_{k+1}}^2$ ; with that correction, blocks of ratio $2$ prove (4.2) only with $\sqrt2$ in place of $1$ . A faithful formal proof must recover the constant $1$ , so the block ratio has to be tuned to $\varepsilon$ . Here the hypothesis $a_n^2/D_n^2\to0$ is essential, because it means a single term cannot carry $D_n^2$ past the next block boundary.

Lemma 2 needs Doob's inequality in $L^\alpha$ form for every even integer $\alpha=2j$ , uniformly enough to sum an exponential series. The weak-type inequality available in Mathlib does not give this directly.

Formalization scope

Index base and filtration. Sequences are ℕ → Ω → ℝ with sums over Finset.Icc 1 n; $x_0$ and $a_0$ are ignored. The paper fixes $\mathfrak A_0=\{\emptyset,\Omega\}$ ; here $\mathfrak A_0$ is arbitrary, which makes every statement at least as strong.
[G]. For each $n\ge1$ and each real $t$ , the conditional bound holds almost surely, in the paper's quantifier order, and $\exp(tx_n)$ is assumed integrable. Without integrability, Lean's conditional expectation is $0$ and the hypothesis would be empty. $\tau$ is not defined as an infimum: " $\tau(x_n)\le1$ " is stated as admissibility of the constant $1$ .
Expectations. Expectations of exponentials and powers are lower Lebesgue integrals in $[0,\infty]$ , so the inequalities also assert finiteness. A Bochner integral, which is $0$ for non-integrable functions, would make them trivially true.
The lim sup is not Lean's real-valued limsup, which is $0$ on unbounded sequences. The goal states the equivalent: for every $\varepsilon>0$ , almost surely, $|S_n|\le(1+\varepsilon)\sqrt{2D_n^2\log\log D_n^2}$ for all sufficiently large $n$ . Because $D_n^2\to\infty$ , $\log\log D_n^2>0$ for those $n$ , so Real.log is never evaluated at a junk argument that matters.
Ruled-out trivialisations. Dropping $a_n^2/D_n^2\to0$ , replacing [G] by boundedness, weakening the constant $1$ , or stating the bound with Lean's real limsup would each change the theorem. None of these is used.
Infrastructure. A complete proof needs conditional-expectation pull-out lemmas for the induction in (2.4), Doob's $L^p$ inequality (reusable well beyond this mission), Chernoff's bound and the first Borel–Cantelli lemma (both in Mathlib), and a block construction. Proofs of any milestone are welcome, as is a proof of Doob's $L^\alpha$ inequality in Mathlib's own form.

Selected references

K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967) 357–367. https://doi.org/10.2748/tmj/1178243286
J. L. Doob, Stochastic Processes, Wiley, New York, 1953 (the $L^\alpha$ maximal inequality, p. 317; reference [2] of Azuma 1967).
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830
P. Hartman and A. Wintner, On the law of the iterated logarithm, American Journal of Mathematics 63 (1941) 169–176. https://doi.org/10.2307/2371287
V. F. Gaposhkin, The law of the iterated logarithm for Cesàro's and Abel's methods of summation, Theory of Probability and its Applications 10 (1965) 411–420 (reference [3] of Azuma 1967).

7 thms1 active userReviewed

Control Theory Mathematical Physics Optimization+3·Captain: mikedeng1

Optimization of Mean-field Spin Glasses III: The Lagrangian Value of the Stochastic Control Problem Equals the Parisi FunctionalResearch Paper

Motivation

The ground-state energy of a mixed $p$ -spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$ , converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$ . Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$ . This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$ , with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$ . Its derivatives $\xi'$ , $\xi''$ are nonnegative and nondecreasing on $[0,1]$ .

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$ .

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$ , for $t\in[t_{i-1},t_i)$ ,

\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$ .

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$ , progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$ , with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$ . The value is

\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$ ,

V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .

Formalization targets

Goal: Proposition 4.1

\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .

Milestones

Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$ , with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$ , it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$ .
Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$ , where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$ .
Lemma 7.3: $V$ solves the HJB equation

\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .

Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$ .
Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$ .

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$ , which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ( $M_1\in(-1,1)$ ), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$ .

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$ , where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$ . The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$ ; its value at $t=1$ never matters.
Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$ , the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$ , where it is bounded below.
Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$ , with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$ .
Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$ ), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$ .
Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as " $v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$ ). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$ , and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$ , which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).

14 thms1 active userReviewed

Mathematical Physics Optimization Partial Differential Equations+1·Captain: mikedeng1

Optimization of Mean-field Spin Glasses I: Every Minimizer of the Extended Parisi Functional Has Full SupportResearch Paper

Motivation

The Ising mixed $p$ -spin model assigns to each configuration $\sigma \in \{-1,+1\}^N$ the energy of a random polynomial whose covariance is $\mathbb E\{H_N(\sigma)H_N(\sigma')\} = N\xi(\langle\sigma,\sigma'\rangle/N)$ . Its ground-state energy $\max_\sigma H_N(\sigma)/N$ converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional $\mathsf P$ is minimized over non-decreasing order parameters $\gamma$ . El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is $\inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , where the space $\mathscr L$ drops the monotonicity constraint.

The algorithm that reaches this value is built from a minimizer $\gamma_*$ of $\mathsf P$ over $\mathscr L$ , and it runs along the set of times where $\gamma_*$ is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).

Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with $\Phi(1,x)=|x|$ and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ ; its derivatives $\xi'$ , $\xi''$ are the termwise differentiated power series, non-negative and non-decreasing on $[0,1]$ .

An order parameter is a function $\gamma : [0,1) \to \mathbb R_{\ge0}$ . The extended space is

\mathscr L = \Bigl\{\gamma : [0,1)\to\mathbb R_{\ge0} : \|\xi''\gamma\|_{\mathrm{TV}[0,t]}<\infty\ \forall t\in[0,1),\ \int_0^1\xi''(t)\gamma(t)\,dt<\infty\Bigr\},

with the weighted distance $\|\gamma_1-\gamma_2\|_{1,\xi''} = \int_0^1\xi''(t)|\gamma_1(t)-\gamma_2(t)|\,dt$ . The non-negative step functions $\mathsf{SF}_+$ are the finite sums $\sum_i a_i\mathbb I_{[t_{i-1},t_i)}$ with $0=t_0<\dots<t_m=1$ and $a_i\ge0$ .

For a terminal condition $f_0$ (convex, continuous, even, non-negative, differentiable off $0$ with $0\le f_0'\le1$ on $(0,\infty)$ ) and $\gamma\in\mathsf{SF}_+$ , the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\bigl(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\bigr) = 0,\qquad \Phi(1,x) = f_0(x),

has the explicit Cole–Hopf solution $\Phi^\gamma$ : on $[t_{i-1},t_i)$ , $\Phi(t,x) = \gamma_i^{-1}\log\mathbb E\exp\{\gamma_i\Phi(t_i, x+\sqrt{\xi'(t_i)-\xi'(t)}\,G)\}$ with $G\sim\mathsf N(0,1)$ . For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n\to\gamma$ in the weighted distance. The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

Given a Brownian motion $B$ , the process $X$ solves $dX_t = \xi''(t)\gamma(t)\,\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ . The support of $\gamma$ is $S(\gamma) = \{t\in[0,1):\gamma(t)>0\}$ , and $\overline S(\gamma)$ is its closure in $[0,1)$ .

Formalization targets

Goal: Theorem 5

With $f_0(x) = |x|$ , if $\gamma_*\in\mathscr L$ satisfies $\mathsf P(\gamma_*) = \inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , then

\overline S(\gamma_*) = [0,1).

Milestones

The path to the goal, in attack order:

Proposition 6.1(b),(c): on step functions, $\partial_x\Phi$ is non-decreasing with $|\partial_x\Phi|\le1$ , and $\|\Phi^{\gamma_1}-\Phi^{\gamma_2}\|_\infty\le\|\xi''(\gamma_1-\gamma_2)\|_1$ .
Lemma 6.2: these properties pass to $\gamma\in\mathscr L$ .
Lemma 6.5: the SDE has a unique strong solution on $[0,1]$ .
Corollary 6.6: $\mathbb E\{\partial_x\Phi(t_2,X_{t_2})^2\}-\mathbb E\{\partial_x\Phi(t_1,X_{t_1})^2\}=\int_{t_1}^{t_2}\xi''(s)\,\mathbb E\{(\partial_x^2\Phi(s,X_s))^2\}\,ds$ .
Lemma 6.7: the map $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8: the first variation $\frac{d}{ds}\mathsf P(\gamma+s\delta)|_{s=0+}=\frac12\int_0^1\xi''\delta\,(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t)\,dt$ .
Lemma 6.9: $S(\gamma)$ is a countable disjoint union of intervals.
Corollary 6.10: $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\}=t$ on $\overline S(\gamma_*)$ and $\ge t$ off it.
Corollary 6.11: $\xi''(t)\,\mathbb E\{\partial_x^2\Phi^{\gamma_*}(t,X_t)^2\}=1$ on $\overline S(\gamma_*)$ .
Lemma 6.12: the law of $X_t$ has a density, bounded below on compact sets, once $\gamma$ vanishes.

Significance

The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows $\gamma_*$ through incremental steps whose size is set by $\gamma_*$ , and it needs no special treatment of gaps where $\gamma_* = 0$ . The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over $\mathscr L$ the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing $\inf_{\mathscr L}\mathsf P$ with the Parisi value.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).

Difficulty

Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating $\Phi^\gamma(0,0)$ in $\gamma$ requires comparing the SDE for $\gamma$ with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on $\partial_x^2\Phi$ that degenerate as $t\to1$ . The second is the exclusion of gaps: on an interval where $\gamma_*=0$ the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of $X_t$ to charge every interval (Lemma 6.12). The obvious idea of perturbing $\gamma_*$ upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.

Formalization scope

Conventions committed to in Lean:

The mixture is a coefficient sequence $c$ with $c_0=c_1=0$ ; $\xi,\xi',\xi''$ are explicit series.
Order parameters are functions $\mathbb R\to\mathbb R$ read only on $[0,1)$ . Membership in $\mathscr L$ uses eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.
$\Phi^\gamma$ for step functions is the Cole–Hopf recursion (7.3). For a piece with $\gamma_i = 0$ the formula's limit, the heat semigroup, is used instead of a division by zero. $\mathbb E$ over $G$ is integration against gaussianReal 0 1. For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is a limit along the filter of step functions converging in the weighted $L^1$ distance; it is never "some solution of the PDE".
$\partial_x\Phi$ and $\partial_x^2\Phi$ are iterated derivs in $x$ . Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.
The SDE uses the published strong-solution concept EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time $1$ . The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about $X$ hold for every strong solution, which by Lemma 6.5 is unique.
Section 6.1's results are stated for every admissible $f_0$ ; $\mathsf P$ is parametrized by $f_0$ , and Theorem 5 fixes $f_0=|\cdot|$ .
Minimality is " $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma\in\mathscr L$ ", never a real infimum. $\overline S(\gamma)$ is closure (S γ) ∩ Ico 0 1. Right-continuity of $\gamma_*$ , the paper's convention from p. 28, is a hypothesis.
Disclosed hypothesis $\xi\not\equiv0$ (some $c_k\neq0$ ) on Theorem 5, Corollaries 6.10–6.11 and Lemma 6.12. For $\xi\equiv0$ every $\gamma$ minimizes $\mathsf P$ and $X\equiv0$ , so $\gamma_*\equiv0$ has empty support and each of those statements fails. When $c_2=0$ no minimizer exists (Corollary 6.11 at $t=0$ ), and Theorem 5 is vacuous, as in the paper.
Lemma 6.12's density bound is stated without choosing density versions: $\varepsilon\,\mathrm{Leb}(A)\le\mathbb P(X_t\in A)$ for measurable $A\subseteq[-M,M]$ .

A trivializing formalization is excluded: $\Phi^\gamma$ and $X$ are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over $\mathscr L$ cannot be satisfied by a junk infimum.

Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.

Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on $\gamma$ , the Parisi functional on $\mathscr L$ , and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of $\Phi^\gamma$ are welcome as supporting lemmas.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Annals of Probability, 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proceedings of the AMS, 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Annals of Mathematics 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Annals of Mathematics 177(1), 2013. https://doi.org/10.4007/annals.2013.177.1.8

22 thms1 active userReviewed

Mathematical Physics Optimization Partial Differential Equations+1·Captain: mikedeng1

Optimization of Mean-field Spin Glasses II: Under No Overlap Gap, the Monotone Parisi Minimizer Also Minimizes the Extended FunctionalResearch Paper

Motivation

The mixed $p$ -spin model is a random polynomial on the hypercube $\{-1,+1\}^N$ : a centered Gaussian process $H_N(\boldsymbol\sigma)$ with covariance $\mathbb E\{H_N(\boldsymbol\sigma)H_N(\boldsymbol\sigma')\} = N\xi(\langle\boldsymbol\sigma,\boldsymbol\sigma'\rangle/N)$ . Its maximum $\mathrm{OPT}_N = \max_{\boldsymbol\sigma} H_N(\boldsymbol\sigma)/N$ is a canonical random optimization problem; for $\xi(t) = c_2^2t^2$ it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that $\mathrm{OPT}_N$ converges almost surely to the infimum of the zero-temperature Parisi functional $\mathsf P$ over a space $\mathscr U$ of non-decreasing order parameters.

El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space $\mathscr L$ of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ . The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over $\mathscr U$ can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure $p$ -spin models with $p \ge 3$ . This mission formalizes that equality, stated as a property of the minimizer.

Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed $p$ -spin models and introduced the extended principle over $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ , with derivatives $\xi'$ and $\xi''$ given by the termwise series. Order parameters are functions $\gamma : [0,1) \to \mathbb R_{\ge0}$ , in one of two spaces:

\mathscr U = \Big\{\gamma \text{ non-decreasing},\ \int_0^1\gamma(t)\,dt < \infty\Big\},\qquad \mathscr L = \Big\{\|\xi''\gamma\|_{TV[0,t]} < \infty\ \forall t<1,\ \int_0^1\xi''(t)\gamma(t)\,dt < \infty\Big\}.

Here $\|\cdot\|_{TV[0,t]}$ is total variation on $[0,t]$ , and $\mathscr U \subseteq \mathscr L$ .

For a step function $\gamma = \sum_i \gamma_i \mathbb I_{[t_{i-1},t_i)}$ with $\gamma_i \ge 0$ (the space $\mathrm{SF}_+$ ), the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\big(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\big) = 0,\qquad \Phi(1,x) = |x|,

is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where $\gamma_i = 0$ . For general $\gamma \in \mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n \to \gamma$ in the weighted norm $\int_0^1\xi''|\gamma_n - \gamma|$ . The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

The process $X$ is the strong solution of $dX_t = \xi''(t)\gamma(t)\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ (Eq. (6.3)), driven by a standard Brownian motion $B$ .

Formalization targets

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

If $\gamma_* \in \mathscr U$ is strictly increasing on $[0,1)$ and $\mathsf P(\gamma_*) \le \mathsf P(\gamma)$ for every $\gamma \in \mathscr U$ , then

\mathsf P(\gamma_*) \le \mathsf P(\gamma)\qquad\text{for every }\gamma \in \mathscr L .

Since $\mathscr U \subseteq \mathscr L$ , this is the paper's main result 2 (p. 4), $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ under no overlap gap.

Milestones

Lemma 6.7 (p. 27): for $\gamma\in\mathscr L$ , $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8 (p. 27): the right derivative of $s\mapsto\mathsf P(\gamma+s\delta)$ at $0$ is $\frac12\int_0^1\xi''(t)\delta(t)\big(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t\big)\,dt$ , for admissible directions $\delta$ that vanish near $t = 1$ .
Lemma 6.15 (p. 33): under no overlap gap, $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\} = t$ for every $t\in[0,1)$ .
Convexity (Section 6.3, p. 34): $\mathsf P$ is convex on $\mathscr L$ .

Significance

The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a $(1-\varepsilon)$ -approximation of $\mathrm{OPT}_N$ in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in $\mathscr U$ is not binding.

Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of $\mathsf P$ on $\mathscr L$ . It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.

Difficulty

The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of $\mathsf P$ in directions that keep $\gamma_*+s\delta$ monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of $\mathsf P$ on $\mathscr L$ is not visible from the formula: $\Phi^\gamma(0,0)$ is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction $\gamma - \gamma_*$ , which is generally non-zero near $t = 1$ , where $\xi''\gamma$ may blow up. Proposition 6.8 as stated excludes such directions.

Formalization scope

Mixture. A coefficient sequence c : ℕ → ℝ with $c_0 = c_1 = 0$ and $\sum_k c_k^2(1+\varepsilon)^k < \infty$ for some $\varepsilon>0$ . $\xi'$ and $\xi''$ are explicit power series.
Order parameters. Functions $\mathbb R\to\mathbb R$ ; membership in $\mathscr U$ and $\mathscr L$ reads only $[0,1)$ . Total variation is eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).
Cole–Hopf. Step-function data $(m,t,a)$ with $m\ge1$ . The $\gamma_i = 0$ pieces use the heat semigroup, the limit of (7.3). The terminal condition is $|x|$ . Gaussian expectations are integrals against gaussianReal 0 1.
$\Phi^\gamma$ on $\mathscr L$ . limUnder of the Cole–Hopf values along step-function data converging to $\gamma$ in the weighted $L^1$ distance. $\partial_x$ is deriv in $x$ .
SDE. The published definition EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by $0$ after time $1$ . Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.
Minimality. Always attainment, $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma$ in the space, never a real infimum (which Lean sets to $0$ on unbounded sets).
Disclosed hypothesis. Lemma 6.15 assumes that some $c_k \ne 0$ . For $\xi\equiv0$ it is false: $\mathsf P\equiv0$ , $X\equiv0$ , and the left side is constant in $t$ . The goal does not need it.
Ruled out. A formalization that defines $\Phi^\gamma$ as an arbitrary weak solution of the PDE, or via a choice from an unproved existence statement, would make $\mathsf P$ unconstrained. It is not acceptable. Encoding the hypothesis on $\gamma_*$ as minimality over $\mathscr L$ would make the goal trivial.
Proof gaps in the source. Convexity of $\mathsf P$ on $\mathscr L$ is cited, not proved. The step from stationarity to the goal applies Proposition 6.8 outside its stated hypotheses. The statements are the paper's and are believed true.
Out of scope. The paper's algorithmic results (Theorems 2–4, Corollary 2.2) assert algorithms with complexity bounds in an informal computation model, and rest on a long state-evolution analysis. They are not part of this mission.

Contributions welcome: Cole–Hopf regularity (smoothness and the bound $|\partial_x\Phi|\le1$ ), the Lipschitz estimate in $\gamma$ that makes $\Phi^\gamma$ well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904v1
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144(7), 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Ann. Math. 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Ann. Math. 177(1), 2013. https://arxiv.org/abs/1112.1003

11 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

Convergence in law of the minimum of a branching random walk: The Minimum Centred at (3/2) ln n Converges to a Gumbel Law Shifted by the Derivative MartingaleResearch Paper

Motivation

A branching random walk is the simplest model of a population that both reproduces and moves: every particle dies and leaves a random cloud of children displaced relative to it. Its extreme particles control the speed of travelling waves in reaction–diffusion equations (the KPP/Fisher equation), the free energy of directed polymers on trees, the cover and hitting times of random walks on trees, and the maxima of log-correlated fields such as the two-dimensional Gaussian free field. The basic quantity is the position of the leftmost particle at time $n$ .

Timeline.

1974–1976: Hammersley, Kingman and Biggins prove the law of large numbers $M_n/n\to\gamma$ for the minimum.
1978–1983: Bramson shows that for branching Brownian motion the maximum, centred at $\sqrt2\,t-\frac{3}{2\sqrt2}\ln t$ , converges in law (Bramson 1983). Lalley and Sellke (1987, Ann. Probab. 15) identify the limit as a Gumbel law randomly shifted by the limit of the derivative martingale.
2004: Biggins and Kyprianou prove that the derivative martingale of a branching random walk converges to a limit that is non-trivial in the boundary case (Adv. Appl. Probab. 36).
2009: Hu and Shi (arXiv:math/0702799) and Addario-Berry and Reed (Ann. Probab. 37) find the logarithmic correction: $M_n-\frac32\ln n$ is tight. Bramson and Zeitouni (2009) obtain tightness around the median under tail assumptions.
2013: Aïdékon proves convergence in law of $M_n-\frac32\ln n$ for general non-lattice branching random walks, the result this mission formalizes (arXiv:1101.1810, Ann. Probab. 41 (2013)).

Setting

Let $\mathcal L$ be a point process on $\mathbb R$ : a random, possibly infinite, collection of points. Start one particle at $0$ . At time $1$ it dies and leaves children at the points of $\mathcal L$ ; each particle of generation $n$ then dies and leaves children at the points of an independent copy of $\mathcal L$ , translated to its own position. Vertices of the genealogical tree $\mathbb T$ (a Galton–Watson tree) are labelled by finite words $u=(i_0,\dots,i_{k-1})$ ; $|u|=k$ is the generation, $u_j$ the ancestor at generation $j$ , and $V(u)$ the position.

The paper works in the boundary case

\mathbf E\Big[\sum_{|x|=1}1\Big]>1,\qquad \mathbf E\Big[\sum_{|x|=1}e^{-V(x)}\Big]=1,\qquad \mathbf E\Big[\sum_{|x|=1}V(x)e^{-V(x)}\Big]=0,\tag{1.1}

and assumes throughout that $\mathcal L$ is non-lattice and that

\mathbf E\Big[\sum_{|x|=1}V(x)^2e^{-V(x)}\Big]<\infty,\qquad \mathbf E\big[X(\ln_+X)^2\big]<\infty,\qquad \mathbf E\big[\tilde X\ln_+\tilde X\big]<\infty,\tag{1.3–1.4}

with $X=\sum_{|x|=1}e^{-V(x)}$ and $\tilde X=\sum_{|x|=1}V(x)_+e^{-V(x)}$ . The objects of the main theorem are the minimum $M_n=\min\{V(x):|x|=n\}$ (with $\min\varnothing=+\infty$ ) and the derivative martingale

D_n=\sum_{|x|=n}V(x)e^{-V(x)},

which converges almost surely to a limit $D_\infty\ge0$ , strictly positive on non-extinction. A standard example: two children with i.i.d. normal displacements of mean and variance $2\ln2$ .

Formalization targets

Goal: Theorem 1.1

There is a constant $C^*\in(0,\infty)$ such that for every real $x$ ,

\lim_{n\to\infty}\mathbf P\Big(M_n\ge\tfrac32\ln n+x\Big)=\mathbf E\Big[e^{-C^*e^xD_\infty}\Big].

The constant is not specified numerically. It is the product $C_1c_0$ of the constants below.

Milestones, in the order the proof uses them

Many-to-one lemma (2.1): $\mathbf E_a[\sum_{|x|=n}g(V(x_1),\dots,V(x_n))]=\mathbf E_a[e^{S_n-a}g(S_1,\dots,S_n)]$ for a centred random walk $S$ .
Renewal function (2.13): the renewal function $R$ of the strict descending ladder heights of $S$ satisfies $R(x)/x\to c_0>0$ .
Corollary 3.2 and Proposition 1.2: for the walk killed below $0$ , $e^z\,\mathbf P(M_n^{\rm kill}<\frac32\ln n-z)\to C_1$ , uniformly for $z\in[A,\frac32\ln n-A]$ .
Global minimum bound: $\mathbf P(\exists u\in\mathbb T: V(u)\le-y)\le e^{-y}$ .
Corollary 3.5: $\mathbf P(M_n\le\frac32\ln n-y)\le(1+c_{10}(1+y))e^{-y}$ .
Proposition 4.1: $\frac{e^z}{z}\mathbf P(M_n<\frac32\ln n-z)\to C_1c_0$ , uniformly on the same window.
Derivative martingale: $D_n\to D_\infty$ a.s., $D_\infty\ge0$ , $D_\infty>0$ a.s. on non-extinction.
(5.2): $\sum_{u\in\mathcal Z[A]}V(u)e^{-V(u)}\to D_\infty$ a.s. as $A\to\infty$ , where $\mathcal Z[A]$ is the set of particles absorbed at level $A$ .

Significance

The theorem identifies the limit law of the extreme particle: $M_n-\frac32\ln n$ converges in law, on the event of survival, to a Gumbel variable shifted by $-\ln(C^*D_\infty)$ . It is the input for the study of the whole extremal process of the branching random walk seen from its leftmost particle (Madaule, J. Theoret. Probab., 2017), and it is the discrete-time counterpart of the Bramson and Lalley–Sellke results that later work on log-correlated fields takes as its template. The $\frac32$ correction and the role of the derivative martingale are the signature of the boundary case, and of log-correlated extremes generally.

The result is proved and published. It has not been formalized: Mathlib has no branching processes, no Galton–Watson trees with positions, no renewal theory, and no derivative martingale. This mission produces the first machine-checkable statement of the convergence-in-law theorem and of the intermediate results it rests on. A complete development would also give reusable formal versions of the many-to-one lemma and of renewal theory for ladder heights.

Difficulty

The first-moment computation through the many-to-one lemma gives the wrong centring. It predicts that the minimum sits near $\frac12\ln n$ , because the expected number of particles below a level is dominated by rare realisations. The true centring $\frac32\ln n$ only appears after restricting to particles whose ancestral path stays above a barrier, and this restriction requires random-walk estimates (ballot theorems and local limit theorems for walks conditioned to stay positive) that hold uniformly in a window of starting points. A second difficulty is that the limit must be identified, not only shown to exist. Tightness and subsequence arguments do not give the factor $D_\infty$ ; the identification needs the precise tail $C_1c_0\,z\,e^{-z}$ of Proposition 4.1, with a known constant, and the almost-sure behaviour of the sum over the stopping line $\mathcal Z[A]$ .

Formalization scope

Point process. The law $L$ of $\mathcal L$ is a probability measure on configurations $(N,p)\in\mathbb N_\infty\times(\mathbb N\to\mathbb R)$ , where the points are $p_i$ for $i<N$ .
Tree. Labels are List ℕ. The branching random walk is any family $(\xi_u)_{u}$ of independent measurable configurations of law $L$ on a probability space. Every theorem holds for every such realisation, and a canonical realisation exists (product space).
Assumptions. Every expectation in (1.1), (1.3), (1.4) is a lower Lebesgue integral of a $[0,\infty]$ -valued sum. The signed condition in (1.1) is "the expectations of $\sum V_+e^{-V}$ and $\sum V_-e^{-V}$ are equal and finite". Non-lattice means: there are no $a\in\mathbb R$ and $d>0$ with all points a.s. in $a+d\mathbb Z$ .
Which assumptions where. The goal and §§3–5 assume all of them. The many-to-one lemma and the global minimum bound assume only (1.1), and the derivative-martingale milestone drops non-lattice, as in Appendix A.
Minima and limits. $M_n$ and $M_n^{\rm kill}$ are extended reals, $+\infty$ on an empty generation, so extinction lies in $\{M_n\ge\frac32\ln n+x\}$ . $D_n$ is a real sum over generation $n$ , absolutely summable almost surely, and $D_\infty$ is its pointwise limit. The expectation in the goal is a lower integral of $e^{-C^*e^xD_\infty}\in(0,1]$ .
Constants. $C^*$ is chosen before $x$ . In Proposition 4.1, $C_1$ and $c_0$ are hypotheses tied to Proposition 1.2 and (2.13), not re-chosen. Corollaries 3.2 and 3.5 assert existence of their constants without Proposition 3.1 and Corollary 3.4.
Not trivial. A formalization with a real-valued $M_n$ equal to $0$ on extinction, a $D_\infty$ never shown to be the limit, or a $C^*$ depending on $x$ would not be this theorem. The definitions above rule out each of these.

Out of scope: the spine-measure lemmas (Lemmas 2.3, 3.3, 3.8–3.10, 4.3), Propositions 2.1–2.2 cited from Lyons, and Appendices B–C. Contributions are welcome on all milestones. The many-to-one lemma and the renewal statement are independent of the rest and are natural first targets.

Selected references

E. Aïdékon, Convergence in law of the minimum of a branching random walk, Ann. Probab. 41(3A) (2013) 1362–1426. arXiv:1101.1810, doi:10.1214/12-AOP750
J. D. Biggins, A. E. Kyprianou, Measure change in multitype branching, Adv. Appl. Probab. 36 (2004) 544–581. Reference [7] of Aïdékon (2013), arXiv:1101.1810, p. 68
M. Bramson, Convergence of solutions of the Kolmogorov equation to travelling waves, Mem. Amer. Math. Soc. 44, no. 285 (1983). doi:10.1090/memo/0285
S. P. Lalley, T. Sellke, A conditional limit theorem for the frontier of a branching Brownian motion, Ann. Probab. 15 (1987) 1052–1061. Reference [21] of Aïdékon (2013), arXiv:1101.1810, p. 69
Y. Hu, Z. Shi, Minimal position and critical martingale convergence in branching random walks, and directed polymers on disordered trees, Ann. Probab. 37 (2009) 742–789. arXiv:math/0702799
L. Addario-Berry, B. Reed, Minima in branching random walks, Ann. Probab. 37 (2009) 1044–1079. Reference [1] of Aïdékon (2013), arXiv:1101.1810, p. 68
R. Lyons, A simple path to Biggins' martingale convergence for branching random walk, in Classical and Modern Branching Processes, IMA Vol. Math. Appl. 84 (1997) 217–221. Reference [22] of Aïdékon (2013), arXiv:1101.1810, p. 69

13 thms1 active userReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications 3: The Continuation Region Widens as the Fixed Intervention Cost GrowsResearch Paper

Motivation

In an impulse control problem a controller does not steer a process continuously: at times of its choosing it shifts the state by a finite jump, paying a fixed cost plus a cost proportional to the jump. Such models describe central-bank interventions on an exchange rate, inventory replenishment and cash management. Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) study nonzero-sum games in which two players control the same diffusion by impulses. They prove a verification theorem for such games and apply it to a linear game whose Nash equilibria are explicit.

The paper's interpretation of the linear game is two central banks with different targets for an exchange rate. An explicit equilibrium gives explicit intervention thresholds, and Section 4.4 of the paper asks how these thresholds respond to the fixed cost of intervening. This mission formalizes that comparative-statics question: when intervening becomes more expensive, do the players intervene less?

Setting

The game of Section 4.1 has a discount rate $\rho > 0$ , a volatility $\sigma > 0$ , running payoffs $f_1(x) = x - s_1$ and $f_2(x) = s_2 - x$ with $s_1 < s_2$ , and intervention costs: a player who shifts the state by $\delta$ pays $c + \lambda|\delta|$ and the opponent receives $\tilde c + \tilde\lambda|\delta|$ . The standing assumptions of the section are

c \ge \tilde c \ge 0,\qquad \lambda \ge \tilde\lambda \ge 0,\qquad (c,\lambda) \ne (\tilde c,\tilde\lambda),\qquad 1 - \lambda\rho > 0 .

All parameters except the fixed cost $c$ are held fixed. Set $\theta = \sqrt{2\rho/\sigma^2}$ and $\eta = (1-\lambda\rho)/\rho$ , both positive. For $c > 0$ the function

F_c(y) = 2y + \theta c - \eta\log\frac{\eta + y}{\eta - y},\qquad y \in (0,\eta),

has a unique zero $\xi(c) \in (0,\eta)$ . With

\Gamma(c) = \frac{\theta(c-\tilde c)}{4\xi(c)} + \frac{\theta c(\lambda-\tilde\lambda)}{4\eta\,\xi(c)} + \frac{\lambda-\tilde\lambda}{2\eta}

and a parameter $\tilde s \in \mathbb R$ , the paper's formulas (4.20) are

\bar x_i(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta+\xi}{\eta-\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],\qquad x_i^*(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta-\xi}{\eta+\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],

for $i \in \{1,2\}$ , with $\xi = \xi(c)$ and $\Gamma = \Gamma(c)$ . In the Nash equilibrium of the paper's Proposition 4.7, player 1 intervenes when the state falls below $\bar x_1$ and moves it to $x_1^*$ ; player 2 intervenes above $\bar x_2$ and moves it to $x_2^*$ . The interval $]\bar x_1(c), \bar x_2(c)[$ is the continuation region, where nobody intervenes. The equilibrium payoffs $V_1^c$ , $V_2^c$ are explicit as well (4.27).

Formalization targets

Goal: Proposition 4.13

c \mapsto \bar x_2(c)\ \text{is strictly increasing and}\ c \mapsto \bar x_1(c)\ \text{is strictly decreasing on}\ ]\tilde c, +\infty[ .

The continuation region therefore widens strictly as the fixed cost grows. The statement concerns the explicit functions (4.20); that they are equilibrium thresholds is mission 2 of this series.

Milestones

(4.17). For $c > 0$ , $\xi(c)$ is the unique zero of $F_c$ in $(0,\eta)$ .
(4.28). $\xi \in C^\infty(]0,\infty[)$ with $\xi' = \frac\theta2\frac{\eta^2-\xi^2}{\xi^2}$ and $\xi'' = -\theta\eta^2\frac{\xi'}{\xi^3} = -\frac{\theta^2\eta^2}{2}\frac{\eta^2-\xi^2}{\xi^5}$ .
(4.29). $\xi$ , $c/\xi$ and $c\,\xi'$ tend to $0$ as $c \to 0^+$ ; $c(\eta-\xi) \to 0$ and $\xi \to \eta$ as $c \to +\infty$ .
Proposition 4.12. As $c \to +\infty$ , $\bar x_2, x_1^* \to +\infty$ , $\bar x_1, x_2^* \to -\infty$ , and pointwise $V_1^c(x) \to (x-s_1)/\rho$ , $V_2^c(x) \to (s_2-x)/\rho$ .
Proposition 4.14 (with a corrected hypothesis, below). If $\tilde c = 0$ , then $x_2^*$ is strictly decreasing and $x_1^*$ strictly increasing on $]0,\infty[$ ; if moreover $\lambda = \tilde\lambda$ , then $x_2^*(c) < \tilde s < x_1^*(c)$ for all $c > 0$ .

Significance

Proposition 4.13 is the rigorous form of the economic intuition that costlier intervention makes players more patient. Together with Proposition 4.12 it describes the whole range of costs: the region of inaction grows strictly and invades the real line as $c \to \infty$ , where the payoffs converge to those of the uncontrolled Brownian motion. Proposition 4.14 adds that, when the fixed gain vanishes, the targets $x_i^*$ move away from the centre $\tilde s$ . The paper's numerical section shows that without $\tilde c = 0$ the targets need not be monotone.

The results are proved in the paper, in a few lines each, by differentiating the implicit function $\xi(c)$ . None of them is formalized. The mission produces a machine-checked treatment of a parametrised implicit function, $c \mapsto \xi(c)$ defined by a transcendental equation: smoothness, explicit derivatives, and the asymptotics at both ends. On top of it, it gives a fully verified comparative-statics result for an explicit game equilibrium.

Difficulty

The thresholds depend on $c$ only through $\xi(c)$ , which has no closed form, and through $\Gamma(c)$ , a sum of terms in $c/\xi(c)$ and $1/\xi(c)$ . Monotonicity of $\xi$ alone does not settle the goal: $c/\xi(c)$ is a ratio of two increasing functions, and its direction is decided by how fast $\xi$ grows compared with $c$ , uniformly on $]\tilde c,\infty[$ , including near $c = 0$ , where $F_0$ has no zero and $\xi$ degenerates. The limits as $c \to +\infty$ need more than $\xi(c) \to \eta$ : $\Gamma(c)$ grows linearly in $c$ , so the rate at which $\eta - \xi(c)$ decays decides whether the targets $x_i^*$ diverge and whether the payoff coefficients vanish.

Formalization scope

The parameters $\rho, \sigma, \lambda, \tilde\lambda, \tilde c, \tilde s, s_1, s_2$ are bundled in a structure, and the standing assumptions not involving $c$ in a predicate $\rho > 0$ , $\sigma > 0$ , $s_1 < s_2$ , $\tilde c \ge 0$ , $\lambda \ge \tilde\lambda \ge 0$ , $1 - \lambda\rho > 0$ . $\theta$ and $\eta$ are computed from $\rho, \sigma, \lambda$ as in (4.21), not taken as free parameters. All quantities are real numbers.

$\xi(c)$ is defined as $\sup\{y \in (0,\eta) : F_c(y) \ge 0\}$ . Milestone 1 proves that this is the paper's unique zero for every $c > 0$ . For $c \le 0$ the set is empty and the definition returns the placeholder $0$ . Every statement therefore restricts $c$ to $c > 0$ , to $c > \tilde c$ , or to $c \to +\infty$ , and no statement can be satisfied through a junk value. On $]\tilde c, \infty[$ one has $\Gamma > 0$ , so the square roots in (4.20) are the paper's. "Increasing" and "decreasing" are read strictly, as the proofs give. $C^\infty$ is ContDiffOn ℝ ∞, and $\xi'$ is deriv ξ. Limits at $0^+$ use the right neighbourhood filter.

Two departures from the page are disclosed in the items:

$c > 0$ in (4.17). The standing assumptions allow $c = 0$ when $\tilde c = 0$ and $\lambda > \tilde\lambda$ , but then $F_0$ has no zero; the paper's argument uses $F(0^+) = \theta c > 0$ .
$\lambda = \tilde\lambda$ in the last sentence of Proposition 4.14. For $\lambda > \tilde\lambda$ , Proposition 4.11 gives $x_2^*(0^+) > \tilde s$ and the inequality $x_2^* < \tilde s$ fails for small $c$ . The monotonicity claims keep the hypothesis $\tilde c = 0$ alone.

A complete development needs the intermediate value theorem and strict monotonicity on an interval, a differentiable implicit (or inverse) function theorem in one variable, and asymptotic estimates of $\log\frac{\eta+y}{\eta-y}$ near $0$ and near $\eta$ . These one-variable lemmas about implicitly defined functions are reusable beyond this mission. Proofs of the milestones in any order are welcome.

Selected references

R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 — accepted manuscript arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039

7 thms1 active userReviewed

Algorithmic Game Theory Control Theory Operations Research+1·Captain: mikedeng1

Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications 1: Regular Solutions of the Quasi-Variational Inequalities Give Nash Equilibrium PayoffsResearch Paper

Motivation

Many economic and engineering systems are steered by agents who act at discrete instants rather than continuously: a central bank intervenes on an exchange rate, two energy producers adjust a shared stock, a firm rebalances inventory. Each action has a fixed cost, so continuous control is not realistic. The mathematical model is impulse control: the state follows a diffusion, and a controller may shift it at chosen stopping times by paying a cost. The single-controller theory is classical (Øksendal and Sulem, Applied Stochastic Control of Jump Diffusions, 2007). When two controllers with different objectives act on the same state, the result is a nonzero-sum stochastic differential game with impulse controls.

Before Aïd, Basei, Callegaro, Campi and Vargiolu, the literature on games with impulse controls was almost entirely zero-sum: Cosso (SIAM J. Control Optim., 2013) characterised the value of zero-sum impulse games through a double-obstacle quasi-variational inequality in the viscosity sense. Their paper (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) gives the first general formulation of the nonzero-sum case together with a verification theorem: a system of quasi-variational inequalities (QVIs) whose sufficiently regular solutions are the equilibrium payoffs. Its Section 4 then computes Nash equilibria in closed form for a one-dimensional game.

Setting

A $k$ -dimensional Brownian motion $W$ on a filtered probability space satisfying the usual conditions drives the state equation

dY_s=b(Y_s)\,ds+\sigma(Y_s)\,dW_s ,\qquad Y_s\in\mathbb R^d,

with globally Lipschitz $b$ and $\sigma$ . The game takes place in an open set $S\subseteq\mathbb R^d$ and ends at the exit time $\tau_S$ of the state from $S$ . Each of two players $i\in\{1,2\}$ has a nonempty impulse set $Z_i\subseteq\mathbb R^{l_i}$ and a continuous impulse map $\Gamma^i:S\times Z_i\to S$ : an intervention with impulse $\delta$ moves the state from $y$ to $\Gamma^i(y,\delta)$ .

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$ with $\mathcal C_i\subseteq S$ open and $\xi_i:S\to Z_i$ continuous. Player $i$ intervenes as soon as the state leaves $\mathcal C_i$ , with impulse $\xi_i(y)$ at the current state $y$ . Player 1 has priority on ties, and several interventions may happen at the same instant. This defines the controlled process $X$ , the intervention times $\tau_{i,n}$ and impulses $\delta_{i,n}$ of each player, and the states $X_{(\tau_{i,n})^-}$ just before each intervention. The payoff of player $i$ is

J^i(x;\varphi_1,\varphi_2)=\mathbb E\Big[\int_0^{\tau_S}e^{-\rho_is}f_i(X_s)ds+\sum_{\tau_{i,n}<\tau_S}e^{-\rho_i\tau_{i,n}}\phi_i(X_{(\tau_{i,n})^-},\delta_{i,n})+\sum_{\tau_{j,n}<\tau_S}e^{-\rho_i\tau_{j,n}}\psi_i(X_{(\tau_{j,n})^-},\delta_{j,n})+e^{-\rho_i\tau_S}h_i(X_{\tau_S})\mathbf 1_{\{\tau_S<\infty\}}\Big],

where $j\ne i$ , $\rho_i>0$ , $f_i$ is a running payoff, $\phi_i$ the cost of one's own interventions, $\psi_i$ the gain from the opponent's, and $h_i$ a terminal payoff on $\partial S$ . A pair of strategies is $x$ -admissible, $(\varphi_1,\varphi_2)\in\Phi_x$ , when these four terms are integrable, $\sup_{s\le\tau_S}|X_s|$ has all moments, and the interventions do not accumulate before $\tau_S$ . A Nash equilibrium is a pair in $\Phi_x$ from which no player gains by a unilateral admissible deviation.

Given candidate payoff functions $V_1,V_2$ on $\bar S$ , let $\delta_i(x)$ be the unique maximiser of $V_i(\Gamma^i(x,\delta))+\phi_i(x,\delta)$ over $Z_i$ . Define $\mathcal M_iV_i(x)=V_i(\Gamma^i(x,\delta_i(x)))+\phi_i(x,\delta_i(x))$ , $\mathcal H_iV_i(x)=V_i(\Gamma^j(x,\delta_j(x)))+\psi_i(x,\delta_j(x))$ , the continuation region $\mathcal D_i=\{\mathcal M_iV_i-V_i<0\}$ and the generator $\mathcal AV=b\cdot\nabla V+\tfrac12\operatorname{tr}(\sigma\sigma^tD^2V)$ . The QVI system is

V_i=h_i\ \text{on }\partial S,\quad \mathcal M_jV_j-V_j\le0\ \text{on }S,\quad \mathcal H_iV_i-V_i=0\ \text{on }\{\mathcal M_jV_j=V_j\},\quad \max\{\mathcal AV_i-\rho_iV_i+f_i,\ \mathcal M_iV_i-V_i\}=0\ \text{on }\mathcal D_j .

Formalization targets

Goal: Theorem 3.3 (verification theorem)

Suppose $V_1,V_2$ solve the QVI system, $V_i\in C^2(\mathcal D_j\setminus\partial\mathcal D_i)\cap C^1(\mathcal D_j)\cap C(\bar S)$ with polynomial growth, $\partial\mathcal D_i$ is a Lipschitz surface near which $V_i$ has locally bounded first and second derivatives, $x\in S$ , and the threshold pair $\varphi_i^*=(\mathcal D_i,\delta_i)$ is $x$ -admissible. Then

(\varphi_1^*,\varphi_2^*)\ \text{is a Nash equilibrium and}\quad V_i(x)=J^i(x;\varphi_1^*,\varphi_2^*),\qquad i=1,2 .

Milestones

Lemma 2.3: the controlled process is the concatenation of diffusion pieces, it jumps only at interventions, and between interventions it stays in $\mathcal C_1\cap\mathcal C_2$ .
Remark 3.6, (3.8b), (3.8d), (3.8f): against $\varphi_2^*$ , the state stays in $\mathcal D_2$ , and player 2 intervenes only on $\{\mathcal M_2V_2=V_2\}$ with impulse $\delta_2$ .
Step 1 of the proof: $V_1(x)\ge J^1(x;\varphi_1,\varphi_2^*)$ for every admissible deviation $\varphi_1$ .
Step 2 of the proof: $V_1(x)=J^1(x;\varphi_1^*,\varphi_2^*)$ .

The goal follows from Steps 1 and 2 and their mirror images for player 2.

Significance

The theorem turns the search for Nash equilibria of nonzero-sum impulse games, an infinite-dimensional fixed-point problem over strategy pairs, into a deterministic problem: find functions satisfying a system of coupled QVIs with prescribed regularity. The regularity conditions become smooth-pasting conditions, hence a system of algebraic equations; Section 4 of the paper solves it explicitly for a one-dimensional game with linear payoffs. A further consequence is structural: equilibrium payoffs need only be $C^2$ on the opponent's continuation region, which is what lets non-smooth, piecewise-defined candidates qualify.

The result is proved in the paper; no machine-checked version exists. A complete formalization would be the first verified verification theorem for impulse control, single-player or game, and would expose every convention of the model: priority on ties, simultaneous interventions, the treatment of exit, and the integrability of the payoff. Several of these conventions need correction on the page, as listed below.

Difficulty

The heuristic argument applies Itô's formula to $e^{-\rho_1t}V_1(X_t)$ and uses the QVIs term by term. This fails on two counts. First, $V_1$ is only $C^1$ across the free boundary $\partial\mathcal D_1$ , so Itô's formula does not apply directly. The paper mollifies $V_1$ (following Øksendal's proof of his verification theorem for optimal stopping) and must control the second derivatives near a Lipschitz boundary. Second, the sums over interventions may be infinite and the horizon unbounded, so expectations and limits do not commute. The passage to the limit needs the integrability built into $\Phi_x$ and the polynomial growth of $V_i$ . The stochastic-calculus infrastructure itself (Itô's formula for continuous semimartingales stopped at random times, strong solutions of Lipschitz SDEs restarted at stopping times) is largely missing from Mathlib.

Formalization scope

The Lean model is pathwise. A realization is a sequence of diffusion pieces, each solving the state equation from the random restart time with the restart value. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and the stochastic basis uses the published You2015.Shared.UsualConditions and IsFBrownian. Times take values in $[0,\infty]$ with $e^{-\rho\cdot\infty}=0$ , and the state space is EuclideanSpace ℝ (Fin d). $\Phi_x$ asks for one admissible realization, while the Nash inequalities and the payoff identity hold on every admissible realization; strong uniqueness makes these readings equivalent.

The following deviate from the page and are disclosed in the items:

$\delta_i$ is assumed continuous, so that $\varphi_i^*$ is a strategy.
The fourth QVI is imposed on $\mathcal D_j\setminus\partial\mathcal D_i$ , where $\mathcal AV_i$ exists.
The exit time is $\alpha^S_{\bar k+1}$ , not the printed $\alpha^S_{\bar k}$ .
The gain term of (2.7) is read with the opponent's interventions.
The supremum in (2.8) is taken over $[0,\tau_S]$ .
Interventions accumulating at a finite $\tau_S$ are excluded from $\Phi_x$ , since the page leaves $X_{\tau_S}$ undefined there.
Lemma 2.3 is stated in corrected form for simultaneous and boundary interventions.

The payoff is a Bochner expectation only inside $\Phi_x$ , which requires the $L^1$ conditions of (2.7) and the integrability of each payoff. A non-integrable deviation therefore never receives the junk payoff $0$ , and the Nash inequality cannot hold vacuously.

Contributions are welcome on the stochastic-calculus layer this needs (Itô's formula, strong existence and uniqueness for Lipschitz SDEs, optional stopping for stochastic integrals) and on the mollification lemma for functions that are $C^1$ with piecewise bounded second derivatives across a Lipschitz surface. These are reusable well beyond this mission.

Selected references

R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-sum stochastic differential games with impulse controls: a verification theorem with applications, Math. Oper. Res. 45(1), 2020 (accepted manuscript, arXiv:1605.00039v4). https://arxiv.org/abs/1605.00039
A. Cosso, Stochastic differential games involving impulse controls and double-obstacle quasi-variational inequalities, SIAM J. Control Optim. 51(3), 2102–2131, 2013.
B. Øksendal, Stochastic Differential Equations, 6th ed., Springer, 2003. https://doi.org/10.1007/978-3-642-14394-6
B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69826-5

9 thms1 active userReviewed

Completed

Combinatorics·Captain: mysticflounder

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

The Schur number $S(n)$ is the largest $N$ such that $[1, N] = \{1, \dots, N\}$ can be partitioned into $n$ sumfree sets, sets with no $x, y, z$ such that $x + y = z$ ( $x = y$ allowed). Schur's argument gives $S(n) \le R_n(3) - 2$ , where the triangle Ramsey number $R_n(3)$ is the least $N$ such that every colouring of the edges of $K_N$ with $n$ colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known (Heule 2018). For six colours the published range is $536 \le S(6) \le 1836$ ; the upper bound is $R_6(3) - 2$ with $R_6(3) \le 1838$ (DS1, rev. 18).

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and $R_{n+1}(3) \le (n+1)(R_n(3) - 1) + 2$ (Theorem 6) (doi).
1961: Baumert finds $S(4) = 44$ by computer, as reported by Fredricksen and Sweet; they and Heule cite Golomb–Baumert 1965 for it.
1973: Chung proves $R_4(3) \ge 51$ (doi).
1997: Wan bounds $R_n(3)$ and, for even $n \ge 6$ , states $S_n < n!\,(e - e^{-1} + 3)/2 - n + 2$ (zbMATH 0882.05095 summary; doi). If his $S_n$ is the least $N$ that forces a monochromatic solution, this is the centred bound below, applied to his own bound on $R_{n-1}(3)$ ; if it is the largest $N$ , it is $1$ above it. His proof was not read.
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, which also lists $R_5(3) \le 307$ ).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (AAAI-18; preprint arXiv:1711.08076).
2026: a public repository of M. Tatarevic gives a computer-assisted argument for $R_4(3) \le 61$ . Its Lean development assumes that a family of 56,830 SAT instances is unsatisfiable, and the repository records solver results for them. The project of this mission's author produced LRAT certificates for all 56,830 instances and checked them; the report is in the repository's issue tracker. This mission does not depend on it.

The first target is a centred-interval bound: if $R_k(3) \le r$ , then $S(k+1) \le 2(k+1)\lfloor (r-1)/2 \rfloor + 1$ . With $R_4(3) \le 61$ the recursive bound gives $R_5(3) \le 302$ , and the centred bound gives $S(6) \le 1801$ ; with $R_5(3) \le 307$ it gives only $1837$ . The mission formalizes what a Schur colouring of $[1, 1801]$ with six colours would have to look like under $R_4(3) \le 61$ .

Setting

All numbers are natural numbers, $\mathbb{N} = \{0, 1, 2, \dots\}$ , and $[a, b] = \{a, \dots, b\}$ .

Schur colourings and covers. A colouring with $n$ colours is a map $c : \mathbb{N} \to \mathrm{Fin}\,n$ . It is a Schur colouring of $[1, N]$ (SchurColoring N c) if there are no $x, y \ge 1$ with $x + y \le N$ and $c(x) = c(y) = c(x + y)$ , the case $x = y$ included. The cover form uses SumFree S and CoveredBySumFree X n ( $X$ lies in the union of $n$ sumfree sets); for $n \ge 1$ the two bridge theorems pass between the two forms in both directions.

Triangle Ramsey property. $\mathrm{TR}(k, r)$ (TriangleRamsey k r): every colouring with at most $k$ colours of the pairs $x < y$ of a finite set of at least $r$ naturals has a monochromatic triangle. For $k \ge 1$ it is the inequality $R_k(3) \le r$ .

Neighbourhoods. The difference colouring gives a pair $\{x, y\}$ the colour $c(|x - y|)$ . For a Schur colouring of $[1, N]$ it has no monochromatic triangle on $[0, N]$ , since $(y - x) + (z - y) = z - x$ . Write

$\Gamma_i(V, v) = \{\, w \in V : w \ne v,\ c(|v - w|) = i \,\}$ (colorNbhd c V v i);
$V_m = \Gamma_{c(m+1)}([0, 2m+1], m)$ , the central neighbourhood (centralNbhd c m), which contains $2m + 1$ ;
$P_i = \Gamma_i(V_m, 2m+1)$ , the endpoint neighbourhoods (endpointNbhd c m i).

The frontier. The frontier hypotheses are $\mathrm{TR}(k, u + 1)$ , $2t = (k+1)u$ , $m = (k+2)t$ , and $c$ a Schur colouring of $[1, 2m + 1]$ with $k + 2$ colours. From the first two, $\mathrm{TR}(k + 1, 2t + 2)$ holds, and the centred bound excludes Schur colourings of $[1, 2m + 2]$ with $k + 2$ colours; $[1, 2m + 1]$ is the frontier interval. Six colours: $k = 4$ , $u = 60$ , $t = 150$ , $m = 900$ , $2m + 1 = 1801$ .

Example. For $k = 1$ , $u = 2$ , $t = 2$ , $m = 6$ (and $13 = S(3)$ ), the classes $\{1, 4, 7, 10, 13\}$ , $\{2, 3, 11, 12\}$ , $\{5, 6, 8, 9\}$ form a Schur colouring of $[1, 13]$ , with $V_6 = \{2, 5, 7, 10, 13\}$ and endpoint neighbourhoods $\{2, 10\}$ and $\{5, 7\}$ , both closed under $x \mapsto 12 - x$ .

Formalization targets

Goal: six colours under $R_4(3) \le 61$

\mathrm{TR}(4, 61) \ \text{ and } \ c \text{ a Schur colouring of } [1, 1801] \text{ with six colours} \implies (1)\text{–}(5),

where $q = c(901)$ , $V = V_{900}$ and $P_i = \Gamma_i(V, 1801)$ :

each colour occurs $150$ times in $[1, 900]$ ;
$|V| = 301$ ;
$|\Gamma_i(V, v)| = 60$ for every $v \in V$ and every colour $i \ne q$ ;
$c(901 - d) = c(901 + d)$ for every $d \in [1, 900]$ with $c(d) = q$ ;
for every colour $i \ne q$ : $|P_i| = 60$ ; $x \mapsto 1800 - x$ maps $P_i$ to itself without fixed points; and $c(|x - y|) \notin \{i, q\}$ for distinct $x, y \in P_i$ .

The goal is a structure theorem under the hypothesis $R_4(3) \le 61$ . It does not prove $S(6) \le 1800$ , and it does not assert that a Schur colouring of $[1, 1801]$ with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.

Centred-interval bound

\mathrm{TR}(k, r) \implies \Bigl[1,\ 2(k+1)\Bigl\lfloor \tfrac{r-1}{2} \Bigr\rfloor + 2\Bigr] \text{ is not covered by } k + 1 \text{ sumfree sets.}

Balanced colour classes

\mathrm{TR}(k, 2t + 2),\ m = (k+1)t,\ c \text{ a Schur colouring of } [1, 2m+1] \text{ with } k + 1 \text{ colours} \implies \bigl|\{\, d \in [1, m] : c(d) = j \,\}\bigr| = t \ \text{ for every colour } j.

Nested saturation

\text{frontier hypotheses} \implies |\Gamma_i(V_m, v)| = u \qquad (v \in V_m,\ i \ne c(m+1)).

Automorphism extension

For a colouring $\mathrm{col}$ of ordered pairs, a finite set $W$ , a point $e \notin W$ and a map $J$ with $J(W) \subseteq W$ , $J \circ J = \mathrm{id}$ on $W$ and $\mathrm{col}(J(x), J(y)) = \mathrm{col}(x, y)$ on $W$ :

v \in W \text{ and } J(v) \text{ have equal colour degrees in } W \cup \{e\} \implies \mathrm{col}(v, e) = \mathrm{col}(J(v), e).

Forced reflection

\text{frontier hypotheses} \implies c(m + 1 - d) = c(m + 1 + d) \qquad (d \in [1, m],\ c(d) = c(m+1)).

The saturation degree is even

\text{frontier hypotheses} \implies u \text{ is even}.

Significance

The result itself. Under $R_4(3) \le 61$ , $S(6) \le 1801$ , and the goal constrains a six-colour Schur colouring of $[1, 1801]$ as listed above. In particular, each of its five endpoint neighbourhoods is a set of $30$ pairs $\{900 - d, 900 + d\}$ whose difference colouring uses at most four colours, is invariant under $x \mapsto 1800 - x$ and, like that of every subset of $[0, 1801]$ , has no monochromatic triangle. So such a colouring yields five colourings of $K_{60}$ with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give $S(6) \le 1800$ under the same hypothesis. Whether it can occur, and whether $S(6) \le 1800$ , are open.

Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. $R_4(3) \le 61$ is not formalized in the mission.

Difficulty

The centred bound counts, for one colour class, the points $h \pm a$ around the centre of the interval. At the frontier every such count is tight: each colour has $t$ elements in $[1, m]$ , and inside $V_m$ each colour other than $c(m+1)$ has degree $u$ , the largest value that $R_k(3) \le u + 1$ allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd $u$ ; at six colours $u = 60$ .

The reflection is not a property of Schur colourings in general: the colouring $\{1, 4\}$ , $\{2, 3\}$ , $\{5\}$ of $[1, 5]$ has $c(2) = c(3)$ but $c(1) \ne c(5)$ . At the frontier the theorem asserts it only for the $d$ with $c(d) = c(m+1)$ , so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: $S(5) = 160$ already needed a large certified SAT computation (Heule 2018), and $[1, 1801]$ with six colours is a much larger instance.

Formalization scope

Colourings are functions ℕ → Fin n on all of $\mathbb{N}$ ; SchurColoring N c constrains only $[1, N]$ , with $x = y$ allowed. Distances are Nat.dist.
Neighbourhoods are Finsets. $V_m$ lies in range (2 * m + 2) $= [0, 2m+1]$ , so the point $0$ is a candidate member; the centre $m$ never is.
TriangleRamsey k r takes colours from any Finset of at most $k$ naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs $x < y$ of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.
Covers. CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in $X$ .
Subtraction is truncated. Under the hypotheses, none of $r - 1$ , $N - 1$ , $m + 1 - d$ , $2m - x$ (with $x \in P_i$ ), $901 - d$ and $1800 - x$ truncates.
No trivialization. The frontier theorems are vacuous for $u = 0$ , and for $k = 0$ (then $[1, 2m + 1] \supseteq [1, 5]$ , while $S(2) = 4$ ). For $k = 1$ they are not: the Schur colourings of $[1, 13]$ meet the hypotheses, and every conclusion can be checked by hand. The goal holds vacuously if $R_4(3) > 61$ or if no six-colour Schur colouring of $[1, 1801]$ exists; it is a structure theorem, not a claim that such a colouring exists.

Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every $k$ , and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired $60$ -point sets exists.

Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.

Selected references

R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
S. W. Golomb, L. D. Baumert, Backtrack programming, J. ACM 12 (1965) 516–524. https://doi.org/10.1145/321296.321300
F. R. K. Chung, On the Ramsey numbers $N(3, 3, \dots, 3; 2)$ , Discrete Math. 5 (1973) 317–321. https://doi.org/10.1016/0012-365X(73)90125-8
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI Conf. Artif. Intell. 32 (2018). https://doi.org/10.1609/aaai.v32i1.12209 ; preprint arXiv:1711.08076 (2017). https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
M. Tatarevic, An improved upper bound for the Ramsey number R(3,3,3,3), GitHub repository, 2026, commit ddd7755. https://github.com/milostatarevic/r3333-upper-bound/commit/ddd7755476db3f0751181db0daec75342576cdd1
A. McKenna, $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier, Zenodo, 2026. https://doi.org/10.5281/zenodo.23156099 ; Lean code: https://github.com/mysticflounder/schur-centred-bound (release v1.0.1).

15 thms1 active userReviewed

Linear algebra Numerical Analysis Optimization·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds IV: Within σ_r(X̄)/2 of a Rank-r Matrix, the Truncated SVD Is the Unique Nearest Matrix of Rank Exactly rResearch Paper

Motivation

Optimization over sets of matrices of fixed rank comes up in low-rank matrix completion, model reduction, and the low-rank approximation of solutions of large matrix equations. A standard approach treats the constraint set as a Riemannian manifold and runs gradient or Newton-type methods on it (Absil, Mahony & Sepulchre 2008). Each iteration takes a step in the tangent space and then has to return to the manifold. A map that does this to first order is called a retraction, and its cost is often what decides whether a manifold method is practical.

Absil and Malick (2012) study retractions defined by projection: step to $X+Z$ in the ambient space, then take the nearest point of the manifold. Their Proposition 3.2 shows that for any $C^k$ submanifold ( $k\ge2$ ) this projective retraction is a retraction. Section 3.2 makes it explicit for the manifold of fixed-rank matrices: near any matrix of rank $r$ , the nearest matrix of rank exactly $r$ is the truncated singular value decomposition (Proposition 3.3). Section 4.4 also gives a closed form for a second retraction on the same manifold, the orthographic retraction (Proposition 4.11).

Setting

Fix natural numbers $n$ , $m$ and $r\ge1$ . The space $\mathbb R^{n\times m}$ of real $n\times m$ matrices carries the Frobenius norm $\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X)$ (3.6). The fixed-rank set is

\mathcal R_r=\{X\in\mathbb R^{n\times m}:\ \operatorname{rank}(X)=r\},

a smooth submanifold of $\mathbb R^{n\times m}$ . It is not closed: its closure is the set of matrices of rank at most $r$ .

A singular value decomposition (3.5) of $X$ is a factorization $X=U\Sigma V^\top$ in which $U=[u_1,\dots,u_n]\in\mathbb R^{n\times n}$ and $V=[v_1,\dots,v_m]\in\mathbb R^{m\times m}$ are orthogonal and $\Sigma\in\mathbb R^{n\times m}$ is zero off its diagonal. The diagonal of $\Sigma$ holds the singular values of $X$ in nonincreasing order,

\sigma_1(X)\ge\sigma_2(X)\ge\cdots\ge\sigma_{\min\{n,m\}}(X)\ge0,

and $\sigma_i(X)=0$ for $i>\min\{n,m\}$ . A matrix has rank $r$ exactly when $\sigma_r(X)>0=\sigma_{r+1}(X)$ . The truncated SVD of rank $r$ is $\hat X=\sum_{i=1}^r\sigma_i(X)u_iv_i^\top$ (3.7).

For a set $Q$ and a point $X$ , the projection $P_Q(X)$ is the set of nearest points: the $Y\in Q$ with $\|X-Y\|\le\|X-W\|$ for all $W\in Q$ . For a set that is not closed, $P_Q(X)$ may be empty or contain several points.

Formalization targets

Goal: Proposition 3.3

Let $\bar X\in\mathcal R_r$ . For every $X$ with $\|X-\bar X\|<\sigma_r(\bar X)/2$ and every singular value decomposition $X=U\Sigma V^\top$ ,

P_{\mathcal R_r}(X)=\Bigl\{\sum_{i=1}^r\sigma_i(X)\,u_iv_i^\top\Bigr\}.

The projection exists, is unique, and is the truncated SVD. The radius $\sigma_r(\bar X)/2$ and the strict inequality are those of the paper.

Milestones

The paper's proof goes through four claims, which are the milestones in attack order:

Weyl's bound (§3.2, proof of Proposition 3.3, citing Horn–Johnson 7.3.8): $|\sigma_i(\bar X)-\sigma_i(X)|\le\|X-\bar X\|$ for every $i\ge1$ .
Eckart–Young (3.7): for every singular value decomposition of $X$ , $\hat X$ is a nearest matrix to $X$ of rank at most $r$ .
The gap (3.8): if $\operatorname{rank}\bar X=r$ and $\|X-\bar X\|<\sigma_r(\bar X)/2$ , then $\sigma_{r+1}(X)<\sigma_r(\bar X)/2<\sigma_r(X)$ .
Uniqueness under a gap (§3.2, proof of Proposition 3.3, citing Helmke–Moore): if $\sigma_r(X)>\sigma_{r+1}(X)$ , then $\hat X$ is the only nearest matrix of rank at most $r$ .

Further result: Proposition 4.11

Write $X=U\left[\begin{smallmatrix}\Sigma_0&0\\0&0\end{smallmatrix}\right]V^\top$ (4.7), with $\Sigma_0$ the positive diagonal of nonzero singular values, and a tangent vector $Z=U\left[\begin{smallmatrix}A&C\\B&0\end{smallmatrix}\right]V^\top$ (4.8). If $\Sigma_0+A$ is invertible, the orthographic retraction is

R(X,Z)=U\begin{bmatrix}\Sigma_0+A&C\\B&B(\Sigma_0+A)^{-1}C\end{bmatrix}V^\top .

Here $R(X,Z)$ is the nearest point to $X+Z$ of $\mathcal R_r\cap(X+Z+N_{\mathcal R_r}(X))$ .

Significance

The result. Proposition 3.3 reduces the projective retraction on $\mathcal R_r$ to one truncated singular value decomposition. With Proposition 3.2 this gives an explicit, computable retraction for Riemannian optimization on fixed-rank matrices. It is used, for instance, in low-rank matrix completion algorithms. The point is local: $\mathcal R_r$ is not closed, so far from $\mathcal R_r$ the nearest matrix of rank exactly $r$ need not exist, and the proposition gives an explicit radius on which it does exist and is unique. Proposition 4.11 gives a second retraction that needs only products of matrices and one $r\times r$ inverse.

Formalizing it. All results here are proved, on paper. To the best of a search of Mathlib and the Prove2Me catalog, none is machine-checked. Mathlib has singular values of linear maps between finite-dimensional inner product spaces (LinearMap.singularValues), but no singular value decomposition in matrix form, no Weyl perturbation inequality for singular values, and no Eckart–Young theorem. A complete development would add these, and the Eckart–Young theorem with its uniqueness case is a standard result of numerical linear algebra in its own right.

Difficulty

The proof in the paper is short only because it cites three facts, and each of them is a real piece of matrix analysis.

Weyl's bound needs the variational (min–max) description of singular values, which Mathlib does not have for singular values.
Eckart–Young requires comparing $\|X-Y\|$ with the singular values of $X$ for every $Y$ of rank at most $r$ , not only for those diagonal in the same bases. The obvious approach, writing $Y$ in the singular bases of $X$ , fails because $Y$ need not be diagonal there.
Uniqueness under the gap requires showing that every minimizer is diagonal in some singular bases of $X$ and then using the gap to fix its support. Without the gap uniqueness fails: for $X=I_2$ and $r=1$ every $uu^\top$ with $\|u\|=1$ is a nearest point.

A further subtlety: Proposition 3.3 must hold for any singular value decomposition of $X$ . Singular vectors are not unique, so the proof has to show that the truncation does not depend on the choice under the gap (3.8).

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius). The projection is the published platform predicate RandomGradFree.Nonsmooth.IsMetricProjection, and $P_{\mathcal R_r}(X)$ is the set {Y | IsMetricProjection (rankSet r) X Y}. The set equality with a singleton states existence, uniqueness and the formula together.

Conventions committed to:

sv X i is $\sigma_i(X)$ , 1-based as on the page. It is Mathlib's 0-based singularValues of Matrix.toEuclideanLin X at i - 1, so the index $0$ is meaningless and every statement uses indices $\ge1$ .
IsSVD X U S V is the predicate of (3.5). The singular value decomposition is a hypothesis of the theorems, never a choice made inside them, so the theorems hold for every singular value decomposition.
truncSVD r U S V is $\sum_{i\le r}\Sigma_{ii}u_iv_i^\top$ , written with the diagonal of S. That these entries are the singular values $\sigma_i(X)$ is a fact to be proved, not part of the definition.
The hypothesis $r\ge1$ is added, because $\sigma_r$ needs it (and $\mathcal R_0=\{0\}$ ). It is the only hypothesis of Proposition 3.3 not printed on the page.
In Proposition 4.11, matrices use the block index types Fin r ⊕ Fin p and Fin r ⊕ Fin q. The tangent vector and the normal space are taken in the form the page gives, and invertibility of $\Sigma_0+A$ is an explicit hypothesis. In the paper's proof it comes from " $Z$ in a neighborhood of the origin".

A formalization in which the radius is replaced by a smaller one, the projection is taken onto the matrices of rank at most $r$ , or the singular value decomposition is chosen inside the statement is a different theorem and is ruled out.

Wanted contributions, all reusable beyond this mission:

existence of a singular value decomposition in matrix form, and the identification of its diagonal with singularValues;
Weyl's inequality for singular values;
the Eckart–Young theorem and its uniqueness case;
the Schur-complement rank formula for $2\times2$ block matrices, used for Proposition 4.11.

Selected references

P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version HAL hal-00651608v2: https://hal.science/hal-00651608v2)
P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
C. Eckart and G. Young, The approximation of one matrix by another of lower rank, Psychometrika 1(3):211–218, 1936. https://doi.org/10.1007/BF02288367
R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (§7.3, §7.4). https://doi.org/10.1017/CBO9780511810817
U. Helmke and J. B. Moore, Optimization and Dynamical Systems, Springer, 1994 (Ch. 5). https://doi.org/10.1007/978-1-4471-3467-1

8 thms1 active userReviewed

Differential Geometry Linear algebra Optimization·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds III: Near a Locally Symmetric Point, the Projection onto a Spectral Manifold Is U Diag(P_M(λ(X))) UᵀResearch Paper

Motivation

Riemannian optimization algorithms move along a manifold by taking a step in a tangent direction and then coming back to the manifold. The map that does the coming back is a retraction, and the most natural candidate on a submanifold of a Euclidean space is the projective retraction: add the tangent step, then take the nearest point of the manifold. Its practical value depends on whether that nearest point can be computed.

For many manifolds of symmetric matrices the defining property is a property of the eigenvalues: matrices whose largest eigenvalue has multiplicity $p$ , matrices with prescribed spectrum, and similar sets that arise in eigenvalue optimization and in alternating projection methods (Lewis and Malick 2008). Daniilidis, Malick and Sendov (reference [8] of the paper) showed that such a spectral set is a smooth manifold when the underlying set of eigenvalue vectors is a smooth, locally symmetric manifold. P.-A. Absil and J. Malick (SIAM J. Optim. 2012; authors' version hal-00651608v2) then showed that, close to such a manifold, the metric projection onto it has a closed form: one eigendecomposition and one projection in $\mathbb R^n$ . This mission formalizes that result, Theorem 3.9 of the paper.

Setting

Write $\mathbf S_n$ for the real symmetric $n \times n$ matrices with the Frobenius norm $\|X\|^2 = \sum_{i,j} X_{ij}^2$ , $\mathbf O_n$ for the orthogonal matrices, and $\mathbf \Sigma_n$ for the permutation matrices, which act on $\mathbb R^n$ (with the Euclidean norm) by permuting coordinates. Let

\mathbb R^n_\downarrow = \{x \in \mathbb R^n : x_1 \ge x_2 \ge \cdots \ge x_n\}.

For $X \in \mathbf S_n$ , $\lambda(X) \in \mathbb R^n_\downarrow$ is the vector of its eigenvalues, with multiplicity, in nonincreasing order; every $X$ has an eigendecomposition $X = U \operatorname{Diag}(\lambda(X)) U^\top$ with $U \in \mathbf O_n$ . For $M \subseteq \mathbb R^n$ the spectral set of $M$ is

\lambda^{-1}(M) = \{X \in \mathbf S_n : \lambda(X) \in M\}.

For a set $Q$ and a point $y$ , $P_Q(y)$ is the set of nearest points of $Q$ to $y$ (it may be empty or contain several points).

Let $\mathcal M$ be a $C^2$ submanifold of $\mathbb R^n$ : around each of its points it is a coordinate slice of a $C^2$ chart with $C^2$ inverse. Let $\mathcal S = \lambda^{-1}(\mathcal M \cap \mathbb R^n_\downarrow)$ , let $\bar X \in \mathcal S$ and $\bar x = \lambda(\bar X)$ . The set $\mathcal M \cap B(\bar x, \delta)$ (open ball) is strongly locally symmetric if for every $x \in \mathcal M \cap B(\bar x, \delta)$ and every $P \in \mathbf \Sigma_n$ with $Px = x$ ,

P\big(\mathcal M \cap B(\bar x, \delta)\big) = \mathcal M \cap B(\bar x, \delta). \qquad (3.15)

Formalization targets

Goal: Theorem 3.9 (projection onto spectral manifolds)

Assume $\mathcal M$ is a $C^2$ submanifold of $\mathbb R^n$ , $\bar X \in \mathcal S$ , $\delta > 0$ and (3.15). Then there is $\delta_0 \in (0, \delta]$ such that for every $X \in \mathbf S_n$ with $\|X - \bar X\| \le \delta_0/2$ , the set $P_{\mathcal M}(\lambda(X))$ is a single point $p$ , and for every $U \in \mathbf O_n$ with $X = U \operatorname{Diag}(\lambda(X)) U^\top$ ,

P_{\mathcal S}(X) = \{\, U \operatorname{Diag}(p)\, U^\top \,\}.

The goal fixes no constant: $\delta_0$ is only asserted to exist, as the paper's proof restricts $\delta$ to make the local uniqueness of $P_{\mathcal M}$ and Lemma 3.8 apply.

Milestones

(3.11): $\|\lambda(X) - \lambda(Y)\| \le \|X - Y\|$ for $X, Y \in \mathbf S_n$ .
Lemma 3.7: for closed $M \subseteq \mathbb R^n_\downarrow$ , an eigendecomposition $X = U\operatorname{Diag}(\lambda(X))U^\top$ and sorted $z$ , $U \operatorname{Diag}(z) U^\top \in P_{\lambda^{-1}(M)}(X) \iff z \in P_M(\lambda(X))$ .
Lemma 3.8: for $\bar x \in \mathbb R^n_\downarrow$ and all small $\delta > 0$ , for $y \in B(\bar x, \delta)$ and sorted $x \in B(\bar x, \delta)$ , the maximum of $x^\top P y$ over permutations fixing $\bar x$ is attained at some $P$ with $Py$ sorted.
(3.20): under (3.15) and for small $\delta$ , the distance from a sorted $x \in B(\bar x, \delta)$ to $\mathcal M \cap B(\bar x, \delta)$ is attained up to equality on sorted points.

Significance

The theorem turns the projective retraction on a spectral manifold, an optimization problem over $n \times n$ matrices, into a projection in $\mathbb R^n$ onto $\mathcal M$ plus one eigendecomposition. For the matrices whose largest eigenvalue has multiplicity $p$ , the projection onto $\mathcal M_p$ is an explicit averaging of the top $p$ eigenvalues (Example 3.10 of the paper), which completes a partial result of Oustry (reference [29, Th. 13] of the paper). Together with Theorem 3.5, it is what makes the projective retraction a practical alternative on manifolds where the Riemannian exponential has no known efficient formula.

The result is proved in the paper; to our knowledge none of it is formalized. The mission produces a machine-checked version of the theorem and of the spectral-set toolkit beneath it: the Lipschitz property of sorted eigenvalues, the reduction of projections onto spectral sets to projections onto sets of vectors, and the permutation rearrangement lemma. The formalization also corrects a misstatement: Lemma 3.7 as printed quantifies over all $z \in \mathbb R^n$ , and its direction " $\Rightarrow$ " fails for unsorted $z$ (for $n = 2$ , $M = \{(2, 0)\}$ , $X = U = I$ , $z = (0, 2)$ ). The mission states it for $z \in \mathbb R^n_\downarrow$ , which is the only case Theorem 3.9 uses.

Difficulty

The obvious argument shows only half of the goal. Lemma 3.7 characterizes the nearest points of $\mathcal S$ that share the eigenvectors $U$ of $X$ ; it does not exclude a nearest point with other eigenvectors, and the goal asserts that $P_{\mathcal S}(X)$ is a single point. Excluding the others needs the equality case of the trace inequality $\operatorname{trace}(XY) \le \lambda(X)^\top \lambda(Y)$ (3.10), which the paper quotes from the literature without proof, and the fact that the projection $p$ inherits the ties of $\lambda(X)$ , which comes from strong local symmetry and uniqueness of $P_{\mathcal M}$ .

The local uniqueness of $P_{\mathcal M}$ near a point of a $C^2$ submanifold (Lemma 3.1 of the paper) is itself a tubular-neighbourhood argument through the inverse function theorem. Mathlib has no metric projection onto embedded submanifolds, no von Neumann trace inequality for sorted eigenvalues, and no Hoffman–Wielandt inequality. Finally, the radii interact: the restriction $\delta_0$ must make Lemma 3.1, Lemma 3.8 and the ball inclusion $P_{\mathcal M}(x) \in B(\bar x, \delta)$ all hold at once.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), with the Euclidean norm (not the sup norm of Fin n → ℝ). Matrices are Matrix (Fin n) (Fin n) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius); $\mathbf S_n$ is IsHermitian (symmetry over $\mathbb R$ ) and $\mathbf O_n$ is Matrix.orthogonalGroup.
$\lambda(X)$ is eig X, built from Mathlib's sorted IsHermitian.eigenvalues₀; on a non-symmetric matrix it returns $0$ , and every statement assumes symmetry. $\mathbb R^n_\downarrow$ is sortedDesc n, spectral sets are specSet, permutations act by permAct (an isometry), and (3.15) is IsStronglyLocallySymmetric on the open ball.
Nearest points are the platform predicate RandomGradFree.Nonsmooth.IsMetricProjection; $P_Q(y)$ is {z | IsMetricProjection Q y z}.
The submanifold hypothesis is a local slice-chart predicate IsSubmanifold 2 d M. The paper allows $k = 2$ or $\infty$ ; $k = 2$ covers both. Only the hypotheses of Theorem 3.5 (cited from Daniilidis–Malick–Sendov without proof) are assumed, not its conclusion that $\mathcal S$ is a manifold.
"For $\delta$ small enough" is $\exists \delta_1 > 0, \forall \delta \in (0, \delta_1]$ ; the radius of Theorem 3.9 is an existential $\delta_0 \le \delta$ , with the paper's non-strict $\|X - \bar X\| \le \delta_0/2$ .
Both singleton claims of Theorem 3.9 are part of the conclusion. A version proving only $\subseteq$ would be satisfied by the empty set, and a version that assumes $P_{\mathcal M}(\lambda(X))$ is a singleton would delete the theorem's local-uniqueness content; neither is the target.

Infrastructure that a full development needs and that is reusable beyond this mission: the von Neumann/Fan trace inequality and its equality case for real symmetric matrices, the Hoffman–Wielandt inequality (3.11), the rearrangement inequality over permutations fixing a vector, and the local existence and uniqueness of metric projections onto $C^2$ submanifolds. Useful platform items: RHLinalg.vonNeumann_trace_ineq (the trace inequality for Hermitian matrices), RHLinalg.bilinear_doublyStochastic_le_of_monovary (the rearrangement step), and Bhatia.trace_mul_perm_bounds (trace pairings between permutation pairings of unsorted spectra). Contributions of these lemmas, of alternative proofs of (3.11), and of the equality case of (3.10) are welcome.

Selected references

P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529; authors' version https://hal.science/hal-00651608v2
A. Daniilidis, J. Malick and H. Sendov, Locally symmetric submanifolds lift up to spectral manifolds, preprint, 2009 (reference [8] of the paper; the source of Theorem 3.5).
A. S. Lewis and J. Malick, Alternating projections on manifolds, Math. Oper. Res. 33(1):216–234, 2008. https://doi.org/10.1287/moor.1070.0291
F. Oustry, A second-order bundle method to minimize the maximum eigenvalue function, Math. Program. 89:1–34, 2000 (reference [29] of the paper).
A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6(1):164–177, 1996. https://doi.org/10.1137/0806009

8 thms1 active userReviewed

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

Project Scheduling with Time Windows and Scarce Resources VI: Stable, Semistable, Pseudostable and Quasistable Schedules Are Extreme Points of the Feasible RegionTextbook

Motivation

Resource-constrained project scheduling with minimum and maximum time lags is the model behind make-to-order production, process-industry batch planning and large engineering projects. When the objective is the project duration or another regular function (nondecreasing in every start time), an optimum can be found among schedules that cannot be shifted to the left. Many objectives in practice are nonregular: net present value, earliness–tardiness costs, resource levelling and resource investment. For these, delaying an activity can pay, and "shift as far left as possible" no longer identifies a finite set of candidate schedules.

Neumann, Nübel and Schwindt (Math. Methods Oper. Res. 52, 2000) answered this with classes of schedules defined by the absence of pairs of opposite shifts: stable, semistable, pseudostable and quasistable schedules, the mirror image of active, semiactive, pseudoactive and quasiactive schedules. Section 3.2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), shows that these classes are exactly the extreme points of the feasible region and of its natural convex pieces. The classification of objective functions in §3.3, and every enumeration scheme of the later chapter, rests on that correspondence.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ . Activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$ , with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. The project network $N$ has node set $V$ and arcs $\langle i,j\rangle\in E$ with integer weights $\delta_{ij}$ , each encoding a temporal constraint $S_j-S_i\ge\delta_{ij}$ . A prescribed deadline $\bar d\in\mathbb N$ is included as the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$ . Renewable resources $k$ have capacities $R_k$ , and activity $i$ uses $r_{ik}\le R_k$ units while it runs.

A schedule is a vector $S\in\mathbb R^{n+2}$ of start times. The time-feasible region $\mathcal S_T$ collects the schedules with $S_0=0$ , $S\ge0$ and $S_j-S_i\ge\delta_{ij}$ on every arc; it is a polyhedron, and a polytope when every activity precedes $n+1$ as in Remarks 1.1.2. A schedule is resource-feasible if at every time $t\ge0$ the running activities $\mathcal A(S,t)=\{i\mid S_i\le t<S_i+p_i\}$ use at most $R_k$ units of every resource. The feasible region is $\mathcal S=\mathcal S_T\cap\mathcal S_R$ . It is in general neither convex nor connected.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ . For a strict order $O$ , the order polytope is $\mathcal S_T(O)=\{S\in\mathcal S_T\mid S_j\ge S_i+p_i\ ((i,j)\in O)\}$ . The order $O$ is feasible if $\emptyset\ne\mathcal S_T(O)\subseteq\mathcal S$ . The schedule polytope of $S$ is $\mathcal S_T(O(S))$ .

A shift moves a schedule $S$ to $S'\neq S$ . It is global if both are feasible, local if in addition a continuous path inside $\mathcal S$ joins them, order-preserving if $O(S)\subseteq O(S')$ , and order-monotone if $O(S)$ and $O(S')$ are comparable. Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$ . A feasible schedule is stable, semistable, pseudostable or quasistable if no pair of opposite global, local, order-monotone or order-preserving shifts, respectively, starts at it. It is antiactive if no global right-shift starts at it.

Formalization targets

Goal: Theorem 3.2.10

For every feasible schedule $S$ :

\begin{aligned} &\text{(a) } S\text{ antiactive}\iff S\text{ maximal in }\mathcal S, \qquad \text{(b) } S\text{ stable}\iff S\in\operatorname{ext}\mathcal S,\\ &\text{(c) } S\text{ semistable}\iff S\in\operatorname{ext}C_S,\ C_S\text{ the component of }\mathcal S\text{ containing }S,\\ &\text{(d) } S\text{ pseudostable}\iff S\in\operatorname{ext}\mathcal S_T(O)\ \text{for all feasible }O\subseteq O(S),\\ &\text{(e) } S\text{ quasistable}\iff S\in\operatorname{ext}\mathcal S_T(O(S)). \end{aligned}

Milestones

Lemma 3.2.4: opposite order-preserving or order-monotone shifts can be taken uniform (all moved activities move by one common amount).
Lemma 3.2.8: pseudostable schedules are the local extreme points of $\mathcal S$ , the points on no segment that lies entirely in $\mathcal S$ .
Lemma 3.2.9: when $S$ is not pseudostable, a segment through $S$ can be found inside one order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$ feasible.
Proposition 3.2.13: the quasistable schedules, and every class below them in Fig. 3.2.6, form finite sets.
Proposition 3.2.16: every vertex of $\mathcal S_T$ is the unique solution of $S_0=0$ , $S_j-S_i=\delta_{ij}$ on the arcs of a spanning tree of $N$ ; for the minimal point, an outtree rooted at $0$ .
Theorem 3.2.18: $S$ is quasistable iff it is the unique solution of such a tree system in the schedule network $N(O(S))$ .
Remark 3.2.7: every activity of a quasistable schedule is tied to another one by a tight duration or time lag, so quasistable schedules are integer-valued.

Significance

The theorem makes four shift-defined classes computable objects: extreme points of explicit polytopes, or of a finite union of them. Together with Proposition 3.2.13, it gives each class of nonregular objective functions in §3.3 a finite candidate set of schedules among which an optimum can be sought (§3.2, p. 207). Theorem 3.2.18 gives the certificate for quasistable schedules: a spanning tree of the schedule network, which the later sections use to enumerate vertices.

The results are proved in the book, except Lemma 3.2.9, whose proof is cited to Neumann, Nübel and Schwindt (2000). As far as a search of the platform shows, none of them has been formalized. A formalization supplies the missing details, among them that connected and path components of $\mathcal S$ coincide and the degenerate vertices behind the tree description. It also produces a reusable library of schedule classes on real-valued start times.

Difficulty

Part (b) is close to the definition, since a pair of opposite global shifts is a segment through $S$ with feasible endpoints. The content is elsewhere. In (c) the definition speaks of continuous trajectories and the right-hand side of connected components, so the proof needs local path-connectedness of a finite union of polytopes. In (d) the feasible region is not convex: an order-monotone shift keeps $S$ and $S'$ in a common order polytope, but $S'$ and $S''$ may lie in different ones. The segment through $S$ has to be moved into a single order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$ , and that is Lemma 3.2.9. Proposition 3.2.16 and Theorem 3.2.18 need the passage from $n+2$ linearly independent tight constraints to a spanning tree. They must allow degenerate vertices, where several trees describe the same point, and must represent the nonnegativity constraints $S_i\ge0$ by arcs of the network.

Formalization scope

Activities are Fin (n + 2); start times are real vectors Fin (n + 2) → ℝ with the pointwise order. Durations, capacities and requirements are natural numbers, and time lags integers. The deadline is the arc $\langle n+1,0\rangle$ of weight $-\bar d$ , which is always present, as §3.1 prescribes. Resource constraints are imposed for every $t\ge0$ , not only for $0\le t\le\bar d$ as (3.1.2) writes; the proofs use the first reading. Extreme points are Mathlib's Set.extremePoints ℝ, maximal points are Maximal for the pointwise order, and components are connectedComponentIn. A local shift carries an explicit continuous map from unitInterval into $\mathcal S$ . Strict orders are asymmetric, transitive relations on $V$ . A spanning tree is an arc set of size $n+1$ whose underlying simple graph is connected. Its arcs must be arcs of $N$ , resp. of $N(O(S))$ , with their network weights, so an arbitrary equation system does not count.

The schedule classes are defined through shifts and nothing else. Defining "stable" as "extreme point", or "pseudostable" as "local extreme point", would make the goal and Lemma 3.2.8 tautologies, and such encodings are ruled out. Proposition 3.2.16 carries the book's standing convention (§1.2, p. 8) that every node is reached from $0$ by a walk of nonnegative length. Without it the statement is false.

The definitions duplicate, under this mission's namespace, the model of the book's Chapter 2 missions (order polytopes, shifts, active classes). They are written to be merged with those once published. Contributions on the geometry of finite unions of polytopes, and on spanning-tree bases of difference constraint systems, are reusable beyond this mission.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1–3.2. https://doi.org/10.1007/978-3-540-24800-2
K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), 441–465. https://doi.org/10.1007/s001860000092
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 199–240. https://doi.org/10.1007/BF02283745

12 thms1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 6101 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $6101$ , from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 6101,\ \textstyle\sum s = n.

This is the campaign template with the value $6101$ filled in. The source proves the stronger statement that every odd $n \ge 12\,203$ is a sum of exactly $6101$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the first moment:

Whole-triangle count. Counting all pairs with $p + q \le x$ gives $\sum_{s \le x} r(s) \ge 2(x-2000)^2/(9(\log x)^2)$ for $x \ge 2000$ .
Weighting. Weighting $r(s)$ by $(\log s)^2/s$ cancels the varying factor in the sieve bound $r(s) \le 9\,C(s)\,s/(\log s)^2$ , giving a weighted first moment of at least $\tfrac{44}{100}x$ .
Second moment of $C$ . With $\sum_{s \le x,\, 2\mid s} C(s)^2 \le \tfrac{21}{2}x$ , Cauchy–Schwarz yields $\sigma(A) \ge 1/2200$ for $A = B + B$ , $B = \{(p-3)/2\}$ .
Schnirelmann's inequality with $m = 1525$ (the least $m$ with $(1 - 1/2200)^m < 1/2$ ) gives $K = 4m + 1 = 6101$ .

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$ , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$ . Reusable components:

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ .
Moment bounds for the singular-series factor $C(s)$ .
Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$ .

Formalization scope

The Lean statement is the campaign template verbatim with $6101$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $6101$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 97041 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $97\,041$ , from the same elementary circle of ideas.

Setting

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 97\,041,\ \textstyle\sum s = n.

This is the campaign template with the value $97\,041$ filled in. The source proves the stronger statement that every odd $n \ge 194\,083$ is a sum of exactly $97\,041$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It is the argument behind the $100\,001$ entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give $\sigma(A) \ge 1/35\,000$ for $A = B + B$ , $B = \{(p-3)/2 : p \text{ odd prime}\}$ . The only change is to take the smallest admissible $m$ in Schnirelmann's inequality: $(1 - 1/35\,000)^{m} < 1/2$ first holds at $m = 24\,260$ (rather than the rounded $25\,000$ ), so $2mA = \mathbb{Z}_{\ge 0}$ and $K = 4m + 1 = 97\,041$ .

Significance

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ .
Moment bounds for the singular-series factor $C(s)$ .
Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$ .

Formalization scope

The Lean statement is the campaign template verbatim with $97\,041$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $97\,041$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Group Theory·Captain: dbenbenn

Moore: the Følner function of Thompson's group F grows faster than any tower of exponentialsResearch Paper

This mission formalizes J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651 (doi:10.4171/GGD/201; arXiv:0905.1118v7, whose page numbers are used): if Thompson's group $F$ has Følner sets at all, they are larger than any tower of exponentials.

Motivation

Whether Thompson's group $F$ is amenable is a long-standing open problem, the goal of the F-amenability mission on this platform. By Følner's criterion a finitely generated group is amenable exactly when it has Følner sets, finite sets almost invariant under translation by the generators, of every precision. Moore's theorem is unconditional: for every finite symmetric generating set there is a constant $C > 1$ such that every $C^{-n}$ -Følner set has at least $\exp_n(0)$ elements, a tower of $n$ exponentials. If $F$ is amenable, its Følner function therefore outgrows every tower, and $F$ would answer negatively Gromov's question whether some primitive recursive function dominates the Følner functions of all amenable finitely presented groups (Moore's Question 1.2, from Gromov 2008, p. 578).

Timeline.

1979: Geoghegan conjectures that $F$ is not amenable (Cannon–Floyd–Parry 1996, p. 227).
2001: Burillo, Cleary and Stein estimate word length in $F$ by the size of reduced tree diagrams (doi:10.1090/S0002-9947-00-02650-7).
2008: Gromov asks whether the Følner functions of amenable finitely presented groups are dominated by a primitive recursive function (doi:10.4171/ggd/48).
2013: Moore proves the tower lower bound for $F$ (doi:10.4171/GGD/201).

Setting

Thompson's group $F$ (CannonFloydParry.F, published) is the group of order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, all dyadic rationals, and all slopes powers of $2$ . Moore multiplies elements as " $f$ followed by $g$ "; that group, the opposite of the group of maps under composition, is MooreF, and it acts on the right.

A finite set $A \subseteq F$ is $\varepsilon$ -Følner with respect to a finite $\Gamma$ (IsFolnerSet Γ A ε) when $\sum_{\gamma \in \Gamma} |(A \cdot \gamma) \mathbin{\triangle} A| < \varepsilon |A|$ , where $A \cdot \gamma = \{a \gamma : a \in A\}$ . The tower function is $\exp_0(n) = n$ , $\exp_{p+1}(n) = 2^{\exp_p(n)}$ (ThompsonAmenability.towerExp, published). The Følner function $\mathrm{Føl}_{F,\Gamma}(n)$ (folnerFunction) is the least size of a $1/n$ -Følner set, and $\infty$ if there is none.

The proof works with finite rooted binary trees, recorded as the sets of addresses of their leaves (IsTree), on which $F$ acts partially by acting on the addresses (treeAct), and with weighted Følner sets and marginal sets for partial actions of a group (IsWeightedFolner, IsMarginal). These are defined in the two definitions items.

Formalization targets

Goal: Theorem 1.1

For every finite symmetric generating set $\Gamma$ of $F$ there is $C > 1$ such that, for every $n$ ,

A \text{ is } C^{-n}\text{-Følner} \implies |A| \ge \exp_n(0).

The goal is the published F-amenability milestone ThompsonAmenability.exists_const_forall_isFolner_le_card, for the product of maps by composition and left translates; a milestone states the same theorem in Moore's conventions, and another states its second sentence, that $\mathrm{Føl}_{F,\Gamma}$ is not eventually dominated by any $\exp_p$ .

Milestones

Every numbered result of §§3–5 (Lemmas 3.4, 3.5, 3.9–3.12, 3.14, 3.15, 4.1, 4.2, 5.2, 5.4, 5.5, 5.7, 5.9, 5.10, 5.12, 5.13, Remark 3.8 and Claim 5.14), the unnumbered facts about trees and tree diagrams stated in §2, and the word-length bound Moore cites from Burillo, Cleary and Stein.

Significance

The result. The theorem constrains any proof that $F$ is amenable: Følner sets of $F$ , if they exist, cannot be found by any search whose size is bounded by a tower of fixed height. If $F$ is amenable, it answers Gromov's question negatively. If $F$ is not amenable, the bound is vacuous but its method, controlling how Følner sets distribute over tree diagrams, is one of the few quantitative tools on the problem.

Formalizing it. None of the paper is formalized. The general theory of §3 (partial actions, weighted Følner sets, marginal sets) applies to any group acting partially on a set and is reusable; the partial action of $F$ on binary trees is the natural model for combinatorial arguments about $F$ .

Difficulty

The difficulty is quantitative. A Følner set is defined only by an inequality between counts, and nothing in that inequality forces its elements to be large; yet the bound must hold for every Følner set, with a single constant $C$ for all $n$ , while the height of the tower grows with $n$ . Any argument can therefore afford to lose only a constant factor in the Følner constant for each level of the tower.

Formalization scope

Lean representation and conventions.

Moore's $F$ is (CannonFloydParry.F)ᵐᵒᵖ, so products and right translates match the paper; the goal is stated for CannonFloydParry.F with left translates.
Trees are finite sets of binary sequences (List Bool). Tree diagrams, their maps on sequences, equivalence and reducedness follow Moore's §2; a tree diagram describes an element of the published $F$ through the dyadic intervals of its leaves, and Moore's sentence defining $F$ as the reduced tree diagrams is a milestone.
A partial action is an Option-valued function, and the action of $F$ is defined on all finite sets of sequences; on trees it is Moore's action.
Weighted Følner sets are finitely supported non-negative functions; sums over $S$ are finite sums over their supports.

What is left out, and deviations.

Question 1.2 (Gromov's question) and Remark 5.11 (consequences for invariant measures on trees, not used in the proof) are not formalized.
In Definition 3.1, Moore's "for which all computations involving $\cdot$ are defined" can be read two ways. It is read here as asserting that $x \cdot (gh)$ is defined whenever $x \cdot g$ and $(x \cdot g) \cdot h$ are (Exel's composition law for partial actions), which Moore's proof of Lemma 3.5 uses and the action of $F$ on trees satisfies. On the weaker reading, equality only where all three are defined, Lemmas 3.5, 3.9, 3.10 and 3.12 fail (the note on the §3 definitions links p2m theorems proving this).
Definition 3.13 is read with the joining chain staying inside the set; the literal reading makes every subset of a group acting on itself by right multiplication $\Gamma$ -connected for a symmetric generating set $\Gamma$ .
Lemmas 3.5 and 3.9 assume $g \ne e$ , where the strict inequalities fail; Claim 5.14 bounds the reduced diagram, where "a tree diagram" would be vacuous. Each is explained in the milestone's statement.
The word-length bound is cited: Burillo, Cleary and Stein prove it for elements with positive normal form, and Moore applies it to all of $F$ .

What a development needs. Tree diagrams, normal forms and generation of $F$ are published and proved on this platform (the Cannon–Floyd–Parry missions on tree diagrams and the normal form and the two presentations of $F$ ); Følner's criterion is published by Garrido's first mission. New are the combinatorics of binary trees as leaf sets, the bridge between them and the published tree diagrams, and the theory of §3. Proofs of any milestone are welcome.

Selected references

J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877
J. Burillo, S. Cleary, M. I. Stein, Metrics and embeddings of generalizations of Thompson's group F, Trans. Amer. Math. Soc. 353 (2001) 1677–1689. doi:10.1090/S0002-9947-00-02650-7
R. Exel, Partial actions of groups and actions of inverse semigroups, Proc. Amer. Math. Soc. 126 (1998) 3481–3494. doi:10.1090/S0002-9939-98-04575-4
M. Gromov, Entropy and isoperimetry for linear and non-linear group actions, Groups Geom. Dyn. 2 (2008) 499–593. doi:10.4171/ggd/48

36 thms1 active userReviewed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions VI: The Homogeneous Self-Dual Predictor–Corrector MethodTextbook

Motivation

Interior-point methods are the standard polynomial-time algorithms for linear programming, and the path-following method that practitioners implement (Chapter 18 of Vanderbei's Linear Programming: Foundations and Extensions) comes without a complete convergence proof. Chapter 22 of the same book presents a closely related algorithm for which a complete analysis can be written down: the homogeneous self-dual predictor–corrector method. It combines two ideas. The first is the self-dual embedding of Ye, Todd and Mizuno (1994), which folds a linear program and its dual into one auxiliary problem that always has feasible solutions, so no feasible starting point is needed. The second is the predictor–corrector scheme of Mizuno, Todd and Ye (1993), which alternates an affine-scaling step with a centering step while keeping the iterates in a neighbourhood of the central path, and reduces the duality measure by a factor $1 - 1/(2\sqrt n)$ every two iterations. The result is an $O(\sqrt n\,L)$ iteration bound, the best known for interior-point methods on linear programs.

Setting

Let $A$ be a real $n \times n$ matrix with $n \ge 2$ that is skew symmetric, $A = -A^T$ . The homogeneous self-dual problem (22.4) is

\text{maximize } 0 \quad \text{subject to } Ax + z = 0,\quad x, z \ge 0.

For $x, z \in \mathbb{R}^n$ write $X, Z$ for the diagonal matrices with the entries of $x, z$ on the diagonal and $e$ for the vector of ones. The infeasibility is $\rho(x, z) = Ax + z$ and the noncomplementarity is $\mu(x, z) = \frac1n x^T z$ . For a centering parameter $0 \le \delta \le 1$ , step directions $(\Delta x, \Delta z)$ solve the linear system

A\Delta x + \Delta z = -(1 - \delta)\rho(x, z), \qquad Z\Delta x + X\Delta z = \delta\mu(x, z)e - XZe. \qquad (22.5)\text{–}(22.6)

For $0 \le \beta \le 1$ the neighbourhood is

\mathcal N(\beta) = \{(x, z) > 0 : \|XZe - \mu(x, z)e\| \le \beta\mu(x, z)\},

with $\|\cdot\|$ the Euclidean norm and $(x, z) > 0$ meaning that every component is strictly positive. The algorithm starts at $x^{(0)} = z^{(0)} = e$ and alternates two steps. A predictor step starts from $(x, z) \in \mathcal N(1/4)$ , uses $\delta = 0$ , and takes the step length (22.10) $\theta = \max\{t : (x + t\Delta x, z + t\Delta z) \in \mathcal N(1/2)\}$ . A corrector step starts from $(x, z) \in \mathcal N(1/2)$ , uses $\delta = 1$ and $\theta = 1$ .

A general linear program (22.1), $\max c^Tx$ subject to $Ax \le b$ , $x \ge 0$ with $A$ now $m \times n$ , and its dual (22.2), $\min b^Ty$ subject to $A^Ty \ge c$ , $y \ge 0$ , are embedded in the homogeneous self-dual problem (22.21):

-A^Ty + c\phi + z = 0,\quad Ax - b\phi + w = 0,\quad -c^Tx + b^Ty + \psi = 0,\quad x, y, \phi, z, w, \psi \ge 0.

A feasible solution of (22.21) is strictly complementary if $x_j + z_j > 0$ , $y_i + w_i > 0$ and $\phi + \psi > 0$ for all $i, j$ .

Formalization targets

Goal: Theorem 22.5 (p. 330)

In each predictor step, starting from $(x, z) \in \mathcal N(1/4)$ with any solution $(\Delta x, \Delta z)$ of (22.5)–(22.6) at $\delta = 0$ ,

\theta \ge \frac{1}{2\sqrt n}.

The formal statement asserts that every $t \in [0, 1/(2\sqrt n)]$ keeps $(x + t\Delta x, z + t\Delta z)$ in $\mathcal N(1/2)$ , and that the supremum of the admissible step lengths is at least $1/(2\sqrt n)$ .

Milestones

Theorem 22.1: (22.4) is feasible, every feasible point is optimal, and $z^Tx = 0$ on the feasible set.
Theorem 22.2: $\Delta z^T\Delta x = 0$ , $\bar\rho = (1 - \theta + \theta\delta)\rho$ , $\bar\mu = (1 - \theta + \theta\delta)\mu$ , and $\bar X\bar Ze - \bar\mu e = (1 - \theta)(XZe - \mu e) + \theta^2\Delta X\Delta Ze$ .
Lemma 22.4: $\|PQe\| \le \frac12\|r\|^2$ for the scaled directions $p = X^{-1/2}Z^{1/2}\Delta x$ , $q = X^{1/2}Z^{-1/2}\Delta z$ , $r = p + q$ ; $\|r\|^2 = n\mu$ when $\delta = 0$ ; $\|r\|^2 \le \beta^2\mu/(1 - \beta)$ when $\delta = 1$ and $(x, z) \in \mathcal N(\beta)$ .
Theorem 22.3: a predictor step lands in $\mathcal N(1/2)$ with $\bar\mu = (1 - \theta)\mu$ ; a corrector step lands in $\mathcal N(1/4)$ with $\bar\mu = \mu$ .
Theorem 22.7: there are constants $c_j > 0$ with $x_j + z_j \ge c_j$ for every iterate $(x, z) \in \mathcal N(\beta)$ .
Theorem 22.8: a strictly complementary solution of (22.21) with $\bar\phi > 0$ yields optimal solutions $\bar x/\bar\phi$ , $\bar y/\bar\phi$ of (22.1)–(22.2); with $\bar\phi = 0$ it certifies that the primal or the dual is infeasible.

Significance

Theorem 22.5 is the quantitative core of the method. Combined with Theorem 22.3 it gives $\mu^{(2k)} \le (1 - \frac{1}{2\sqrt n})^k$ along the iterates, and therefore at most $4L\sqrt n$ iterations to bring $\mu$ below $2^{-L}$ (§22.2.4). Since the infeasibility tracks the noncomplementarity, $\rho^{(k)} = \mu^{(k)}\rho^{(0)}$ , both go to zero at that rate. Theorem 22.8 then converts the output into an answer for the original linear program: optimal primal and dual solutions, or a certificate that one of them is infeasible. Theorem 22.7 is the mechanism behind strict complementarity of the limit (Theorem 22.6, stated in the book without proof).

All results are classical and proved in the book. The mission formalizes those proofs. To the best of the curator's knowledge there is no machine-checked convergence analysis of an interior-point method for linear programming in Mathlib or on this platform; the existing platform material on interior-point methods covers a different, short-step path-following method in equality form.

Difficulty

The algebra of Theorem 22.2 is the first obstacle: the orthogonality $\Delta z^T\Delta x = 0$ is not a consequence of (22.5) alone but of skew symmetry combined with both step equations and the definition of $\mu$ , and parts (3)–(4) depend on it. The second is that the book's step length (22.10) is a maximum that need not exist, so a statement about $\theta$ must be phrased about the admissible set of step lengths, and membership in $\mathcal N(1/2)$ requires strict positivity of every component along the whole segment, not only the norm bound at its end. The norm bound alone does not control positivity; an argument that ignores this proves membership in a larger set than $\mathcal N(1/2)$ . Theorem 22.7 needs a strictly complementary feasible solution of (22.4), whose existence (Theorem 10.6 in the book, the Goldman–Tucker theorem) is itself a substantial result not available in Mathlib.

Formalization scope

Vectors are functions Fin n → ℝ (and Fin m → ℝ), matrices are Matrix (Fin m) (Fin n) ℝ, and all declarations sit in the namespace VanderbeiLP.SelfDual. The committed conventions are:

The Euclidean norm is defined explicitly (euclidNorm); Mathlib's default norm on Fin n → ℝ is the sup norm and is not used.
$\mu(x, z) = \frac1n x^Tz$ with $n \ge 2$ , the standing assumption of §22.2, carried as a hypothesis by every theorem about (22.4) together with $A^T = -A$ .
Step directions are any solution of (22.5)–(22.6); existence and uniqueness of the solution are neither assumed nor claimed.
The predictor step length is the supremum of $\{t \in \mathbb{R} : (x + t\Delta x, z + t\Delta z) \in \mathcal N(1/2)\}$ . This set contains $0$ and is bounded above by $1$ along a predictor direction, so the supremum is never a default value. Theorem 22.3(1) is stated under the hypothesis that the maximum exists, as (22.10) presumes.
Theorem 22.7 is stated for points of $\mathcal N(\beta)$ with $0 \le \beta < 1$ satisfying $\rho(x, z) = \mu(x, z)\rho(e, e)$ , the relation all iterates satisfy. The constants $c_j$ are quantified before $(x, z)$ and depend only on $A$ and $\beta$ . The existence of a strictly complementary solution of (22.4) is not a hypothesis.
Theorem 22.8 is for arbitrary $m, n$ and data $(A, b, c)$ ; "optimal" means feasible and attaining the best objective value among feasible points.
No explicit constants beyond those printed in the statements ( $1/4$ , $1/2$ , $1/(2\sqrt n)$ , $\beta^2/(1-\beta)$ ) occur; the book leaves no constant implicit in the formalized results.

A trivializing formalization is ruled out: the step length is not a default-valued supremum, $\mathcal N(\beta)$ requires strict positivity and uses the Euclidean norm, and the goal is also stated as the segment property its proof establishes.

Theorem 22.6 (convergence of the iterates to a strictly complementary solution) is stated without proof in the book and is not part of this mission; the $4L\sqrt n$ iteration count of §22.2.4 is an unnumbered corollary. Both are welcome as follow-up work, as is a proof of Theorem 10.6 for skew-symmetric systems, which Theorem 22.7 needs.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 22. https://doi.org/10.1007/978-1-4614-7630-6
S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal–dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt n L)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97. https://doi.org/10.1515/9781400881987-005

10 thms1 active userReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions VIII: Quadratic Convergence of the Gradient Orthogonalization Method for Nonlinear EquationsTextbook

Motivation

Solving a square system of nonlinear equations $\psi_i(x) = 0$ , $i = 1, \dots, n$ , $x \in \mathbb{R}^n$ , is one of the oldest tasks of numerical analysis. It appears whenever optimality conditions, equilibrium conditions or discretized differential equations have to be solved. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński) treats such a system as the nonsmooth minimization problem

\min_{x \in E_n} f(x), \qquad f(x) = \max_{1 \le i \le n} |\psi_i(x)|,

whose optimal value is $0$ exactly when the system is consistent. Section 3.5 of the book applies the subgradient method with space dilation to this problem. At each iteration that method needs the gradient of one of the $\psi_i$ , not all $n$ of them. Taking the dilation coefficient to its extreme value ( $\beta = 0$ ) turns the method into a gradient orthogonalization method. The book shows that this method converges at a quadratic rate near a regular solution, like Newton's method, although it never forms or factorizes the Jacobian.

This mission is the eighth in a series formalizing Shor's book. It covers Sections 3.5–3.6 (printed pp. 62–71).

Setting

$E_n$ is the $n$ -dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$ . The data are functions $\psi_1, \dots, \psi_n : E_n \to \mathbb{R}$ with gradients $g_{\psi_i}(x)$ , and the max-residual function is $f(x) = \max_i |\psi_i(x)|$ (3.24). The Jacobian is the matrix $J(x) = \{\partial\psi_i/\partial t_j\}_{i,j=1}^n$ of partial derivatives with respect to the coordinates $x = \{t_1, \dots, t_n\}$ .

An almost-gradient of a function $f$ at $x_0$ is an accumulation point of a sequence of gradients $\nabla f(x_k)$ , where $x_k \to x_0$ and $f$ is differentiable at every $x_k$ (p. 18).

The regular case (p. 63) is the situation in which $f^* = \min f = 0$ is attained at a point $x^*$ , the $\psi_i$ are continuously differentiable near $x^*$ , and $J(x^*)$ is nonsingular.

The gradient orthogonalization method (3.27) runs in stages of $n$ steps. A stage starting at $x_0$ produces $x_1, \dots, x_n$ as follows. At step $k+1$ , $0 \le k < n$ , the gradient $g_{\psi_{k+1}}(x_k)$ is projected on the subspace orthogonal to the gradients $g_{\psi_1}(x_0), \dots, g_{\psi_k}(x_{k-1})$ used earlier in the stage. Call the result $\varphi_{k+1}$ . The step is

x_{k+1} = x_k - \frac{\psi_{k+1}(x_k)}{\|\varphi_{k+1}\|^2}\, \varphi_{k+1}.

For $k = 0$ there is nothing to project, so $\varphi_1 = g_{\psi_1}(x_0)$ . The next stage starts at $x_n$ .

Formalization targets

Goal: Theorem 3.9, one stage squares the error

Let $x^* = 0$ solve the system, let the $\psi_i$ be continuously differentiable with gradients Lipschitz with constant $L$ on a ball $S_\delta = \{x : \|x\| < \delta\}$ (3.28), and let $g_{\psi_1}(0), \dots, g_{\psi_n}(0)$ be linearly independent. Then there exist $\varepsilon > 0$ and $c > 0$ such that every stage with $\|x_0\| \le \varepsilon$ satisfies

\|x_n\| \le c\, \|x_0\|^2 .

Milestones inside the proof

The proof of Theorem 3.9 passes through these displayed results, stated here in attack order:

Eq. (3.29): near the solution, the orthogonalized gradients satisfy $\|\varphi_{k+1}\| > b > 0$ , with $b$ uniform over stages.
Eq. (3.33): after step $k+1$ , $|\psi_{k+1}(x_{k+1})| \le (L/b^2)\, \psi_{k+1}^2(x_k)$ .
Lemma 3.1: a step of length $h$ in a unit direction orthogonal to $g_{\psi_i}(x_1)$ changes $\psi_i$ by at most $L h (h + \|x_1 - x_2\|)$ .
Eqs. (3.36)–(3.37): within a stage, $\max_k \|x_k\| \le c_1 \|x_0\|$ , and at the end point $f(x_n) \ge c_2 \|x_n\|$ .

Companion result: Theorem 3.8

In the regular case, for every $\delta > 0$ there is a neighborhood of $x^*$ in which every almost-gradient satisfies

(1-\delta) f(x) \le (g_f(x), x - x^*) \le (1+\delta) f(x).

Significance

Theorem 3.9 says that a method which evaluates one equation and one gradient per step, and never solves a linear system, has the local quadratic rate of Newton's method on a regular system. The stages combine: once one stage starts close enough to the solution, the errors of later stages satisfy $\|x_0^{(r+1)}\| \le c\|x_0^{(r)}\|^2$ . Theorem 3.8 describes the geometry of $f$ near a regular solution. The ratio of $(g_f(x), x - x^*)$ to $f(x)$ tends to $1$ , which is what allows the dilation parameters of the book's Theorem 3.3 to approach their extreme values near the solution. Both results connect the nonsmooth space-dilation methods of Chapter 3 to classical Newton-type theory.

All results of this mission are proved in the book. None of them has, to our knowledge, a machine-checked proof: the platform has local quadratic convergence results for cubic-regularized Newton, proximal Newton and semismooth Newton, but not for this method. The work is formalizing Shor's proof. This includes building the Gram-determinant argument behind (3.29) and the second-order estimates, which are reusable for other projection-based solvers of Kaczmarz type.

Difficulty

A naive argument analyses each step as a Newton step for one equation and stops there. That shows each equation $\psi_{k+1}$ is small right after its own step, but the theorem needs all equations to be small at the end of the stage. Later steps move the point and can undo the progress on earlier equations. The step directions are orthogonal to the earlier gradients, but those gradients were taken at earlier points, not at the current one. Controlling this drift needs Lemma 3.1 together with the bound (3.36), which says that the whole stage stays within a multiple of $\|x_0\|$ .

A second difficulty is that the method is only defined near the solution. The step divides by $\|\varphi_{k+1}\|^2$ , and a uniform positive lower bound on these norms comes from the nonvanishing of a Gram determinant evaluated at $n$ different points. The final passage from small residuals to a small error needs the growth bound (3.37), which uses the nonsingularity of the Jacobian once more.

Formalization scope

Representation. $E_n$ is EuclideanSpace ℝ (Fin n). The equations are a family ψ : Fin n → E_n → ℝ indexed from $0$ , so ψ k is the book's $\psi_{k+1}$ . Gradients are Mathlib's gradient, and $S_\delta$ is the open ball Metric.ball 0 δ. Continuous differentiability is ContDiff ℝ 1; in Theorem 3.8 it is ContDiffOn ℝ 1 on a neighborhood of $x^*$ .
The stage. A stage is a predicate IsOrthStage ψ x on a sequence $x : \mathbb{N} \to E_n$ , which fixes $x_1, \dots, x_n$ from $x_0$ . The projection is starProjection onto the orthogonal complement of the span of the earlier gradients.
Corrected misprint. The printed Step 1, (3.27a), divides by $\|g_{\psi_1}(x_0)\|$ rather than its square. The formalization uses the square, which is what (3.27b) and the proof's (3.31)–(3.33) require at $k = 0$ .
Division by zero. The book gives no rule for $\varphi_{k+1} = 0$ ; Lean's $t/0 = 0$ would leave the point unchanged. All statements apply the method only near the solution, where (3.29) bounds $\|\varphi_{k+1}\|$ away from zero.
Quantifier order. In Theorem 3.9 and in (3.29), (3.36)–(3.37), the constants ( $\varepsilon$ , $c$ , $\delta'$ , $b$ , $\varepsilon_0$ , $c_1$ , $c_2$ ) are existentials placed before the stage. They depend only on the data $\psi, \delta, L$ . A statement with $c$ chosen after $x_0$ would be trivial, with $c = \|x_n\|/\|x_0\|^2$ , and is ruled out.
Nonsingularity. In Theorem 3.9 it is the linear independence of $g_{\psi_i}(0)$ , the book's primary hypothesis. In Theorem 3.8 it is $\det J(x^*) \ne 0$ , with $J$ defined by coordinate partial derivatives.
Almost-gradients. They are quantified universally: Theorem 3.8 holds for every almost-gradient, not for one chosen one.

Not formalized: Theorem 3.10 (pp. 70–71), the $n$ -step quadratic convergence of the $\beta = 0$ r-algorithm with resetting. Its directional minimization rule is not pinned down on the page. The algorithm says "determined by minimizing", while the proof uses "the smallest positive root" of a stationarity equation. A contribution that fixes this rule and states the theorem is welcome as a follow-up.

Contributions of any of the five milestones are welcome independently. The Gram-determinant lower bound (3.29) and Lemma 3.1 are general facts about orthogonalization and Lipschitz gradients, and are useful beyond this mission.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.5–3.6, pp. 62–71. https://doi.org/10.1007/978-3-642-82118-9
J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970. https://doi.org/10.1137/1.9780898719468

10 thms1 active userReviewed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions VI: Almost-Sure Convergence of the Stochastic Subgradient MethodTextbook

Motivation

Many optimization problems in operations research are posed on an expectation: a two-stage or multistage stochastic program minimizes $f(x) = E\,F(x,\xi)$ , where $F(\cdot,\xi)$ is convex but nonsmooth and the expectation cannot be computed exactly. What can be computed is a stochastic subgradient, a random vector whose mean is a subgradient of $f$ . The stochastic subgradient method replaces the exact subgradient in the classical method by such a random vector. It was introduced by Yu. M. Ermoliev and N. Z. Shor in 1968 and developed by Ermoliev, Nurminski and others into a standard tool of stochastic programming; the same scheme, under the name stochastic (sub)gradient descent, underlies most of large-scale machine learning.

This mission formalizes Section 2.6 of N. Z. Shor, Minimization Methods for Non-Differentiable Functions (Springer 1985): the almost-sure convergence theorem for the stochastic subgradient method (Theorem 2.19), together with two deterministic results of the same section on perturbed and restarted variants of the subgradient method (Theorems 2.18 and 2.20).

Timeline, as recorded in the book:

1968, Ermoliev and Shor: the notion of a stochastic subgradient, introduced for a random search method for two-stage stochastic programs; the convergence theorem reproduced as Theorem 2.19.
1972, Bazhenov: convergence of a subgradient method with restarts for almost differentiable (in general nonconvex) functions, Theorem 2.18.
1976, Shepilov: stability of the subgradient method with respect to errors in the point where the subgradient is computed, Theorem 2.20.

Setting

$E_n$ is $n$ -dimensional Euclidean space with inner product $(x,y)$ . A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$ ; $M^*$ is the set of minimum points of $f$ .

Stochastic subgradient method. Fix a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_k)_{k \ge 0}$ , a deterministic starting point $x_0$ , stepsize rules $h_k : E_n \to \mathbb{R}$ and random vectors $g_k : \Omega \to E_n$ . The iterates are

x_{k+1} = x_k - h_k(x_k)\, g_k, \qquad k = 0,1,\dots

In the book's notation $g_k = g_\omega(x_k)$ : a random vector whose expectation, given the state at step $k$ , is a subgradient of $f$ at $x_k$ . In the Lean development the iterates are stochIter h G x₀ k ω.

Perturbed subgradient method (Shepilov). Given a subgradient selection $g_f$ , points $\tilde x_k$ with $\|\tilde x_k - x_k\| \le \delta_k$ , and steps $h_k > 0$ : $x_{k+1} = x_k - h_k\, g_f(\tilde x_k)/\|g_f(\tilde x_k)\|$ .

Restarted method (Bazhenov). For a function $f$ that is almost differentiable (Lipschitz on bounded sets, differentiable almost everywhere, with gradient continuous where it exists) and a selection $g_f(x)$ of almost-gradients (limit points of gradients at nearby points of differentiability), with $S_r = \{x : \|x - x^*\| \le r\}$ : take the normalized step $\bar x_{k+1} = x_k - h_k\, g_f(x_k)/\|g_f(x_k)\|$ and restart from $x_0$ whenever $\bar x_{k+1}$ leaves $S_r$ (resetIter).

Formalization targets

Goal: Theorem 2.19 (p. 46)

Let $f$ be convex with a unique minimum point $x^*$ . Suppose $E\{g_k \mid \mathcal F_k\}$ is a subgradient of $f$ at $x_k$ , $E\{\|g_k\|^2 \mid \mathcal F_k\} \le c$ , and almost surely $h_k(x_k) > 0$ , $\sum_k h_k(x_k) = +\infty$ , $\sum_k h_k^2(x_k) < \infty$ . Then

P\Big(\lim_{k\to\infty} \|x_k - x^*\| = 0\Big) = 1 .

Milestones

Eq. (2.42), the conditional one-step inequality

E\{\|x_{k+1} - x^*\|^2 \mid \mathcal F_k\} \le \|x_k - x^*\|^2 + c\,h_k^2(x_k).

Proof of Theorem 2.19, pp. 46–47: with probability one $\|x_k - x^*\|^2$ converges to a finite limit (no divergence condition on the steps).
Theorem 2.20 (Shepilov): under $\delta_k \to 0$ , $\sum h_k\delta_k < \infty$ , $\sum h_k^2 < \infty$ , $\sum h_k = \infty$ , the perturbed method converges to a point of $M^*$ .
Theorem 2.18 (Bazhenov): if $f(x^*) = \min_{S_r} f$ and $\inf_{S_r\setminus S_\varepsilon} (g_f(x), x - x^*) > 0$ for every $0 < \varepsilon < r$ , the restarted method with $h_k \to 0$ , $\sum h_k = \infty$ converges to $x^*$ from any $x_0 \in S_r$ .

Significance

Theorem 2.19 is the basic justification of stochastic subgradient methods: without computing $f$ or any exact subgradient, the method reaches the minimizer with probability one, under stepsize conditions that are met by $h_k = 1/(k+1)$ . It is the nonsmooth convex counterpart of the Robbins–Monro theorem and the prototype of the almost-sure convergence results for stochastic quasi-gradient methods used in stochastic programming. Theorem 2.20 shows that the deterministic method tolerates summable errors in the point where the subgradient is evaluated, which is what allows subgradients to be approximated by finite differences (Section 1.3). Theorem 2.18 extends the convergence of the normalized method to local minima of a class of nonconvex functions.

All four results are proved in the literature. To the best of the platform search (September 2026), none is machine-checked: the platform has almost-sure convergence theorems for smooth stochastic approximation under ODE-type hypotheses (Borkar–Meyn) and in-expectation bounds for stochastic gradient descent, neither of which covers this recursion. A formal proof of the goal would give a reusable almost-sure convergence argument for nonsmooth stochastic methods on top of Mathlib's martingale theory.

Difficulty

The deterministic proof of convergence of the subgradient method compares $\|x_{k+1}-x^*\|^2$ with $\|x_k - x^*\|^2$ along the whole trajectory. With random directions this comparison holds only in conditional expectation, and the term $h_k(g_k - E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ is not controlled pathwise. Taking expectations of the one-step inequality and summing gives only bounds on $E\|x_k - x^*\|^2$ , which do not yield almost-sure convergence. Moreover the stepsize $h_k(x_k)$ depends on the random iterate, so the conditions $\sum h_k^2(x_k) < \infty$ and $\sum h_k(x_k) = \infty$ hold only almost surely, not uniformly, and the iterates need not be square-integrable. Identifying the almost-sure limit as $0$ requires using the uniqueness of the minimizer to bound $(E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ away from zero outside a neighbourhood of $x^*$ .

In Theorems 2.18 and 2.20 the difficulty is that the distance to $x^*$ is not monotone: steps taken near the solution, or with a perturbed subgradient, can increase it, and a restart can move the iterate far away.

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere); convexity is ConvexOn ℝ Set.univ f; uniqueness of $x^*$ is a separate hypothesis.
Probabilistic model. The book assumes the distribution of $g_\omega(x_k)$ is determined by $x_k$ and independent of the past, and remarks this is inessential. The formalization uses a filtration: $g_k$ is $\mathcal F_{k+1}$ -measurable, each $h_k$ is Borel measurable, $x_0$ is deterministic, and the hypotheses are on conditional expectations given $\mathcal F_k$ . This contains the book's model.
Condition (iii) is printed as $E\|g_\omega(x_k)\|^2 \le c$ ; the proof uses the conditional bound in (2.42), and the formalization assumes the conditional bound $E\{\|g_k\|^2\mid\mathcal F_k\} \le c$ almost surely.
Every expectation carries an integrability hypothesis ( $g_k$ and $\|g_k\|^2$ integrable), so no conditional expectation defaults to Lean's junk value $0$ . The one-step milestone assumes $\|x_k - x^*\|^2$ integrable and a bounded stepsize rule at that step, and concludes integrability of $\|x_{k+1}-x^*\|^2$ .
Conditions (i)–(ii) on the random stepsizes are required almost surely. "With probability one $\lim\|x_k - x^*\| = 0$ " is ∀ᵐ ω ∂μ, Tendsto (fun k => ‖x k ω - x*‖) atTop (𝓝 0).
Division by zero. In Theorems 2.18 and 2.20 the normalized step is undefined when the subgradient vanishes; the formalization skips the step (the iterate is repeated) by an explicit branch, not through Lean's convention $x/0 = 0$ . When the subgradient never vanishes the sequences are exactly the book's.
The printed display (2.42) has $x_k$ where $x_{k+1}$ is meant on its left-hand side; the corrected inequality is stated.
A trivializing formalization, for instance dropping the integrability hypotheses so that the conditional expectations vanish, or quantifying the stepsize conditions so that they cannot hold, is excluded by the hypotheses above; the hypotheses are satisfiable (deterministic subgradients of $f(x) = \|x\|$ with $h_k = 1/(k+1)$ ).
Mathlib supplies conditional expectation (MeasureTheory.condExp), filtrations, and almost-sure convergence of $L^1$ -bounded (sub/super)martingales; the supermartingale convergence theorem the book cites from Doob is used from Mathlib, not restated. A Robbins–Siegmund-type lemma for nonnegative almost-supermartingales would be the natural reusable contribution. The almost-differentiability and subgradient definitions duplicate drafts of other missions in this series.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Section 2.6, pp. 44–47. https://doi.org/10.1007/978-3-642-82118-9
Yu. M. Ermoliev and N. Z. Shor, A random search method for two-stage problems of stochastic programming and its generalization, Kibernetika (Kiev), no. 1, 90–92, 1968.
L. G. Bazhenov, On the conditions for convergence of methods for minimizing almost differentiable functions, Kibernetika (Kiev), no. 4, 71–72, 1972.
M. A. Shepilov, On a method of generalized gradient for finding the absolute minimum of a convex function, Kibernetika (Kiev), no. 4, 52–57, 1976.
Yu. M. Ermoliev, Methods of Stochastic Programming, Nauka, Moscow, 1976.
H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971, pp. 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
J. L. Doob, Stochastic Processes, Wiley, New York, 1953 (supermartingale convergence theorem).

11 thms1 active userReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions V: Polyak's Stepsize and Fejér-Type ApproximationsTextbook

Motivation

The subgradient method for a convex function $f$ moves from $x_k$ against a subgradient $g_f(x_k)$ , and everything hinges on the step length. Divergent-series stepsizes guarantee convergence but are slow and need no information about $f$ . When the optimal value $f^*$ , or any level $c$ that is known to be attainable, is available, B. T. Polyak proposed in 1969 the step

x_{k+1} = x_k - \frac{\gamma\,[f(x_k) - c]}{\|g_f(x_k)\|^2}\, g_f(x_k),

which uses the current gap $f(x_k) - c$ to scale the move. This Polyak stepsize is still the reference adaptive rule in nonsmooth convex optimization, in the solution of convex feasibility problems, and in the Lagrangian relaxation heuristics of integer programming (Held–Wolfe–Crowder, Camerini–Fratta–Maffioli), where it is known under the name "relaxation step".

Section 2.4 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) places Polyak's rule in the framework of Fejér-type approximations developed by I. I. Eremin: an iteration whose map strictly decreases the distance to every point of a target set. It then proves convergence of the rule, linear rates under growth conditions, its behaviour when the level is set too low, and a property of the conjugate-subgradient direction of Camerini, Fratta and Maffioli (1975).

Timeline:

1965–1969: Eremin introduces Fejér mappings for systems of convex inequalities.
1969: Polyak, Minimization of unsmooth functionals, proposes the step with the known optimal value and proves convergence and a linear rate under a sharp-minimum condition.
1975: Camerini, Fratta and Maffioli combine the Polyak step with a conjugate direction for Lagrangian relaxation.
1985: Shor's book collects these results in Section 2.4 (Theorems 2.10–2.16).

Setting

$E_n$ is the $n$ -dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$ . A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$ . A subgradient selection is a map $g_f$ with $g_f(x)$ a subgradient at every $x$ ; nothing else is assumed about it, in particular not continuity.

For a nonempty set $M \subseteq E_n$ , a map $\varphi : E_n \to E_n$ is $M$ -Fejér if $\varphi(y) = y$ and $\|\varphi(x) - y\| < \|x - y\|$ for all $y \in M$ and $x \notin M$ .

For a convex $f$ with $f^* = \inf f$ and a level $c \ge f^*$ , let $M(c) = \{x : f(x) \le c\}$ . Polyak's method (2.32) is the iteration $x_{k+1} = \varphi_c(x_k)$ with the map displayed above for $x \notin M(c)$ and $\varphi_c(y) = y$ on $M(c)$ ; the factor $\gamma$ is fixed in $(0, 2)$ .

The conjugate-subgradient procedure (2.38), for a convex $f$ with minimum point $x^*$ and $f^* = f(x^*)$ , is

x_{k+1} = x_k - h_k s_k, \quad h_k = \frac{[f(x_k) - f^*]\gamma_k}{\|s_k\|^2}, \qquad s_0 = g_f(x_0),\quad s_k = g_f(x_k) + \beta_k s_{k-1}.

Formalization targets

Goal: Theorem 2.11

If $0 < \gamma < 2$ and $M(c) \neq \emptyset$ , then for any $x_0 \in E_n$

\exists k^* : x_{k^*} \in M(c) \qquad \text{or} \qquad \lim_{k \to \infty} x_k \text{ exists and lies in } M(c).

The goal fixes no constant and no rate; it asserts only that the method finds a point of the level set, in finite time or in the limit.

Milestones

Theorem 2.10. Iterates of a continuous $M$ -Fejér map converge to a point of $M$ .
Inequality (2.33). For $x_k \notin M(c)$ and $y \in M(c)$ ,

\|x_{k+1} - y\|^2 \le \|x_k - y\|^2 - \gamma(2-\gamma)\frac{[f(x_k) - c]^2}{\|g_f(x_k)\|^2} < \|x_k - y\|^2 .

Theorem 2.12. Under $f(x) - f^* \ge m\|x - x^*\|^2$ and an $L$ -Lipschitz gradient near $x^*$ , with $c = f^*$ : $\|x_k - x^*\| \le q^k \|x_0 - x^*\|$ , $q = (1 - \gamma(2-\gamma)m^2/L^2)^{1/2} < 1$ .
Theorem 2.13. Under the sharp-minimum condition $f(x) - f(x^*) \ge m\|x - x^*\|$ and subgradients bounded by $L$ near $x^*$ , with $c = f(x^*)$ : $\|x_{k+1} - x^*\| \le q\|x_k - x^*\|$ .
Theorem 2.14. If $\min \psi = d > 0$ and the method runs with $c = 0$ , then $\lim_k \min_{0 \le i \le k} \psi(x_i) \le 2d/(2-\gamma)$ .
Theorem 2.15. For (2.38) with $0 < \gamma_k \le 1$ , $\beta_k \ge 0$ : $(x_k - x^*, s_k) \ge (x_k - x^*, g_f(x_k))$ .
Theorem 2.16. With the Camerini–Fratta–Maffioli coefficient $\beta_k$ and $0 \le \alpha_k \le 2$ : $(x_k - x^*, s_k)/\|s_k\| \ge (x_k - x^*, g_f(x_k))/\|g_f(x_k)\|$ .

Significance

Theorem 2.11 is the convergence guarantee of the most widely used adaptive step rule for nonsmooth convex problems. With $c = f^*$ it yields a minimizer; with $c > f^*$ it solves the convex inequality $f(x) \le c$ , and applied to $\psi = \max_i f_i^+$ it solves consistent systems of convex inequalities. The linear rates of Theorems 2.12–2.13 are the prototype of the "sharpness implies linear convergence" results of modern first-order methods, and Theorem 2.14 quantifies the loss when the level is underestimated, which is the situation of every practical variant that estimates $f^*$ on the fly. Theorems 2.15–2.16 are the justification of the conjugate-subgradient directions used in Lagrangian relaxation.

All results are classical and proved on paper. None of them is formalized on Prove2Me: the platform has a smooth, strongly convex Polyak gradient-descent bound (a different theorem) and Fejér-monotonicity statements for polyhedral relaxation methods, but no Polyak subgradient step, no $M$ -Fejér map and no conjugate-subgradient procedure. The mission produces machine-checked versions of the whole section, with the page's misprints corrected where the proof and the statement disagree.

Difficulty

The obvious argument for the goal is to observe that $\varphi_c$ is $M(c)$ -Fejér, by (2.33), and invoke Theorem 2.10. That argument fails: Theorem 2.10 needs a continuous map, and $\varphi_c$ depends on an arbitrary subgradient selection, which is discontinuous wherever $f$ is not differentiable. The book says so explicitly. Fejér monotonicity gives boundedness and a limit of each distance $\|x_k - y\|$ , but convergence of the whole sequence to a single point of $M(c)$ , and the fact that an accumulation point cannot lie outside $M(c)$ , have to be obtained without continuity of the map.

For Theorem 2.14 the level $c = 0$ lies strictly below the minimum, so $M(0) = \emptyset$ , the target set of the iteration as run is empty, no Fejér property is available for it, and the theorem controls only the best value found, not the iterates.

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued on all of $E_n$ and ConvexOn ℝ Set.univ f.
The subgradient selection is universally quantified; no theorem assumes continuity of it.
Iterations are sequences x : ℕ → E_n with the recursion as a hypothesis; the first term is arbitrary.
Polyak's step map is defined piecewise: it returns $x$ on $M(c)$ (as the book sets $\varphi_c(y) = y$ ) and at $g_f(x) = 0$ . No statement relies on Lean's convention $x/0 = 0$ . The same holds for $h_k$ when $s_k = 0$ .
$M(c) \neq \emptyset$ is a hypothesis of the goal: the book's proof picks $y \in M(c)$ , and for $c = f^*$ not attained the conclusion is false (for $f = e^x$ , $c = 0$ , the method moves by $\gamma$ each step and diverges).
" $\lim x_k \in M(c)$ " is the existence of a limit in $M(c)$ , not a statement about cluster points.
$\gamma \in (0, 2)$ is stated in every theorem on Polyak's method; the book fixes this range at Theorem 2.11.
Theorem 2.12's "strongly convex" is used through its displayed growth condition only; the statement is made for convex $f$ satisfying it, with $L > 0$ and $q$ computed with Real.sqrt.
Theorem 2.13 assumes the bound $\|g\| \le L$ on subgradients in the ball, which is what the proof uses; a Lipschitz constant on the closed ball alone does not give it, and the printed statement fails without it.
Theorem 2.14 is stated with " $\le 2d/(2-\gamma)$ "; the printed " $=$ " is false in general.
Theorem 2.16's inequality is stated at indices where $s_k \neq 0$ and $g_f(x_k) \neq 0$ .

A formalization in which $M(c)$ may be empty, the selection is assumed continuous, or the step divides by zero through Lean's conventions would be a different theorem; these are ruled out above.

Needed infrastructure: Fejér monotone sequences in finite dimensions (bounded, with convergent distances), the subgradient inequality, and the fact that a zero subgradient characterizes a minimum. These are reusable for every subgradient-type method. Contributions of general lemmas on Fejér-monotone sequences are welcome.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §2.4, pp. 36–42. https://doi.org/10.1007/978-3-642-82118-9
B. T. Polyak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9(3), 1969, 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
I. I. Eremin, The relaxation method of solving systems of inequalities with convex functions on the left-hand side, Soviet Mathematics Doklady 6, 1965, 219–222.
P. M. Camerini, L. Fratta, F. Maffioli, On improving relaxation methods by modified gradient techniques, Mathematical Programming Study 3, 1975, 26–34.

10 thms1 active userReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions IV: Linear Convergence of the Subgradient Method under Level-Set Shape ConditionsTextbook

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$ , $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$ -dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$ ; $g_f(x)$ denotes an arbitrary subgradient at $x$ , chosen once for each $x$ . Let $M^*$ be the set of minimum points of $f$ , assumed nonempty; for $x \in E_n$ , $x^*(x)$ is the point of $M^*$ nearest to $x$ .

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$ , the normalized subgradient method is

x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$ ).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$ , asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$ .

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$ , $\sigma \ge \sqrt2$ , $h_1 \ge \|x_0 - x^*\|/\sigma$ , and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$ , then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots

Milestones

Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$ ,

\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .

Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$ .
Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$ ,

\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$ . 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$ , the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$ .

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$ . The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$ , so the iterates must be shown to stay in $Y$ , and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$ , $h_1$ being the chosen initial step (the book's " $k = 0, 1, 2, \dots$ " in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$ , never through $x/0 = 0$ ; the bounds are asserted for every $k$ , which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$ . The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$ . In (2.16) the ratio is $1/(2\cos\varphi)$ , as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$ , which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$ . In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$ , nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

9 thms1 active userReviewed