All missions

Motivation

Chapter 15 bounded the sample complexity of large-margin halfspaces by the norms of the data and of the separator, independently of the dimension. Chapter 16 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) removes the remaining obstacle to using halfspaces in very high-dimensional feature spaces: computation. After embedding the data by a feature map $\psi$ into a Hilbert space, every SVM-like problem has the form $\min_w f(\langle w, \psi(x_1)\rangle, \dots, \langle w, \psi(x_m)\rangle) + R(\|w\|)$ (16.2), and the representer theorem (Theorem 16.1) says that an optimal solution lies in the span of the mapped examples. Consequently the problem can be rewritten in terms of the $m$ coefficients and the kernel $K(x, x') = \langle\psi(x), \psi(x')\rangle$ alone (16.3): this is the kernel trick. The chapter exhibits the polynomial and Gaussian kernels (Examples 16.1 and 16.2), characterizes the functions that are kernels as the positive semidefinite ones (Lemma 16.2), and shows that the SGD solver for Soft-SVM of §15.5 can be run entirely on kernel evaluations (Lemma 16.3).

Setting

A feature map $\psi : X \to F$ takes values in a real Hilbert space, a complete real inner product space; its kernel is $K(x, x') = \langle\psi(x), \psi(x')\rangle$, and a function $K$ implements an inner product in some Hilbert space if it is the kernel of some feature map into some Hilbert space, quantified existentially in the universe of the domain. The Gram matrix of a sample is $G_{ij} = K(x_i, x_j)$. The general objective (16.2) is $f(\langle w, \psi(x_1)\rangle, \dots, \langle w, \psi(x_m)\rangle) + R(\|w\|)$ with $f$ arbitrary and $R$ nondecreasing on $[0, \infty)$. The SGD procedure of §15.5 in the feature space keeps $\theta^{(t)}$ with $w^{(t)} = \theta^{(t)}/(\lambda(t+1))$ (iterates indexed from $0$) and, at each step, for the chosen index $i$, adds $y_i\psi(x_i)$ to $\theta$ when $y_i\langle w^{(t)}, \psi(x_i)\rangle < 1$; its kernelized version keeps coefficients $\beta^{(t)}$ with $\alpha^{(t)} = \beta^{(t)}/(\lambda(t+1))$ and tests $y_i\sum_j\alpha^{(t)}_j K(x_j, x_i) < 1$. Both are driven by the same sequence of chosen indices, which stands for the uniformly random choices of the book.

Formalization targets

Goal: Theorem 16.1 (Representer Theorem)

If $R$ is nondecreasing on $[0,\infty)$ and the problem (16.2) has an optimal solution, then there is $\alpha \in \mathbb{R}^m$ such that $\sum_i \alpha_i\psi(x_i)$ is an optimal solution.

Milestones

Equation (16.3). For $w = \sum_j\alpha_j\psi(x_j)$ the objective equals $f\big(\sum_j\alpha_jK(x_j, x_1), \dots\big) + R\big(\sqrt{\sum_{i,j}\alpha_i\alpha_jK(x_j, x_i)}\big)$.

Example 16.1. The polynomial kernel $(1 + \langle x, x'\rangle)^k$ on $\mathbb{R}^n$ is $\langle\psi(x), \psi(x')\rangle$ for the monomial map into $\mathbb{R}^{(n+1)^k}$.

Example 16.2. On $\mathbb{R}$, the map $\psi(x)_n = e^{-x^2/2}x^n/\sqrt{n!}$ into $\ell^2$ has $\langle\psi(x), \psi(x')\rangle = e^{-(x-x')^2/2}$; the Gaussian kernel $e^{-\|x-x'\|^2/(2\sigma)}$ on $\mathbb{R}^n$ is a kernel for every $\sigma > 0$.

Lemma 16.2. A symmetric $K$ is a kernel iff all its Gram matrices are positive semidefinite.

Lemma 16.3. The kernelized SGD reproduces the feature-space SGD: $\theta^{(t)} = \sum_j\beta^{(t)}_j\psi(x_j)$ for all $t$, hence the outputs coincide.

Further items: Exercise 16.3 (kernel ridge regression: minimizers of the coefficient objective give minimizers of the ridge objective, and $(2\lambda mI + G)\alpha = y$ gives one), Exercise 16.4 ($\min\{x, x'\}$ is a kernel), Exercise 16.6 (the nearest-class-mean rule is a halfspace).

Significance

The representer theorem is the reason kernel methods exist: it reduces an optimization over an arbitrary Hilbert space to one over $\mathbb{R}^m$, and Lemma 16.2 says the reduction needs nothing but a positive semidefinite similarity function, so one may design the kernel directly, as in the string example of §16.2.1. Lemma 16.3 makes the connection to Chapter 14 concrete: a first-order method never leaves the span of the examples, so it too can be run on the Gram matrix. Together with Chapter 15, the chapter closes the book's treatment of linear predictors: expressive through the embedding, statistically controlled through the margin, and computable through the kernel.

Nothing here is machine-checked. The statements are faithful to the book with two clarifications: the representer theorem assumes the existence of an optimal solution, which the book's proof also assumes, and the kernel-SGD equivalence is stated for a fixed sequence of chosen indices, which is the content of the book's inductive proof.

Difficulty

Equation (16.3) and Exercise 16.6 are inner-product algebra and the entry points. The representer theorem needs the orthogonal decomposition $w^\star = \sum_i\alpha_i\psi(x_i) + u$ with $u$ orthogonal to the span, which is available in Mathlib for the finite-dimensional, hence complete, subspace spanned by the $\psi(x_i)$, together with the Pythagorean identity and the monotonicity of $R$. Example 16.1 is the multinomial expansion of $(1 + \langle x, x'\rangle)^k$ as a sum over index vectors, packaged as an inner product in the Euclidean space indexed by $\{0, \dots, n\}^k$. Example 16.2 needs the summability of $x^n(x')^n/n!$ and the exponential series, and, for the general Gaussian kernel, either an explicit construction or Lemma 16.2 together with the positive semidefiniteness of the Gaussian Gram matrix. Lemma 16.2 in the nontrivial direction is the construction of the reproducing kernel Hilbert space: the pre-Hilbert space of finite combinations of the functions $K(\cdot, x)$, the inner product defined through $K$, its well-definedness and positive definiteness from the Gram matrices, and the completion, which Mathlib provides for inner product spaces. Lemma 16.3 is an induction on $t$ with the identity $\langle w^{(t)}, \psi(x_i)\rangle = \sum_j\alpha^{(t)}_jK(x_j, x_i)$. Exercise 16.3 combines the representer theorem with the identity between the two objectives on the span and the first-order condition for a convex quadratic; Exercise 16.4 needs a feature map such as $\psi(x) = (\mathbb{1}[1 \le j \le x])_j$, or the positive semidefiniteness of the min matrix.

Formalization scope

Hilbert spaces are real, complete inner product spaces; the existential in IsKernel ranges over Hilbert spaces in the universe of the domain, which the reproducing kernel construction respects. The objective (16.2) has real-valued $f$, so the hard-SVM instance with $f \in \{0, \infty\}$ is not covered by the representer item as stated. The SGD procedures are deterministic given the index sequence; the random choice of indices is not modelled, exactly as in Lemma 16.3's proof. The string kernel of §16.2.1 and Exercise 16.1, the kernelized Perceptron (Exercise 16.2), Exercise 16.5 and part (2) of Exercise 16.6 are not stated.

Trivializing readings are excluded: the representer theorem asserts optimality against every $w$, Lemma 16.2 is a biconditional with symmetry assumed as the book does, and the kernels of the examples are exhibited with explicit feature spaces where the book gives them. Welcome contributions: the orthogonal decomposition against a finite span, the multinomial identity of Example 16.1, and the reproducing kernel Hilbert space construction behind Lemma 16.2.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 16. doi:10.1017/CBO9781107298019
• B. Schölkopf, R. Herbrich, A. J. Smola, A generalized representer theorem, Proceedings of COLT, 2001. doi:10.1007/3-540-44581-1_27
• N. Aronszajn, Theory of reproducing kernels, Transactions of the American Mathematical Society 68(3), 1950. doi:10.1090/S0002-9947-1950-0051437-7
• B. Schölkopf, A. J. Smola, Learning with Kernels, MIT Press, 2002.
• M. A. Aizerman, E. M. Braverman, L. I. Rozonoer, Theoretical foundations of the potential function method in pattern recognition learning, Automation and Remote Control 25, 1964.

Motivation

The sample complexity of learning halfspaces in $\mathbb{R}^d$ grows with $d$, which is bad news when features are many or infinite. Chapter 15 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) introduces the support vector machine, the learning rule that replaces dimension by geometry. Among the halfspaces separating a sample, Hard-SVM picks the one of largest margin, the distance from the hyperplane to the nearest example (Claim 15.1, Lemma 15.2); if the data are separable with margin $\gamma$ and lie in a ball of radius $\rho$, the resulting classifier has error $O(\rho/(\gamma\sqrt m))$ whatever the dimension (Theorem 15.4), and the Perceptron of Chapter 9 makes at most $(\rho/\gamma)^2$ updates (Remark 15.1). Soft-SVM drops separability by allowing slack variables, and Claim 15.5 identifies it with regularized hinge-loss minimization, so that the stability theory of Chapter 13 applies: the hinge loss is $\|x\|$-Lipschitz (Claim 15.6), and Corollary 15.7 gives an expected-risk bound depending only on the norms of the data and of the comparison halfspace. The chapter closes with the optimality conditions that explain the name: the Hard-SVM solution is a combination of the examples on the margin (Theorem 15.8, via the Fritz John conditions, Lemma 15.9).

Setting

Vectors live in $\mathbb{R}^d$ as in Mission VI; labels are real numbers, with $y \in \{\pm 1\}$ as a hypothesis wherever the book needs it. A sample is linearly separable if some halfspace $(w, b)$ has $y_i(\langle w, x_i\rangle + b) > 0$ for all $i$, and the margin of $(w, b)$ on the sample is $\min_i y_i(\langle w, x_i\rangle + b)$. Hard-SVM solutions are minimizers of $\|w\|$ subject to $y_i(\langle w, x_i\rangle + b) \ge 1$, formalized as a relation; the minimizer is unique whenever the constraints are feasible, and the homogenous version sets $b = 0$. A distribution over $\mathbb{R}^d \times \{\pm 1\}$ is separable with a $(\gamma, \rho)$-margin if some unit $w^\star$ (and $b^\star$) has $y(\langle w^\star, x\rangle + b^\star) \ge \gamma$ and $\|x\| \le \rho$ almost surely. Soft-SVM is the problem $\lambda\|w\|^2 + \frac1m\sum\xi_i$ under $y_i(\langle w, x_i\rangle + b) \ge 1 - \xi_i$, $\xi_i \ge 0$; its homogenous form is the regularized loss minimization rule of Mission IX for the hinge loss $\max\{0, 1 - y\langle w, x\rangle\}$, and the 0–1 loss is $\mathbb{1}[y\langle w, x\rangle \le 0]$. Expectations over samples are integrals against $D^m$, with the measurability conventions of Mission IX.

Formalization targets

Goal: Corollary 15.7, last part

For $D$ on $\{\|x\| \le \rho\} \times \{\pm 1\}$ almost surely, $B > 0$, and the Soft-SVM learner with $\lambda = \sqrt{2\rho^2/(B^2 m)}$: $\mathbb{E}_S[L^{0-1}_D(A(S))] \le \mathbb{E}_S[L^{hinge}_D(A(S))]$, and for every $w$ with $\|w\| \le B$, $\mathbb{E}_S[L^{hinge}_D(A(S))] \le L^{hinge}_D(w) + \sqrt{8\rho^2 B^2/m}$.

Milestones

Claim 15.1. The distance from $x$ to $\{v : \langle w, v\rangle + b = 0\}$ with $\|w\| = 1$ is $|\langle w, x\rangle + b|$.

Lemma 15.2. For a sample with both labels present, the normalized Hard-SVM output has unit norm and margin at least that of every unit-norm halfspace.

Theorem 15.4. Under homogenous $(\gamma, \rho)$-separability, with probability at least $1 - \delta$ the 0–1 risk of the Hard-SVM output is at most $\sqrt{4(\rho/\gamma)^2/m} + \sqrt{2\log(2/\delta)/m}$.

Claim 15.5. Every feasible slack vector has average at least the hinge loss, and the hinge losses are feasible slacks.

Claim 15.6. For $y \in \{\pm 1\}$, $w \mapsto \max\{0, 1 - y\langle w, x\rangle\}$ is $\|x\|$-Lipschitz.

Corollary 15.7, first parts. For every $u$, $\mathbb{E}_S[L^{hinge}_D(A(S))]$ and $\mathbb{E}_S[L^{0-1}_D(A(S))]$ are at most $L^{hinge}_D(u) + \lambda\|u\|^2 + 2\rho^2/(\lambda m)$.

Theorem 15.8. The homogenous Hard-SVM solution is $\sum_{i \in I}\alpha_i x_i$ with $I = \{i : |\langle w_0, x_i\rangle| = 1\}$.

Lemma 15.9. Fritz John conditions, in the correct form with a multiplier on $\nabla f$.

Further items: Exercise 15.1 (the two Hard-SVM formulations agree) and Exercise 15.2 (the Perceptron makes at most $(\rho/\gamma)^2$ updates).

Significance

SVM is the bridge between the statistical theory of Part I and the kernel methods of Chapter 16: because the bounds of Theorem 15.4 and Corollary 15.7 involve only $\rho$, $\gamma$ and $B$, the same algorithm can be run after an embedding into a huge or infinite-dimensional feature space, and Theorem 15.8, that the solution lies in the span of the examples, is what makes the embedding computable. Corollary 15.7 is also the first place where the abstract machinery of Chapter 13 is applied to a specific learning rule.

Nothing here is machine-checked. One correction is built in: the Fritz John lemma is stated with the multiplier $\alpha_0 \ge 0$ on $\nabla f(w^\star)$ and nonnegative multipliers not all zero, since the printed form, with $\nabla f(w^\star)$ unweighted and $\alpha$ unrestricted, fails already for $f(w) = w$ and $g_1(w) = w^2$ on the line. Theorem 15.8 is unaffected: its constraints are affine, so the multiplier on $\nabla f$ can be taken to be $1$.

Difficulty

Claim 15.6 and Claim 15.5 are short inequalities and the intended entry points, and Exercise 15.2 is Theorem 9.1 of Mission VI with $B \le 1/\gamma$ and $R \le \rho$. Claim 15.1 is the book's computation with the foot of the perpendicular $v = x - (\langle w, x\rangle + b)w$ and a Pythagorean inequality for every other point of the hyperplane, packaged as an infimum distance. Lemma 15.2 is the rescaling argument of the book, together with the observation that both labels force $w_0 \ne 0$; Exercise 15.1 needs the positivity of the optimal margin on a separable sample. Corollary 15.7 is Corollaries 13.8 and 13.9 of Mission IX for the hinge loss, whose Lipschitz constant is $\|x\|$ only on the support of $D$, so the stability argument must be run with the almost-sure bound; the 0–1 clause is the pointwise inequality $\ell_{0-1} \le \ell_{hinge}$. Theorem 15.4 is the content of §26.3: Rademacher complexity of the class of norm-bounded halfspaces, the contraction lemma for the ramp loss, the observation that the Hard-SVM output has zero ramp loss on the sample and norm at most $1/\gamma$, and a concentration step, all of which will be items of the Rademacher mission. Theorem 15.8 is the KKT theorem for a strictly convex quadratic with affine constraints (Slater's condition holds), and Lemma 15.9 is the general Fritz John theorem for differentiable data, whose proof goes through a separation or penalty argument; neither is in Mathlib.

Formalization scope

Hard-SVM and Soft-SVM are relations and learners, not programs; the margin is a real infimum over the sample; the ramp loss is defined but its bounds belong to Chapter 26. Theorem 15.4 is stated for any learner that returns the Hard-SVM solution whenever the sample is feasible, which is almost surely the case under the margin assumption, and bounds the failure event in outer measure. Corollary 15.7 carries the measurability conventions of Mission IX. The Fritz John lemma is stated correctly rather than as printed. The duality of §15.4, the SGD implementation of §15.5 (whose guarantee needs the trajectory bound of §14.5.3 rather than Theorem 14.11 as stated in Mission X), Exercises 15.3 and 15.4, and Remark 15.2 are not stated.

Trivializing readings are excluded: both labels must be present for the normalized Hard-SVM output, the margin assumption and the support condition are almost sure with respect to $D$, and the risks are genuine integrals. Welcome contributions: the uniqueness of the Hard-SVM minimizer, the KKT conditions for affine constraints, and the pointwise comparison of the 0–1, ramp and hinge losses.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 15. doi:10.1017/CBO9781107298019
• C. Cortes, V. Vapnik, Support-vector networks, Machine Learning 20(3), 1995. doi:10.1007/BF00994018
• B. E. Boser, I. M. Guyon, V. N. Vapnik, A training algorithm for optimal margin classifiers, Proceedings of COLT, 1992. doi:10.1145/130385.130401
• F. John, Extremum problems with inequalities as subsidiary conditions, in Studies and Essays Presented to R. Courant, 1948.
• N. Cristianini, J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. doi:10.1017/CBO9780511801389

Motivation

Chapter 3 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) is the book's first complete example of its effective-theory method. For deep linear networks at initialization, the two- and four-point correlators of the network outputs can be computed exactly at any width and depth. The resulting formulas exhibit, in the simplest setting, the phenomena that organize the rest of the book: criticality of the weight variance $C_W=1$, non-Gaussianity that grows with depth, and the depth-to-width ratio $\ell/n$ as the parameter controlling deviations from the infinite-width limit. This mission formalizes §§3.1–3.3. It is the second mission in a series formalizing the book (namespace DeepLearningTheory).

Setting

A deep linear network with widths $n_0, n_1, n_2, \dots$ (all positive) and zero biases maps an input $x\in\mathbb{R}^{n_0}$ to preactivations

$$z^{(0)}_i = x_i,\qquad z^{(\ell+1)}_i = \sum_{j=1}^{n_\ell} W^{(\ell+1)}_{ij}\, z^{(\ell)}_j \quad (i=1,\dots,n_{\ell+1}),$$

(eqs. 3.1–3.2 with $b^{(\ell)}=0$). At initialization all weights $W^{(\ell)}_{ij}$ are independent centered Gaussians with $\mathbb{E}[W^{(\ell)}_{i_1j_1}W^{(\ell)}_{i_2j_2}] = \delta_{i_1i_2}\delta_{j_1j_2}\, C_W/n_{\ell-1}$ (eq. 3.4), with a layer-independent $C_W\ge0$. For inputs $x_{\alpha_1}, x_{\alpha_2}$ let $G^{(0)}_{\alpha_1\alpha_2} = \frac1{n_0}\sum_j x_{j;\alpha_1}x_{j;\alpha_2}$ (eq. 3.9).

Formalization targets

Goal: the exact four-point correlator (eqs. 3.21, 3.25)

For every layer $\ell\ge1$, a single input $x$, and neurons $i_1,\dots,i_4$,

$$\mathbb{E}\big[z^{(\ell)}_{i_1}z^{(\ell)}_{i_2}z^{(\ell)}_{i_3}z^{(\ell)}_{i_4}\big] = (\delta_{i_1i_2}\delta_{i_3i_4}+\delta_{i_1i_3}\delta_{i_2i_4}+\delta_{i_1i_4}\delta_{i_2i_3})\; C_W^{2\ell}\Big[\prod_{\ell'=1}^{\ell-1}\Big(1+\frac{2}{n_{\ell'}}\Big)\Big]\big(G^{(0)}\big)^2 .$$

Milestones

1. Eq. (3.6) — the mean preactivation vanishes.
2. Eq. (3.10) — first-layer two-point correlator $\mathbb{E}[z^{(1)}_{i_1;\alpha_1}z^{(1)}_{i_2;\alpha_2}] = \delta_{i_1i_2}C_W G^{(0)}_{\alpha_1\alpha_2}$.
3. Eqs. (3.12), (3.15) — two-point correlator in layer $\ell$: $\delta_{i_1i_2}C_W^{\ell}G^{(0)}_{\alpha_1\alpha_2}$.
4. Eq. (3.18) — first-layer four-point correlator.
5. Eq. (3.20) — the layer-to-layer recursion for the four-point correlator.
6. Eqs. (3.21)–(3.24) — the recursion $G_4^{(\ell+1)} = C_W^2(1+2/n_\ell)G_4^{(\ell)}$ for the coefficient of the Wick tensor structure.
7. Eq. (3.30) — the connected four-point correlator between two distinct neurons, $G_4^{(\ell)} - (G_2^{(\ell)})^2$.

Significance

The closed forms show that a deep linear network is exactly Gaussian only in the strict infinite-width limit: at criticality $C_W=1$ the connected four-point correlator (3.29)–(3.30) is $\big[\prod(1+2/n_{\ell'})-1\big](G^{(0)})^2 \approx \frac{2(\ell-1)}{n}(G^{(0)})^2$ for equal widths $n$, the first appearance of the depth-to-width ratio as the book's emergent scale. The same recursive method is reused for nonlinear networks in Chapters 4–5. The results are exact computations in the book; this mission formalizes them.

Difficulty

Each correlator is an expectation of a polynomial in exponentially many Gaussian weights. The book's recursion uses that the layer-$(\ell+1)$ weights are independent of the layer-$\ell$ preactivations, followed by Wick contraction of the two or four new weights. In Lean this requires independence of a weight family from a measurable function of the earlier layers, integrability of products of Gaussian polynomials, and careful handling of the Kronecker-delta bookkeeping in the sums (3.23).

Formalization scope

• Widths are n : ℕ → ℕ with n 0 the input dimension; neural indices are $0,\dots,n_\ell-1$. Weights are a random field W : Ω → ℕ → ℕ → ℕ → ℝ on a probability space, only entries $W^{(\ell)}_{ij}$ with $\ell\ge1$, $i<n_\ell$, $j<n_{\ell-1}$ are used.
• IsLinearNetInit P n CW W states mutual independence of all these weights and that each has law gaussianReal 0 (CW / n (ℓ-1)).
• linearPreact n (W ω) x ℓ i is $z^{(\ell)}_i(x)$; inputKernel (n 0) x₁ x₂ is $G^{(0)}_{\alpha_1\alpha_2}$; kron and wickDelta4 are the Kronecker delta and the three-term tensor structure.
• Widths are assumed positive where the source's formulas require it (division by $n_\ell$, nonempty hidden layers). Every hypothesis is satisfiable by a product of independent Gaussians.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022, Chapter 3. arXiv:2106.10165
• B. Hanin, M. Nica, Products of many large random matrices and gradients in deep neural networks, Commun. Math. Phys. 376 (2020). arXiv:1812.05994

Motivation

Chapter 4 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) begins the analysis of general multilayer perceptrons (MLPs) with a nonlinear activation function $\sigma$ at initialization. The first layer is exactly Gaussian; the second layer is the first place where non-Gaussianity appears, as a connected four-point correlator suppressed by $1/n_1$ and governed by the four-point vertex $V^{(2)}$. This mission formalizes §§4.1–4.2, which are exact at any width. It is the third mission in a series formalizing the book (namespace DeepLearningTheory) and reuses the definitions of Mission II (Deep Linear Networks at Initialization).

Setting

An MLP with widths $n_0,n_1,n_2,\dots$ and activation $\sigma:\mathbb{R}\to\mathbb{R}$ maps inputs $x_\alpha\in\mathbb{R}^{n_0}$ to preactivations

$$z^{(1)}_{i;\alpha}=b^{(1)}_i+\sum_{j=1}^{n_0}W^{(1)}_{ij}x_{j;\alpha},\qquad z^{(\ell+1)}_{i;\alpha}=b^{(\ell+1)}_i+\sum_{j=1}^{n_\ell}W^{(\ell+1)}_{ij}\,\sigma\big(z^{(\ell)}_{j;\alpha}\big)$$

(eqs. 4.2, 4.30). At initialization all biases and weights are independent centered Gaussians with $\mathbb{E}[b^{(\ell)}_ib^{(\ell)}_j]=\delta_{ij}C_b^{(\ell)}$ and $\mathbb{E}[W^{(\ell)}_{i_1j_1}W^{(\ell)}_{i_2j_2}]=\delta_{i_1i_2}\delta_{j_1j_2}C_W^{(\ell)}/n_{\ell-1}$ (eqs. 4.3–4.4). The first-layer metric is $G^{(1)}_{\alpha_1\alpha_2}=C_b^{(1)}+C_W^{(1)}\frac1{n_0}\sum_jx_{j;\alpha_1}x_{j;\alpha_2}$ (eq. 4.8), and $\langle F(z_{\alpha_1},\dots,z_{\alpha_m})\rangle_{g}$ denotes the expectation over a centered Gaussian vector $(z_\alpha)$ with covariance $g$ (eq. 4.25), with $\sigma_\alpha\equiv\sigma(z_\alpha)$.

Formalization targets

Goal: second-layer connected four-point correlator (eq. 4.43)

$$\mathbb{E}\big[z^{(2)}_{i_1;\alpha_1}z^{(2)}_{i_2;\alpha_2}z^{(2)}_{i_3;\alpha_3}z^{(2)}_{i_4;\alpha_4}\big]\Big|_{\text{connected}}=\frac{1}{n_1}\Big[\delta_{i_1i_2}\delta_{i_3i_4}V^{(2)}_{(\alpha_1\alpha_2)(\alpha_3\alpha_4)}+\delta_{i_1i_3}\delta_{i_2i_4}V^{(2)}_{(\alpha_1\alpha_3)(\alpha_2\alpha_4)}+\delta_{i_1i_4}\delta_{i_2i_3}V^{(2)}_{(\alpha_1\alpha_4)(\alpha_2\alpha_3)}\Big]$$

with the four-point vertex $V^{(2)}_{(\alpha_1\alpha_2)(\alpha_3\alpha_4)}=\big(C_W^{(2)}\big)^2\big[\langle\sigma_{\alpha_1}\sigma_{\alpha_2}\sigma_{\alpha_3}\sigma_{\alpha_4}\rangle_{G^{(1)}}-\langle\sigma_{\alpha_1}\sigma_{\alpha_2}\rangle_{G^{(1)}}\langle\sigma_{\alpha_3}\sigma_{\alpha_4}\rangle_{G^{(1)}}\big]$ (eq. 4.40).

Milestones

1. Eq. (4.6) — first-layer mean vanishes.
2. Eqs. (4.7)–(4.8) — first-layer two-point correlator $\delta_{i_1i_2}G^{(1)}_{\alpha_1\alpha_2}$.
3. Eq. (4.9) — first-layer four-point correlator is the Wick value.
4. Eq. (4.23) — the first-layer preactivations are exactly Gaussian with covariance $\delta_{i_1i_2}G^{(1)}_{\alpha_1\alpha_2}$.
5. Eqs. (4.27), (4.28), (4.29) — activation correlators in the first layer as Gaussian expectations.
6. Eq. (4.40) — two-point correlator of the second-layer metric fluctuation.
7. Eq. (4.41) — second-layer two-point correlator.

Significance

These identities are the base case of the book's recursion (Chapter 4.3 onward) for the kernel and four-point vertex in deeper layers, and they show concretely that a finite-width network is not a Gaussian process: the $1/n_1$ connected correlator is generically nonzero for nonlinear $\sigma$. The results are exact computations in the book; this mission formalizes them.

Difficulty

The second layer is a Gaussian conditional on the first layer, with a random covariance (the stochastic metric, eq. 4.36). Turning this into unconditional correlators requires conditioning on the first-layer preactivations, independence of different first-layer neurons, and the identification of first-layer activation correlators with Gaussian expectations over the metric $G^{(1)}$, which may be degenerate (e.g. repeated inputs). Integrability of $\sigma$ against Gaussians must be controlled.

Formalization scope

• Definitions from Mission II are reused: kron, inputKernel, WeightIndex. New definitions: mlpPreact ($z^{(\ell)}_i(x)$), IsMLPInit (independent Gaussian biases and weights with layer-dependent $C_b^{(\ell)},C_W^{(\ell)}$), firstLayerMetric ($G^{(1)}$ on finitely many inputs), gaussAvg ($\langle\cdot\rangle_g$, via Mathlib's multivariateGaussian, which handles singular positive-semidefinite $g$), and HasPolyGrowth.
• Statements about activations assume $\sigma$ measurable with polynomial growth, the standing convention guaranteeing that all Gaussian averages are finite; this covers ReLU, tanh, sigmoid, GELU, SWISH and the perceptron step function.
• The sample set is Fin D (for the specific statements, $D=2$ or $4$ inputs, possibly repeated). $n_1>0$ is assumed where the formulas divide by $n_1$.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022, Chapter 4. arXiv:2106.10165
• R. M. Neal, Bayesian Learning for Neural Networks, Springer, 1996. doi:10.1007/978-1-4612-0745-0

Motivation

Chapter 13 showed that convex-Lipschitz-bounded and convex-smooth-bounded problems are learnable by regularized loss minimization; Chapter 14 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) shows how to learn them with the simplest possible algorithm. Gradient descent moves against the gradient with a fixed step size and outputs the average of its iterates; its analysis (Lemma 14.1) is a single telescoping identity that bounds $\sum_t \langle w^{(t)} - w^\star, v_t\rangle$ for any sequence of directions $v_t$, and this generality is the whole point. It gives the rate $B\rho/\sqrt T$ for convex Lipschitz functions (Corollary 14.2), extends to nondifferentiable functions through subgradients (Definition 14.4, Lemmas 14.3 and 14.7), and, because it never used that the directions were gradients, extends to stochastic gradient descent, in which each direction is random with a subgradient as its conditional expectation (Theorem 14.8). Applied to the risk $L_D(w)$ with a fresh example at each step, SGD is a learning algorithm whose sample complexity is the iteration count: $B^2\rho^2/\epsilon^2$ examples for convex-Lipschitz-bounded problems (Corollary 14.12) and $12B^2\beta/\epsilon^2$ for convex-smooth-bounded ones (Theorem 14.13, Corollary 14.14). A projected, decreasing-step variant for strongly convex objectives has rate $(\rho^2/(2\lambda T))(1 + \log T)$ (Theorem 14.11).

Setting

Hypotheses are vectors in $\mathbb{R}^d$; convex, Lipschitz and smooth losses, convex-Lipschitz-bounded and convex-smooth-bounded problems, and strong convexity are those of Mission IX. A vector $v$ is a subgradient of $f$ at $w$ if $f(u) \ge f(w) + \langle u - w, v\rangle$ for all $u$. The iterates of an update rule $w^{(1)} = 0$, $w^{(t+1)} = w^{(t)} - \eta v_t$ are indexed from $0$, and the output after $T$ steps is $\bar w = \frac1T\sum_{t < T} w^{(t)}$. The randomness of SGD is modelled as the chapter uses it in §14.5: a sample $z_0, \dots, z_{T-1}$ drawn i.i.d. from $D$ and an oracle $g$ with $v_t = g(w^{(t)}, z_t)$, where $g$ is a stochastic subgradient oracle for $f$ if $\mathbb{E}_{z \sim D}\, g(w, z) \in \partial f(w)$ for every $w$. This is the book's condition $\mathbb{E}[v_t \mid w^{(t)}] \in \partial f(w^{(t)})$ in the case where the direction depends on the past only through $w^{(t)}$ and on fresh randomness, which is what every application in the book does; the expectation $\mathbb{E}[f(\bar w)]$ is then an integral over $D^T$. For learning, $g(w, z)$ is a subgradient of $\ell(\cdot, z)$ at $w$, so that $\mathbb{E}_z g(w,z)$ is a subgradient of $L_D$ at $w$ (14.13). The projection of $w$ onto a convex set $H$ is a nearest point of $H$, and the strongly convex variant projects after each step with step size $1/(\lambda t)$.

Formalization targets

Goal: Theorem 14.8

For a convex $f$, $B, \rho > 0$, a measurable oracle $g$ with $\mathbb{E}_z g(w, z) \in \partial f(w)$ and $\|g(w, z)\| \le \rho$, any $w^\star$ with $\|w^\star\| \le B$, $T \ge 1$ and $\eta = B/(\rho\sqrt T)$: $\mathbb{E}[f(\bar w)] - f(w^\star) \le B\rho/\sqrt T$; and for every $\epsilon > 0$, $T \ge B^2\rho^2/\epsilon^2$ gives $\mathbb{E}[f(\bar w)] - f(w^\star) \le \epsilon$.

Milestones

Lemma 14.1. For any directions, $\sum_{t<T}\langle w^{(t)} - w^\star, v_t\rangle \le \|w^\star\|^2/(2\eta) + (\eta/2)\sum_{t<T}\|v_t\|^2$; with $\|v_t\| \le \rho$, $\|w^\star\| \le B$ and $\eta = B/(\rho\sqrt T)$ the average is at most $B\rho/\sqrt T$.

Corollary 14.2. Subgradient descent on a convex $\rho$-Lipschitz $f$ with $\eta = B/(\rho\sqrt T)$ has $f(\bar w) - f(w^\star) \le B\rho/\sqrt T$ for every $\|w^\star\| \le B$, and $T \ge B^2\rho^2/\epsilon^2$ gives $\epsilon$.

Lemma 14.7. A convex $f$ on $\mathbb{R}^d$ is $\rho$-Lipschitz iff all its subgradients have norm at most $\rho$.

Lemma 14.9. For the projection $v$ of $w$ onto a convex $H$ and $u \in H$, $\|w - u\|^2 \ge \|v - u\|^2$.

Theorem 14.11. For $\lambda$-strongly convex $f$, a closed convex $H$, an oracle with $\mathbb{E}_z\|g(w,z)\|^2 \le \rho^2$ and any $w^\star \in H$, the projected variant with $\eta_t = 1/(\lambda t)$ has $\mathbb{E}[f(\bar w)] - f(w^\star) \le (\rho^2/(2\lambda T))(1 + \log T)$.

Corollary 14.12. SGD on the risk of a convex-Lipschitz-bounded problem with $T \ge B^2\rho^2/\epsilon^2$ examples has $\mathbb{E}[L_D(\bar w)] \le L_D(w) + \epsilon$ for every $w \in H$.

Theorem 14.13. For convex, $\beta$-smooth, nonnegative losses and $\eta\beta < 1$, SGD with gradient directions has $\mathbb{E}[L_D(\bar w)] \le \frac{1}{1-\eta\beta}(L_D(w^\star) + \|w^\star\|^2/(2\eta T))$.

Corollary 14.14. For a convex-smooth-bounded problem with $\ell(0,z) \le 1$ and any $\epsilon > 0$, SGD with $\eta = 1/(\beta(1 + 3/\epsilon))$ and $T \ge 12B^2\beta/\epsilon^2$ has $\mathbb{E}[L_D(\bar w)] \le L_D(w) + \epsilon$ for every $w \in H$.

Further items: Lemma 14.3, Claims 14.5, 14.6 and 14.10, and the hinge-loss subgradient of Example 14.2.

Significance

SGD is the algorithm behind most of modern machine learning, and Theorem 14.8 is its basic guarantee: dimension-free, independent of the form of $f$ beyond convexity, and with a sample complexity matching the regularization bound of Chapter 13 up to a constant. Lemma 14.1 isolates the deterministic identity that makes both gradient descent and its stochastic version work, and Lemma 14.7 is the bridge between the Lipschitz assumption of Chapter 12 and the bounded directions the analysis needs. The learning corollaries make the point that runs through Part II of the book: for convex problems, optimization and learning are the same activity, and one pass over the data suffices.

Nothing here is machine-checked. The chapter's statements are essentially correct, and the formalization records the reading choices rather than corrections: the i.i.d.-oracle model of the randomness, the subgradient form of gradient descent, the bound at every point of the ball rather than at a minimizer, and, in Corollary 14.14, the assumptions $\epsilon \le 1$ and $0 \in H$ under which the derivation from Theorem 14.13 goes through.

Difficulty

Lemma 14.1 is a completed square and a telescoping sum and is the intended entry point; the $B\rho/\sqrt T$ clause is the substitution of $\eta$. Corollary 14.2 is Lemma 14.1 with Jensen's inequality for the average and the subgradient inequality at each iterate, plus Lemma 14.7 to bound the directions. The subgradient facts need convex analysis: Lemma 14.3 in the direction "convex implies subgradients exist" is the supporting hyperplane theorem on $\mathbb{R}^d$, which Mathlib does not offer directly; Claim 14.5 uses the first-order characterization of convexity for differentiable functions; Lemma 14.7's "Lipschitz implies bounded subgradients" is the book's one-line argument along $u = w + \epsilon v/\|v\|$. Theorem 14.8 is Lemma 14.1 plus the conditioning argument of the book, which in the i.i.d.-oracle model is Fubini on the product $D^T$: the iterate $w^{(t)}$ is a measurable function of $z_0, \dots, z_{t-1}$, and integrating $\langle w^{(t)} - w^\star, g(w^{(t)}, z_t)\rangle$ over $z_t$ first gives $\langle w^{(t)} - w^\star, \mathbb{E}_z g(w^{(t)}, z)\rangle \ge f(w^{(t)}) - f(w^\star)$. Theorem 14.11 adds the projection lemma, the strong-convexity inequality of Claim 14.10, the telescoping of $\frac{\lambda t}{2}(a_t - a_{t+1}) - \frac\lambda2 a_t$ and the harmonic sum $\sum_{t \le T} 1/t \le 1 + \log T$; the second-moment hypothesis makes $\mathbb{E}\|w^{(t)} - w^\star\|^2$ finite inductively. Corollary 14.12 is Theorem 14.8 for $f = L_D$ with the oracle of (14.13), which requires exchanging a subgradient inequality with the integral over $z$. Theorem 14.13 replaces the Lipschitz bound by self-boundedness, $\|\nabla\ell\|^2 \le 2\beta\ell$, and rearranges; Corollary 14.14 is its arithmetic under the added assumptions. In all expectation statements the measurability of the iterates in the sample, from the measurability of the oracle, is a routine but necessary lemma.

Formalization scope

Iterates are defined by structural recursion, so no argmin is chosen; the sample-driven SGD stops after $T$ updates; the projection onto $H$ is a chosen nearest point, unique for closed convex $H$. Bounds are stated for every $w^\star$ in the ball (or in $H$) rather than for a minimizer, which is what the proofs give and is stronger. The oracle bound $\|g(w,z)\| \le \rho$ is required surely (the book: with probability $1$); the almost-sure version is a routine extension. The second-moment hypothesis of Theorem 14.11 is a lower Lebesgue integral, so that a non-integrable oracle cannot satisfy it vacuously. The learning corollaries assume a measurable loss, nonnegative and bounded at the origin, so that the risks are genuine integrals, and a measurable selector of subgradients. Variable step sizes (§14.4.2), other averaging schemes (§14.4.3), SGD for regularized loss minimization (§14.5.3) and the exercises are not stated.

Trivializing readings are excluded: the expectations are over the product law of the examples with measurable integrands, the subgradient conditions are pointwise inequalities, and the iteration counts are the book's. Welcome contributions: Lemma 14.1 as a reusable telescoping lemma, the measurability of the SGD iterates, and the Fubini step that turns an oracle condition into the inequality (14.10).

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 14. doi:10.1017/CBO9781107298019
• H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3), 1951. doi:10.1214/aoms/1177729586
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, Proceedings of ICML, 2003.
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. doi:10.1137/070704277
• S. Shalev-Shwartz, Online learning and online convex optimization, Foundations and Trends in Machine Learning 4(2), 2012. doi:10.1561/2200000018

Motivation

Chapters 12 and 13 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) leave binary classification for the general framework in which a hypothesis is a vector $w \in \mathbb{R}^d$ and the loss $\ell(w, z)$ is a convex function of $w$. Convexity makes the ERM problem tractable (Lemma 12.11), but Examples 12.8 and 12.9 show that convexity, even with a bounded class, does not by itself make a problem learnable: one-dimensional linear regression with the squared loss defeats every learner. The chapter therefore isolates two families, the convex-Lipschitz-bounded and the convex-smooth-bounded problems (Definitions 12.12 and 12.13), and Chapter 13 proves that both are learnable, not by ERM but by Regularized Loss Minimization with Tikhonov regularization, $A(S) \in \operatorname{argmin}_w L_S(w) + \lambda\|w\|^2$. The proof goes through a new idea: stability. Theorem 13.2 expresses the expected overfitting $\mathbb{E}[L_D(A(S)) - L_S(A(S))]$ exactly as the expected effect of replacing one training example, strong convexity of the regularized objective bounds that effect (Lemma 13.5, Corollaries 13.6 and 13.7), and balancing the regularization against the fit gives oracle inequalities (Corollaries 13.8 and 13.10) and sample-complexity guarantees (Corollaries 13.9 and 13.11), with ridge regression as the worked example (Theorem 13.1).

Setting

Hypotheses are vectors in $\mathbb{R}^d$ with the Euclidean norm, as in Mission VI; risk, empirical risk, the product law of a sample and agnostic PAC learnability are those of Mission I. A problem is convex when $H$ is convex and every $\ell(\cdot, z)$ is convex; it is convex-Lipschitz-bounded with parameters $\rho, B$ when moreover $\|w\| \le B$ on $H$ and every $\ell(\cdot, z)$ is $\rho$-Lipschitz on $\mathbb{R}^d$, and convex-smooth-bounded with parameters $\beta, B$ when every $\ell(\cdot, z)$ is nonnegative and differentiable with a $\beta$-Lipschitz gradient. Lipschitzness and smoothness are required on all of $\mathbb{R}^d$ because the RLM rule is unconstrained and its outputs need not lie in $H$. The RLM rule is a relation: $w$ is an output on $S$ if it minimizes $L_S(w) + \lambda\|w\|^2$ over $\mathbb{R}^d$, and a learner implements the rule if all its outputs are minimizers. For the losses of the chapter the minimizer exists and is unique. Given $S = (z_1, \dots, z_m)$ and a further example $z'$, $S^{(i)}$ is $S$ with $z_i$ replaced by $z'$; a learner is on-average-replace-one-stable with rate $\epsilon(m)$ if $\mathbb{E}_{(S,z') \sim D^{m+1},\, i \sim U(m)}[\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i)] \le \epsilon(m)$ for every distribution. Strong convexity is Mathlib's StrongConvexOn, which is Definition 13.4 verbatim.

Expectations over samples are integrals against product laws. For them to be genuine, the theorems about arbitrary learners assume a jointly measurable loss bounded by a constant and a measurable learner, and the theorems about RLM assume a jointly measurable, nonnegative loss bounded at the origin and a measurable learner; for RLM the latter is automatic, since the minimizer is unique.

Formalization targets

Goal: Corollary 13.9

For a convex-Lipschitz-bounded problem with parameters $\rho, B > 0$ and the RLM learner with $\lambda(m) = \sqrt{2\rho^2/(B^2 m)}$: for every distribution, every $m \ge 1$ and every $w \in H$, $\mathbb{E}_S[L_D(A(S))] \le L_D(w) + \rho B\sqrt{8/m}$; hence for every $\epsilon > 0$ and $m \ge 8\rho^2B^2/\epsilon^2$, $\mathbb{E}_S[L_D(A(S))] \le L_D(w) + \epsilon$.

Milestones

Examples 12.8–12.9. Linear regression on $\mathbb{R}$ with the squared loss is not agnostic PAC learnable, over $H = \mathbb{R}$ or over $H = [-1, 1]$.

Theorem 13.2. For any measurable learner and $m \ge 1$, $\mathbb{E}_S[L_D(A(S)) - L_S(A(S))]$ equals the replace-one expectation of (13.6).

Lemma 13.5. $\lambda\|w\|^2$ is $2\lambda$-strongly convex; a strongly convex function plus a convex one is strongly convex; at a minimizer $u$ of a $\lambda$-strongly convex $f$, $f(w) - f(u) \ge \frac\lambda2\|w - u\|^2$.

Corollary 13.6. For a convex $\rho$-Lipschitz loss and $\lambda > 0$, RLM satisfies $\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i) \le 2\rho^2/(\lambda m)$ for every $S, z', i$, is stable with that rate, and has $\mathbb{E}_S[L_D(A(S)) - L_S(A(S))] \le 2\rho^2/(\lambda m)$.

Corollary 13.7. For a convex, nonnegative, $\beta$-smooth loss and $\lambda \ge 2\beta/m$, the replace-one expectation is at most $(48\beta/(\lambda m))\,\mathbb{E}[L_S(A(S))]$, and at most $48\beta C/(\lambda m)$ if $\ell(0, z) \le C$.

Corollary 13.8. $\mathbb{E}_S[L_D(A(S))] \le L_D(w^*) + \lambda\|w^*\|^2 + 2\rho^2/(\lambda m)$ for every $w^*$.

Corollary 13.10. $\mathbb{E}_S[L_D(A(S))] \le (1 + 48\beta/(\lambda m))\,\mathbb{E}_S[L_S(A(S))] \le (1 + 48\beta/(\lambda m))(L_D(w^*) + \lambda\|w^*\|^2)$.

Corollary 13.11. A convex-smooth-bounded problem with $\ell(0, z) \le 1$ is learned by RLM with $\lambda = \epsilon/(3B^2)$ once $m \ge 150\beta B^2/\epsilon^2$.

Theorem 13.1. Ridge regression on the unit ball with labels in $[-1, 1]$, $\lambda = \epsilon/(3B^2)$ and $m \ge 150 B^2/\epsilon^2$ has $\mathbb{E}_S[L_D(A(S))] \le \min_{\|w\| \le B} L_D(w) + \epsilon$.

Further items: Lemma 12.11, the hinge loss as a convex surrogate of the 0–1 loss, the stability-implies-no-overfitting remark of §13.2, and the ridge regression system (13.4)–(13.5).

Significance

Stability is the third route to learnability in the book after uniform convergence and nonuniform learnability, and the only one that applies to convex-Lipschitz-bounded problems in general, for which uniform convergence can fail (the book's Exercise 13.2). The chain from strong convexity through replace-one stability to oracle inequalities is the template for the analysis of every regularized learner, and Theorem 13.2 is an exact identity, not a bound. Ridge regression, support vector machines (Chapter 15) and the regularized algorithms of later chapters are all instances.

Nothing here is machine-checked. The sample sizes of Corollary 13.11 and Theorem 13.1 are the book's $150$. Chaining Corollary 13.10 as printed would need $216$, but the derivation of Corollary 13.7 actually gives the stability rate $20\beta/(\lambda m)$, with which $90$ suffices.

Difficulty

Lemma 12.11 and the hinge surrogate are direct. Lemma 13.5 is elementary but part (3) needs the limit $\alpha \to 0$ of the strong-convexity inequality at a minimizer. Examples 12.8–12.9 require constructing the two finitely supported distributions of the book and computing the risk of a fixed output on each; the probability that all $m$ examples are of the second type is at least $0.99$ under both, and the deterministic learner's output on that sample decides which distribution defeats it. Theorem 13.2 is the exchangeability argument of the book: $\mathbb{E}[\ell(A(S), z')] = \mathbb{E}[\ell(A(S^{(i)}), z_i)]$ because swapping $z_i$ and $z'$ preserves the product law; the formal work is the measure-preserving transposition on $Z^{m+1}$ and the integrability of the functions involved. Corollaries 13.6 and 13.7 follow the book's pointwise derivation from (13.7) to (13.11) and (13.12) to (13.14), where the smooth case uses the self-boundedness $\|\nabla\ell\|^2 \le 2\beta\ell$ of nonnegative smooth functions and the inequality $(a + b)^2 \le 3(a^2 + b^2)$; passing to expectations then uses Theorem 13.2 and, for the smooth case, the symmetry $\mathbb{E}[\ell(A(S^{(i)}), z')] = \mathbb{E}[\ell(A(S), z_i)]$. Corollaries 13.8 to 13.11 are the arithmetic of the book once (13.16), $\mathbb{E}[L_S(A(S))] \le L_D(w^*) + \lambda\|w^*\|^2$, is in hand, with the corrected constant for 13.11. The ridge system is the gradient condition for a strongly convex quadratic, and Theorem 13.1 is Corollary 13.11 applied to $\frac12(\langle w, x\rangle - y)^2$, which is $\|x\|^2$-smooth with $\ell(0, z) = y^2/2 \le 1/2$ on the support. In every expectation statement the measurability of $S \mapsto A(S)$ for the RLM rule, which the theorems take as a hypothesis, is provable from uniqueness of the minimizer and is worth a lemma.

Formalization scope

Losses are real-valued functions of a vector and an example; Lipschitz and smoothness conditions are global on $\mathbb{R}^d$. The RLM rule is a minimizer relation with the regularization parameter as an explicit argument, and Corollary 13.9's learner uses a parameter depending on $m$. Stability quantifies over $m \ge 1$ and averages over the replaced index. Expectation statements carry measurability hypotheses that make every integral genuine, and the theorems about arbitrary learners assume a bounded loss. The minimum over $H$ is stated as "for every $w \in H$", so no minimizer is needed. Definitions 12.1–12.9 and Claims 12.4–12.9 (general convex analysis) are not restated, nor are Examples 12.10–12.11, the discussion of §12.3 beyond the surrogate property, Remark 13.1, and Exercises 12.1–12.4 and 13.1–13.2.

Trivializing readings are excluded: the nonlearnability examples are stated as negations of the framework's learnability, the stability identity is an equality with both sides genuine integrals, and the constants of the oracle inequalities are the book's. Welcome contributions: the transposition invariance of product laws behind Theorem 13.2, the bound $\|A(S)\|^2 \le L_S(0)/\lambda$ for RLM outputs, the measurability of the RLM minimizer, and the self-boundedness inequality (12.6).

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 12 and 13. doi:10.1017/CBO9781107298019
• O. Bousquet, A. Elisseeff, Stability and generalization, Journal of Machine Learning Research 2, 2002.
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, Journal of Machine Learning Research 11, 2010.
• A. N. Tikhonov, On the stability of inverse problems, Doklady Akademii Nauk SSSR 39(5), 1943.
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. doi:10.1017/CBO9780511804441

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — $U(1)$, $SU(2)$ and $SU(3)$ — from a single linear-algebra statement applied at three node sizes. A node carrying $n$ oscillator pairs has a $2n$-dimensional real state space with a complex structure $J$. Within the model, the couplings that do no net work (passive couplings) are the symmetric matrices, and those that respect $J$ are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly $n^2$, which is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ (Unitary group):

node size $n$	admissible dimension	Lie algebra
1	1	$\mathfrak{u}(1)$
2	4	$\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$
3	9	$\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$

The dimension count has so far been checked numerically for $n = 1, \dots, 5$ only, giving $1, 4, 9, 16, 25$. A machine-checked proof covers every $n$, and it is the claim a physicist examining the model would check first.

What this mission does NOT prove. This mission proves the linear algebra: symmetric matrices commuting with $J$ form a space of dimension $n^2$. It does not prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it.

Setting

Fix a natural number $n$. Consider real $2n \times 2n$ matrices, with rows and columns indexed by two copies of $\{0, \dots, n-1\}$, so that each matrix is written in $2 \times 2$ block form with $n \times n$ blocks:

$$W = \begin{pmatrix} A & B \\ C & D \end{pmatrix}.$$

Let $I$ be the $n \times n$ identity matrix and define the standard complex structure

$$J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix},$$

which satisfies $J^2 = -1$. In the Lean development this matrix is PassivityUn.stdJ n, and the index type is PassivityUn.Blk n, the disjoint union of two copies of Fin n.

Two real linear subspaces of the $4n^2$-dimensional space of such matrices are defined:

1. symm n: the symmetric matrices, $W^{\mathsf T} = W$;
2. commJ n: the matrices commuting with $J$, $WJ = JW$.

The admissible coupling class admissible n is their intersection:

$$\mathcal{A}_n = \{\, W \in \mathbb{R}^{2n \times 2n} : W^{\mathsf T} = W \ \text{and}\ WJ = JW \,\}.$$

Formalization targets

Goal: the admissible class has dimension $n^2$

$$\dim_{\mathbb{R}} \mathcal{A}_n = n^2 \qquad \text{for every } n \in \mathbb{N}.$$

This is PassivityUn.admissible_finrank. It asserts the exact dimension for all $n$ at once, not for a particular node size.

Milestones

1. M1. $J \cdot J = -1$, so $J$ is a complex structure.
2. M2. A block matrix $\begin{pmatrix} A & B \\ C & D \end{pmatrix}$ commutes with $J$ exactly when $D = A$ and $B = -C$.
3. M3. A block matrix $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$ is symmetric exactly when $A^{\mathsf T} = A$ and $B^{\mathsf T} = -B$.
4. M4. The dimension counts of symmetric and antisymmetric $n \times n$ matrices add to $n^2$: $\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$.

Significance

The result itself. The goal identifies the admissible coupling class with the real form of the $n \times n$ Hermitian matrices, the space whose dimension is that of $\mathfrak{u}(n)$ (Hermitian matrix). Applied at $n = 1, 2, 3$ it gives the dimensions $1$, $4$ and $9$, which the Shape Zero model matches with $\mathfrak{u}(1)$, $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$. Without a proof for general $n$, the model rests on a finite numerical check.

Formalizing it. The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps (Linear complex structure). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general-$n$ statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise.

Difficulty

Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the $2n \times 2n$ matrix indexed by a disjoint union and its four $n \times n$ blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every $n$.

Formalization scope

• Matrices are real (ℝ), not complex. The complex structure enters only through the fixed real matrix $J$.
• Matrices are indexed by Fin n ⊕ Fin n (PassivityUn.Blk n) rather than Fin (2n), so that block decomposition via Mathlib's Matrix.fromBlocks is direct. The first copy of Fin n indexes the upper/left blocks.
• Each condition is defined as the kernel of a linear map: symmetry as the kernel of $W \mapsto W^{\mathsf T} - W$, and commuting with $J$ as the kernel of $W \mapsto WJ - JW$. Both are therefore subspaces by construction, with no hand-written closure proofs.
• Dimension is Module.finrank ℝ. The ambient space is finite-dimensional, so the convention that finrank of an infinite-dimensional space is $0$ never applies.
• The case $n = 0$ is included, and there the statement reads $0 = 0$. This is not a trivialization: the claim is quantified over all $n$, and every $n \ge 1$ is a nontrivial instance.
• M4 is stated with natural-number division and truncated subtraction. Both are exact here, because $n(n \pm 1)$ is always even and $n \cdot (n - 1) = 0$ when $n = 0$.

The development needs only Mathlib's block matrices, transpose, linear maps and finrank. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with $J$ to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism.

Selected references

• B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
• Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
• Wikipedia, Linear complex structure. https://en.wikipedia.org/wiki/Linear_complex_structure
• Wikipedia, Hermitian matrix. https://en.wikipedia.org/wiki/Hermitian_matrix
• Mathlib, Mathlib.Data.Matrix.Block (block matrices, Matrix.fromBlocks). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.html