Machine Learning

Motivation

Many learning problems take an unordered collection as input: the points of a point cloud, the particles of a physical system, the atoms of a molecule, the nodes of a graph. Storing such data in memory fixes an order of the elements, but the order carries no information, and a model whose output changes when the rows of its input are shuffled is answering a different question from the one posed. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), §4.1, make this the first instance of their blueprint: the domain is a set (or a graph) of $n$ nodes, and the symmetry group is the symmetric group $\Sigma_n$ of all reorderings.

Two architectures used in practice follow this pattern. Deep Sets (Zaheer et al., NeurIPS 2017) and PointNets (Qi et al., CVPR 2017) process sets; message-passing graph neural networks process graphs. The design question in both cases is which layers respect the symmetry. For linear layers the question has a complete answer, and the answer determines the layer used by Deep Sets. For graphs, Maron, Ben-Hamu, Shamir and Lipman (2018) counted the linear layers acting on adjacency matrices.

Setting

A set of $n$ nodes $\mathcal V=\{1,\dots,n\}$ carries node features $\mathbf x_u\in\mathbb R^d$, stacked as the rows of a matrix $\mathbf X\in\mathbb R^{n\times d}$. A graph adds an adjacency matrix $\mathbf A\in\mathbb R^{n\times n}$, eq. (8), whose nonzero entries are the edges.

A permutation $\sigma\in\Sigma_n$ acts through its permutation matrix $\mathbf P$ by reordering rows: row $u$ of $\mathbf P\mathbf X$ is row $\sigma^{-1}(u)$ of $\mathbf X$. On adjacency matrices it acts by $\mathbf A\mapsto\mathbf P\mathbf A\mathbf P^\top$, reordering rows and columns together.

A function $f$ is permutation invariant if $f(\mathbf P\mathbf X)=f(\mathbf X)$ for every permutation matrix $\mathbf P$, and a matrix-valued function $\mathbf F$ is permutation equivariant if $\mathbf F(\mathbf P\mathbf X)=\mathbf P\mathbf F(\mathbf X)$. On graphs the book's definitions (9) and (10) are

$$f(\mathbf P\mathbf X,\mathbf P\mathbf A\mathbf P^\top)=f(\mathbf X,\mathbf A)\quad(9),\qquad \mathbf F(\mathbf P\mathbf X,\mathbf P\mathbf A\mathbf P^\top)=\mathbf P\mathbf F(\mathbf X,\mathbf A)\quad(10),$$

for any permutation matrix $\mathbf P$.

The section's constructions are the sum readout $f(\mathbf X)=\phi\big(\sum_{u\in\mathcal V}\psi(\mathbf x_u)\big)$ (6); the shared node-wise linear map $\mathbf F_{\boldsymbol\Theta}(\mathbf X)=\mathbf X\boldsymbol\Theta$ (7); the neighbourhood $\mathcal N_u=\{v:(u,v)\in\mathcal E\text{ or }(v,u)\in\mathcal E\}$ (11) and the multiset of neighbourhood features $\mathbf X_{\mathcal N_u}=\{\!\{\mathbf x_v:v\in\mathcal N_u\}\!\}$ (12); and the local layer whose $u$-th row is $\phi(\mathbf x_u,\mathbf X_{\mathcal N_u})$ (13). For one feature channel the two linear generators are the identity $\mathbf F_1x=x$ and the average $\mathbf F_2x=\tfrac1n\mathbf 1\mathbf 1^\top x$, every entry of which is the mean $\tfrac1n\sum_u x_u$.

The book numbers no theorems, lemmas or definitions; every item of this mission is cited by section, equation number and printed page.

Formalization targets

Goal: linear equivariant maps on one channel

For $n\ge1$ and a linear map $\mathbf F:\mathbb R^n\to\mathbb R^n$,

$$\big(\forall\,\mathbf P,\ \forall x:\ \mathbf F\mathbf P x=\mathbf P\mathbf F x\big)\iff \exists\,\alpha,\beta\in\mathbb R\ \ \forall x:\ \mathbf F x=\alpha\,x+\beta\,\tfrac1n\mathbf 1\mathbf 1^\top x .$$

This is the book's sentence on p. 33: any linear equivariant "can be written as a linear combination of two generators, the identity … and the average". Both directions are stated; the content is the "only if" direction.

Milestones

1. The sum readout (6) is permutation invariant (p. 32).
2. The node-wise linear map (7) is permutation equivariant, with rows $\mathbf h_u=\boldsymbol\Theta^\top\mathbf x_u$ (p. 33).
3. The local layer (13) satisfies (10) whenever $\phi$ is invariant to the order of the neighbourhood (p. 34).
4. Invariant and equivariant functions give identical outputs on isomorphic graphs (p. 35).
5. On the complete graph $\mathbf A=\mathbf 1\mathbf 1^\top$, the aggregate $\bigoplus_{v\in\mathcal V}\psi(\mathbf x_v)$ is the same at every node (§5.4, p. 81).

Stronger statements

• Several channels (corrected). A linear $\mathbf F:\mathbb R^{n\times d}\to\mathbb R^{n\times d'}$ is permutation equivariant iff $\mathbf F(\mathbf X)=\mathbf X\boldsymbol\Theta_1+\tfrac1n\mathbf 1\mathbf 1^\top\mathbf X\boldsymbol\Theta_2$.
• Adjacency matrices (Maron et al., corrected). For $n\ge4$, the linear maps $L:\mathbb R^{n\times n}\to\mathbb R^{n\times n}$ with $L(\mathbf P\mathbf A\mathbf P^\top)=\mathbf P L(\mathbf A)\mathbf P^\top$ form a space of dimension $15=B_4$.

Significance

The result. The goal classifies the linear layers of a set network. Any equivariant linear layer on scalar node features mixes each node's own value with the mean of all values, and nothing else; with several channels the two scalars become two weight matrices, which is exactly the Deep Sets layer. Read the other way, the theorem says that the commutant of the permutation representation of $\Sigma_n$ on $\mathbb R^n$ is two-dimensional (for $n\ge2$), the algebraic fact behind the decomposition $\mathbb R^n=\mathrm{span}(\mathbf 1)\oplus\mathbf 1^\perp$ into two irreducible pieces. The Maron et al. count does the same for layers acting on adjacency matrices and fixes the size of the parameter space of invariant graph networks. The milestones give the elementary invariance and equivariance facts on which the graph-network chapter rests, including the constant aggregate on a complete graph.

Formalizing it. All results here are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no statement about the commutant of the permutation representation or about equivariant layers on sets. The mission produces a vocabulary of permutation actions on feature and adjacency matrices, and the invariance and equivariance definitions (9)–(10), that later missions of this series (the WL comparison, the E(3)-equivariant layer) also use. Two of the book's printed claims need correction to be true, and the formal statements record the corrected versions.

Difficulty

The milestones are short reindexing arguments; the work is in choosing encodings that keep them faithful. The goal's "if" direction is a one-line computation. The "only if" direction is where an argument is needed: equivariance under all of $\Sigma_n$ must force the matrix of $\mathbf F$ to have one value on the diagonal and one value off it. Equivariance under a smaller group does not suffice: commuting with the cyclic shift alone gives all circulant matrices, an $n$-dimensional space, so the argument must use permutations beyond the shifts. The channel version adds a tensor-product layer to the same argument. The Maron et al. count is a dimension statement, so it needs both a spanning family and its independence, and the count is sensitive to $n$: for $n<4$ the dimension is strictly smaller than 15, so any argument must use $n\ge4$ somewhere.

Formalization scope

Node features are Matrix (Fin n) (Fin d) ℝ (rows are nodes); a single channel is Fin n → ℝ. A permutation is σ : Equiv.Perm (Fin n), acting by X.submatrix σ.symm id (row $u$ of $\mathbf P\mathbf X$ is row $\sigma^{-1}(u)$) and on adjacency matrices by A.submatrix σ.symm σ.symm; this one convention is used in every statement. Adjacency matrices are real; the edge set is the set of nonzero entries, which for the book's 0/1 matrix (8) is its edge set and also admits weighted graphs. The function $\phi$ of (13) and the aggregator $\bigoplus$ of §5.4 take a Multiset, so their invariance to the order of the neighbours holds by construction. The average $\tfrac1n\mathbf 1\mathbf 1^\top$ is written with $(n:\mathbb R)^{-1}$, and the goal and channel version assume $0<n$. Equivariance quantifies over every permutation of $\Sigma_n$, never a generating subset. The complete-graph item states the identical-aggregate clause of §5.4. The page's later claim of equal expressive power across inputs is false: with $n=2$, $\psi(x)=x$, $\bigoplus=\sum$, and $\phi(x,s)=s$, changing $x_2$ changes $h_1$ while $x_1$ stays fixed, which no node-only map can reproduce.

A trivializing formalization is ruled out: "equivariant" is the commutation property itself, never defined as "of the form $\alpha\mathbf I+\beta\tfrac1n\mathbf 1\mathbf 1^\top$".

Two printed claims are corrected. On p. 33 the two-generator form is stated for matrices $\mathbf X$ with $d$ channels; it is false for $d>1$ (the map $\mathbf X\mapsto\mathbf X\boldsymbol\Theta$ of (7) is a counterexample), so the goal is single-channel and the multi-channel statement uses weight matrices. On p. 34 the fifteen generators are said to be independent of $n$; the dimension is 1, 8 and 14 for $n=1,2,3$, so that item assumes $n\ge4$, and it is stated for adjacency-to-adjacency maps as the side-note on p. 33 specifies.

The development needs Mathlib's Equiv.Perm, Matrix.submatrix, Finset sums and reindexing (Equiv.sum_comp), Multiset.map, and Module.finrank. Proofs of the commutant statements, of the multi-channel version and of the dimension count are welcome; the permutation-action and invariance lemmas proved along the way are reusable by any later development on graph networks.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021. https://arxiv.org/abs/2104.13478v2
• M. Zaheer, S. Kottur, S. Ravanbakhsh, B. Póczos, R. Salakhutdinov, A. Smola, Deep Sets, NeurIPS, 2017. https://arxiv.org/abs/1703.06114
• H. Maron, H. Ben-Hamu, N. Shamir, Y. Lipman, Invariant and Equivariant Graph Networks, ICLR, 2019. https://arxiv.org/abs/1812.09902
• C. R. Qi, H. Su, K. Mo, L. J. Guibas, PointNet: Deep Learning on Point Sets for 3D Classification and Segmentation, CVPR, 2017. https://arxiv.org/abs/1612.00593

Motivation

Convolutional networks use the same filter at many locations. A shift of the input then shifts the output in a predictable way, allowing one set of filter coefficients to serve every location. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning, §4.3, pp. 40–43 ask how this idea extends when the transformations form a group and the signal domain need not be the group itself. A grid and its cyclic shifts are one example; a sphere and its rotation group are another. In the latter example, a rotation is an output index even though it is not a point of the sphere. This distinction matters when a second convolutional layer processes the first layer's output.

The chapter places this construction within its general account of geometric deep learning: symmetries specify how inputs transform, and a compatible map should transform its outputs in a corresponding way. Here the concrete question is whether the integral defining group convolution has that compatibility. The source calls this property equivariance and gives it immediately after equation (14). The book numbers equations but no theorems, lemmas, propositions, or definitions, so the items below are cited by section, equation, and printed page.

Setting

Let $G$ be a group acting transitively on a domain $\Omega$; write $g\cdot u$ for the image of $u\in\Omega$. The section makes this homogeneous-domain assumption explicit on p. 43. A signal is a scalar function $x:\Omega\to\mathbb R$, and a filter is another such function $\theta$. The group acts on signals by the inverse action on their arguments:

$$(\rho(g)x)(u)=x(g^{-1}\cdot u).$$

This convention makes $\rho$ a left group representation on functions. Let $\mu$ be a measure on $\Omega$ invariant under the action of every element of $G$. The book states this measure convention beside its pairing formula on p. 41. The pairing and group convolution are

$$\langle x,\theta\rangle_\mu=\int_\Omega x(u)\theta(u)\,d\mu(u),\qquad (x\star\theta)(g)=\langle x,\rho(g)\theta\rangle_\mu =\int_\Omega x(u)\theta(g^{-1}\cdot u)\,d\mu(u).$$

The convolution is indexed by $g\in G$, so it is a signal on $G$, even when $\Omega$ and $G$ are different spaces. Signals $y:G\to\mathbb R$ use the regular action $(\rho_G(h)y)(g)=y(h^{-1}g)$. On the cyclic grid $\mathbb Z_n$, the source uses $u\cdot v=v-u$ for the action of a shift $u$ on an index $v$. These conventions are the ones used throughout this mission. Equation (14) and the surrounding definitions, §4.3, pp. 41–43.

Formalization targets

Group convolution is equivariant

For every $h,g\in G$ and scalar signals $x,\theta$ on $\Omega$, the main target is

$$((\rho(h)x)\star\theta)(g) = (\rho_G(h)(x\star\theta))(g) = (x\star\theta)(h^{-1}g).$$

The theorem keeps the domain action $\rho$ and the output regular action $\rho_G$ distinct. The invariant measure and transitive action are part of the source's setting. §4.3, equation (14) and the following displayed identity, p. 41; homogeneous-domain assumption, p. 43.

Source claims that support the target

The milestone list records three claims from the same section. First, the pairing matches a transformed filter to the inversely transformed signal: $\langle x,\rho(g)\theta\rangle_\mu=\langle\rho(g^{-1})x,\theta\rangle_\mu$. Second, the signal action satisfies $\rho(h^{-1})\rho(g)=\rho(h^{-1}g)$. Third, for $n>0$ on the cyclic grid, the finite-sum instance of group convolution has the form $(x\star\theta)_u=\sum_{v=0}^{n-1}x_v\theta_{v+u\pmod n}$. The source's side-note calls the last expression cross-correlation. §4.3, pp. 41–42.

Significance

The equality specifies what happens to every output coordinate after a group transformation of the input. Its output is a function on $G$, so the statement also fixes which action later layers must use. In the sphere example, the first convolution produces a function on the rotation group rather than a function on the sphere; the book then describes applying a second group convolution on that output. §4.3, pp. 42–43.

The result is proved in the source. The remaining work here is to make the invariant measure, the two actions, and the real integral into separately inspectable Lean definitions and to supply machine-checked proofs of the open theorem statements. The cyclic example checks the sign convention at a concrete boundary: using $v-u$ for the group action yields $v+u$ after applying the inverse shift. Those definitions can also support later formalizations of group-indexed layers. This mission does not assert results for learned networks or approximation power; its target is the mathematical convolution identity displayed in the book.

Difficulty

The two occurrences of $\rho$ in the printed identity act on different function spaces. On the left, $\rho(h)$ transforms a signal on $\Omega$; on the right, the regular action transforms a function on $G$. Treating both as a single action obscures the type and can silently reverse the group multiplication order. The group need not be commutative, so this order matters. The measure must also be invariant: a Dirac measure concentrated at a point that moves under the group generally changes the pairing and breaks the claimed equivariance. In the cyclic example, an inverse shift changes the sign again, which is why the output has $v+u$ rather than $v-u$.

Formalization scope

Lean represents a signal as a function $\Omega\to\mathbb R$, the group action using MulAction, and the measure as a measure on $\Omega$. The action on signals, the pairing, group convolution, and the output regular action are explicit functions. The integral theorems require a transitive action, as the section specifies on p. 43, plus measurable spaces on $G$ and $\Omega$, a measurable group action, and an invariant measure. These are the conditions under which the source's change of variables is meaningful. The cyclic example applies the same group convolution to the counting measure on ZMod n, $n>0$, with the shift group acting by $v\mapsto v-u$. It does not identify a cyclic convolution with a planar convolution or assume the group and domain coincide in the general theorem.

The source describes $\mathcal X(\Omega)$ as a Hilbert space. The Lean theorem states the integral identity for arbitrary real functions; on integrable products the pairing has its ordinary meaning, while Lean assigns zero to a nonintegrable integral. The identity remains valid at those totalized inputs because the same measure-preserving transformation relates the two integrands. No integrability hypothesis is used to reduce the stated range. The zero measure is included, but the theorem is universal over invariant measures, including nonzero counting measure on finite group actions; it cannot be proved by choosing a zero measure or an empty domain. Reusable contributions include properties of the signal action, invariant integration under actions, and finite cyclic examples. The transform-and-convolve equation (32) and the second-layer composition on $G$ are outside this chunk's milestone list.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen and P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint arXiv:2104.13478v2, 2021. arXiv.

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

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