Machine Learning

Motivation

A classifier built from a neural network produces a real score and predicts a binary label from its sign. A network can have many hidden units, so a guarantee based only on the number of parameters can be uninformative even when its output weights are small. Bartlett's 1998 paper asks whether a classifier's margin on training examples and the total magnitude of its weights can control its probability of error without fixing the number of units. Its Theorem 28 gives such a statement for two-layer networks whose activation is bounded and nondecreasing. The paper also discusses why this parameter-magnitude view supports weight decay and early stopping as learning heuristics, while leaving their algorithmic behavior outside the theorem's scope (Bartlett 1998, pp. 526, 534–535).

The theorem combines two results in the same paper. Theorem 2 turns the fat-shattering dimension of a real-valued function class into a margin generalization bound. Corollary 24 controls that dimension for finite combinations of affine-input units when the sum of the absolute combination weights is bounded. Lemmas 19, 22, and 23 supply covering estimates along that path. These are the milestones of this mission, with the source statements preserved in the milestone record (Bartlett 1998, pp. 527, 532–534).

Setting

An input is a vector $x\in\mathbb R^n$, represented in Lean as Fin n → ℝ. A label is $y\in\{-1,+1\}$; Lean's Bool is converted by pm, where true means $+1$. A probability distribution $P$ lives on labeled inputs. From an independent sample $z=((x_i,y_i))_{i=1}^m$, the empirical margin error at scale $\gamma>0$ is the fraction of indices with $y_i h(x_i)<\gamma$. The population error is the probability that $\operatorname{sgn}(h(x))\ne y$, where $\operatorname{sgn}(0)=+1$. The inequality in the empirical error is strict, as in the paper's definition (Bartlett 1998, p. 526).

Fix a bounded nondecreasing activation $\sigma:\mathbb R\to[-1,1]$. The first-layer class $F$ contains every $x\mapsto\sigma(w\cdot x+w_0)$, with an arbitrary weight vector and bias. The network class $H$ contains all finite sums $\sum_{i=1}^N\alpha_i f_i$ with $f_i\in F$ and $\sum_i|\alpha_i|\le A$. Thus $A$ bounds the output layer's total weight magnitude, while $N$ can vary without an imposed width limit. The bias $w_0$ is part of every unit. For a class $G$, $\operatorname{fat}_G(\eta)$ records the largest length of an input sequence whose every sign pattern can be realized with separation at least $\eta$ around one vector of thresholds (Bartlett 1998, pp. 526, 533–534).

Formalization targets

Two-layer generalization

For $0<\gamma\le1$, $0<\delta<1/2$, $A\ge1$, and an independent sample of length $m\ge1$, the goal is one universal $c>0$ such that, with probability at least $1-\delta$, every $h\in H$ satisfies

$$\operatorname{er}_P(h)<\widehat{\operatorname{er}}_z^\gamma(h)+ \sqrt{\frac{c}{m}\left( \frac{A^2n}{\gamma^2}\log\!\left(\frac{32A}{\gamma}\right)(\log m)^2+ \log\!\left(\frac1\delta\right)\right)}.$$

The paper prints $\log(A/\gamma)$ in this display. That term vanishes at $A=\gamma=1$, although the class can then contain halfspace classifiers with nonzero sample complexity. The proof obtains a positive factor at that corner through Corollary 24 at scale $\gamma/16$, giving $\log(32A/\gamma)$. The goal states this correction and records the printed statement separately in the moderation notes. The constant precedes all network, distribution, margin, confidence, and sample parameters in Lean; it cannot be selected after observing the instance (Bartlett 1998, pp. 533–534).

Capacity and margin milestones

Corollary 24 bounds $\operatorname{fat}_H(\eta)$ by a constant multiple of $M^2A^2n\eta^{-2}\log(MA/\eta)$ when the activation has range $[-M/2,M/2]$. Theorem 2 then converts a finite fat dimension at scale $\gamma/16$ into a simultaneous bound on population error for all members of $H$. The three covering lemmas track how shattering, pseudodimension, and an $\ell_1$ weight budget affect covers in sample $\ell_1$, $\ell_\infty$, and $\ell_2$ distances. Each bound retains the scale and explicit constants printed by the paper, subject to the stated corrections to undefined or false boundary cases (Bartlett 1998, pp. 527, 532–533).

Significance

The goal gives a width-independent generalization guarantee for a chosen network when its empirical margin error and total output weight are small. It applies to the entire class $H$ at once, so choosing a network after inspecting the sample does not turn the bound into a claim about only one fixed predictor. It does not assert that a learning algorithm finds such a network or that the displayed constants are optimal. Bartlett notes that later work had improved a logarithmic factor, and that empirical agreement with neural-network performance remained an open experimental question at the time (Bartlett 1998, pp. 534–535).

The paper proves the mathematical result. This mission asks for a machine-checked proof of its corrected formal statement and the stated supporting results; the draft theorem files currently contain proof obligations. A completed development would also make the fat dimension and strict external sample-cover definitions available for other margin analyses. Those objects differ from the platform's fixed-architecture neural networks and closed-ball covering numbers, so they are defined here with the conventions of this paper.

Difficulty

Counting hidden units gives no finite width-independent capacity bound, because $H$ permits arbitrarily many terms. Bounding each unit separately also does not control the full combination class: different small contributions can produce distinct values on a sample. The challenging step is relating covers of the base class to covers of all finite combinations under the total absolute-weight constraint, and then relating those covers back to fat-shattering. Even once a finite capacity estimate is available, the probability statement must hold simultaneously for every $h\in H$, including a network selected after sampling (Bartlett 1998, pp. 532–534).

Formalization scope

Lean uses $\mathbb N\cup\{\infty\}$ for fat dimensions and covering numbers, so an unbounded class cannot acquire a spurious dimension zero. Covers are external finite sets of real functions and use the strict distance $<\varepsilon$ of Definition 3. Sample $\ell_1$ and $\ell_2$ distances are normalized by $m$. Pseudodimension is the supremum of positive-scale fat dimensions, matching the paper's right limit. Theorems assume $m\ge1$, and sample indices are zero-based. The network class is generated from its weights rather than supplied as an arbitrary set satisfying the desired bound.

The paper says it ignores measurability issues and assumes all sets considered are measurable (Bartlett 1998, p. 526). The goal makes the event of a violating network measurable. Its individual network functions are measurable from monotonicity of $\sigma$ and finite sums; the restated Theorem 2 has explicit hypotheses for measurable class members, the violating event, and the double-sample event in its proof. Theorem 2 additionally restricts $d=\operatorname{fat}_H(\gamma/16)$ to $d\le34m$, where its printed logarithmic bound remains valid. Corollary 24 uses $n\ge1$ because a zero-dimensional input still permits a biased constant unit. Lemma 23 uses $d\ge1$ and $0<\gamma<emM/d$ in place of the printed $\gamma\ge0$: at $\gamma=0$ or $d=0$, or for $\gamma\ge emM/d$, the printed strict inequality fails, while on the rest of the printed range it is kept. These are recorded as corrections rather than attributed to the printed wording.

The deeper-network part of Theorem 28 is outside this proposal. Its printed chain through Corollary 27 has an unresolved range issue when the input box bound $B$ is smaller than the activation range, and the displayed $\log n$ factor also vanishes at $n=1$. This mission's goal is Part 1 and uses none of those claims. Contributions that establish the corrected covering lemmas, the capacity corollary, or the simultaneous margin bound fit the present proof frontier (Bartlett 1998, pp. 533–534).

Selected references

• P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Transactions on Information Theory 44(2), 525–536, 1998. DOI.

Motivation

A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function $K(x,y)$ that represents evaluation at $y$ is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.

Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.

Setting

Let $X$ be an arbitrary set and $E_1\subset E_2\subset\cdots$ subsets with union $E = E_1+E_2+\cdots = X$. For each $n$ let $F_n$ be a complex Hilbert space of functions on $E_n$, with norm $\|\cdot\|_n$, in which point evaluations are continuous; $K_n(x,y)$, for $x,y\in E_n$, is its reproducing kernel, characterized by $K_n(\cdot,y)\in F_n$ and

$$f(y) = (f, K_n(\cdot,y))_n \qquad (f\in F_n,\ y\in E_n),$$

with the scalar product $(f,g)_n$ linear in $f$. For $f_n\in F_n$ and $m\le n$, $f_{nm}$ denotes the restriction of $f_n$ to $E_m$. The standing assumptions of §9 A (p. 362) are:

1. $E_1\subset E_2\subset\cdots$ and $E = \bigcup_n E_n$;
2. the classes decrease: $f_{nm}\in F_m$ for every $f_n\in F_n$ and $m\le n$;
3. the norms increase: $\|f_{nm}\|_m\le\|f_n\|_n$ for every $f_n\in F_n$ and $m\le n$;

together with the existence of every kernel $K_n$. For two kernels on a set $Y$, $K_1\ll K$ means that $K-K_1$ is a positive matrix: $\sum_{i,j}(K-K_1)(y_i,y_j)\,\bar\xi_i\xi_j\ge 0$ for all finite families $y_i\in Y$, $\xi_i\in\mathbb C$. $K_{nm}$ is the restriction of $K_n$ to $E_m\times E_m$.

The limit class $F_0$ is the set of functions $f_0$ on $E$ such that (1°) every restriction $f_{0n}$ belongs to $F_n$ and (2°) $\lim_n\|f_{0n}\|_n<\infty$.

Formalization targets

Goal: §9, Theorem I (pp. 362–363)

Under the standing assumptions there is $K_0 : E\times E\to\mathbb C$ such that, whenever $x,y\in E_N$,

$$\lim_{n\to\infty}K_n(x,y)=K_0(x,y),$$

and $K_0$ is the reproducing kernel of $F_0$ with the norm

$$\|f_0\|_0=\lim_{n\to\infty}\|f_{0n}\|_n .$$

Milestones (in the order the proof uses them)

1. §9, Eq. (4): $K_{nm}\ll K_m$ for $m<n$.
2. §9, proof of Theorem I, p. 363: for $y\in E_k$, $\{K_m(y,y)\}_{m\ge k}$ is a decreasing sequence of non-negative numbers.
3. §9, Eq. (5): for $y\in E_k$, $k\le m\le n$, $\|K_{mk}(\cdot,y)-K_{nk}(\cdot,y)\|_k^2\le K_m(y,y)-K_n(y,y)$.
4. §9, Eq. (6): with $K_0$ the pointwise limit, $K_{0k}(\cdot,y)\in F_k$ and $\|K_{mk}(\cdot,y)-K_{0k}(\cdot,y)\|_k^2\le K_m(y,y)-K_0(y,y)$.
5. §9, Remark after Theorem I: under 1°, $\|f_{0n}\|_n$ is non-decreasing, so its limit exists, possibly infinite.
6. §9, Eq. (7): if $F_0$ carries the limit norm, then $(f_0,g_0)_0=\lim_n(f_{0n},g_{0n})_n$.

Significance

The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With $E_n=E$ for all $n$ (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels $K_1\gg K_2\gg\cdots$ on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of $K_m(\cdot,y)$ in every $F_k$.

Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order $\ll$ between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over $\mathbb C$, with kernels on varying domains.

Difficulty

The kernels $K_n$ live on different sets $E_n\times E_n$, so convergence is not convergence of a sequence of functions on one set: a pair $x,y$ enters the sequence only from the first $E_N$ containing both. The identification of the limit class needs three separate facts: that $F_0$ with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that $K_0(\cdot,y)\in F_0$, and that $K_0$ reproduces. The natural first idea, to embed all $F_n$ in one space and take an intersection, fails: the $F_n$ are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.

Formalization scope

• Scalars and spaces. Complex scalars throughout (Aronszajn works with complex Hilbert spaces from §1 on). Each $F_n$ is a type H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set $E$ is a type X with no topology, measure or nonemptiness assumption.
• Kernel. The scalar kernel kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's $(f,g)$ is ⟪g, f⟫_ℂ.
• Standing assumptions. (1)–(3) are the structure IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on $E_m$. Indexing starts at $0$.
• Order. $K_1\ll K$ is KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).
• Comparisons of kernel values ($K_m(y,y)\ge 0$, the right-hand sides of (5), (6)) are in Mathlib's ComplexOrder, which also asserts that these values are real.
• Convergence of kernels is stated only where the terms are defined: for $x,y\in E_N$, the sequence $j\mapsto K_{N+j}(x,y)$ converges to $K_0(x,y)$. Kernels are never extended by $0$ outside $E_n$.
• Condition 2° is convergence of $\|f_{0n}\|_n$ to a real number, not a supremum, and the norm of $F_0$ is stated as a limit (Tendsto).
• The goal asserts (a) the convergence, (b) the existence of an RKHS on $X$ with kernel $K_0$, and (c) that every RKHS on $X$ with kernel $K_0$ has exactly the functions of $F_0$ as its elements and the limit norm. A formalization that defines $F_0$ as RKHS.OfKernel K₀ and then asserts that its kernel is $K_0$ would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.
• Eq. (7) is stated for an inner product space of functions whose norm is assumed to be the limit norm; the paper's derivation that the limit norm is a quadratic form is the content of the goal.
• Non-vacuity. The constant sequence $E_n=E$, $F_n=F$ satisfies the standing assumptions (checked in Lean), and the one-point example $F_n=\mathbb C$ with norms $c_n|f|$, $c_n$ increasing, satisfies them with $K_n=c_n^{-2}$.

Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• E. H. Moore, General Analysis, Part I, Memoirs of the American Philosophical Society 1 (1935). (Positive matrices.)
• Mathlib, Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4

Motivation

Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.

Setting

Let $E$ be an arbitrary set and let $F$ be a class of complex-valued functions on $E$ that forms a complex Hilbert space with scalar product $(f, g)$, linear in $f$ and conjugate-linear in $g$. A reproducing kernel of $F$ is a function $K : E \times E \to \mathbb{C}$ such that, for every $y \in E$, the function $K(\cdot, y)$ belongs to $F$ and

$$f(y) = (f, K(\cdot, y)) \qquad \text{for every } f \in F.$$

Such a kernel exists exactly when every point evaluation $f \mapsto f(y)$ is continuous.

For a bounded linear operator $L$ on $F$, with adjoint $L^*$ defined by $(Lf, g) = (f, L^* g)$, the kernel of $L$ is

$$\Lambda(x, y) = L^*_x K(x, y),$$

the value at $x$ of the element $L^*(K(\cdot, y))$ of $F$. By the reproducing property, $Lf(y) = (f, \Lambda(\cdot, y))$ for every $f \in F$ and $y \in E$, so $L$ is determined by $\Lambda$.

A function $P : E \times E \to \mathbb{C}$ is a positive matrix if $\sum_{i,j} \overline{\xi_i}\, P(y_i, y_j)\, \xi_j \ge 0$ for every finite family of points $y_i \in E$ and complex numbers $\xi_i$. For two arbitrary functions $\Lambda_1, \Lambda_2$ on $E \times E$, one writes $\Lambda_1 \ll \Lambda_2$ if $\Lambda_2 - \Lambda_1$ is a positive matrix. A bounded operator $L$ is symmetric if $L = L^*$, and positive if $(Lf, f) \ge 0$ for every $f$. A symmetric $L$ has lower bound $\ge m$ and upper bound $\le M$ if

$$m\,(f, f) \le (Lf, f) \le M\,(f, f) \qquad \text{for every } f \in F.$$

A kernel $\Lambda$ is hermitian symmetric if $\Lambda(x, y) = \overline{\Lambda(y, x)}$.

Formalization targets

Goal: §11, Theorem I (p. 373)

For an arbitrary hermitian symmetric function $\Lambda : E \times E \to \mathbb{C}$ and real numbers $m, M$:

$$\exists\, L \text{ bounded, symmetric, with } \Lambda = L^*_x K(x,y) \text{ and } m(f,f) \le (Lf,f) \le M(f,f)\ \ \forall f \quad\Longleftrightarrow\quad mK \ll \Lambda \ll MK .$$

The function $\Lambda$ is not assumed to have $\Lambda(\cdot, y) \in F$; that membership is part of what the condition yields.

Milestones

1. §11, (3): the kernel of the adjoint, $\Lambda^*(y, z) = \overline{\Lambda(z, y)}$.
2. §11, (6): $L$ is symmetric if and only if $\Lambda$ is hermitian symmetric.
3. §11, (7): $L$ is positive if and only if $\Lambda$ is a positive matrix.
4. §11, (4): the kernel of a composition, $\Lambda(y, z) = (\Lambda_1(x, z), \overline{\Lambda_2(y, x)})_x$ for $L = L_1 L_2$.
5. §11, Theorem II: if $L_n u \to L u$ weakly for every $u$, then $\Lambda_n \to \Lambda$ pointwise; if $\|L_n - L\| \to 0$, then $\Lambda_n \to \Lambda$ uniformly on every set of couples $(x, y)$ on which $K(x, x)$ and $K(y, y)$ are uniformly bounded.
6. §11, Theorem III, first sentence: for complete orthonormal systems $\{g'_m\}$, $\{g''_n\}$ and $\alpha_{mn} = (g''_n, L g'_m)$,

$$\Lambda(x, y) = \lim_{p, q \to \infty} \sum_{m=1}^{p} \sum_{n=1}^{q} \alpha_{mn}\, g'_m(x)\, \overline{g''_n(y)} .$$

Significance

Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities $mI \le L \le MI$) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence $L \mapsto \Lambda$ a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.

All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.

Difficulty

The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: $\Lambda$ is an arbitrary function, and the hypothesis $mK \ll \Lambda \ll MK$ is only about finite families of points. One has to produce an operator on all of $F$. The obvious attempt, defining $L$ on the dense span of the functions $K(\cdot, y)$ by the kernel and extending by continuity, needs the bound $|(\,L f, g)| \le C\|f\|\|g\|$ on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of $\Lambda - mK$ and $MK - \Lambda$ does not by itself give the membership $\Lambda(\cdot, y) \in F$, which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of $F$, while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.

Formalization scope

• The space is Mathlib's RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function $K(\cdot, y)$ is the element RKHS.kerFun H y 1.
• The kernel of L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's $(f, g)$ is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point $E$ with $F = \mathbb{C}$, $K = 1$ and $L = cI$, the kernel is $\bar c$.
• Positive matrices and $\ll$ are Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.
• Symmetric is IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume $m \le M$ and neither does the statement: for $m > M$ both sides hold exactly when $F = \{0\}$ and $\Lambda = 0$.
• In (4) the statement asserts that the functions $x \mapsto \Lambda_1(x, z)$ and $x \mapsto \overline{\Lambda_2(y, x)}$ are elements of H, and that the kernel of L₁ ∘L L₂ is their scalar product.
• Weak convergence in Theorem II is ⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.
• In Theorem III the orthonormal systems are HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by $\mathbb{N}$ this contains the paper's $\lim_{p,q}$ over $\{1..p\}\times\{1..q\}$; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in $F \otimes \overline{F}$ correspond to operators of finite norm) needs the direct product $F \otimes \overline F$ and is not stated.
• A trivializing formalization is ruled out: Theorem I quantifies over every hermitian function $\Lambda$, not over functions already known to be kernels of operators, and the right-hand side is the finite-matrix condition, not a statement about an operator built from $\Lambda$.
• Not stated: the decomposition (8)–(9) into hermitian parts and the remark on general bounded operators (p. 374), and formula (5). Available substrate: RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function $\Lambda$ with $0 \ll \Lambda \ll K$ is the kernel of an operator $0 \le L \le I$, and the inclusion theorem $K_1 \ll K \Rightarrow F_1 \subset F$, both reusable beyond this mission.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• E. H. Moore, General Analysis, Part II, Mem. Amer. Philos. Soc. 1 (1939).
• V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781316219232

Motivation

In the mid-1990s, neural networks trained by gradient descent were observed to generalize well even when the number of weights far exceeded the number of training examples. The classical theory could not explain this: VC-dimension bounds for networks grow with the number of parameters, so for large networks they are vacuous. Bartlett's paper (IEEE Trans. Inform. Theory 44 (1998)) showed that, for classification with a margin, what controls generalization is the size of the weights, not the size of the network. Its two main technical results are a margin bound in terms of the fat-shattering dimension (Theorem 2, the subject of mission I of this series) and a bound on the fat-shattering dimension of networks with bounded weights (Theorem 17, the subject of this mission). The same idea of weight-norm capacity control underlies much of the later theory of margins, boosting and kernel methods.

Timeline. Kearns and Schapire (1994) introduced the fat-shattering dimension. Alon, Ben-David, Cesa-Bianchi and Haussler (1997) bounded ℓ∞ covering numbers by it. Bartlett, Kulkarni and Posner (1997) gave the matching lower bound on ℓ1 covering numbers used here as Lemma 19. Maurey's approximation lemma (reported by Pisier, 1981) was used by Jones (1992) and Barron (1993) for approximation by networks, and by Lee, Bartlett and Williamson (1996) for covering numbers of convex hulls. Bartlett (1998) combined these into Theorem 17.

Setting

Let $X$ be a set and $H$ a class of functions $X\to\mathbb R$. For $\gamma>0$, a sequence $x=(x_1,\dots,x_m)\in X^m$ is $\gamma$-shattered by $H$ if there is $r\in\mathbb R^m$ such that for every $b\in\{-1,1\}^m$ some $h\in H$ satisfies $(h(x_i)-r_i)b_i\ge\gamma$ for all $i$. The fat-shattering dimension is

$$\operatorname{fat}_H(\gamma)=\max\{m:\ H\ \gamma\text{-shatters some }x\in X^m\}\in\mathbb N\cup\{\infty\}.$$

A cover of a class $F$ at scale $\varepsilon$ for a pseudometric $\rho$ on functions is a set $T$ of functions such that every $f\in F$ has some $t\in T$ with $\rho(t,f)<\varepsilon$; $\mathcal N(F,\varepsilon,\rho)$ is the least size of a cover. For a sample $x\in X^m$ the pseudometrics $d_{\ell_\infty(x)}$, $d_{\ell_1(x)}$, $d_{\ell_2(x)}$ are the maximum, the mean, and the root mean square of $|f(x_i)-g(x_i)|$ over $i$, and the uniform covering numbers are $\mathcal N_p(F,\varepsilon,m)=\max_{x\in X^m}\mathcal N(F,\varepsilon,d_{\ell_p(x)})$.

The hidden units form a nonempty class $F$ of functions $X\to[-M/2,M/2]$. For $A>0$ the two-layer network class with ℓ1-bounded output weights is

$$H=\Big\{\sum_{i=1}^Nw_if_i:\ N\in\mathbb N,\ f_i\in F,\ \sum_{i=1}^N|w_i|\le A\Big\}.$$

In Lean these are BartlettNN.Margin.fat, BartlettNN.Margin.coverNum and BartlettNN.Margin.Ninf (shared with mission I), and BartlettNN.FatNet.N1, BartlettNN.FatNet.N2 and BartlettNN.FatNet.combos F A.

Formalization targets

Goal: Theorem 17

There is a universal constant $c$ such that for every $X$, $F$, $M$, $A>0$ and $\gamma>0$ with $d=\operatorname{fat}_F(\gamma/(32A))\ge1$,

$$\operatorname{fat}_H(\gamma)\le\frac{cM^2A^2d}{\gamma^2}\ln^2\Big(\frac{MAd}{\gamma}\Big).$$

The constant is left unspecified, as in the paper, so that the goal survives any improvement of the numerical constants.

Milestones (in the order the proof uses them)

1. Lemma 19 (cited from Bartlett–Kulkarni–Posner): for $[0,1]$-valued $F$ with $\operatorname{fat}_F(4\gamma)\ge d$, $\log_2\mathcal N_1(F,\gamma,d)\ge d/32$.
2. Lemma 20, (5): for $d=\operatorname{fat}_F(\gamma/4)$ and $m\ge2+2d\log_2(32M/\gamma)$, $\log_2\mathcal N_2(F,\gamma,m)<1+d\log_2(4emM/(d\gamma))\log_2(9mM^2/\gamma^2)$.
3. Lemma 21 (Maurey): in a Hilbert space, a point of the closed convex hull of a set of norm at most $b$ is within $\sqrt{c/k}$ of an average of $k$ points of the set, for every $c>b^2-\|h\|^2$.
4. Lemma 22: $\log_2\mathcal N_2(H,\gamma,m)\le(2M^2A^2/\gamma^2)\log_2(2\mathcal N_2(F,\gamma/(2A),m)+1)$.
5. Inequality (6): if $m=\operatorname{fat}_H(4\gamma)\ge2+2d\log_2(64MA/\gamma)$ with $d=\operatorname{fat}_F(\gamma/(8A))$, then $m\le(64M^2A^2/\gamma^2)(3+d\log_2(8emMA/\gamma)\log_2(36mM^2A^2/\gamma^2))$.

Significance

Theorem 17 bounds the capacity of a network class without reference to the number of hidden units $N$. With Theorem 2 (mission I) it gives misclassification bounds for networks with small weights that hold for networks of any size, and by iteration it yields the bounds for deep sigmoid networks of Theorem 28 (mission III). Its method — upper-bound ℓ2 covering numbers through Maurey's lemma and compare with a lower bound in terms of fat-shattering — is a template for bounding the fat-shattering dimension of convex hulls in general.

The results are proved in the paper (Lemmas 19 and 21 by citation). None of them is formalized: the platform has no fat-shattering dimension, no uniform sample covering numbers of function classes, and only a finite-dimensional, diameter-based form of Maurey's lemma (HighDimProb.Appetizer.approx_caratheodory), which is not Lemma 21. This mission produces machine-checked statements of all five ingredients and of the theorem.

Difficulty

The obvious route would bound $\operatorname{fat}_H$ through a VC-type count of the network's parameters, which fails because $N$ is unbounded. The paper's route needs a lower bound on covering numbers by the fat-shattering dimension (Lemma 19, a combinatorial packing argument not proved in the paper), an upper bound by the fat-shattering dimension at a finer scale (Lemma 20, which goes through the Alon et al. scale-sensitive Sauer lemma and a quantization argument), and a probabilistic approximation argument in the empirical $L_2$ space (Lemmas 21 and 22). The final step solves a transcendental inequality (6) for $m$, with care at the boundary where the logarithm is small.

Formalization scope

• Functions are maps X → ℝ; fat is valued in ℕ∞, so an unbounded shattering is $\infty$, not a junk $0$. Labels $\pm1$ are Bool read through pm (true ↦ 1); sequences are indexed by Fin m (0-based).
• Covers are external (finite sets of arbitrary functions $X\to\mathbb R$) with the strict inequality of Definition 3; the covering number is $\infty$ when no finite cover exists. The ℓ1 and ℓ2 distances carry the factor $1/m$. Mathlib's Metric.coveringNumber (closed balls, metric types) is not used.
• Bounds of the form "$\log_2\mathcal N\le B$" are stated for every finite value of $\mathcal N$, and where the paper's bound implies finiteness (Lemmas 20, 22, Theorem 17) finiteness is part of the conclusion.
• The constant $c$ of Theorem 17 is quantified before $X$, $F$, $M$, $A$, $\gamma$ and $d$; a constant chosen after them would make the statement trivially true.
• Corrections of the printed statement. Theorem 17 is stated for $\gamma>0$ (printed $\gamma\ge0$, under which the bound is meaningless) and $A>0$ (printed $A\ge0$, under which $\gamma/(32A)$ is undefined). Implicit positivity ($M>0$, $\gamma>0$, $A>0$) in Lemmas 20, 22 and (6) is stated as hypotheses. Inequality (6) is copied as printed, with $\log_2(8emMA/\gamma)$.
• In Theorem 17 the logarithm is natural (the base is absorbed by $c$); (5) and (6) use $\log_2$.
• Lemma 21 is stated in a complete real inner product space, with "convex closure" read as the closure of the convex hull.

Contributions welcome: proofs of the five milestones and of the goal, and reusable infrastructure on fat-shattering and covering numbers of function classes.

Selected references

• P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Trans. Inform. Theory 44(2), 1998, 525–536. https://doi.org/10.1109/18.661502
• N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, J. ACM 44(4), 1997, 615–631. https://doi.org/10.1145/263867.263927
• P. L. Bartlett, S. R. Kulkarni, S. E. Posner, Covering numbers for real-valued function classes, IEEE Trans. Inform. Theory 43(5), 1997, 1721–1724. https://doi.org/10.1109/18.623181
• M. J. Kearns, R. E. Schapire, Efficient distribution-free learning of probabilistic concepts, J. Comput. Syst. Sci. 48(3), 1994, 464–497. https://doi.org/10.1016/S0022-0000(05)80062-5
• W. S. Lee, P. L. Bartlett, R. C. Williamson, Efficient agnostic learning of neural networks with bounded fan-in, IEEE Trans. Inform. Theory 42(6), 1996, 2118–2132. https://doi.org/10.1109/18.556601
• A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inform. Theory 39(3), 1993, 930–945. https://doi.org/10.1109/18.256500

Motivation

Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point $x$ does not change for any perturbation $\delta$ in a stated set, typically an $\ell_2$ ball $\|\delta\|_2<R$. Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$ (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.

Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.

Setting

Inputs live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$; classes form a set $\mathcal Y$. A base classifier is a map $f:\mathbb R^d\to\mathcal Y$ with Borel decision regions. For a noise level $\sigma>0$, write $\mathcal N(x,\sigma^2I)$ for the isotropic Gaussian law of $x+\varepsilon$ with $\varepsilon\sim\mathcal N(0,\sigma^2I)$. The class probability of $c$ at $x$ is $\mathbb P(f(x+\varepsilon)=c)$, and the smoothed classifier is

$$g(x)=\arg\max_{c\in\mathcal Y}\ \mathbb P(f(x+\varepsilon)=c).$$

Let $\Phi$ be the standard Gaussian CDF and $\Phi^{-1}$ its inverse on $(0,1)$. A classifier $f$ is consistent with the observed class probabilities (6) for a top class $c_A$ and numbers $\underline{p_A}\ge\overline{p_B}$ if

$$\mathbb P(f(x+\varepsilon)=c_A)\ \ge\ \underline{p_A}\ \ge\ \overline{p_B}\ \ge\ \max_{c\ne c_A}\mathbb P(f(x+\varepsilon)=c).$$

The certified radius is $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$. In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces $A=\{z:\delta^T(z-x)\le\sigma\|\delta\|\Phi^{-1}(\underline{p_A})\}$ and $B=\{z:\delta^T(z-x)\ge\sigma\|\delta\|\Phi^{-1}(1-\overline{p_B})\}$ of the paper's Appendix A are setA and setB.

Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.

Formalization targets

Goal: Theorem 2 (corrected)

Assume $0<\overline{p_B}\le\underline{p_A}<1$, $\underline{p_A}+\overline{p_B}\le1$, and that some finite set $s$ of classes other than $c_A$ satisfies $1\le\underline{p_A}+|s|\,\overline{p_B}$. Then for every $\delta$ with $\|\delta\|_2>R$ there is a base classifier $f^*$ consistent with (6) and a class $c\ne c_A$ with

$$\mathbb P(f^*(x+\delta+\varepsilon)=c_A)\ <\ \mathbb P(f^*(x+\delta+\varepsilon)=c),$$

so that $g(x+\delta)\ne c_A$ under any tie-breaking. The classifier may depend on $\delta$.

The class-capacity hypothesis is a correction. As printed, with only $\underline{p_A}+\overline{p_B}\le1$, the theorem fails for two classes: with $\mathcal Y=\{c_A,c_B\}$, $\underline{p_A}=0.6$, $\overline{p_B}=0.1$ and $\sigma=\|\delta\|_2=1$, one has $R\approx0.767<1$, yet every consistent $f$ gives $c_A$ probability at least $0.9$, and Theorem 1 then certifies radius $\Phi^{-1}(0.9)\approx1.28$.

Milestones

The milestones are the steps the paper itself states, in its order: the Claims $\mathbb P(X\in A)=\underline{p_A}$ and $\mathbb P(X\in B)=\overline{p_B}$ for $X\sim\mathcal N(x,\sigma^2I)$; the disjointness of $A$ and $B$ (corrected to "null" when $\underline{p_A}+\overline{p_B}=1$); equations (13) and (14) for $Y\sim\mathcal N(x+\delta,\sigma^2I)$,

$$\mathbb P(Y\in A)=\Phi\Big(\Phi^{-1}(\underline{p_A})-\tfrac{\|\delta\|}{\sigma}\Big),\qquad \mathbb P(Y\in B)=\Phi\Big(\Phi^{-1}(\overline{p_B})+\tfrac{\|\delta\|}{\sigma}\Big);$$

the equivalence $\mathbb P(Y\in A)<\mathbb P(Y\in B)\iff\|\delta\|_2>R$; and the existence of the worst-case classifier $f^*$ satisfying (6) with equalities.

Significance

Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about $f$, the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open $\ell_2$ ball of radius $R$. It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.

The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim $A\cap B=\emptyset$ fails at $\underline{p_A}+\overline{p_B}=1$. To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.

Difficulty

Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on $\mathbb R^d$ under a linear functional $z\mapsto\delta^T z$ is the one-dimensional Gaussian with variance $\|\delta\|^2$, and $\Phi$ is a continuous strictly increasing bijection $\mathbb R\to(0,1)$ with $\Phi^{-1}(1-p)=-\Phi^{-1}(p)$. The construction of $f^*$ has a further step the paper leaves informal: the region between $A$ and $B$, of mass $1-\underline{p_A}-\overline{p_B}$, must be shared among "other classes" with none exceeding $\overline{p_B}$, which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $\mathcal N(x,\sigma^2I)$ is the pushforward of Mathlib's stdGaussian under $z\mapsto x+\sigma z$, with $\sigma>0$ a binder. $\Phi$ is cdf (gaussianReal 0 1); $\Phi^{-1}(p)$ is the generalized inverse $\inf\{t:p\le\Phi(t)\}$, which is the true inverse on $(0,1)$ and the junk value $0$ at the endpoints, so every statement that evaluates it assumes $0<p<1$; at $\overline{p_B}=0$ or $\underline{p_A}=1$ the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of $c_A$ to be a strict unique argmax.

A formalization in which the junk endpoint value of $\Phi^{-1}$ makes $R$ negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.

Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on $(0,1)$. Contributions of general Mathlib-style lemmas (the law of $\delta^T X$ for $X\sim\mathcal N(x,\sigma^2I)$, properties of $\Phi^{-1}$) are welcome.

Selected references

• J. M. Cohen, E. Rosenfeld, J. Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML 2019; arXiv:1902.02918v2. https://arxiv.org/abs/1902.02918v2
• M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, S. Jana, Certified Robustness to Adversarial Examples with Differential Privacy, IEEE S&P 2019. https://arxiv.org/abs/1802.03471
• B. Li, C. Chen, W. Wang, L. Carin, Certified Adversarial Robustness with Additive Noise, NeurIPS 2019. https://arxiv.org/abs/1809.03113
• J. Neyman, E. S. Pearson, On the Problem of the Most Efficient Tests of Statistical Hypotheses, Phil. Trans. R. Soc. A 231, 1933. https://doi.org/10.1098/rsta.1933.0009

Motivation

A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size $m$ changes the loss of the output at every point by at most $\beta$, the generalization error exceeds the empirical error by roughly $2\beta + (4m\beta + M)\sqrt{\ln(1/\delta)/(2m)}$ with probability $1-\delta$ (their Theorem 12). The bound is useful only when $\beta = O(1/m)$, and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.

Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate $1/(\lambda m)$. The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.

Setting

Let $\Theta$ be a measurable space with a reference measure $\nu$, and write $d\theta$ for integration against $\nu$. A base class $\mathcal H = \{h_\theta : \theta \in \Theta\}$ is indexed by $\Theta$, and $r(h_\theta, z) \in [0, M]$ is the loss of the base hypothesis $h_\theta$ at an example $z \in Z$.

The algorithm outputs a density $g$ with respect to $\nu$: a measurable, nonnegative, integrable $g : \Theta \to \mathbb R$ with $\int_\Theta g\,d\theta = 1$. $F$ denotes the set of all densities. A density is scored by the averaged loss

$$\ell(g, z) = \int_\Theta r(h_\theta, z)\, g(\theta)\, d\theta \qquad (28),$$

the expected loss of a randomized predictor that draws $h_\theta$ from $g$. The relative entropy of $g$ to $g'$ is

$$K(g, g') = \int_\Theta g(\theta) \ln \frac{g(\theta)}{g'(\theta)}\, d\theta \in [0, \infty],$$

with $K(g, g') = +\infty$ when $g\,\nu$ is not absolutely continuous with respect to $g'\,\nu$ or the integrand is not integrable.

Fix a prior $f_0 \in F$, a parameter $\lambda > 0$, and a training set $S = (z_1, \dots, z_m)$. The algorithm returns a minimizer over $F$ of

$$R_r(g) = \frac1m \sum_{j=1}^m \ell(g, z_j) + \lambda K(g, f_0) \qquad (29).$$

For an index $i$, the truncated objective is $R_r^{\setminus i}(g) = \frac1m \sum_{j \ne i} \ell(g, z_j) + \lambda K(g, f_0)$, and $f^{\setminus i}$ denotes one of its minimizers over $F$.

Formalization targets

Goal: Theorem 24

For every minimizer $f$ of (29), every minimizer $f^{\setminus i}$ of the truncated objective, and every example $z$,

$$|\ell(f, z) - \ell(f^{\setminus i}, z)| \le \frac{M^2}{\lambda m}.$$

Milestones

1. $M$-admissibility of (28) (§5.2.3, p. 518): $|\ell(g,z) - \ell(g',z)| \le M \int_\Theta |g - g'|\,d\theta$.
2. Pinsker's inequality, $L^1$ form (proof of Theorem 24): $\tfrac12 \bigl(\int_\Theta |g - g'|\,d\theta\bigr)^2 \le K(g, g')$ for densities $g, g'$.
3. Lemma 21 (p. 513): for a differentiable convex regularizer $N$ on a vector space and a $\sigma$-admissible loss,

$$d_N(f, f^{\setminus i}) + d_N(f^{\setminus i}, f) \le \frac{1}{\lambda m}\Bigl(\ell(f^{\setminus i}, z_i) - \ell(f, z_i) - d_{\ell(\cdot, z_i)}(f^{\setminus i}, f)\Bigr) \le \frac{\sigma}{\lambda m}|\Delta f(x_i)|.$$

4. Bregman divergence of the relative entropy (proof of Theorem 24): $d_{K(\cdot, f_0)}(g, g') = K(g, g')$.
5. $L^1$ displacement bound (proof of Theorem 24):

$$\int_\Theta |f - f^{\setminus i}|\,d\theta \le \frac{M}{\lambda m}.$$

Significance

Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order $M^2/(\lambda m) + (M^2/\lambda + M)\sqrt{\ln(1/\delta)/m}$. The proof also yields the $L^1$ bound $\int |f - f^{\setminus i}| \le M/(\lambda m)$, which by itself gives classification stability $M/(\lambda m)$ for base hypotheses with values in $\{-1, 1\}$ (remark after Theorem 24, p. 518).

The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in $L^1$ form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.

Difficulty

The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy $K(\cdot, f_0)$ is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity $d_{K(\cdot,f_0)} = K$ needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the $+\infty$ values of $K$. Pinsker's inequality itself requires a separate argument at the level of general measures.

Formalization scope

• Densities are IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral $d\theta$ is always against ν, never Lebesgue measure.
• The base loss is r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).
• $K$ is InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts $K$ to a real number with toReal would send $K = +\infty$ to $0$ and make the worst densities minimizers; that reading is excluded.
• The minimizers are given as hypotheses: f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.
• Corrected reading of the algorithm on $S^{\setminus i}$. The goal is stated in the pairwise form of the paper's proof: $f^{\setminus i}$ minimizes the truncated objective with factor $1/m$, the analogue of (20), not (29) run on the $m-1$ points of $S^{\setminus i}$ with factor $1/(m-1)$.
• Corrected display. The objective displayed before Theorem 24 has $\ell(g, z)$ inside the sum; (29) has $\ell(g, z_i)$, which is used.
• Lemma 21 is stated as printed, in its differentiable case, on a real normed space whose elements act as functions on $X$ through a linear map; the goal does not instantiate it. The Bregman identity is stated with the explicit gradient $\ln(g'/f_0) + 1$, for $f_0, g' > 0$, finite $K(g, f_0)$, $K(g', f_0)$, and integrable $g \ln(g'/f_0)$.

Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Pinsker's inequality). https://doi.org/10.1002/0471200611
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Bregman divergences, Appendix C of the paper). https://doi.org/10.1515/9781400873173