All missions

Why ill-posed problems appear in learning

Estimating a probability density, a conditional probability or a conditional density from data can be written as solving a linear operator equation $Af = F$ whose right-hand side $F$ is a distribution function. The true $F$ is unknown; only its empirical estimate $F_\ell$ is available, built from $\ell$ observations. The Glivenko–Cantelli theorem and the Kolmogorov–Smirnov law (Vapnik 2000, §7.3) guarantee that $F_\ell$ is close to $F$ in the uniform metric. However, the operator $A$ (for densities, integration) has an unbounded inverse. A small change in the right-hand side can produce an arbitrarily large change in the solution, so solving $Af = F_\ell$ directly gives nonsense. Hadamard called such problems ill-posed.

Regularization handles this. Tikhonov (1963) proposed replacing the equation by the minimization of a penalized residual. Tikhonov and Arsenin (1977) proved that the regularized solutions converge to the true solution when the data error and the regularization parameter go to zero together in a controlled way. Vapnik and Stefanyuk (1978) extended this to random right-hand sides, the case of statistical estimation, and Stefanyuk (1986) to the case where the operator is estimated as well. Chapter 7 of The Nature of Statistical Learning Theory collects these results, without proofs, as the foundation of its SVM approach to density and conditional-probability estimation. This mission formalizes them.

Setting

Let $(E_1, \rho_{E_1})$ and $(E_2, \rho_{E_2})$ be metric spaces and $A : E_1 \to E_2$ a continuous one-to-one operator. The operator equation (7.12) is $Af = F$. Its solution $f$ exists and is unique, but $A^{-1}$ need not be continuous.

A regularization functional is a map $\Omega : E_1 \to [0, \infty]$ that is lower semicontinuous and whose sublevel sets $\{g : \Omega(g) \le c\}$ are compact for every $c > 0$. Its domain is $\{\Omega < \infty\}$. In Lean this is NatureSLT.IllPosed.IsRegularizer.

Tikhonov's functional (Method T) for a parameter $\gamma > 0$ and a right-hand side $F'$ is

$$W_T(g) = \rho^2_{E_2}(A g, F') + \gamma\, \Omega(g),$$

which is NatureSLT.IllPosed.tikhonovFunctional. A regularized solution is any minimizer of $W_T$ over $E_1$.

In the deterministic problem, for every $\delta > 0$ an approximation $F_\delta$ with $\rho_{E_2}(F, F_\delta) \le \delta$ is given, and $f_\delta$ minimizes $W_T$ with $F' = F_\delta$ and $\gamma = \gamma(\delta)$. In the stochastic problem, $F_\ell$ are random elements of $E_2$ converging to $F$ in probability, and $f_\ell$ minimizes $W_T$ with $F' = F_\ell$ and $\gamma = \gamma_\ell \to 0$. When the operator is also estimated by random continuous operators $A_\ell$, their distance to $A$ is measured by (7.48),

$$\|A_\ell - A\| = \sup_{\Omega(f) < \infty} \frac{\rho_{E_2}(A_\ell f, A f)}{\Omega^{1/2}(f)},$$

which is NatureSLT.IllPosed.operatorDistance.

Formalization targets

Goal: Theorem 7.1 (p. 238)

Let the exact solution $f$ lie in the domain of $\Omega$, and suppose $\gamma(\delta) > 0$ satisfies (7.17):

$$\gamma(\delta) \to 0 \ (\delta \to 0), \qquad \limsup_{\delta \to 0^+} \frac{\delta^2}{\gamma(\delta)} \le r < \infty .$$

Then every family of minimizers $f_\delta$ of $\rho^2_{E_2}(Ag, F_\delta) + \gamma(\delta)\Omega(g)$ satisfies $f_\delta \to f$ in $E_1$ as $\delta \to 0^+$. This is the weakest statement in the chapter: it fixes no rate and assumes only metric structure.

Milestones

1. Theorem 7.2 (p. 238). $E_1$ is a real Hilbert space, $A$ is linear, $\Omega(f) = \|f\|^2$, $\gamma(\delta) \to 0$ and $\delta^2/\gamma(\delta) \to 0$ (7.18). Then minimizers of (7.19) converge to $f$ in norm.
2. Theorem 7.3 (p. 239). For any $\varepsilon, \mu > 0$ there is $n(\varepsilon,\mu)$ such that for all $\ell > n(\varepsilon,\mu)$

$$P\{\rho_{E_1}(f_\ell, f) > \varepsilon\} \le P\{\rho_{E_2}(F_\ell, F) > \sqrt{\gamma_\ell\,\mu}\}. \tag{7.21}$$

3. Theorem 7.4 (p. 239). $E_1$ Hilbert, $A$ linear, $\Omega(f) = \|f\|^2$. For any $\varepsilon > 0$ there is $n(\varepsilon)$ such that for all $\ell > n(\varepsilon)$

$$P\{\|f_\ell - f\|^2 > \varepsilon\} < 2\,P\{\rho^2_{E_2}(F_\ell, F) > \tfrac{\varepsilon}{2}\gamma_\ell\}.$$

4. Theorem 7.5 (p. 251). For any $\varepsilon > 0$ and constants $C_1, C_2 > 0$ there is $\gamma_0 > 0$ such that for any $\gamma_\ell \le \gamma_0$

$$P\{\rho_{E_1}(f_\ell, f) > \varepsilon\} \le P\{\rho_{E_2}(F_\ell, F) > C_1\sqrt{\gamma_\ell}\} + P\{\|A_\ell - A\| > C_2\sqrt{\gamma_\ell}\}. \tag{7.49}$$

The constants are the book's: the $r$ of (7.17), the $\sqrt{\gamma_\ell\mu}$ of (7.21), the factor $2$ and the threshold $\tfrac{\varepsilon}{2}\gamma_\ell$ of Theorem 7.4, and the $C_1\sqrt{\gamma_\ell}$, $C_2\sqrt{\gamma_\ell}$ of (7.49).

Significance

Theorem 7.1 is what makes regularization a method rather than a heuristic: it names the admissible parameter choices, $\gamma(\delta) \to 0$ no faster than $\delta^2$, under which the regularized solution recovers the true one. Theorems 7.3 and 7.4 turn it into probability statements. Combined with any rate of convergence of the empirical distribution function, they give consistency of density estimation by Method T, which is the Corollary on p. 239. Theorem 7.5 does the same when the operator itself is estimated from data, as in conditional probability estimation (§7.9). Chapter 7's SVM estimators of densities and conditional probabilities rest on these statements.

The results are classical and proved in the literature cited. None of them is machine-checked. The platform has Tikhonov-regularized dynamics (TikhonovHDD) and finite-dimensional ridge identities (RobustLS.Tikhonov), but not the convergence theory of Tikhonov's method for operator equations. A formalization supplies a reusable notion of regularization functional on a metric space, the Tikhonov functional over $[0,\infty]$, and the operator distance (7.48), for later work on inverse problems and nonparametric estimation.

Difficulty

The obvious approach, inverting $A$ and passing to the limit, fails because $A^{-1}$ is not continuous: $\rho_{E_2}(Af_\delta, F) \to 0$ alone does not force $f_\delta \to f$. The deterministic theorems need control of the regularized solutions that the residual does not give, and in Theorem 7.2 that control must be obtained without compact sublevel sets, since the balls of an infinite-dimensional Hilbert space are not compact. In the stochastic theorems the difficulty is uniformity: a deterministic convergence statement for each outcome does not give the explicit comparison of probabilities that (7.21) and (7.49) assert. In (7.49) the bound must hold for every parameter below a threshold that depends only on $\varepsilon$, $C_1$, $C_2$.

Two warnings from reading the chapter apply. Theorem 7.4 as printed is false: with exact data ($F_\ell = F$) both probabilities vanish for all large $\ell$, and the strict inequality $0 < 0$ fails (finding F1). Also, the three "uniqueness" properties of $\Omega$ listed on p. 235 are mutually inconsistent at $f = 0$, which is why they are not assumed (finding F3).

Formalization scope

All statements live in NatureSLT.IllPosed. $\Omega$ takes values in ℝ≥0∞. The book's "positive" is nonnegativity and its domain $\mathcal F$ is $\{\Omega \ne \infty\}$. "Semicontinuous" is lower semicontinuity. The exact solution is assumed to lie in the domain of $\Omega$ (the book assumes this tacitly); otherwise every point could minimize $W_T$. Every theorem is stated for every family of minimizers, given as a hypothesis, never for a chosen sequence, and does not assert that minimizers exist. Statements of the form "there exists a sequence that converges" are a trivializing formalization and are ruled out. The limit in (7.17) is read as a limsup in $[0,\infty]$, and $\delta \to 0$ is taken along $\delta > 0$. Hilbert spaces are real. Linearity of $A$ (Theorems 7.2 and 7.4) makes $E_2$ a real normed space. In the stochastic theorems the probability space $(S, P)$ is arbitrary, and the random elements $F_\ell$, $f_\ell$ (and in 7.5 the random distance $\|A_\ell - A\|$) are Borel measurable by hypothesis, so no event gets probability zero by convention. In (7.48) a point with $\Omega(f) = 0$ contributes $0$ if $A_\ell f = Af$ and $\infty$ otherwise. In Theorem 7.5, $\gamma_0$ is quantified before the random data, so it is uniform over all of them.

Beyond the paper. One variant item is posed: [Corrected] Theorem 7.4, the same statement with $\le$ in place of $<$. Its evidence is the exact-data counterexample above, which has been checked in Lean. The faithful Theorem 7.4 stays a milestone.

Not included: the Glivenko–Cantelli theorem in the book's in-probability form (the platform's GlivenkoCantelli.glivenko_cantelli is the almost-sure form), the Kolmogorov–Smirnov limit laws (7.10)–(7.11), and Theorem 7.6, whose notion of consistency is not pinned down on the page. Contributions welcome: compactness arguments in metric spaces, weak compactness and the Radon–Riesz property in Hilbert spaces, and measurability lemmas for minimizers.

Selected references

• V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000, Chapter 7. https://doi.org/10.1007/978-1-4757-3264-1
• A. N. Tikhonov, "On solving ill-posed problem and method of regularization", Doklady Akademii Nauk USSR 153 (1963), 501–504 (as cited in Vapnik 2000; no stable link).
• A. N. Tikhonov and V. Y. Arsenin, Solution of Ill-Posed Problems, W. H. Winston, Washington, DC, 1977 (no stable link).
• V. N. Vapnik and A. R. Stefanyuk, "Nonparametric methods for estimating probability densities", Automation and Remote Control (8), 1978 (as cited in Vapnik 2000; no stable link).
• A. R. Stefanyuk, 1986, cited in Vapnik 2000, p. 251, for Theorem 7.5; the book's bibliography gives no entry for it.
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998, which contains the proofs the 2000 book omits (no stable link).

Motivation

A support vector machine never computes its feature map. It only evaluates a kernel $K(x, y)$, the inner product of the feature vectors of $x$ and $y$. When the features are the first $N$ terms of an expansion, or infinitely many terms damped by regularizing weights, the learning algorithm is practical only if that inner product has a closed form. Chapter 6 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1), §6.3–6.5, gives such closed forms for the kernels generating orthogonal-polynomial, spline and Fourier expansions. It also states Theorem 6.1, which lifts any one-dimensional kernel to $n$ dimensions. The book prints these identities without proof and cites classical sources (Mikhlin 1964; Gradshtein and Ryzhik 1980). Several of them, as printed, are off by a constant factor, which a formal check settles.

Setting

Kernels in this mission are real functions of two real variables (or of two vectors of $\mathbb R^n$) of the form $K(x, y) = \sum_i r_i\, \psi_i(x)\, \psi_i(y)$, a finite or convergent sum over basis functions $\psi_i$ with weights $r_i \ge 0$.

• Orthonormal polynomials. $P_1, P_2, \dots$ are real polynomials with $\deg P_k = k - 1$ that are orthonormal for a measure $\mu$ on $\mathbb R$ with finite moments. $K_n(x, y) = \sum_{k=1}^n P_k(x) P_k(y)$ is the kernel of the first $n$ of them.
• Hermite. $P_k(x) = (-1)^k e^{x^2} (d/dx)^k e^{-x^2}$, and $H_k(x) = \mu_k P_k(x) e^{-x^2}$ with normalization constants $\mu_k$ (6.23). The regularized kernel is $\sum_{i \ge 0} q^i H_i(x) H_i(y)$ with $0 \le q < 1$.
• Tensor products. Given coordinatewise basis functions $b_i$ on a set $X$, the $n$-dimensional basis is $b_{i_1 \dots i_n}(x) = b_{i_1}(x^1) \cdots b_{i_n}(x^n)$ (6.25).
• Splines. The truncated power $(x - t)^d_+$ is $0$ for $x \le t$ and $(x - t)^d$ for $x > t$. The spline kernel with infinitely many nodes on $(0, a)$ is $\int_0^a (x_j - t)^d_+ (x_i - t)^d_+\, dt + \sum_{r=0}^d x_j^r x_i^r$ for $x_j, x_i \in [0, a]$.
• Fourier. $K_N(x, x_i) = \tfrac12 + \sum_{k=1}^N (\sin kx \sin kx_i + \cos kx \cos kx_i)$ is the kernel of the trigonometric polynomials of degree $N$. Its regularized versions damp the $k$-th harmonic by $q^k$ ($0 < q < 1$) or by $1/(1 + \gamma^2 k^2)$ ($\gamma > 0$).

Formalization targets

Goal: Eq. (6.33)

For $\gamma > 0$ and real $x_i, x_j$ with $0 \le |x_i - x_j| \le 2\pi$, the series converges and

$$\frac12 + \sum_{k=1}^{\infty} \frac{\cos kx_i \cos kx_j + \sin kx_i \sin kx_j}{1 + \gamma^2 k^2} = \frac{\pi}{2\gamma}\, \frac{\cosh\frac{\pi - |x_i - x_j|}{\gamma}}{\sinh\frac{\pi}{\gamma}} .$$

The only numbered theorem of the section, Theorem 6.1, is close to an unfolding of the definitions. The goal is therefore the deepest identity of the section that is correct as printed.

Milestones

1. (6.21), Christoffel–Darboux. There is a constant $a_n$ such that $K_n(x, y) = a_n \frac{P_{n+1}(x)P_n(y) - P_n(x)P_{n+1}(y)}{x - y}$ for $x \ne y$ and $K_n(x, x) = a_n[P'_{n+1}(x)P_n(x) - P'_n(x)P_{n+1}(x)]$.
2. (6.24), Hermite kernel. For some constants $\mu_k$: $\sum_{i \ge 0} q^i H_i(x)H_i(y) = \frac{1}{\sqrt{\pi(1-q^2)}} \exp\{\frac{2xyq}{1+q} - \frac{(x-y)^2q^2}{1-q^2}\}$ for all $0 \le q < 1$ and real $x, y$.
3. Theorem 6.1. $\sum_{(i_1, \dots, i_n)} b_{i_1 \dots i_n}(x)\, b_{i_1 \dots i_n}(y) = \prod_{k=1}^n \sum_i b_i(x^k) b_i(y^k)$, for finite bases or bases whose one-dimensional kernel converges.
4. (6.26). $\prod_{i=1}^n \frac{1}{\sqrt{\pi(1-q^2)}} \exp\{\cdots\} = \frac{1}{(1-q^2)^{n/2}} \exp\{\frac{2(x*y)q}{1+q} - \frac{|x-y|^2q^2}{1-q^2}\}$.
5. (6.30), splines. For $d \ge 0$, the spline kernel equals $\sum_{r=0}^d \frac{C_d^r}{2d - r + 1} (x_j \wedge x_i)^{2d-r+1} |x_j - x_i|^r + \sum_{r=0}^d x_j^r x_i^r$. For $d = 1$ this is $1 + x_jx_i + \frac12|x_j - x_i|(x_j \wedge x_i)^2 + (x_j \wedge x_i)^3/3$.
6. Dirichlet kernel (p. 197). $K_N(x, x_i) = \frac12 + \sum_{k=1}^N \cos k(x - x_i) = \sin\frac{(2N+1)(x - x_i)}{2} \big/ \sin\frac{x - x_i}{2}$ for $x - x_i \notin 2\pi\mathbb Z$.
7. (6.32), Poisson kernel. For $0 < q < 1$: $\frac12 + \sum_{k \ge 1} q^k \cos k(x_i - x_j) = \frac{1 - q^2}{2(1 - 2q\cos(x_i - x_j) + q^2)}$.

Milestones 2, 4 and 6 are stated exactly as printed and are believed false (see Formalization scope). A disproof of each is a complete answer.

Significance

The result itself. Each closed form replaces an infinite or high-dimensional inner product by a constant number of elementary operations. That is what makes the regularized Fourier, Hermite and spline kernels usable in an SVM. Theorem 6.1 is the mechanism by which every multidimensional kernel of Chapter 6 is obtained from a one-dimensional one. The constants matter in practice. A wrong prefactor rescales the kernel matrix, and so the effective regularization of the SVM solution.

Formalizing it. The identities themselves are classical (Christoffel 1858, Darboux 1878, Mehler 1866, and the Fourier series of $\cosh$ on $[0, 2\pi]$). As far as a search of the platform shows, none is stated on Prove2Me in these forms. SpikedWishart.Separated.eq_299 (Open) is one Christoffel–Darboux instance for a specific Hermite family. AronszajnRK.Product.direct_product_kernel concerns reproducing-kernel Hilbert spaces, not finite or summable feature sums. The mission produces machine-checked versions of the book's catalogue, together with a formal verdict on the three displays that are off by a constant.

Difficulty

The goal and (6.32) are infinite-series identities with no ready-made counterpart in the library, and the goal holds only on $|x_i - x_j| \le 2\pi$. Outside that range the left side is $2\pi$-periodic and the right side is not, so no argument that ignores the range can succeed. The Christoffel–Darboux formula needs a theory of orthogonal polynomials for a general measure, which Mathlib does not yet provide. (6.24) involves the iterated derivatives of $e^{-x^2}$ and a doubly infinite parameter family. The spline identity requires evaluating a piecewise-polynomial integral exactly. Theorem 6.1 for infinite bases requires summability over a product index set $\iota^n$. The three false displays (2, 4, 6) hide their error in a constant factor. Two of them still reduce to an identity a solver may expect to hold.

Formalization scope

Everything is over $\mathbb R$. Series are stated with HasSum, or as Summable together with an equation for tsum. A divergent series therefore never reads as $0$. Sums over $k \ge 1$ are written over $k \in \mathbb N$ with $k + 1$ in place of $k$. The Christoffel–Darboux polynomials are indexed as in the book ($P_1$ is the constant), they are orthonormal up to $P_{n+1}$, and the measure has all moments finite. The Hermite $P_k$ is the physicists' family, defined through iteratedDeriv. It is not Mathlib's probabilists' Polynomial.hermite. The normalization constants of (6.24) are existentially quantified, since the book does not give them. The range of $q$ in (6.24) and (6.26) is $0 \le q < 1$: the book's $0 \le q \le 1$ without the singular point $q = 1$. The Dirichlet display is stated where $\sin\frac{x - x_i}{2} \ne 0$. The goal adds $\gamma > 0$, which the page leaves unstated. Spline points lie in $[0, a]$ with $a > 0$. In Theorem 6.1, the multidimensional kernel is the sum over multi-indices of products of basis functions, a statement to be proved and not the product of kernels by definition. A formalization that defined the $n$-dimensional kernel as $\prod_k K(x^k, y^k)$ would make the theorem trivial, and is ruled out.

Beyond the paper. Three corrected variants sit beside the faithful statements. Each changes one clause only. dirichlet_kernel_corrected (finding F1) uses the denominator $2\sin\frac{x - x_i}{2}$, since at $N = 0$ and $x - x_i = \pi$ the printed display reads $\frac12 = 1$. hermite_kernel_corrected (F2) takes $H_k = \mu_k P_k$ without the Gaussian factor. At $q = 0$ the printed (6.24) forces $\mu_0^2 e^{-x^2-y^2} = \pi^{-1/2}$ for all $x, y$, and the corrected form is Mehler's formula. hermite_kernel_multidim_corrected (F3) uses the prefactor $(\pi(1 - q^2))^{-n/2}$, since at $n = 1$, $x = y = 0$, $q = 0$ the printed (6.26) reads $\pi^{-1/2} = 1$. One further observation is recorded without a variant: (6.33) also holds for $\gamma < 0$, because both sides are even in $\gamma$.

Reusable beyond this mission are the two definitions (the physicists' Hermite functions and the truncated power) and any proof of the summable form of Theorem 6.1. Proofs, disproofs of the three false milestones, and general lemmas on Fourier series of $\cosh$ and $q^k\cos k\theta$ are all welcome.

Selected references

• V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000. doi:10.1007/978-1-4757-3264-1
• I. S. Gradshteyn and I. M. Ryzhik, Table of Integrals, Series, and Products, Academic Press, 1980 (7th ed. 2007). doi:10.1016/C2009-0-22516-5
• G. Szegő, Orthogonal Polynomials, AMS Colloquium Publications 23, 1939 (Christoffel–Darboux formula, §3.2). doi:10.1090/coll/023
• F. G. Mehler, Ueber die Entwicklung einer Function von beliebig vielen Variablen nach Laplaceschen Functionen höherer Ordnung, J. reine angew. Math. 66 (1866), 161–176. doi:10.1515/crll.1866.66.161
• S. G. Mikhlin, Variational Methods in Mathematical Physics, Pergamon, 1964.

Motivation

Primal-dual interior-point methods are the standard polynomial-time algorithms for linear programming and the basis of most commercial LP solvers. They do not move along the boundary of the feasible polyhedron, as the simplex method does. Instead they follow a curve through its interior, the central path, toward the solution set. Every convergence and complexity result about these methods assumes that this curve exists. Stephen J. Wright's monograph Primal-Dual Interior-Point Methods (SIAM, 1997, doi:10.1137/1.9781611971453) proves existence in its Chapter 2 from the standard LP background: existence of solutions, boundedness of solution sets, the Goldman–Tucker partition, and a primal-dual logarithmic barrier.

This mission is the first in a series that formalizes the book chapter by chapter. Later missions (potential reduction, path following, infeasible methods, finite termination, the homogeneous self-dual form) take the objects defined here as given.

Setting

Let $A \in \mathbb{R}^{m\times n}$, $b \in \mathbb{R}^m$ and $c \in \mathbb{R}^n$. Nothing is assumed about the rank of $A$. The primal and dual linear programs in standard form are

$$\text{(2.1)}\quad \min_x\ c^{\mathsf T}x \ \ \text{s.t.}\ Ax = b,\ x \ge 0, \qquad\qquad \text{(2.2)}\quad \max_{\lambda,s}\ b^{\mathsf T}\lambda \ \ \text{s.t.}\ A^{\mathsf T}\lambda + s = c,\ s \ge 0,$$

with all vector inequalities componentwise. The primal-dual feasible set $\mathcal F$ consists of the triples $(x,\lambda,s)$ with $Ax = b$, $A^{\mathsf T}\lambda + s = c$ and $(x,s) \ge 0$. The strictly feasible set $\mathcal F^\circ$ is the same set with $(x,s) > 0$. The solution sets are $\Omega_P$, the minimizers of (2.1); $\Omega_D$, the maximizers $(\lambda^*, s^*)$ of (2.2); and $\Omega = \Omega_P \times \Omega_D$. The index sets $\mathcal B$ and $\mathcal N$ collect the coordinates $j$ for which some $x^* \in \Omega_P$ has $x^*_j \neq 0$, and some $(\lambda^*, s^*) \in \Omega_D$ has $s^*_j \ne 0$, respectively.

For $\tau > 0$, the central path conditions (2.25) ask for $(x,\lambda,s)$ with

$$A^{\mathsf T}\lambda + s = c, \qquad Ax = b, \qquad x_j s_j = \tau \ \ (j = 1,\dots,n), \qquad (x,s) > 0 .$$

The reduced strictly feasible set $\mathcal H^\circ$ is the set of pairs $(x,s)$ such that $(x,\lambda,s) \in \mathcal F^\circ$ for some $\lambda \in \mathbb{R}^m$. The primal-dual log barrier on it is

$$f_\tau(x,s) = \frac1\tau\, x^{\mathsf T}s - \sum_{j=1}^n \log(x_j s_j).$$

In Lean all of these objects live in the single definition module WrightPDIPM.CentralPath.LP, under the names F, Fo, OmegaP, OmegaD, Omega, indexB, indexN, Hcirc, ftau and CentralPathConditions.

Formalization targets

Goal: Theorem 2.8 (p. 39)

If $\mathcal F^\circ \ne \emptyset$ and $\tau > 0$, then two things hold. First, $f_\tau$ has exactly one local minimizer relative to $\mathcal H^\circ$:

$$\exists!\,(x,s) \in \mathcal H^\circ \ \text{such that}\ (x,s) \text{ is a local minimizer of } f_\tau \text{ on } \mathcal H^\circ .$$

Second, the central path conditions (2.25) have a solution $(x,\lambda,s)$.

Milestones

1. Theorem 2.1 (p. 25). If $\mathcal F \neq \emptyset$, then $\Omega \ne \emptyset$. If either problem has an optimal solution, so does the other, and the optimal values agree.
2. Theorem 2.3 (p. 26). Suppose $\mathcal F \neq \emptyset$. If the dual is strictly feasible, then $\Omega_P$ is nonempty and bounded. If the primal is strictly feasible, then $\{s^* : (\lambda^*, s^*) \in \Omega_D\}$ is nonempty and bounded.
3. Theorem 2.4 (Goldman–Tucker, p. 28). $\mathcal B \cup \mathcal N = \{1,\dots,n\}$; equivalently, some $x^* \in \Omega_P$ and $(\lambda^*, s^*) \in \Omega_D$ satisfy $x^* + s^* > 0$. It is stated here under $\mathcal F \ne \emptyset$.
4. Lemma 2.5 (p. 30). If $\mathcal F^\circ \ne \emptyset$, then for every $K \ge 0$ the set $\{(x,s) : (x,\lambda,s) \in \mathcal F \text{ for some } \lambda,\ x^{\mathsf T}s \le K\}$ is bounded.

Significance

The result itself. Theorem 2.8 shows that the central path $\{(x_\tau, \lambda_\tau, s_\tau) : \tau > 0\}$ exists as soon as the problem has a strictly feasible primal-dual point. Every path-following and potential-reduction method in the book either tracks this curve or measures its iterates against neighbourhoods of it, so the theorem is the foundation the book's convergence and complexity results stand on. Theorem 2.4 provides the strictly complementary partition $\mathcal B \cup \mathcal N$, which the local and superlinear convergence analysis and the finite-termination results use. Theorems 2.1 and 2.3 are the duality and boundedness facts beneath both.

Formalizing it. These are classical results with complete textbook proofs. The work left is machine-checking them in the book's own form: standard-form LP, no rank assumption, the primal-dual barrier rather than the primal barrier, and minimality relative to $\mathcal H^\circ$. Related statements are already on the platform: Farkas's lemma and LP strong duality in Bertsimas–Tsitsiklis form, a central-path theorem in Matoušek–Gärtner form under the assumption $\operatorname{rank} A = m$ with the primal barrier, and Goldman–Tucker for the inequality-form LP. None of them is any of the statements above, but their proofs may be reusable.

Difficulty

The natural first step is to minimize $f_\tau$ by compactness. This does not work directly, because $\mathcal H^\circ$ is neither closed nor bounded and $f_\tau$ is not coercive on all of $\mathbb{R}^{2n}$. The quadratic term $x^{\mathsf T}s$ is indefinite in general, and only its restriction to the affine set of feasible pairs is linear. To obtain a minimizer one must show that the level sets of $f_\tau$ inside $\mathcal H^\circ$ are compact. This needs a boundedness statement (Lemma 2.5) that uses a strictly feasible point in an essential way, together with lower bounds that keep $x_j s_j$ away from $0$. A second difficulty is that $\mathcal H^\circ$ has empty interior in $\mathbb{R}^{2n}$ whenever $A \ne 0$. Passing from the minimizer to the conditions (2.25) is therefore a constrained first-order argument with multipliers, and it must work without $A$ having full row rank, so the multiplier $\lambda$ is not unique. For Goldman–Tucker, the obstacle is the step from "every index is positive at some optimum" to a single optimum that is positive on every index of $\mathcal B$ and of $\mathcal N$ at once.

Formalization scope

Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ. Inequalities are componentwise. Indices are 0-based in Lean and $\{1,\dots,n\}$ is Set.univ. Primal-dual points are triples (x, λ, s). "Bounded" means Bornology.IsBounded. $\Omega_P$ and $\Omega_D$ are defined as sets of optimal points (feasible, and at least as good as every feasible point), so no infimum or supremum is taken and an unattained optimum gives the empty set. No rank assumption on $A$ is made anywhere. No result in this chapter has an $O(\cdot)$ or an unspecified constant, so no constants are instantiated.

"Local minimizer in $\mathcal H^\circ$" means IsLocalMinOn (ftau τ) (Hcirc A b c), that is, minimality among nearby points of $\mathcal H^\circ$. Local minimality in all of $\mathbb{R}^{2n}$ would make the claim false. Uniqueness is asserted for the minimizer $(x,s)$ only, never for $\lambda$. $f_\tau$ uses Real.log and is only ever evaluated on $\mathcal H^\circ$, where every $x_j s_j > 0$.

The hypothesis $\mathcal F^\circ \neq \emptyset$ is part of the goal and cannot be weakened. If $\mathcal F^\circ = \emptyset$, then $\mathcal H^\circ = \emptyset$ and the first conclusion becomes false. A formalization that drops it, or one that replaces "unique local minimizer on $\mathcal H^\circ$" with "a global minimizer exists", is not this theorem.

The book prints Theorem 2.4 without a hypothesis. The faithful item carries the section's standing case $\mathcal F \ne \emptyset$, which by Theorem 2.1 gives $\Omega \neq \emptyset$.

Beyond the paper. One sharpness probe, theorem_2_4_probe, states Theorem 2.4 exactly as printed, with no hypothesis. It is expected to be false. For $m = n = 1$, $A = (1)$, $b = -1$, $c = 0$ the primal is infeasible and the dual objective is unbounded, so $\mathcal B \cup \mathcal N = \emptyset$. A disproof is the sought outcome.

Infrastructure that is reusable beyond this mission includes the standard-form LP objects, the solution sets and the $\mathcal B$/$\mathcal N$ partition, all of which later chapters use; KKT conditions for linearly constrained convex minimization; and strict convexity of $\sum_j -\log t_j$. Contributions of general lemmas toward any of these are welcome.

Selected references

• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, Philadelphia, 1997, Chapter 2. doi:10.1137/1.9781611971453
• A. J. Goldman and A. W. Tucker, "Theory of linear programming," in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, pp. 53–97.
• N. Megiddo, "Pathways to the optimal set in linear programming," in Progress in Mathematical Programming, Springer, 1989, pp. 131–158.
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997.

Motivation

A separating hyperplane in $\mathbb R^n$ is a classifier of VC dimension $n + 1$, so a bound on its generalization error that goes through the VC dimension degrades with the dimension of the space. Support vector machines construct hyperplanes in feature spaces of enormous dimension and still generalize. Chapter 5 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) explains this by a different capacity measure. When a hyperplane is required to separate the data with a margin $\Delta$, and the data lie in a ball of radius $R$, the VC dimension is bounded by roughly $R^2/\Delta^2$, independently of $n$.

Timeline. The optimal (maximal margin) hyperplane goes back to Vapnik and Chervonenkis (1965, 1974). Its use with kernels, in place of an explicit feature space, is due to Boser, Guyon and Vapnik (COLT 1992), and the soft-margin support vector machine to Cortes and Vapnik (Machine Learning 20 (1995)). The margin bound appears as Theorem 5.1 of the book, which prints no proofs (Preface, p. xi). In Burges's tutorial (Data Min. Knowl. Disc. 2 (1998)) the bound for "gap tolerant classifiers" carries a ceiling, $\min(\lceil D^2/M^2\rceil, d) + 1$.

Setting

Vectors live in $\mathbb R^n$ with the Euclidean inner product $(w \cdot x)$. A $\Delta$-margin separating hyperplane is a hyperplane $(w^* \cdot x) - b = 0$ with $|w^*| = 1$ and $b \in \mathbb R$. It classifies $x$ as $y = 1$ if $(w^* \cdot x) - b \ge \Delta$ and as $y = -1$ if $(w^* \cdot x) - b \le -\Delta$; vectors in the strip $|(w^* \cdot x) - b| < \Delta$ get no label (§5.4.2, p. 132). Vectors $x_1, \dots, x_h$ are shattered by these hyperplanes if each of the $2^h$ labelings $y_1, \dots, y_h \in \{1, -1\}$ is realized by one hyperplane that classifies every $x_i$ with label $y_i$. The VC dimension on a set $X$ is the largest $h$ for which some $x_1, \dots, x_h \in X$ are shattered, or $\infty$. In Lean these are MarginClassifies, MarginShatters and marginVCDim in NatureSLT.Margin.

For training data $(x_1, y_1), \dots, (x_\ell, y_\ell)$ with $y_i \in \{+1, -1\}$, a hyperplane $(w \cdot x) - b = 0$ is in canonical form if $y_i[(w \cdot x_i) - b] \ge 1$ for all $i$ (5.8). The optimal hyperplane $(w_0, b_0)$ satisfies (5.8) and minimizes $\Phi(w) = \|w\|^2$ over $w$ and $b$ (5.9). Its support vectors are the $x_i$ with equality in (5.8). The dual functional is $W(\alpha) = \sum_i \alpha_i - \frac12\sum_{i,j}\alpha_i\alpha_j y_i y_j (x_i \cdot x_j)$ (5.17). In Lean: IsCanonicalSeparating, IsOptimalHyperplane, supportVectors and dualW.

Formalization targets

Goal: Theorem 5.1 (pp. 132–133)

If every $x \in X$ lies in a sphere (closed ball) of radius $R > 0$ and $\Delta > 0$, then

$$h \le \min\left(\left[\frac{R^2}{\Delta^2}\right], n\right) + 1,$$

with $[\cdot]$ the integer part. As printed this is false (see Beyond the paper), and a disproof of the goal is a legitimate outcome of the mission.

Milestones

1. §5.4.1, (5.8)–(5.9): the canonical hyperplane minimizing $\|w\|^2$ separates the data without error with maximal distance from the closest vector. Conversely, a maximal-margin hyperplane, rescaled to canonical form, minimizes $\|w\|^2$.
2. §5.4.2: the optimal hyperplane, normalized to $|w^*| = 1$, is a $\Delta$-margin separating hyperplane with $\Delta = 1/|w_0|$.
3. (5.13)–(5.16): a hyperplane satisfying (5.11) is optimal if and only if there are $\alpha^0_i \ge 0$ with $\sum_i \alpha^0_i y_i = 0$, $w_0 = \sum_i y_i \alpha^0_i x_i$ (a sum over support vectors only), and $\alpha^0_i\{[(x_i \cdot w_0) - b_0]y_i - 1\} = 0$.
4. Display after (5.19): for a solution $\alpha_0$ of the dual problem, $|w_0|^2 = 2W(\alpha_0) = \sum_{\text{support vectors}} \alpha^0_i\alpha^0_j (x_i \cdot x_j) y_i y_j$.
5. Theorem 5.3 (Mercer): a symmetric $K \in L_2$ has an expansion $K(u, v) = \sum_k a_k \psi_k(u)\psi_k(v)$ with $a_k > 0$ if and only if $\iint K(u, v) g(u) g(v)\, du\, dv > 0$ for all $g \ne 0$ in $L_2$.

Significance

Theorem 5.1 is the reason the book gives for the generalization of the optimal hyperplane in high-dimensional feature spaces (§5.6.1). With the bound (3.24) it drives the Corollary on p. 133 and the choice of $\Delta$ in structural risk minimization. Milestones 1–4 are the convex-optimization facts on which the construction of the support vector machine rests: margin maximization as a quadratic program, its Kühn–Tucker characterization and the dual problem. Milestone 5 is the condition under which a kernel can replace the feature-space inner product.

On the platform, UnderstandingML.hard_svm_max_margin (the analogue of milestone 1 with the convention $+b$) and UnderstandingML.support_vectors (the bias-free Hard-SVM) are proved. UnderstandingML.kernel_iff_posSemidef characterizes kernels by positive semidefinite Gram matrices, and HighDimStat.Rkhs.thm12_20_mercer_v2 (open) is the eigen-expansion of a continuous kernel on a compact space. There is no margin-dependent VC dimension bound; the BartlettNN.Margin.* results bound fat-shattering dimensions of real-valued classes. The mission adds the book's bias-carrying statements, the first formal Δ-margin VC bound, and machine-checked settlements of the misprinted statements.

Difficulty

The dimension part of the bound, $h \le n + 1$, is the classical VC dimension of affine half-spaces; the content is the radius part. A solver has to control how far apart the two classes of an arbitrary dichotomy of $h$ points in a ball can be pushed by a unit-normal hyperplane with a free bias. The bias does not cancel for unbalanced dichotomies, and this is exactly where the printed integer part and the correct bound part ways. The Kühn–Tucker milestone requires optimality conditions for a convex quadratic program with linear inequality constraints. The Mercer milestone requires the spectral theory of Hilbert–Schmidt integral operators on $L_2$ of a set of positive Lebesgue measure. Neither is packaged in Mathlib in this form.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n); training data are indexed by Fin ℓ; labels are real numbers with $y_i \in \{+1, -1\}$ as a hypothesis, and both classes present, the setting of §5.5. In the shattering definition, labels are booleans. "Sphere of radius $R$" is a closed ball about an arbitrary center; $R > 0$ and $\Delta > 0$ are hypotheses. The VC dimension takes values in $\mathbb N \cup \{\infty\}$, so an unbounded family is $\infty$, never a junk value. Shattering requires every point to be classified with its margin: a definition that let points fall into the strip would make the bound trivial, and is ruled out. Optimality is a predicate on a given pair $(w_0, b_0)$; no item asserts that an optimum exists. The typo "$\Delta = 1/|w^*|$" of §5.4.2 is read as $1/|w_0|$. The Mercer items take $U \subseteq \mathbb R^d$ ($d \ge 1$) measurable of positive Lebesgue measure, with $\psi_k$ orthonormal in $L_2(U)$ and the expansion converging in $L_2(U \times U)$.

Not drafted: the Corollary on p. 133 and Theorem 5.2 (p. 139). Both are probabilistic, and their hypotheses (what the VC dimension of a set of partial classifiers means inside (3.24), the training-set size in the leave-one-out argument) are not pinned down on the page.

Beyond the paper. Two [Corrected] variants are posed beside the faithful items. (1) Theorem 5.1 with the ceiling $\lceil R^2/\Delta^2\rceil$: the vertices of an equilateral triangle inscribed in the unit circle of $\mathbb R^2$ are shattered with $\Delta = 3/4$, while $\min([16/9], 2) + 1 = 2$, a counterexample to the printed bound that has been checked in Lean. (2) Mercer's theorem with $\ge 0$ in the condition and the coefficients: a kernel $\sum_k 2^{-k}\psi_k(u)\psi_k(v)$ over the incomplete system $\sqrt2\sin(2\pi k u)$ on $[0,1]$ has positive coefficients, yet $\iint Kgg = 0$ for $g \equiv 1$.

Contributions welcome: a convex-quadratic-programming KKT library for finitely many linear constraints; integral operators with $L_2$ kernels and their spectral expansion; disproofs of the faithful Theorem 5.1 and Theorem 5.3.

Selected references

• V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000. doi:10.1007/978-1-4757-3264-1
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998. ISBN 978-0-471-03003-4.
• B. E. Boser, I. M. Guyon, V. N. Vapnik, A training algorithm for optimal margin classifiers, COLT 1992. doi:10.1145/130385.130401
• C. Cortes, V. Vapnik, Support-vector networks, Machine Learning 20, 1995. doi:10.1007/BF00994018
• C. J. C. Burges, A tutorial on support vector machines for pattern recognition, Data Mining and Knowledge Discovery 2, 1998. doi:10.1023/A:1009715923555
• J. Mercer, Functions of positive and negative type, and their connection with the theory of integral equations, Phil. Trans. R. Soc. A 209, 1909. doi:10.1098/rsta.1909.0016

Motivation

Empirical risk minimization (ERM) chooses, from a fixed set of functions, the one with the smallest average loss on the training sample. Its risk is controlled by bounds whose confidence term grows with the VC dimension of the set and shrinks with the sample size $\ell$. When the ratio $\ell/h$ is small, a fixed set is either too poor to approximate the target or too rich to be estimated reliably. The structural risk minimization (SRM) principle of Vapnik and Chervonenkis (1974) resolves this by nesting sets of growing capacity and choosing, as a function of the sample size, the element in which to minimize the empirical risk. It is the conceptual ancestor of model selection by complexity penalties, of support vector machines' margin control, and of the minimum description length principle.

Chapter 4 of Vapnik's The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) states the asymptotic rate of SRM (Theorem 4.1) together with the two finite-sample risk bounds it rests on, (4.1) and (4.2), and the finite-class bound (4.25) from which the book derives its minimum description length bound. The book prints no proofs; the standard ones are in Vapnik, Statistical Learning Theory (Wiley 1998), and Vapnik–Chervonenkis, Theory of Pattern Recognition (1974).

Setting

Let $F$ be a probability measure on a set $Z$ and $Q(z, \alpha)$, $\alpha \in \Lambda$, a set of nonnegative measurable functions indexed by an arbitrary set $\Lambda$. The risk is $R(\alpha) = \int Q(z,\alpha)\,dF(z)$ and the empirical risk on an i.i.d. sample $z_1, \dots, z_\ell$ is $R_{\mathrm{emp}}(\alpha) = \frac1\ell \sum_{i=1}^\ell Q(z_i, \alpha)$.

The VC dimension of a set of real functions $A \le Q \le B$ is the largest number of points shattered by the indicators $\theta\{Q(z,\alpha) - \beta\}$, $\alpha \in \Lambda$, $\beta \in (A, B)$, where $\theta(u) = 1$ for $u \ge 0$ and $0$ otherwise (§3.6). In Lean: NatureSLT.SRM.vcDimReal Q A B : ℕ∞.

A structure is a sequence of nested nonempty subsets $S_k = \{Q(z,\alpha), \alpha \in \Lambda_k\}$, $S_1 \subset S_2 \subset \cdots$ (4.3). It is admissible if each $S_k$ has finite VC dimension $h_k$ and either (i) $0 \le Q \le B_k$ on $S_k$, or (ii) $\sup_{\alpha \in \Lambda_k} (\int Q^p\,dF)^{1/p} / \int Q\,dF \le \tau_k$ for some $p > 2$ (4.4). Write $T_k = B_k$ in case (i) and $T_k = \tau_k$ in case (ii). The union $S^* = \bigcup_k S_k$ is assumed dense in $S$ for the metric $\rho(Q_1, Q_2) = \int |Q_1 - Q_2|\,dF$.

A law $n = n(\ell)$ (4.5) chooses an element, and $\alpha^{n(\ell)}_\ell$ minimizes $R_{\mathrm{emp}}$ over $\Lambda_{n(\ell)}$. The rate of approximation is $r_n = \inf_{\Lambda_n} R - \inf_\Lambda R$ (4.8).

Following footnote 3 (p. 97), random variables $\xi_\ell$ converge to $\xi_0$ with asymptotic rate $V(\ell)$ if, for some constant $C$, $V^{-1}(\ell)|\xi_\ell - \xi_0| \to C$ in probability. In Lean: NatureSLT.SRM.ConvergesWithRate.

Formalization targets

Goal: Theorem 4.1 (pp. 97–98)

If the law satisfies

$$\lim_{\ell\to\infty} \frac{T^2_{n(\ell)}\, h_{n(\ell)} \ln \ell}{\ell} = 0 \qquad (4.7),$$

then $R(\alpha^{n(\ell)}_\ell)$ converges in probability to $R(\alpha_0) = \inf_{\alpha \in \Lambda} R(\alpha)$ with asymptotic rate

$$V(\ell) = r_{n(\ell)} + T_{n(\ell)} \sqrt{\frac{h_{n(\ell)} \ln \ell}{\ell}} \qquad (4.6).$$

This is NatureSLT.SRM.theorem_4_1, stated as printed. Finding F1 shows that as printed it is false: a law that keeps returning to a small element satisfies (4.7) while the risks oscillate. Finding F4 shows that the footnote-3 notion of rate can fail even when $n(\ell) \to \infty$. A disproof of the goal is therefore a legitimate outcome.

Milestones

• (4.1) For an infinite set of functions $0 \le Q \le B$ with VC dimension $h$, $1 \le h \le 2\ell$, and $\mathcal E = 4\,(h(\ln(2\ell/h) + 1) - \ln(\eta/4))/\ell$, with probability at least $1 - \eta$, for all $\alpha$:

$$R(\alpha) \le R_{\mathrm{emp}}(\alpha) + \frac{B\mathcal E}{2}\left(1 + \sqrt{1 + \frac{4 R_{\mathrm{emp}}(\alpha)}{B \mathcal E}}\right).$$

• (4.2) For an infinite set of nonnegative functions $Q$ with $(\int Q^p)^{1/p} \le \tau \int Q$, $p > 2$, the same $\mathcal E$ and $a(p) = \sqrt[p]{\tfrac12 ((p-1)/(p-2))^{p-1}}$, with probability at least $1 - \eta$, for all $\alpha$:

$$R(\alpha) \le \frac{R_{\mathrm{emp}}(\alpha)}{\left(1 - a(p)\tau\sqrt{\mathcal E}\right)_+}.$$

• (4.25) For $N$ indicator functions, with probability at least $1 - \eta$, for all $\alpha$:

$$R(\alpha) \le R_{\mathrm{emp}}(\alpha) + \frac{\ln N - \ln \eta}{\ell}\left(1 + \sqrt{1 + \frac{2 R_{\mathrm{emp}}(\alpha)\,\ell}{\ln N - \ln \eta}}\right).$$

Every constant is the book's: the $4$ and $\ln(\eta/4)$ of $\mathcal E$, the $B\mathcal E/2$ and the $4$ under the root in (4.1), $a(p)$ in (4.2), and the $2$ under the root in (4.25).

Significance

Theorem 4.1 is the book's asymptotic statement that SRM is consistent and adapts to the target. The rate is the sum of an approximation term and an estimation term, so a priori knowledge of the approximation rate $r_n$ yields the best law $n(\ell)$, as in the Example (4.9) on p. 98, where $r_n = n^{-c}$ gives the rate $(\ln \ell/\ell)^{c/(2c+1)}$. The bounds (4.1) and (4.2) are the finite-sample inequalities SRM minimizes in practice, for bounded and for heavy-but-not-too-heavy-tailed losses. (4.25) is the starting point of the book's comparison of SRM with the minimum description length principle (Theorem 4.3).

The platform holds related but different statements: UnderstandingML.srm_bound and UnderstandingML.srm_nonuniform_rate (SRM as nonuniform learning over a countable union with weights), UnderstandingML.mdl_bound (a prefix-free description-length bound with other constants), and FoundationsML.ModelSelection.srm_learning_guarantee_v2 (Open, Mohri et al.'s form). None states the asymptotic rate of Theorem 4.1 or the relative-deviation bounds (4.1), (4.2), (4.25) in the book's form. As far as is known, none of the four statements of this mission has a machine-checked proof.

Difficulty

The goal combines three things that each fail in a naive treatment. First, the uniform bound must be applied to a different class $S_{n(\ell)}$ at every sample size, so its constants must be uniform in the element. Second, the approximation term $r_{n(\ell)}$ tends to $0$ only if $n(\ell) \to \infty$, which (4.7) does not imply; a proof that assumes it proves a different theorem. Third, the footnote-3 rate is a statement about the limit of a normalized error, not a bound on it, so an $O_P$ bound alone does not establish it.

For (4.1) and (4.2), the step from a VC dimension to a bound with these exact constants goes through the relative-deviation inequality with the annealed entropy at $2\ell$ and the bound on the growth function in terms of $h$. For (4.25) the obstacle is the relative (not additive) form: Hoeffding's inequality gives the wrong shape and does not suffice.

Formalization scope

Samples are functions $\{0, \dots, \ell-1\} \to Z$ under the product measure $F^\ell$ (Measure.pi). $\Lambda$ is a type, the structure is Λs : ℕ → Set Λ (monotone, every element nonempty, indexed from $0$), and $h_k \in \mathbb N$, $T_k \in \mathbb R$ are given sequences tied to the structure by the two admissibility cases. The empirical minimizer is a given map from samples to $\Lambda_{n(\ell)}$, and its existence is not claimed. Measurability is explicit throughout. Each $Q(\cdot,\alpha)$ is measurable and integrable, and the risk of the minimizer is a measurable function of the sample. In (4.1) and (4.2), the event "the bound holds for all $\alpha$" is assumed measurable. The ratio in (4.4) and (3.19) is multiplied out, with $Q^p$ assumed integrable. Infima are over nonempty sets bounded below by $0$, so no junk value of ⨅ enters. In (4.1) and (4.2) the range $1 \le h \le 2\ell$ is assumed: the page leaves it implicit, and outside it the printed $\mathcal E$ can be negative and the printed bound false (finding F5). The trivializing formalization the series warns about, a non-measurable event read as probability $0$ or an infimum over an empty element read as $0$, is ruled out by those hypotheses.

Beyond the paper. One variant is posed: NatureSLT.SRM.theorem_4_1_corrected ([Corrected], finding F1). It adds $n(\ell) \to \infty$ and reads the rate as $P\{|R(\alpha^{n(\ell)}_\ell) - R(\alpha_0)| > C\,V(\ell)\} \to 0$ for some constant $C$. It is not a milestone. The planner also notes (F3) that the printed derivation of (4.27) from (4.25)–(4.26) has a gap. Those statements are not part of this mission.

Reusable infrastructure: the VC dimension of a real class, the product-measure sample space, and the footnote-3 notion of rate. Contributions welcome: proofs or disproofs of each item, and a published definition of vcDimReal that the other missions of this series could reference.

Selected references

• V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000. doi:10.1007/978-1-4757-3264-1
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998. ISBN 978-0-471-03003-4.
• V. N. Vapnik, A. Ya. Chervonenkis, Theory of Pattern Recognition (in Russian), Nauka, Moscow, 1974.
• V. N. Vapnik, Estimation of Dependences Based on Empirical Data, Springer, 1982. doi:10.1007/0-387-34239-7
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014. doi:10.1017/CBO9781107298019

Motivation

Statistical learning theory asks when minimizing the error on a finite sample also controls the error on unseen data. For a set of classifiers, the answer given by Vapnik and Chervonenkis is governed by a single combinatorial quantity: how many different ways the set can label $\ell$ points. Bounds on the generalization error of empirical risk minimization are stated in terms of the logarithm of this number, the growth function, and they are informative only if the growth function grows sublinearly in $\ell$.

The theorem at the centre of this mission says that there is no middle ground: the growth function is either exactly $\ell \ln 2$ for every $\ell$, or, from some point on, it is bounded by a logarithmic function $h(\ln(\ell/h) + 1)$. The integer $h$ is the VC dimension. This dichotomy is what turns the abstract bounds of Chapter 3 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) into constructive ones (Eq. (3.24) of the book).

Timeline. Vapnik and Chervonenkis announced the connection between the growth function and the shattering number in 1968 and proved it in 1971 (Theory Probab. Appl. 16 (1971)), in the form $m^S(r) = 2^r$ for all $r$ or $m^S(r) \le r^n + 1$. Sauer (J. Combin. Theory A 13 (1972)) and Shelah (Pacific J. Math. 41 (1972)) independently proved the sharp polynomial bound $\sum_{i=0}^{h}\binom{\ell}{i}$. The logarithmic form used in the book follows from that sum together with the estimate $\sum_{i \le h}\binom{\ell}{i} \le (e\ell/h)^h$. The book states its results without proofs (Preface, p. xi).

Setting

Let $Z$ be a nonempty set and $\Lambda$ a nonempty set of parameters, and let $Q(z, \alpha)$, $\alpha \in \Lambda$, be a set of indicator functions on $Z$: each takes only the values $0$ and $1$. For a sample $z_1, \dots, z_\ell \in Z$ (repetitions allowed), let

$$N^\Lambda(z_1, \dots, z_\ell)$$

be the number of different binary vectors $(Q(z_1, \alpha), \dots, Q(z_\ell, \alpha))$ obtained as $\alpha$ ranges over $\Lambda$ (Section 2.3.2, p. 42). The growth function is

$$G^\Lambda(\ell) = \ln \sup_{z_1, \dots, z_\ell} N^\Lambda(z_1, \dots, z_\ell)$$

(Section 2.7, p. 55), with $\ln$ the natural logarithm. Since $N^\Lambda \le 2^\ell$, always $G^\Lambda(\ell) \le \ell \ln 2$.

Points $z_1, \dots, z_h$ are shattered if for every $\delta_1, \dots, \delta_h \in \{0, 1\}$ some $\alpha$ has $Q(z_i, \alpha) = \delta_i$ for all $i$. The VC dimension is the maximum number of shattered points, or $\infty$ if arbitrarily many points are shattered (Section 3.6, p. 80). For a set of real functions $A \le Q(z, \alpha) \le B$, the VC dimension is that of the indicators $\theta\{Q(z, \alpha) - \beta\}$, $\beta \in (A, B)$ (Eq. (3.22)), where the step function is $\theta(u) = 0$ for $u < 0$ and $\theta(u) = 1$ for $u \ge 0$.

In the Lean development these are numSeparations, growthFunction, Shatters, vcDim, stepFunction and vcDimReal in the namespace NatureSLT.GrowthFunction.

Formalization targets

Goal: Theorem 3.3 (p. 79)

Either

$$G^\Lambda(\ell) = \ell \ln 2 \quad \text{for every } \ell,$$

or there is an integer $h \ge 0$ with $G^\Lambda(h) = h \ln 2$ and $G^\Lambda(h+1) < (h+1)\ln 2$ such that

$$G^\Lambda(\ell) \le h\left(\ln\frac{\ell}{h} + 1\right) \qquad \text{for every } \ell > h .$$

The range $\ell > h$ is the one the book gives in both of its restatements of the theorem: the display after the Definition on p. 79 and Eq. (3.23) on p. 83.

Milestones

1. Equivalent definition of the VC dimension (Section 3.6, p. 80): the VC dimension is infinite if and only if $G^\Lambda(\ell) = \ell\ln 2$ for all $\ell$, and equals $h$ if and only if $G^\Lambda(h) = h\ln 2$ and $G^\Lambda(h+1) < (h+1)\ln 2$.
2. Eq. (3.23) (p. 83): if the VC dimension is a finite $h$, then $G^\Lambda(\ell) \le h(\ln(\ell/h) + 1)$ for $\ell > h$.
3. Example 1(i) (p. 81): the linear indicator functions $\theta\{\sum_{p=1}^n \alpha_p z_p + \alpha_0\}$ on $\mathbb R^n$ have VC dimension $n + 1$.
4. Example 1(ii) (p. 81): the real linear functions $\sum_{p=1}^n \alpha_p z_p + \alpha_0$ have VC dimension $n + 1$.
5. Example 2(i) (p. 82): $\theta(\sin \alpha z)$, $\alpha \in \mathbb R$, has infinite VC dimension; the points $10^{-1}, \dots, 10^{-\ell}$ are shattered by the explicit parameter $\alpha = \pi(\sum_{i=1}^\ell (1 - \delta_i)10^i + 1)$.

Significance

The dichotomy is what makes the VC dimension a usable complexity measure. Combined with the bounds of Section 3.3, it gives distribution-free generalization bounds whose confidence term depends on $\ell$ and $h$ only (Eq. (3.24)). It also explains why finiteness of the VC dimension is a sufficient condition for consistency of empirical risk minimization for every probability measure (p. 80): the growth function, divided by $\ell$, tends to zero exactly when it is not linear. Examples 1 and 2 show that the VC dimension is not the number of parameters: linear functions have as many as their parameters, while a one-parameter family of sines has infinitely many.

The theorem is classical and has been proved many times. Related statements are already machine-checked on the platform in other forms: Sauer's lemma for concept classes (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah), the bound $\Phi_d(m) \le (em/d)^d$ (ComputationalLearning.phi_polynomial_bound), the 1971 dichotomy with the bound $r^n + 1$ for sets of events (VapnikChervonenkis.GrowthFunction.theorem1_growth_dichotomy), and the VC dimension of open halfspaces with $\pm$ labels (UnderstandingML.vcDim_halfspaces). What is not on the platform is the book's statement: the logarithmic bound for the growth function of an indexed set of $\{0,1\}$-valued functions, with $h$ characterized through the growth function itself, and the book's examples with the closed half-space convention $\theta(0) = 1$. This mission produces that statement and connects it to the shattering definition.

Difficulty

The obvious argument proves only half. That $G^\Lambda(h) = h\ln 2$ and $G^\Lambda(h+1) < (h+1)\ln 2$ pin down the largest shattered set is elementary; the content lies in the bound for $\ell > h$: a class that shatters no $h + 1$ points must realize only polynomially many labelings of every $\ell$ points, with the explicit constant of the logarithmic form, and nothing in the definition of the growth function gives this directly. A tempting shortcut is to read the bound as valid for every $\ell$, as the theorem's display does in isolation: this is false whenever $h \ge 2$, since $G^\Lambda(1) = \ln 2$ exceeds $h(\ln(1/h) + 1)$. The range $\ell > h$ is essential. For the examples, the upper bound $n + 1$ in Example 1 is a Radon-type statement about $n + 2$ points in $\mathbb R^n$, and Example 2 requires controlling the sign of $\sin(\alpha\, 10^{-i})$ simultaneously for all $i$ with one parameter.

Formalization scope

Indicator functions are boolean-valued, true standing for $1$, and written Q α z for the book's $Q(z, \alpha)$; samples are maps Fin ℓ → Z, so indices run from $0$. $N^\Lambda$ is the cardinality of the finite set of realized vectors in Fin ℓ → Bool; the supremum over samples is a supremum of natural numbers bounded by $2^\ell$, and $G^\Lambda$ is Real.log of its cast. The VC dimension is valued in ℕ∞. $Z$ and $\Lambda$ are assumed nonempty in every theorem, so the supremum is over a nonempty set of samples and is at least $1$; the junk value $\ln 0 = 0$ never enters. At $h = 0$ the book's expression $h(\ln(\ell/h)+1)$ is undefined; the formal statements evaluate it as $0$, the limit as $h \to 0^+$, and the correct bound in that case, where $G^\Lambda \equiv 0$. The step function has $\theta(0) = 1$. Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n); in Example 1(ii) the bounds of the real-function definition are $A = -\infty$, $B = +\infty$.

A trivializing formalization is ruled out: the goal is the disjunction of a linear growth function and the explicit bound $h(\ln(\ell/h) + 1)$ with $h$ fixed by $G^\Lambda(h) = h \ln 2$ and $G^\Lambda(h+1) < (h+1)\ln 2$, not an existence statement over an arbitrary $h$ and not a bound in which an empty parameter set makes the growth function vanish.

Beyond the paper. One variant is posed beside the faithful goal: a sharpness probe (growth_function_dichotomy_probe) claiming the logarithmic bound for every $\ell$, i.e. without $\ell > h$. Its evidence: for $Z = \{1, \dots, 10\}$ and all subsets, $h = 10$ and $G^\Lambda(1) = \ln 2 > 10(\ln(1/10) + 1)$. A disproof is the sought outcome.

A complete development needs: finite cardinality arguments for sets of binary vectors, the Sauer–Shelah lemma for an indexed family (Mathlib has Finset.card_shatterer_le_sum_vcDim for finite set families), the estimate $\sum_{i\le h}\binom{\ell}{i} \le (e\ell/h)^h$, Radon's theorem or an affine-independence argument for Example 1, and elementary trigonometry for Example 2. The bridge between indexed families of indicator functions and set families is reusable by every later mission of this series. Contributions of any milestone, of bridge lemmas to the existing Sauer-type theorems, and of a disproof of the probe are welcome.

Selected references

• V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000. https://doi.org/10.1007/978-1-4757-3264-1
• V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2), 1971. https://doi.org/10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13(1), 1972. https://doi.org/10.1016/0097-3165(72)90019-2
• S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific Journal of Mathematics 41(1), 1972. https://doi.org/10.2140/pjm.1972.41.247
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998. ISBN 978-0-471-03003-4