Functional Analysis

Motivation

Many problems in imaging, signal processing and statistics are convex minimizations of the form

$$\min_{x\in\mathcal X}\ F(x)+G(x)+H(Lx),$$

where $F$ is smooth, $G$ and $H$ are nonsmooth but have computable proximity operators, and $L$ is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only $\nabla F$, the proximity operators of $G$ and $H^*$, and applications of $L$ and $L^*$, without ever inverting $L$ or computing the proximity operator of $H\circ L$.

Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.

Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under $\sigma\tau\|L\|^2<1$ (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term $F$, relaxation and errors (Theorem 3.1), and, for $F=0$, proved weak convergence for relaxation parameters up to $2$ (Theorem 3.2), the result of this mission.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and $L:\mathcal X\to\mathcal Y$ a bounded linear operator with adjoint $L^*$ and operator norm $\|L\|$. Write $\Gamma_0(\mathcal H)$ for the proper, lower semicontinuous, convex functions $\mathcal H\to\mathbb R\cup\{+\infty\}$. For $J\in\Gamma_0(\mathcal H)$, the conjugate is $J^*(s)=\sup_{s'}[\langle s,s'\rangle-J(s')]$, the proximity operator is $\mathrm{prox}_J(s)=\arg\min_{s'}[J(s')+\tfrac12\|s-s'\|^2]$, and the subdifferential is $\partial J(u)=\{v:\ J(u)+\langle v,u'-u\rangle\le J(u')\ \forall u'\}$.

Fix $G\in\Gamma_0(\mathcal X)$, $H\in\Gamma_0(\mathcal Y)$ and $F:\mathcal X\to\mathbb R$. The primal–dual inclusion (6) asks for $(\hat x,\hat y)$ with

$$0\in\partial G(\hat x)+L^*\hat y+\nabla F(\hat x),\qquad 0\in-L\hat x+\partial H^*(\hat y);$$

then $\hat x$ minimizes $F+G+H\circ L$ and $\hat y$ solves the dual problem. The paper assumes this inclusion has a solution.

Given $\tau,\sigma>0$, relaxation parameters $(\rho_n)$ and error terms $e_{F,n},e_{G,n}\in\mathcal X$, $e_{H,n}\in\mathcal Y$, Algorithm 3.1 iterates, from any $(x_0,y_0)$,

$$\tilde x_{n+1}=\mathrm{prox}_{\tau G}\big(x_n-\tau(\nabla F(x_n)+e_{F,n})-\tau L^*y_n\big)+e_{G,n},$$ $$\tilde y_{n+1}=\mathrm{prox}_{\sigma H^*}\big(y_n+\sigma L(2\tilde x_{n+1}-x_n)\big)+e_{H,n},$$ $$(x_{n+1},y_{n+1})=\rho_n(\tilde x_{n+1},\tilde y_{n+1})+(1-\rho_n)(x_n,y_n).$$

Algorithm 3.2 exchanges the roles: it computes $\tilde y_{n+1}$ from $y_n+\sigma Lx_n$ first, then $\tilde x_{n+1}$ using $L^*(2\tilde y_{n+1}-y_n)$.

Formalization targets

Goal: Theorem 3.2

Suppose $F=0$ and $e_{F,n}=0$, $\tau,\sigma>0$, and

$$\sigma\tau\|L\|^2<1,\qquad \rho_n\in\,]0,2[,\qquad \sum_n\rho_n(2-\rho_n)=+\infty,\qquad \sum_n\rho_n\|e_{G,n}\|<+\infty,\ \ \sum_n\rho_n\|e_{H,n}\|<+\infty.$$

Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution $(\hat x,\hat y)$ of (6) with $x_n\rightharpoonup\hat x$ and $y_n\rightharpoonup\hat y$ weakly.

Milestones

1. Lemma 4.1 (Krasnosel'skii–Mann): relaxed inexact iterates of a nonexpansive map converge weakly to a fixed point.
2. Lemma 4.2 (proximal point algorithm): for maximally monotone $M$, $s_{n+1}=s_n+\rho_n((I+M)^{-1}s_n+e_n-s_n)$ converges weakly to a zero of $M$ under the same conditions on $\rho_n$, $e_n$ as the goal.
3. $P$ bounded from below: if $\sigma\tau\|L\|^2<1$, the operators $P=\begin{pmatrix}\tau^{-1}I&-L^*\\-L&\sigma^{-1}I\end{pmatrix}$ and $P'$ (with $+L^*$, $+L$) satisfy $\langle z,Pz\rangle\ge c\|z\|^2$.
4. Inclusions (22) and (44): each error-free step satisfies $-(\nabla F(x_n),0)\in A(\tilde z_{n+1})+P(\tilde z_{n+1}-z_n)$ (resp. $P'$), where $A(x,y)=(\partial G(x)+L^*y)\times(-Lx+\partial H^*(y))$; with $F=0$ the left side is $0$.
5. $A$ is maximally monotone on $\mathcal X\times\mathcal Y$.

Further items

Remark 3.2 (the goal with $F$ affine, $\beta=0$, instead of $F=0$) and Theorem 5.2 (the version with $m\ge2$ composite terms $\sum_iH_i(L_ix)$ and condition $\sigma\tau\|\sum_iL_i^*L_i\|<1$).

Significance

The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation $\rho_n\in\,]0,2[$ and summable errors, in arbitrary real Hilbert spaces. Over-relaxation $\rho_n>1$ often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.

Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition $\sum\rho_n(2-\rho_n)=+\infty$ is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.

Difficulty

The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where $\sigma\tau\|L\|^2<1$, strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.

Formalization scope

The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in $\mathbb R\cup\{+\infty\}$ are EReal-valued, with $\Gamma_0$ the published IsProperClosedConvex. The conjugate is an EReal supremum, so $H^*$ can take the value $+\infty$. Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product $\mathcal X\times\mathcal Y$ with the inner product $\langle x,x'\rangle+\langle y,y'\rangle$ is WithLp 2 (X × Y). Weak convergence is $\langle x_n,v\rangle\to\langle\hat x,v\rangle$ for all $v$. "$\sum a_n=+\infty$" means partial sums tend to $+\infty$, and "$\sum\rho_n\|e_n\|<+\infty$" means summability of a nonnegative series.

Standing assumptions are hypotheses: $G,H\in\Gamma_0$, and (6) has a solution. With $F=0$ the smoothness assumption on $F$ is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit $(\hat x,\hat y)$ is chosen after the run.

The condition is strict, $\sigma\tau\|L\|^2<1$, and relaxation is open, $\rho_n\in\,]0,2[$. A goal quantifying over no run, assuming the limit exists, or fixing $(\hat x,\hat y)$ before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.

Selected references

• L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158(2):460–479, 2013. https://doi.org/10.1007/s10957-012-0245-9 (author's version: https://hal.science/hal-00609728)
• A. Chambolle, T. Pock, A first-order primal-dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40:120–145, 2011. https://doi.org/10.1007/s10851-010-0251-1
• B. He, X. Yuan, Convergence analysis of primal-dual algorithms for a saddle-point problem: from contraction perspective, SIAM J. Imaging Sci. 5(1):119–149, 2012. https://doi.org/10.1137/100814494
• B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38:667–681, 2013. https://doi.org/10.1007/s10444-011-9254-8
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
• P. L. Combettes, Solving monotone inclusions via compositions of nonexpansive averaged operators, Optimization 53:475–504, 2004. https://doi.org/10.1080/02331930412331327157

Motivation

Many problems in imaging, signal processing and statistics take the form

$$\min_{x\in\mathcal X}\ F(x)+G(x)+H(Lx),$$

where $G$ and $H$ are convex functions whose proximity operators can be computed cheaply, $L$ is a linear operator such as a finite-difference gradient, and $F$ is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because $H\circ L$ is generally not proximable even when $H$ is, practical methods split the problem so that each step uses only $\mathrm{prox}_{\tau G}$, $\mathrm{prox}_{\sigma H^*}$, $L$ and $L^*$, without inverting any operator.

L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With $F=0$ the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming $\tau\sigma\|L\|^2<1$, $\rho_n\equiv1$ and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation $\rho_n\equiv\rho\in\,]0,2[$ under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with $F=0$, the iterates converge under the step-size condition $\sigma\tau\|L\|^2\le1$, equality included. Equality matters in practice: one can set $\sigma=1/(\tau\|L\|^2)$ and tune a single parameter, as in the Douglas–Rachford method.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and $L:\mathcal X\to\mathcal Y$ a bounded linear operator with adjoint $L^*$ and operator norm $\|L\|$. Write $\Gamma_0(\mathcal H)$ for the proper, lower semicontinuous, convex functions $\mathcal H\to\mathbb R\cup\{+\infty\}$, and let $G\in\Gamma_0(\mathcal X)$, $H\in\Gamma_0(\mathcal Y)$. The Fenchel conjugate is $H^*(s)=\sup_{s'}[\langle s,s'\rangle-H(s')]$, the proximity operator is $\mathrm{prox}_J(s)=\operatorname{argmin}_{s'}[J(s')+\tfrac12\|s-s'\|^2]$, and the subdifferential is $\partial J(u)=\{v:\ \langle u'-u,v\rangle+J(u)\le J(u')\ \forall u'\}$.

The primal–dual inclusion (6) asks for $(\hat x,\hat y)\in\mathcal X\times\mathcal Y$ with

$$0\in\partial G(\hat x)+L^*\hat y+\nabla F(\hat x),\qquad 0\in-L\hat x+\partial H^*(\hat y).$$

A solution gives a minimiser $\hat x$ of the primal problem and a solution $\hat y$ of its dual.

Algorithm 3.1 chooses $\tau>0$, $\sigma>0$, relaxation parameters $(\rho_n)$, error terms $(e_{F,n}),(e_{G,n}),(e_{H,n})$ and an initial estimate $(x_0,y_0)$, then iterates

$$\tilde x_{n+1}=\mathrm{prox}_{\tau G}\big(x_n-\tau(\nabla F(x_n)+e_{F,n})-\tau L^*y_n\big)+e_{G,n},\qquad \tilde y_{n+1}=\mathrm{prox}_{\sigma H^*}\big(y_n+\sigma L(2\tilde x_{n+1}-x_n)\big)+e_{H,n},$$ $$(x_{n+1},y_{n+1})=\rho_n(\tilde x_{n+1},\tilde y_{n+1})+(1-\rho_n)(x_n,y_n).$$

Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses $2\tilde y_{n+1}-y_n$. Section 5 extends both to $\sum_{i=1}^mH_i(L_ix)$ (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).

Formalization targets

Goal: Theorem 3.3 (p. 6)

Let $\mathcal X$, $\mathcal Y$ be finite-dimensional, $F=0$, $e_{F,n}=0$, and assume (6) has a solution. If

$$\text{(i)}\ \sigma\tau\|L\|^2\le1,\qquad \text{(ii)}\ \rho_n\in[\varepsilon,2-\varepsilon]\ \ \forall n,\ \text{for some }\varepsilon>0,\qquad \text{(iii)}\ \textstyle\sum_n\|e_{G,n}\|<\infty,\ \sum_n\|e_{H,n}\|<\infty,$$

then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, $(x_n,y_n)$ converges to a solution $(\hat x,\hat y)$ of (6).

Milestones (from the proof, pp. 8–13)

With $P(x,y)=(\tfrac1\tau x-L^*y,\,-Lx+\tfrac1\sigma y)$ the operator (20) and $T(x,y)=(\tilde x,\tilde y)$ the error-free step of Algorithm 3.1:

• $P$ (and $P'$ of (44)) is positive under (i): $\langle z,Pz\rangle\ge0$;
• $T$ depends on $z$ only through $Pz$ (the paper's $T\circ S=T$, (32)–(33));
• on solutions of (6), $PT(z)=Pz$ ((41)–(42));
• $PT(z)=Pz$ implies that $T(z)$ solves (6) (via (35));
• $T$ is continuous;
• Lemma 4.1 (Krasnosel'skii–Mann iteration) and Lemma 4.6 (Polyak's lemma).

Further statements

Remark 3.2 (Theorem 3.3 with $F$ affine, i.e. $\beta=0$ in (2)) and Theorem 5.3 (the analogue for $m\ge2$ composite terms, with (i) replaced by $\sigma\tau\|\sum_iL_i^*L_i\|\le1$) are included as draft theorems.

Significance

Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size $\sigma\tau\|L\|^2=1$. It covers relaxation parameters up to $2-\varepsilon$ and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.

None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.

Difficulty

The usual proof treats the iteration as a proximal-point or forward–backward step in the space $\mathcal X\times\mathcal Y$ with the inner product $\langle z,Pz'\rangle$. That argument needs $P$ strictly positive, which is exactly what fails when $\sigma\tau\|L\|^2=1$: then $P$ has a nontrivial kernel, $\langle z,Pz\rangle$ is only a seminorm, and weak convergence in the $P$-geometry says nothing about the components of $z$ in $\ker P$. The proof replaces the iteration by its "shadow" $Sz_n$ on $\operatorname{ran}P$, uses that $T$ factors through $S$, and recovers the full iterates through continuity of $T$ and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.

Formalization scope

Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in $\Gamma_0$ take values in EReal and satisfy the published predicate IsProperClosedConvex (never $-\infty$, finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps $P_G$, $P_H$ satisfying the published minimisation predicate IsProx for $\tau G$ and $\sigma H^*$; such maps exist and are unique for $\Gamma_0$ functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. "$=+\infty$" for a series is divergence of its partial sums, "$<+\infty$" is summability of a nonnegative series, and convergence in the goal is norm convergence.

The standing assumptions of pp. 3–4 are hypotheses: $G,H\in\Gamma_0$, and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators $P$ and $T$ are plain maps on $\mathcal X\times\mathcal Y$. The projector $S$ is not built: "$T\circ S=T$" is stated as "$Pz=Pz'\Rightarrow T(z)=T(z')$", which is equivalent because $P$ is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.

The strict inequality $\sigma\tau\|L\|^2<1$ would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps $\le$. Weak convergence in place of norm convergence, an $\varepsilon$ chosen after $n$, or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.

Useful infrastructure includes: firm nonexpansiveness of $\mathrm{prox}$ for EReal-valued $\Gamma_0$ functions; $\Gamma_0$-ness of the conjugate and Moreau's identity; maximal monotonicity of $\partial G\times\partial H^*$ plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.

Selected references

• L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158(2):460–479, 2013. https://doi.org/10.1007/s10957-012-0245-9 (author's version: https://hal.science/hal-00609728v5)
• B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38:667–681, 2013. https://doi.org/10.1007/s10444-011-9254-8
• A. Chambolle, T. Pock, A first-order primal–dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40:120–145, 2011. https://doi.org/10.1007/s10851-010-0251-1
• P. L. Combettes, Solving monotone inclusions via compositions of nonexpansive averaged operators, Optimization 53:475–504, 2004. https://doi.org/10.1080/02331930412331327157
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
• B. T. Polyak, Introduction to Optimization, Optimization Software, New York, 1987.

Motivation

Many convex optimization models combine a smooth loss, a nonsmooth penalty whose proximity operator is easy to compute, and a second penalty applied after a linear map. Imaging models, for example, often place a data-fitting term on the image and a regularizer on its transformed coefficients. The resulting objective has the form $F(x)+G(x)+H(Lx)$. Condat's primal–dual method evaluates the smooth gradient and two proximity operators separately, without requiring a proximity operator for the composite $H\circ L$. Condat, 2013 establishes weak convergence with relaxation and summably weighted computational errors. This mission targets its main positive-smoothness theorem, Theorem 3.1, in the final author's version.

The theorem matters when a computed gradient or proximal point is inexact, as is common when a proximal subproblem is itself solved numerically. Its conditions account for these errors directly rather than treating the displayed algorithm as exact. It also gives one parameter regime for two orders of updating the primal and dual variables. These two algorithms share an objective and a solution inclusion, but have distinct recursions.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and let $L:\mathcal X\to\mathcal Y$ be bounded linear, with adjoint $L^*$. The smooth term $F:\mathcal X\to\mathbb R$ is convex and differentiable. Its gradient is $\beta$-Lipschitz when $\|\nabla F(x)-\nabla F(x')\|\le\beta\|x-x'\|$ for all $x,x'$. The nonsmooth terms $G$ and $H$ are proper, lower semicontinuous, convex functions with values in $\mathbb R\cup\{+\infty\}$. Such functions form the class $\Gamma_0$. An infinite value may encode a constraint.

For a convex function $J$, its proximity operator $\operatorname{prox}_{\gamma J}(s)$ minimizes $J(u)+\|u-s\|^2/(2\gamma)$ over $u$, where $\gamma>0$. The Fenchel conjugate is $J^*(v)=\sup_u\{\langle v,u\rangle-J(u)\}$. A subgradient $v\in\partial J(u)$ obeys $J(u)+\langle v,u'-u\rangle\le J(u')$ for every $u'$. The sought primal–dual solution $(\hat x,\hat y)$ satisfies

$$-L^*\hat y-\nabla F(\hat x)\in\partial G(\hat x),\qquad L\hat x\in\partial H^*(\hat y).$$

Algorithms 3.1 and 3.2 maintain sequences $x_n\in\mathcal X$ and $y_n\in\mathcal Y$. Algorithm 3.1 updates the primal proximity step before the dual one; Algorithm 3.2 reverses that order. Each uses positive step sizes $\tau,\sigma$, positive relaxation weights $\rho_n$, and errors $e_{F,n}$, $e_{G,n}$ and $e_{H,n}$ in the gradient and the two proximal evaluations. Their full recursions are part of the Lean setting, so a run is determined by its initial pair. The paper specifies the problem in §2 and both algorithms in §3.

Formalization targets

The goal is Theorem 3.1 on p. 5. Suppose $\beta>0$, the primal–dual solution set is nonempty, and $G,H\in\Gamma_0$. Set

$$\delta=2-\frac{\beta}{2}\left(\frac1\tau-\sigma\|L\|^2\right)^{-1}.$$

For $\tau,\sigma>0$, the theorem assumes

$$\frac1\tau-\sigma\|L\|^2\ge\frac\beta2,\qquad 0<\rho_n<\delta\quad\text{for every }n,$$ $$\sum_{n\ge0}\rho_n(\delta-\rho_n)=+\infty,\qquad\sum_{n\ge0}\rho_n\|e_{F,n}\|<\infty,\quad\sum_{n\ge0}\rho_n\|e_{G,n}\|<\infty,\quad\sum_{n\ge0}\rho_n\|e_{H,n}\|<\infty.$$

Under these conditions, both sequences of each algorithm converge weakly to the components of a primal–dual solution. The solution may depend on the initial pair and on the run. The milestone list includes Lemmas 4.1 and 4.3–4.5, the strict positivity claim for the block operator $P$, estimate (29), and the error-free optimality inclusions (22) and (44), ordered as preliminary results followed by the two algorithm-specific claims. These targets match the results stated in §4 of the source version.

Significance

The result supplies a convergence guarantee for a composite objective under an explicit coupling condition on $\tau$, $\sigma$, and $\|L\|$. It permits relaxation weights that vary with $n$ and errors that are summable only after weighting by those same relaxation values. The dual conclusion is substantive: convergence of the primal sequence alone would not give convergence of the dual certificate produced by the algorithm. The weak topology is appropriate in general Hilbert spaces; norm convergence would assert more than the paper proves.

The theorem is proved in the 2013 paper. The present formalization task is to give its statement and the selected operator lemmas machine-checked proofs in Lean. Related platform definitions for proximal maps, monotone operators, nonexpansive maps, subgradients and weak convergence already exist; the paper-specific convergence theorem and its selected milestones are new targets in this proposal. The resulting definitions and abstract Lemmas 4.1, 4.3–4.5 can be reused in later operator-splitting developments.

Difficulty

The displayed recursions involve three errors, two proximal evaluations, a linear map and its adjoint, and two different update orders. A direct estimate on $\|x_{n+1}-\hat x\|$ does not by itself control the coupled dual variable, while a bound on only the combined objective value would not establish weak convergence of either iterate. The relaxation condition permits weights without a fixed positive lower bound, so a convergence argument cannot replace the stated divergent series by a simpler constant-step assumption. The abstract lemmas must also retain the endpoints $\alpha_2=1$ and $\gamma=2\kappa$ present in the source.

Formalization scope

Lean uses complete real inner-product spaces for $\mathcal X$ and $\mathcal Y$, a continuous linear map for $L$, and EReal for $G$, $H$ and their conjugates. The conjugate supremum is taken in EReal. The paper's $\Gamma_0$ class and proximity maps use published definitions; the latter are parameters constrained to be the actual proximal minimizers. Positive step sizes and proper closed convex data ensure such maps exist and are unique. The subgradient predicate explicitly requires a finite value at the base point; this follows from the source's properness assumptions when a subgradient exists.

Both algorithms are represented by recursion predicates on every natural-number index, with all error terms present. The goal quantifies over every run and chooses its weak limit afterwards. Divergence to $+\infty$ means finite partial sums tend to atTop; a finite weighted error sum means the corresponding nonnegative real sequence is summable. These choices prevent a default value of an infinite sum from satisfying the hypotheses. The nonempty solution set is an explicit standing assumption from p. 4 and implies the earlier nonempty-primal-minimizer assumption. A condition that made all runs impossible, or one that discarded either the primal or dual conclusion, would not represent Theorem 3.1.

The block operator $P$ is represented through its quadratic form $q_P$; $P'$ is recorded for Algorithm 3.2. The complete development will need the abstract iteration lemmas, proximal optimality conditions, block-metric estimates, and the links from each algorithm's inclusion to the solution set. Contributions proving those results, or building reusable Hilbert-space operator infrastructure needed by them, are in scope. The several-composite-functions extension in Theorem 5.1 is reserved for separate work.

Selected references

• Laurent Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, Journal of Optimization Theory and Applications 158(2):460–479, 2013. DOI; final author's version, hal-00609728v5.

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