All missions

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1 (p. 9)

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

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

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

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Why the longest increasing subsequence

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

Timeline.

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 7.1.2 (p. 153)

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Why wide neighbourhoods

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2 with an explicit iteration count

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

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

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

Milestones, in the order the proof uses them

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Committed conventions and repairs:

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

$$b(\alpha,t,p)=((1-p)e^{t}+p)(p+(1-p)e^{-t/\alpha})^{\alpha}\quad(p\ge \tfrac12),\qquad b(\alpha,t,p)=b(\alpha,t,1-p)\quad(p\le\tfrac12),$$ $$a(\alpha,t)=\max\Big(1,\ (1-p+pe^{t})(p_1e^{-t/\alpha}+1-p_1)^{\alpha}\Big).$$

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

Formalization targets

Goal: Theorem 2.3.4

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

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

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

Milestones

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

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/bf02699376
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
• M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89 (2001). https://doi.org/10.1090/surv/089