All missions

Motivation

Smooth optimization with nonnegative variables appears when the variables are Lagrange multipliers for inequality constraints or when an objective incorporates an augmented Lagrangian or an exact penalty. Bertsekas studies how to retain a Newton-like convergence rate in this setting while using an iteration that projects a scaled gradient step onto the nonnegative orthant. His 1982 paper also discusses large optimal-control examples, where repeatedly solving a quadratic subproblem may be costly. These are the applications motivating the method, rather than assumptions of the theorem. Bertsekas, 1982.

The paper contrasts a partly diagonal scaling matrix with two other approaches: a fully diagonal projected gradient step, which generally has a linear rate, and a constrained Newton step defined by a quadratic program. The main theoretical question is whether the simpler projected iteration can still identify binding coordinates and converge superlinearly near the solution. The mission covers the nonnegative-orthant method in §2 and its stated convergence results. The paper's later extension to general linear constraints and its computational examples concern different objects. Bertsekas, 1982.

Setting

Fix a dimension $n\ge1$ and a continuously differentiable function $f:\mathbb R^n\to\mathbb R$. Problem (1) minimizes $f(x)$ over the nonnegative orthant $\mathbb R_+^n=\{x:x^i\ge0\text{ for every }i\}$. The positive part $[z]^+$ replaces each negative coordinate of $z$ by zero. A feasible $x$ is critical when every partial derivative $\partial_i f(x)$ is nonnegative and $\partial_i f(x)=0$ wherever $x^i>0$. This is the paper's componentwise first-order condition.

For a feasible iterate $x_k$, the binding set is $B(x_k)=\{i:x_k^i=0\}$. The paper selects a larger working set $I_k^+$ using a fixed $\varepsilon>0$ and the projected-gradient residual $w_k=\|x_k-[x_k-M\nabla f(x_k)]^+\|$, where $M$ is fixed, diagonal and positive definite. More precisely, $I_k^+$ contains the indices with $0\le x_k^i\le\min(\varepsilon,w_k)$ and $\partial_i f(x_k)>0$. The matrix $D_k$ is symmetric positive definite and has zero off-diagonal entries in the rows indexed by $I_k^+$. The projected arc and update are

$$p_k=D_k\nabla f(x_k),\qquad x_k(a)=[x_k-a p_k]^+,\qquad x_{k+1}=x_k(\beta^{m_k}).$$

Here $0<\beta<1$, and $m_k$ is the first nonnegative integer passing the paper's two-sum Armijo test (37), with $0<\sigma<1/2$. One sum uses the scaled gradient outside $I_k^+$; the other uses the actual projected displacement on $I_k^+$. These details define the algorithm whose rate is at issue. Bertsekas, 1982, pp. 228–229.

Formalization targets

The first targets establish the fixed-point and descent properties of the projected arc, positivity of the Armijo right-hand side, well-defined step selection, criticality of limit points, and local attraction with finite binding-set identification. Proposition 3 identifies both the working set and the actual binding set:

$$I_k^+=B(x_k)=B(x^*)\quad\text{for all sufficiently late }k.$$

The goal is Proposition 4. Let $f$ be convex and $C^2$, let $x^*$ be the unique minimizer on $\mathbb R_+^n$ satisfying Assumption (C), and suppose the Hessian quadratic form has uniform positive lower and finite upper bounds on the initial, unrestricted sublevel set. The scaling matrix is $D_k=H_k^{-1}$, where $H_k$ retains Hessian entries except for off-diagonal entries touching $I_k^+$. Then

$$x_k\longrightarrow x^*,\qquad \forall c>0\ \exists K\ \forall k\ge K:\ \|x_{k+1}-x^*\|\le c\|x_k-x^*\|.$$

If the Hessian is Lipschitz in a neighborhood of $x^*$, the same proposition states an at-least-quadratic error bound: $\|x_{k+1}-x^*\|\le C\|x_k-x^*\|^2$ eventually for some $C>0$. The separate final milestone records the paper's claim that the initial unit trial is eventually accepted. Bertsekas, 1982, pp. 233–236.

Significance

Proposition 4 says that this specific orthant-projected Newton iteration converges to the unique constrained optimum with a superlinear rate under its stated smoothness and curvature conditions. Proposition 3 supplies a distinct finite-identification statement: the working and binding coordinates eventually match those at the optimum. These facts specify the behavior of an algorithm that does not define its direction by solving a quadratic program at every step. The paper proves the preceding propositions and states Proposition 4 with its proof left to the reader, referring to its earlier discussion and standard unconstrained Newton results. Bertsekas, 1982, pp. 234–236.

Formalizing the claims would provide machine-checked statements and, once solved, proofs for the exact projected arc, two-part line search, matrix selection, identification result and rate conclusion. The local mission items are open proof obligations; their compilation checks the definitions and theorem types, not the mathematical claims. The geometry definitions can also support other orthant-constrained algorithms, while the enlarged working set and Armijo rule belong to this paper's method.

Difficulty

A positive definite matrix by itself does not make projection along $[x-aD\nabla f(x)]^+$ a descent move. An off-diagonal coupling can push coordinates against the boundary in a way that defeats the usual unconstrained descent calculation; the paper gives such a situation before Proposition 1. The partly diagonal condition is therefore substantive. A second obstacle is that the exact active set $I^+(x)$ can jump at a boundary point: iterates approaching that point from the interior need not have the same indexed rows. The enlarged $I_k^+$ and its dependence on the residual are central to the finite-identification and rate claims. Bertsekas, 1982, pp. 225–229.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with the Euclidean norm and zero-based coordinates. The dimension is positive. gradient and the derivative of gradient represent first and second derivatives; the paper's $M$ is diag μ with every $\mu^i>0$. The run predicate includes a feasible initial point and the first acceptable integer $m_k$, and the matrix choices are indexed by iteration. Propositions 1–3 use the paper's explicit admissibility condition. Proposition 4 constructs $D_k$ from $H_k$ and does not assume its invertibility, admissibility, convergence or eventual active-set equality.

Assumption (C) includes local $C^2$ smoothness, curvature bounds on directions zero at the binding coordinates, and strict complementarity. A local minimum is required to be feasible as well as locally minimal on the orthant. Limit points use subsequential convergence. Superlinearity uses a uniform eventual error inequality, which also covers an iterate that reaches the solution exactly; a ratio with a zero denominator would distort this case. The paper's Proposition 4 display mistakenly binds a direction to the level set while leaving the Hessian's point free. The formalization states the intended reading: every point in the unrestricted initial level set and every direction satisfy the Hessian bounds. The displayed level set has no $x\ge0$ restriction, so neither does the Lean hypothesis.

A definition that accepts any Armijo exponent or a goal that assumes the eventual identification or convergence conclusion would erase the paper's claim. Contributions can build the matrix and projected-arc lemmas, the convergence and identification proofs, and the final rate proof. The local inverse-Hessian observation before Proposition 4 is discussed in the notes but has no separate milestone until its full local setting can be captured without weakening it.

Selected references

• Dimitri P. Bertsekas, Projected Newton Methods for Optimization Problems with Simple Constraints, SIAM Journal on Control and Optimization 20(2), 221–246, 1982. DOI: 10.1137/0320018.

Motivation

A global surface of section reduces a flow on a closed 3-manifold to an area-preserving map of a surface. It is a compact embedded surface whose boundary consists of periodic orbits, whose interior is transverse to the flow, and which every other trajectory hits infinitely often in forward and backward time. Poincaré introduced the idea for the restricted three-body problem. Once a section is a disk, results on area-preserving disk maps (Brouwer, Franks) give periodic orbits and other structure for the whole flow.

For Hamiltonian flows on star-shaped energy surfaces in $\mathbb{R}^4$, equivalently Reeb flows on the tight 3-sphere, it is natural to ask which periodic orbits bound such a disk. Hryniewicz's criterion answers this for dynamically convex flows, with no genericity assumption. The answer is purely topological: a periodic orbit bounds a disk-like global section exactly when it is unknotted with self-linking number $-1$. The criterion is used in celestial mechanics: Joung and van Koert apply it to validated periodic orbits of the restricted three-body problem (arXiv:2407.19159).

Timeline.

• 1998. Hofer, Wysocki and Zehnder prove that every dynamically convex contact form on $S^3$ has some periodic orbit $P_0$, with Conley–Zehnder index $3$, that bounds a disk-like global section. That disk is a page of an open book adapted to the flow. Strictly convex energy surfaces in $\mathbb{R}^4$ are dynamically convex (Ann. of Math. 148).
• 2008/2012. Hryniewicz proves the "unknotted, self-linking $-1$" characterization in the non-degenerate case (arXiv:0812.4076).
• 2010/2011. Hryniewicz and Salomão treat non-degenerate tight contact forms on $S^3$. Two extra conditions appear there: $\mu_{CZ}\ge 3$, and linking with every orbit of index $2$ (arXiv:1006.0049).
• 2011/2014. Hryniewicz removes non-degeneracy for dynamically convex forms (arXiv:1105.2077, Theorem 1.7). In the same paper, Theorem 1.8 shows that any orbit coming from a fixed point of the first-return map of a disk-like section is again such a binding.
• 2012. Albers, Fish, Frauenfelder, Hofer and van Koert use this circle of ideas to get disk-like sections in the planar circular restricted three-body problem (arXiv:1103.3881).

Setting

Use coordinates $x=(q_1,p_1,q_2,p_2)$ on $\mathbb{R}^4$, the Liouville form $\lambda_0=\tfrac12\sum_j (q_j\,dp_j-p_j\,dq_j)$ and the symplectic form $\omega_0=d\lambda_0=\sum_j dq_j\wedge dp_j$.

Let $H:\mathbb{R}^4\to\mathbb{R}$ be smooth and set $S=H^{-1}(1)$. Assume that every ray from the origin meets $S$ exactly once, and that it crosses $S$ transversally:

$$dH(x)\,x>0\qquad(x\in S).$$

Then $S$ is a strictly star-shaped hypersurface diffeomorphic to $S^3$. Every contact form on $S^3$ that matters below arises this way, up to diffeomorphism (see Formalization scope).

The Hamiltonian vector field $X_H$ is defined by $\iota_{X_H}\omega_0=-dH$. With this sign, $\lambda_0(X_H)=\tfrac12\,dH(x)\,x>0$ on $S$. So $X_H|_S$ is a positive multiple of the Reeb vector field of the contact form $\lambda_0|_S$, and its orbits are the Reeb orbits reparametrized. A periodic orbit $P=(x,T)$ is a solution with $x(T)=x(0)$ and $T>0$. It is prime when $T$ is its least positive period. The contact structure is $\xi=\ker\lambda_0|_S$.

• Conley–Zehnder index. Fix the global frame of $\xi$ given by the quaternionic rotations of $\nabla H$. Along $P$, the linearized flow restricted to $\xi$ is a path $\varphi:[0,1]\to Sp(1)$ with $\varphi(0)=I$. The winding interval $I(\varphi)$ collects the total rotations of all nonzero vectors, measured in turns. Then $\mu_{CZ}(P)$ is the lower semicontinuous index of Hryniewicz's §2.1.1. In particular,

$$\mu_{CZ}(P)\ge 3 \iff \min I(\varphi)>1,$$

that is, every nonzero transverse vector turns by more than one full turn.

• Dynamical convexity. The flow is dynamically convex if $\mu_{CZ}(P)\ge 3$ for every periodic orbit $P$ in $S$, prime or multiply covered.
• Disk-like global surface of section. A smoothly embedded closed disk $D\subset S$ such that $\partial D=x(\mathbb{R})$ for a periodic orbit $P$, $X_H$ is transverse to $D\setminus\partial D$, and every trajectory not contained in $\partial D$ meets $D$ at arbitrarily large positive and negative times. Then $P$ bounds $D$.
• Unknotted. $P$ is unknotted if $x(\mathbb{R})$ is the boundary of some smoothly embedded closed disk in $S$.
• Self-linking number. Push $x$ off itself along the global frame of $\xi$ to a disjoint loop $x'$. Then

$$\operatorname{sl}(P)=\operatorname{lk}(x,x')\in\mathbb{Z},$$

the linking number in $S\cong S^3$, with $S$ oriented as the boundary of the star-shaped domain it bounds. This agrees with Hryniewicz's Definition 1.5, which uses a section of $\xi$ over a spanning disk.

Formalization targets

Goal: Hryniewicz's criterion (Theorem 1.7, first sentence)

For every dynamically convex strictly star-shaped $S$ and every prime periodic orbit $\bar P$:

$$\bar P \text{ bounds a disk-like global surface of section} \iff \bar P \text{ is unknotted and } \operatorname{sl}(\bar P)=-1.$$

The statement fixes no constants and no non-degeneracy, and it covers every dynamically convex star-shaped surface.

Stronger: adapted open book (Theorem 1.7, second sentence)

If $\bar P$ is unknotted with $\operatorname{sl}(\bar P)=-1$, then $S\setminus \bar x(\mathbb{R})$ fibres smoothly over $\mathbb{R}/\mathbb{Z}$. Every fibre is the interior of a disk-like global surface of section whose oriented boundary is $\bar P$.

Further: new bindings from fixed points (Theorem 1.8)

Let $D_0$ be any disk-like global section. Every periodic orbit through a fixed point of the first-return map of $D_0\setminus\partial D_0$ is unknotted, has self-linking number $-1$, and so bounds the page of an adapted open book.

Significance

The result. The criterion turns a dynamical question into a topological check. It does not depend on whether the orbit is degenerate, and degenerate orbits are what one meets at bifurcations and on symmetric levels. Every periodic orbit in a strictly convex energy surface that is unknotted with $\operatorname{sl}=-1$ is a binding, so the flow is organised by many open books at once. Theorem 1.8 makes this concrete: the Hamiltonian flow twists around two different bindings, $\partial D_0$ and $\partial D_1$. In applications, numerically validated orbits become analytic global sections without a separate non-degeneracy check (Joung–van Koert, Theorems 1.2 and 1.5).

Formalizing it. The theorem is proved, in a 50-page paper that relies on Hofer–Wysocki–Zehnder's theory of pseudo-holomorphic curves in symplectizations. It has no machine-checked proof. Mathlib has no Conley–Zehnder index, no self-linking number, no linking number of curves in $S^3$, and no global surfaces of section. A Lean statement fixes every sign and orientation convention involved: the sign of $X_H$, the orientation of $S$, which push-off defines $\operatorname{sl}$, and the index of degenerate orbits. Each of these is easy to get wrong in prose. Formal proofs of the parts that use no holomorphic curves are valuable on their own: the necessity direction, the description of the index by winding intervals, and the explicit ellipsoid examples.

Difficulty

The obvious route is to approximate the contact form by non-degenerate forms $\lambda_k\to\lambda$ that keep $\bar P$ as an orbit, and then apply the non-degenerate theorems. This fails. The $\lambda_k$ need not be dynamically convex. They can have orbits of very high action with $\mu_{CZ}=2$ that are not linked with $\bar P$, so the Hryniewicz–Salomão criterion does not apply to $\lambda_k$ (Hryniewicz, p. 4). The families of planes that would give the pages for $\lambda_k$ have to be controlled directly as $k\to\infty$, and this is not a formal limit argument.

A second obstruction is genuinely global. A disk spanning $\bar P$ and transverse to the flow in its interior is easy to produce when $\operatorname{sl}(\bar P)=-1$. Showing that every trajectory returns to it is the whole content of the theorem, and no local or perturbative argument gives it.

For the formalization, nothing in the proof of sufficiency avoids finite-energy pseudo-holomorphic planes: Fredholm theory, asymptotic analysis, bubbling-off and compactness all enter. None of this exists in Lean.

Formalization scope

• Ambient space. $\mathbb{R}^4$ is Fin 4 → ℝ with coordinates ordered $(q_1,p_1,q_2,p_2)$. $\lambda_0$, $\omega_0$ and $X_H$ are defined explicitly, with the sign conventions above.
• Energy surfaces. Star-shaped surfaces are smooth (ContDiff ℝ ⊤) functions $H$ with the ray condition and $dH(x)x>0$ on $H^{-1}(1)$. The Reeb flow of a general dynamically convex form on $S^3$ reduces to this case, up to diffeomorphism and positive time change: such a form is tight (Hofer–Wysocki–Zehnder), and every tight form on $S^3$ comes from a star-shaped hypersurface (Eliashberg 1992). That reduction is not part of the targets. Hryniewicz makes the same reduction (§3, first paragraph).
• Flow. The flow is the flow of $X_H$, not of the Reeb field. All notions in the targets are invariant under positive time change. Periodic orbits are solutions of $\dot x=X_H(x)$ on all of $\mathbb{R}$. "Prime" means the recorded period is least.
• Index. $\mu_{CZ}\ge 3$ is encoded by the winding-interval condition in the global quaternionic frame, with degenerate orbits included. Multiply covered orbits are included in dynamical convexity.
• Disks. Disks are smooth embeddings of the closed unit disk (injective, with injective differential up to the boundary). The return condition demands hits at arbitrarily large positive and negative times.
• Ruling out vacuous encodings. A version without the two-sided return condition, with a dynamical-convexity predicate that no surface satisfies, or with $\operatorname{sl}$ that is not a linking number of the push-off, proves a different theorem. The ellipsoid milestone below is a non-vacuity check on the definitions.
• Infrastructure. A complete development needs the following.
  • Reusable beyond this mission: the Conley–Zehnder index of paths in $Sp(1)$, the linking number of disjoint loops in $S^3$ (or in $\mathbb{R}^3$ after stereographic projection), and global flows of vector fields on compact level sets.
  • Specific to this proof: contact topology of spanning disks (characteristic foliations, elimination of singularities), and finite-energy planes in $\mathbb{R}\times S^3$ with their Fredholm, asymptotic and compactness theory.
• Contributions welcome. The definition layer, the index and linking-number libraries, the ellipsoid examples, Lemma 2.1, the necessity direction, Lemma 3.12, and any sub-step of the holomorphic-curve argument stated as an independent lemma.

Selected references

• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289. https://doi.org/10.2307/120994
• U. L. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931. https://arxiv.org/abs/0812.4076
• U. L. Hryniewicz, P. A. S. Salomão, On the existence of disk-like global sections for Reeb flows on the tight 3-sphere, Duke Math. J. 160 (2011), 415–465. https://arxiv.org/abs/1006.0049
• U. L. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), 791–862. https://arxiv.org/abs/1105.2077
• U. L. Hryniewicz, P. A. S. Salomão, Global surfaces of section for Reeb flows in dimension three and beyond, Proc. ICM 2018 (extended version). https://arxiv.org/abs/1712.01925
• P. Albers, J. W. Fish, U. Frauenfelder, H. Hofer, O. van Koert, Global surfaces of section in the planar restricted 3-body problem, Arch. Ration. Mech. Anal. 204 (2012), 273–284. https://arxiv.org/abs/1103.3881
• C. Joung, O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. https://arxiv.org/abs/2407.19159
• Y. Eliashberg, Contact 3-manifolds twenty years since J. Martinet's work, Ann. Inst. Fourier 42 (1992), 165–192. https://doi.org/10.5802/aif.1288

Motivation

Whether the diameter of a polyhedron is bounded by a polynomial in its number of facets is one of the central open questions of convex geometry, and it bears directly on linear programming: the diameter of the graph of a polyhedron is a lower bound on the number of pivots of any simplex method that moves along edges. Write $\triangle_u(d,n)$ for the largest diameter of a $d$-dimensional polyhedron with $n$ facets. The best known bounds are

$$n - d + \lfloor d/5 \rfloor \;\le\; \triangle_u(d,n) \;\le\; n^{1+\log d},$$

due to Klee and Walkup (1967) and Kalai and Kleitman (1992), and the gap between them has stood for decades.

A recurring approach is to isolate a few purely combinatorial properties of polyhedra and to prove bounds for every object having them. Eisenbrand, Hähnle, Razborov and Rothvoß (2010) proposed a base abstraction defined by a single property, shared by all abstractions from which earlier bounds were derived. They showed that the known upper bounds survive in it, and, as their main result, that it admits almost-quadratic diameter. This mission formalizes that lower bound.

Timeline.

• 1967: Klee and Walkup, lower bound $n-d+\lfloor d/5\rfloor$ for unbounded polyhedra.
• 1970: Larman, $\triangle_u(d,n) \le 2^{d-1} n$ (linear in fixed dimension).
• 1974: Adler, Dantzig and Murty study abstract polytopes and their diameters.
• 1992: Kalai and Kleitman, the quasi-polynomial bound $n^{1+\log d}$.
• 2010: Eisenbrand, Hähnle, Razborov and Rothvoß, the base abstraction; both upper bounds hold in it, and its diameter is $\Omega(n^2/\log n)$ in dimension $n/4$.
• 2012: Santos disproves the Hirsch conjecture for polytopes; the polynomial question remains open.

Setting

Let $[n] = \{1,\dots,n\}$ and let $\binom{[n]}{d}$ be the family of its $d$-element subsets. Consider a graph $G$ whose vertex set $V$ is a nonempty subfamily of $\binom{[n]}{d}$. The graph satisfies condition i) if

for each $u, v \in V$ there exists a path connecting $u$ and $v$ whose intermediate vertices all contain $u \cap v$.

The base abstraction $\mathcal B_{d,n}$ is the class of all such graphs; $d$ is called the dimension and $n$ the number of facets. Write $\mathrm{dist}_G(u,v)$ for the length of a shortest $u$–$v$ path, and

$$D(d,n) = \max\{\mathrm{dist}_G(u,v) : G \in \mathcal B_{d,n},\ u, v \in V(G)\}.$$

The geometry behind the definition: in a non-degenerate polyhedron every vertex lies on exactly $d$ facets, so labelling vertices by their facets gives distinct $d$-subsets of $[n]$; and two vertices can be joined without leaving the smallest face containing both, i.e. through vertices lying on every facet common to $u$ and $v$. Hence $\triangle_u(d,n) \le D(d,n)$ (the subject of a separate mission of this series).

In the Lean development, EHRR10.LowerBound.CondI V G is condition i), and EHRR10.LowerBound.InB d n V G says that $V$ is nonempty, all its members have $d$ elements, and condition i) holds.

Formalization targets

Goal: almost-quadratic diameter in dimension $n/4$

$$D(n/4,\, n) = \Omega\!\left(\frac{n^2}{\log n}\right).$$

Explicitly, there are $c > 0$ and $N$ such that for every $n \ge N$ with $4 \mid n$ there is a graph $G \in \mathcal B_{n/4,\,n}$ and two vertices $u, v$ of $G$ with $\mathrm{dist}_G(u,v) \ge c\, n^2/\log n$. The constants $c$ and $N$ are left unfixed, so the goal survives any improvement in the constant.

There are no milestones: the source is an extended abstract that states the result without a proof and names no intermediate lemma.

Significance

The result. Since $\triangle_u(d,n) \le D(d,n)$, any proof of a bound on $D$ bounds the diameter of all non-degenerate polyhedra. The paper shows that the Kalai–Kleitman and Larman bounds are of this kind. The lower bound shows the limits of the approach: an argument that uses only condition i) cannot prove a linear (Hirsch-type) bound, because $D(n/4,n)$ grows almost quadratically in $n$. Any proof of a linear bound must use further geometric properties of polyhedra. A polynomial, even quadratic, upper bound for $D$ is not excluded by the result.

Formalizing it. The result is proved in the literature (Math. Oper. Res. 35 (2010) 786–794); it has no machine-checked proof. A formal proof requires an explicit combinatorial construction of graphs in the base abstraction with large diameter and a probabilistic existence argument, neither of which is currently on the platform. The platform's Hirsch campaign has the same abstraction in its layer-family form (Hirsch_clf, whose description mentions the $\Omega(n^2/\log n)$ families in prose) and the proved upper bound Hirsch.clf_saturated_quadratic_bound, $L \le d(n-d)$, on a subclass that contains the constructions of this paper; neither states the lower bound.

Difficulty

A long path through all of $\binom{[n]}{d}$ has exponential length but violates condition i): two vertices of the path generally share elements that some intermediate vertex lacks. Condition i) must hold for every pair of vertices simultaneously, which forces the vertices containing any fixed set to induce a connected subgraph. Building a long graph means arranging many $d$-sets so that each of these exponentially many connectivity constraints holds at once while the graph distance between two vertices stays large. The authors announce that their construction relies on disjoint covering designs, and that the existence of such designs with the required parameters is obtained from the Lovász Local Lemma.

Formalization scope

• $[n]$ is Fin n; vertices are the $d$-sets themselves, V : Finset (Finset (Fin n)) and G : SimpleGraph V. Distinct vertices carry distinct labels.
• Condition i) is stated with walks, and requires every vertex of the walk (endpoints included, which is automatic) to contain $u \cap v$. A walk contains a path on a subset of its vertices, so this is the page's condition.
• "Connected" is encoded as $V \ne \emptyset$; connectivity follows from condition i).
• The page writes $D(n/4,n)$ without rounding; the goal is read literally: $4 \mid n$ and dimension exactly $n/4$.
• $\Omega(\cdot)$ is made explicit as $\exists c > 0, \exists N, \forall n \ge N$. The logarithm is natural (Real.log); the base only rescales $c$.
• "$D(n/4,n) \ge B$" is stated as the existence of one graph in the class with two vertices at SimpleGraph.dist at least $B$; $D$ is not defined as a supremum, so no junk value enters. SimpleGraph.dist returns $0$ for unreachable pairs, which could only make the statement harder.
• Only the lower half of $\Omega$ is claimed, as on the page.

The goal cannot be trivialized by a non-injective labelling (vertices are the sets), by checking condition i) only on adjacent pairs (it is required for all pairs, with $u\cap v$ kept along the whole walk), or by a zero constant ($c > 0$ is required).

Infrastructure that a solution needs and that is reusable beyond this mission: covering designs and disjoint covering designs over Finset (Fin n), the Lovász Local Lemma (posed on the platform as AppliedComb.ManyFaces.local_lemma_symmetric), and a toolkit for proving condition i) for graphs assembled from blocks. Contributions of any of these as separate theorems are welcome.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211 (Flexible Network Design), 2010 (the extended abstract this mission cites). http://drops.dagstuhl.de/opus/volltexte/2010/2724
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35(4), 786–794, 2010 (full proofs). https://doi.org/10.1287/moor.1100.0470
• G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26(2), 315–316, 1992. https://doi.org/10.1090/S0273-0979-1992-00285-9
• D. G. Larman, Paths on polytopes, Proc. London Math. Soc. 20(3), 161–178, 1970. https://doi.org/10.1112/plms/s3-20.1.161
• V. Klee, D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117, 53–78, 1967. https://doi.org/10.1007/BF02395040
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176(1), 383–412, 2012. https://doi.org/10.4007/annals.2012.176.1.7
• N. Alon, J. Spencer, The Probabilistic Method, 3rd ed., Wiley, 2008 (Lovász Local Lemma).

Motivation

Stochastic programs often optimize a decision that changes several random outcomes at once. A reference outcome may be acceptable even when no fixed threshold captures its risk: one wants the new outcome to be preferable under every increasing concave assessment of gains. Second order stochastic dominance expresses that comparison. Dentcheva and Ruszczyński study optimization with several such constraints, each imposed on a nonlinear outcome operator, and show how the constraint multipliers can be represented by utility functions rather than scalar penalties (Dentcheva–Ruszczyński, 2004). Their earlier paper, Optimization with stochastic dominance constraints, treats the pure dominance case without the nonlinear decision map; the present result adds decision dependent outcomes, multiple constraints, and split variables. Ogryczak and Ruszczyński's second performance function supplies the stochastic order used here (Ogryczak–Ruszczyński, 2002).

The utility interpretation matters when a modeler wants a certificate explaining why a solution satisfies a risk preference expressed by dominance. The theorem identifies a concave utility for each binding dominance constraint and an essentially bounded multiplier for each comparison between the split outcome and the outcome produced by the decision. The source is a revised April 2003 author manuscript, later published in Mathematical Programming in 2004; the page and equation numbers below follow that manuscript (author manuscript).

Setting

Work on a probability space $(\Omega,\mathcal F,P)$. An integrable random outcome is a measurable real function with finite expected absolute value; $\mathcal L^1$ denotes these outcomes, and $\mathcal L^\infty$ denotes essentially bounded ones. The decisions lie in a convex set $Z$ inside a separable locally convex Hausdorff real vector space $\mathcal Z$. An integrable objective outcome $H(z)$ and integrable constraint outcomes $G_i(z)$ depend continuously in the $\mathcal L^1$ norm on $z$. Almost every realized map $z\mapsto H(z)(\omega)$ and $z\mapsto G_i(z)(\omega)$ is concave and continuous on all of $\mathcal Z$. Fixed integrable outcomes $Y_i$ serve as references; the $i$th comparison is required over a bounded interval $[a_i,b_i]$.

For an outcome $X$, its second performance function is the area below its distribution function:

$$F_2(X;\eta)=\int_{-\infty}^{\eta}P\{X\le\xi\}\,d\xi.$$

The split program (11)–(14) chooses $z\in Z$ and $X=(X_1,\ldots,X_m)\in(\mathcal L^1)^m$ to maximize $\mathbb E H(z)$, subject to $F_2(X_i;\eta)\le F_2(Y_i;\eta)$ for every $\eta\in[a_i,b_i]$, and $X_i\le G_i(z)$ almost surely. Larger outcomes are preferred, so a dominating $X_i$ has the smaller $F_2$ curve. The split variables expose the dominance and decision coupling as separate constraints (manuscript, pp. 3–4).

The utility cone $\mathcal U_1([a,b])$ consists of concave nondecreasing functions $u:\mathbb R\to\mathbb R$ that vanish for $t\ge b$ and are affine with a nonnegative slope for $t\le a$. Given $u_i$ in these cones and $\theta_i\in\mathcal L^\infty$, the Lagrangian is

$$L(z,X,u,\theta)=\mathbb E\!\left[H(z)+\sum_{i=1}^m\bigl(u_i(X_i)-u_i(Y_i)+\theta_i(G_i(z)-X_i)\bigr)\right].$$

Uniform dominance means one decision $\tilde z\in Z$ makes every dominance inequality uniformly strict on its interval: for each $i$, $F_2(Y_i;\eta)-F_2(G_i(\tilde z);\eta)$ has a positive lower bound over $[a_i,b_i]$ (Definition 1, p. 7).

Formalization targets

Utility and bounded multiplier characterization

Theorem 2 is the goal. Under uniform dominance, every optimum $(\hat z,\hat X)$ of the split program admits $\hat u_i\in\mathcal U_1([a_i,b_i])$ and nonnegative $\hat\theta_i\in\mathcal L^\infty$ with

$$L(\hat z,\hat X,\hat u,\hat\theta)=\max_{z\in Z,\,X\in(\mathcal L^1)^m}L(z,X,\hat u,\hat\theta),$$ $$\mathbb E\hat u_i(\hat X_i)=\mathbb E\hat u_i(Y_i),\qquad \hat\theta_i\bigl(\hat X_i-G_i(\hat z)\bigr)=0\quad\text{almost surely}.$$

Conversely, an attained Lagrangian maximum satisfying the split constraints and these complementarity equations is a primal optimum. The milestone list follows the source's measure multiplier equations (23)–(24), the measure to utility identity (25), Theorem 1's expected concave subgradient characterization, and the converse's weak duality inequality (manuscript, pp. 5, 8–10).

Significance

The result gives a concrete optimality certificate in a program whose constraints compare entire outcome distributions. Each utility multiplier represents the active part of one dominance constraint. Each $\theta_i$ accounts for the almost sure inequality linking a split outcome to the decision. The equalities show exactly where those constraints are complementary, while the Lagrangian maximum compares the proposed solution with all integrable split outcomes. The paper derives a dual problem from the same Lagrangian in its following section (manuscript, p. 11).

The mathematical theorem is proved in the paper. This mission seeks a machine checked version of its definitions, measure identity, subgradient statement, and both directions of Theorem 2. The published second performance definition is reused as a reference; the nonlinear split program and its utility and measure Lagrangians require a development specific to this paper. The 2003 pure dominance mission contains related local drafts, but those items are not published and cannot currently be imported as platform theorems.

Difficulty

The dominance inequality contains a continuum of thresholds for each outcome. A scalar multiplier at one threshold cannot capture the whole constraint, while the dual object for continuous functions on $[a_i,b_i]$ is a measure. The split inequality lives in $\mathcal L^1$, where the nonnegative cone has empty interior, so an ordinary interior point argument applied to all constraints at once does not match the paper's setting. The source also needs a subgradient of expected concave utility represented by an almost surely selected, essentially bounded random vector; the conclusion is stronger than merely knowing that the expected objective has a deterministic supporting functional (manuscript, pp. 5–9).

Formalization scope

The Lean development keeps the general separable locally convex Hausdorff decision space, the convex set $Z$, and a finite index type for the $m$ dominance constraints. Operators are function representatives with explicit integrability, continuity in $\mathcal L^1$, and samplewise concavity and continuity. Almost sure comparisons use the probability measure $P$; the null set for each realization condition precedes the quantifier over decisions. Split outcomes range only over integrable functions, and utility multipliers range over the exact cone $\mathcal U_1([a_i,b_i])$. The $\mathcal L^\infty$ condition includes almost sure strong measurability and essential boundedness. Maxima in Theorems 1 and 2 are attained maxima, expressed by membership and comparison against every competitor, never a real supremum with a default value.

The source prints a strictly positive affine slope in its definition of $\mathcal U_1$, but immediately calls this class a cone and later uses the zero measure. The formalization uses $c\ge0$; with $c>0$, Theorem 2 is false for a slack dominance constraint. Uniform dominance is expressed as a positive lower bound rather than a real infimum. The measure milestone uses finite nonnegative measures supported on closed intervals, including endpoint atoms. These conditions exclude default zero integrals, an empty interval disguised by an infimum, and a vacuous utility class. Contributions to the measure to utility correspondence, integration identities, and expected concave subgradient infrastructure can be reused beyond this program.

Selected references

• D. Dentcheva and A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Mathematical Programming (2004), DOI; revised author manuscript, April 2003.
• D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, manuscript submitted for publication (2002), cited as reference [6] in the 2003 author manuscript.
• W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean risk models, SIAM Journal on Optimization 13 (2002), DOI.

Why individual lower rates

Regularized least squares (RLS) in a reproducing kernel Hilbert space is a basic estimator of nonparametric regression and of kernel-based learning. Its learning rate is the speed at which the expected excess risk goes to zero as the sample size $\ell$ grows. A rate is useful only if it is known to be optimal, and optimality is a lower-bound statement about all learning algorithms.

Caponnetto and De Vito (Found. Comput. Math. 7 (2007)) prove two kinds of lower bound. The first is a minimax lower rate (their Theorem 2): for every algorithm and every $\ell$, some distribution in the prior is hard. Their Section 2 (p. 6) points out a weakness of this notion: the bad distribution may change with $\ell$. A practitioner, however, faces one fixed unknown distribution and asks how the error decreases as data accumulate. The individual lower rate answers that question. It asks for a single distribution, chosen against the algorithm but not depending on $\ell$, on which the expected excess risk stays above $a_\ell$ along infinitely many $\ell$.

The notion comes from nonparametric regression. Györfi, Kohler, Krzyżak and Walk (A Distribution-Free Theory of Nonparametric Regression, Springer 2002, §3, Theorem 3.3) proved individual lower rates for classes of smooth regression functions. Theorem 3 of Caponnetto–De Vito carries the result to vector-valued RKHS with the spectral priors $\mathcal P(b, c)$. Theorem 1 of the same paper shows that these priors are learned by RLS at rate $\ell^{-bc/(bc+1)}$.

Setting

The input space $X$ is Polish. The output space $Y$ is a real Hilbert space of finite dimension $d$. The hypothesis space $\mathcal H$ is a separable real Hilbert space of functions $f : X \to Y$ in which evaluation is continuous, so that $f(x) = K_x^* f$ for bounded operators $K_x : Y \to \mathcal H$. Hypothesis 1 asks that $(x, t) \mapsto \langle K_t v, K_x w\rangle_{\mathcal H}$ be measurable and that $\operatorname{Tr}(K_x^*K_x) \le \kappa$ for every $x$.

A distribution $\rho$ on $Z = X \times Y$ has marginal $\rho_X$ and conditional distributions $\rho(\cdot \mid x)$. The risk of $f \in \mathcal H$ is

$$\mathcal E[f] = \int_Z \|f(x) - y\|_Y^2 \, d\rho(x, y).$$

Hypothesis 2 asks for square-integrable outputs, a minimizer $f_{\mathcal H}$ of $\mathcal E$ over $\mathcal H$, and a Bernstein-type moment bound on the noise $y - f_{\mathcal H}(x)$ with constants $M, \Sigma$.

The operator $T = \int_X K_x K_x^*\, d\rho_X(x)$ on $\mathcal H$ satisfies $\langle Tf, g\rangle = \int_X \langle f(x), g(x)\rangle_Y \, d\rho_X$. Its nonzero eigenvalues are $t_1 \ge t_2 \ge \dots$, with orthonormal eigenvectors $e_n$.

For positive constants $M, \Sigma, R, \alpha, \beta$ and parameters $1 < b < \infty$, $1 \le c \le 2$, the prior $\mathcal P(b, c)$ (Definition 1) is the set of probability measures $\rho$ satisfying three conditions:

• Hypothesis 2 holds for the minimal-norm minimizer $f_{\mathcal H}$;
• $f_{\mathcal H} = T^{(c-1)/2} g$ with $\|g\|_{\mathcal H}^2 \le R$ (a source condition);
• the eigenvalues satisfy $\alpha \le n^b t_n \le \beta$ for all $n \ge 1$.

A learning algorithm is a sequence of maps $f_\ell : Z^\ell \to \mathcal H$, and $f^\ell_{\mathbf z}$ is its output on a sample $\mathbf z$ of size $\ell$ drawn from $\rho^\ell$.

Formalization targets

Goal: Theorem 3 (p. 11)

For every $B > b$,

$$\inf_{\{f_\ell\}}\ \sup_{\rho \in \mathcal P(b, c)}\ \limsup_{\ell \to \infty} \frac{\mathbb E_{\mathbf z \sim \rho^\ell}\big(\mathcal E[f^\ell_{\mathbf z}] - \mathcal E[f_{\mathcal H}]\big)}{\ell^{-cB/(cB+1)}} > 0 .$$

Equivalently, there is $C > 0$ such that every algorithm admits one $\rho \in \mathcal P(b, c)$ with expected excess risk at least $C\ell^{-cB/(cB+1)}$ for infinitely many $\ell$. The constant may depend on the prior and on $B$, but not on the algorithm.

Milestones

1. Proposition 7 (pp. 25–26). A fair sign $s$ observed as $y = sg + n$ with i.i.d. $\mathcal N(0, \sigma^2)$ noise has Bayes error $\Phi(-\|g\|/\sigma)$.
2. $\mathcal P' \subset \mathcal P(b, c)$ (pp. 26–27). This concerns distributions with marginal $\nu$ and conditional distribution $\mathcal N(m^{(s)}(x), \sigma^2\mathrm{Id})$, where

$$m^{(s)} = \sum_n s_n\sqrt{\gamma_n/t_n}\,e_n, \qquad \gamma_n = n^{-(Bc+1)}\tfrac{\epsilon}{\epsilon+1}\alpha^c R,$$

with $\epsilon = (B - b)c$ and $s \in \{\pm1\}^\infty$. Every such distribution belongs to the prior. 3. (63) (p. 27). Under these distributions, $\mathcal E[f] - \mathcal E[m^{(s)}] = \sum_n (c_n - s_n)^2\gamma_n$ with $c_n = \sqrt{t_n/\gamma_n}\langle f, e_n\rangle$. 4. (68) (p. 28, corrected). $\sum_{\ell\gamma_n \le 1} \gamma_n \ge \tfrac{u^{1/(Bc+1)}}{2Bc}\,\ell^{-Bc/(Bc+1)}$ for $\ell \ge (2Bc)^{Bc+1}/u$, where $u = \tfrac{\epsilon}{\epsilon+1}\alpha^c R$. 5. (67) (pp. 28–30). Averaged over independent fair signs $S$, the expected number of sign errors over $\{n : \ell\gamma_n \le 1\}$, weighted by $\gamma_n$, is at least $\Phi(-1/\sigma)\sum_{\ell\gamma_n \le 1}\gamma_n$.

Significance

Theorem 3 shows that no algorithm, RLS included, converges on every fixed distribution of $\mathcal P(b, c)$ faster than $\ell^{-cB/(cB+1)}$, for any $B > b$. For $c > 1$ this exponent is arbitrarily close to the exponent $bc/(bc+1)$ of the upper rate of Theorem 1, so RLS with the regularization parameter of Theorem 1 is near-optimal even in the individual sense. The paper notes (p. 6) that full individual optimality would still need an upper rate in expectation or an individual lower rate in probability; that question is outside this mission.

The theorem is proved on paper and has been cited widely. To our knowledge no part of it has been machine-checked. A formalization would produce:

• a checked reduction from a learning lower bound to Gaussian sign testing;
• a Lean model of Gaussian-noise regression with vector outputs;
• an explicit, checked version of the corrected computation (68).

Difficulty

A minimax argument picks a hard distribution for each $\ell$, and that is not allowed here: the distribution must be fixed before $\ell$ varies. The obvious repair, taking the worst distribution for one $\ell$ and keeping it, fails, because a distribution that is hard at sample size $\ell$ can be easy at sample size $10\ell$.

What has to be shown is a lower bound that holds for one distribution simultaneously along infinitely many sample sizes. Bounds that hold separately at each $\ell$, with a distribution that may depend on $\ell$, do not combine into such a bound.

A second difficulty arises in any reduction to a coordinatewise testing problem: each observation $y_i$ depends on all spectral coordinates of the regression function at once, so testing one coordinate is not literally the problem of Proposition 7.

Formalization scope

$\mathcal H$ is Mathlib's RKHS ℝ H X Y, with $K_x$ = RKHS.kerFun H x and $Y$ finite-dimensional. The paper's $\Sigma$ is written Sig.

• The operator $T$. It is never formed as an operator-valued integral. It enters through its quadratic form and through an eigen-system $(e_n, t_n)$ with summable weights.
• Indexing. Indices start at $0$, so the paper's $t_n$ is t (n-1).
• The prior. InPrior encodes $\rho \in \mathcal P(b, c)$, including "probability measure".
• Expectations. Expectations are lintegrals of nonnegative quantities, and samples are Fin ℓ → X × Y under the product measure.
• Algorithms. A learning algorithm is a family of maps from samples to $\mathcal H$, and it must be measurable.
• Added hypothesis. $\mathcal P(b, c)$ is assumed nonempty. The proof starts from "an arbitrary $\rho_0 \in \mathcal P(b, c)$", and with an empty prior the supremum is over the empty set and the statement fails.
• The noise. Gaussian noise with covariance $\sigma^2\mathrm{Id}$ is $\sigma\xi$ with $\xi \sim$ stdGaussian Y.
• $S^d$. It is read as the surface area of the unit sphere of $\mathbb R^d$.

Two parts of the print are corrected, and both corrections are stated in the items.

• (68). The printed constant $v = u^{-Bc/(Bc+1)}/(2Bc)$ and threshold $2Bc(2Bcu)^{Bc}$ come from dropping the factor $u$ in an integral, and the printed inequality fails for $u < 1/2$. The corrected constant is $u^{1/(Bc+1)}/(2Bc)$, with threshold $(2Bc)^{Bc+1}/u$.
• (67). It is stated with the explicit constant $C = \Phi(-1/\sigma)$ that the proof obtains.

The goal mentions none of $\mathcal P'$, $m^{(s)}$, $\gamma_n$ or $\Phi$. It is the lower rate (3) for the full prior $\mathcal P(b, c)$ with $a_\ell = \ell^{-cB/(cB+1)}$. A formalization that fixed the algorithm, let the distribution depend on $\ell$, or let the constant depend on the algorithm would prove a different, weaker statement.

A complete development needs:

• Gaussian measures on finite-dimensional inner product spaces, and the distribution function of the standard normal;
• conditional distributions on Polish products;
• infinite products of fair coins;
• series in Hilbert spaces with orthogonal terms.

Reusable pieces include Proposition 7, the Bayes-error monotonicity argument on p. 29, and the identification of the risk minimizer of a Gaussian-noise model. Contributions on any milestone are welcome, as are proofs of the measurability facts (elements of $\mathcal H$ are measurable under Hypothesis 1).

Selected references

• A. Caponnetto and E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
• L. Györfi, M. Kohler, A. Krzyżak and H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer Series in Statistics, 2002 (§3, Theorem 3.3; Lemma 3.2).
• R. DeVore, G. Kerkyacharian, D. Picard and V. Temlyakov, Approximation methods for supervised learning, Found. Comput. Math. 6 (2006) 3–58.

Why lower bounds for kernel regression matter

Regularized least squares (RLS), also called kernel ridge regression, is one of the standard estimators of statistical learning: given a sample of input–output pairs, it fits a function from a reproducing kernel Hilbert space by minimizing the empirical squared error plus a multiple of the squared norm. Caponnetto and De Vito (FoCM 2007) proved that, over a class of distributions described by two parameters — the decay of the eigenvalues of the kernel's covariance operator and the smoothness of the regression function relative to it — RLS with a well-chosen regularization parameter converges at the rate $\ell^{-bc/(bc+1)}$ in the sample size $\ell$ (their Theorem 1). An upper rate on its own does not say whether another method could do better. This mission formalizes the matching minimax lower rate (their Theorem 2): when the output space is finite dimensional, no learning algorithm whatsoever converges faster than $\ell^{-bc/(bc+1)}$ uniformly over the class. Together the two theorems say that RLS is rate-optimal, and they are the reference point for later work on spectral regularization, early stopping and distributed kernel methods.

The paper's lower bound adapts the minimax analysis of DeVore, Kerkyacharian, Picard and Temlyakov (FoCM 2006) to the vector-valued RKHS setting.

Setting

Inputs $x$ lie in a Polish space $X$ and outputs $y$ in a real Hilbert space $Y$ of finite dimension $d$. The hypothesis space $\mathcal H$ is a separable Hilbert space of functions $f : X \to Y$ in which evaluation is continuous; $K_x : Y \to \mathcal H$ is the adjoint of evaluation at $x$, so $f(x) = K_x^* f$. Hypothesis 1 asks that $(x,t) \mapsto \langle K_t v, K_x w\rangle_{\mathcal H}$ be measurable and that $\operatorname{Tr}(K_x^*K_x) \le \kappa$ for every $x$.

A distribution $\rho$ on $Z = X \times Y$ has risk $\mathcal E[f] = \int \|f(x) - y\|^2\, d\rho$. Hypothesis 2 asks that $\int\|y\|^2 d\rho < \infty$, that the risk has a minimizer $f_{\mathcal H} \in \mathcal H$ (taken of minimal norm), and that the noise $y - f_{\mathcal H}(x)$ satisfies a Bernstein moment condition with constants $M, \Sigma$. With $\rho_X$ the marginal of $\rho$, the operator $T = \int K_x K_x^*\, d\rho_X(x)$ on $\mathcal H$ has the quadratic form $\langle Tf, g\rangle = \int \langle f(x), g(x)\rangle\, d\rho_X$ and a spectral decomposition $T = \sum_n t_n \langle\cdot, e_n\rangle e_n$.

The prior $\mathcal P(b,c)$ (Definition 1, with fixed positive $M, \Sigma, R, \alpha, \beta$, $1 < b < \infty$ and $1 \le c \le 2$) is the set of probability measures $\rho$ satisfying Hypothesis 2 with $M, \Sigma$ such that

• $T$ has infinitely many positive eigenvalues $t_1 \ge t_2 \ge \dots$ with $\alpha \le n^b t_n \le \beta$ (a capacity condition);
• $f_{\mathcal H} = T^{(c-1)/2} g$ for some $g$ with $\|g\|^2 \le R$ (a source condition).

Formalization targets

Goal: Theorem 2 (p. 11)

$$\lim_{\tau \to 0}\ \liminf_{\ell \to \infty}\ \inf_{f_\ell}\ \sup_{\rho \in \mathcal P(b,c)}\ \mathbb P_{\mathbf z \sim \rho^\ell}\Big[\mathcal E[f^\ell_{\mathbf z}] - \mathcal E[f_{\mathcal H}] > \tau\, \ell^{-\frac{bc}{bc+1}}\Big] = 1,$$

the infimum over all learning algorithms $f_\ell : Z^\ell \to \mathcal H$. The constant in front of the rate is left free, so the goal asserts only the exponent.

Milestones

1. Proposition 4 (p. 21): for $f = T^{(c-1)/2}g$, $\|g\|^2 \le R$, the explicit distribution $\rho_f$ with marginal $\nu$ (the marginal of some $\rho_0 \in \mathcal P(b,c)$) and $2d$-point conditional law is a probability measure with regression function $f$, and lies in $\mathcal P(b,c)$ when $\min(M,\Sigma) \ge 2(4d+1)\sqrt{\kappa^c R}$.
2. Proposition 4, (54): $\mathcal K(\rho_f, \rho_{f'}) \le \frac{16}{15 d L^2}\|\sqrt T(f - f')\|^2$ with $L = 4\sqrt{\kappa^c R}$.
3. Proposition 6 (p. 24): for $m > 16$ there are $N \ge e^{m/24}$ sign vectors in $\{-1,+1\}^m$ with pairwise $\sum_n(\sigma_i^n - \sigma_j^n)^2 \ge m$.
4. Proposition 5 (pp. 22–23): for small $\epsilon$ there are $N_\epsilon \ge e^{\gamma\epsilon^{-1/(bc)}}$ functions in the source class with $\epsilon \le \|\sqrt T(f_i - f_j)\|^2 \le 4\epsilon$.
5. Theorem 5 (p. 24): for every algorithm some $\rho_* \in \mathcal P(b,c)$ has $\mathbb P[\text{excess risk} > \epsilon/4] \ge \min\{N^*/(N^*+1),\ e^{-3/e}\sqrt{N^*}\, e^{-4\ell\epsilon/(15 d\kappa^c R)}\}$, $N^* = e^{\gamma\epsilon^{-1/(bc)}}$.

Significance

The result. Theorem 2 shows that the exponent $bc/(bc+1)$ attained by RLS cannot be improved by any estimator over $\mathcal P(b,c)$ when $\dim Y < \infty$; for $c = 1$ RLS is optimal up to a logarithmic factor. It separates what is a property of the problem class from what is a property of the algorithm: improvements to kernel methods must change the class (stronger assumptions) rather than the rate. The construction — a packing of the source class measured in the $\sqrt T$-norm, combined with a KL bound for an explicit noise model — is the template reused in many later lower bounds for kernel and inverse-problem estimators.

Formalizing it. The result has been proved since 2007; no machine-checked version exists. A formal proof needs the information-theoretic lower-bound machinery (a Fano-type inequality for many hypotheses), a Varshamov–Gilbert-type packing of the Hamming cube, KL divergence between explicit mixtures, and the spectral description of the covariance operator of a vector-valued RKHS. Each of these is reusable well beyond this paper. The mission also makes precise the paper's implicit conventions (see below), which a pen-and-paper reader fills in silently.

Difficulty

The upper half of the argument is not the hard part; the hard part is that the lower bound is uniform over all measurable algorithms, which no direct computation reaches. The step that does not follow from the paper alone is Theorem 5: its proof invokes Lemma 3.3 and Eq. 3.12 of DeVore et al., a Fano-type inequality bounding the probability of correct identification among $N$ hypotheses with pairwise KL divergence at most a given level. That lemma is not stated in the paper and is not in Mathlib; it must be formalized. A second obstacle is the packing (Proposition 6), whose proof is a probabilistic union bound with Hoeffding's inequality. A naive attempt to prove Theorem 2 by exhibiting a single bad distribution fails: for any fixed $\rho$ some algorithm (the constant one returning $f_{\rho}$) has zero excess risk, so the bad distribution must depend on the algorithm, and the order of quantifiers is essential.

Formalization scope

Mathlib's RKHS ℝ H X Y provides the function space with continuous evaluation, RKHS.kerFun is $K_x$, and InformationTheory.klDiv is the Kullback–Leibler information. The operator $T$ is never built as an operator-valued Bochner integral: it is recorded through its quadratic form $\int\langle f(x), g(x)\rangle d\rho_X$ and an eigen-system indexed by $\mathbb N$ from $0$ (the paper's $t_n$ is t (n-1)). The trace in Hypothesis 1 is a series over a Hilbert basis of $Y$; the conditional law in Hypothesis 2 is Measure.condKernel, and the moment integral there is a lintegral. $\mathcal E[f_{\mathcal H}]$ in the goal is $\inf_{f \in \mathcal H}\mathcal E[f]$.

Conventions and added hypotheses, each implicit on the page:

• $\mathcal P(b,c)$ is assumed nonempty; the proof fixes $\rho_0 \in \mathcal P(b,c)$, and over an empty prior the supremum is over the empty set and the statement is false.
• Algorithms are measurable maps $Z^\ell \to \mathcal H$; this is the reading under which the probability in the goal is defined, and it restricts the infimum relative to "all mappings".
• The constants $M, \Sigma, R, \alpha, \beta, \kappa$ are positive; the basis $(v_j)$ of $Y$ in Proposition 4 is orthonormal.
• Proposition 4's "$\|g\|^2 \le R$" for $f'$ is read as $\|g'\|^2 \le R$; Proposition 6's "$i \ne, j$" as $i \ne j$; (56) is required for $i \ne j$. The proof's variance display on p. 22 is wrong for $d \ge 2$, but the conclusion of Proposition 4 holds.

The goal is the $\varepsilon$–$\tau$–$L$ unfolding of the limit and mentions neither $\rho_f$, the KL bound nor the packing, so it cannot be discharged by any of the milestones' constructions in isolation; the distribution $\rho$ is chosen after the algorithm, never before it.

Contributions welcome: a general Fano/DeVore-type lemma for finitely many hypotheses, the Varshamov–Gilbert bound, KL ≤ χ² for finite mixtures, and lemmas relating covForm to the excess risk.

Selected references

• A. Caponnetto, E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
• R. DeVore, G. Kerkyacharian, D. Picard, V. Temlyakov, Approximation methods for supervised learning, Found. Comput. Math. 6 (2006) 3–58. https://doi.org/10.1007/s10208-004-0158-6
• L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794

Motivation

Regularized least squares (RLS, also called kernel ridge regression or Tikhonov regularization) is the simplest learning algorithm built on a reproducing kernel Hilbert space. Given $\ell$ examples $(x_i,y_i)$ drawn independently from an unknown distribution $\rho$, it returns the function in a hypothesis space $\mathcal H$ that minimizes the empirical squared error plus $\lambda$ times the squared norm. It is used in regression, in multi-task learning with vector-valued outputs, and as the reference case for spectral regularization methods.

The basic statistical question is how fast the excess risk of the RLS estimator goes to zero as $\ell$ grows, and how to choose $\lambda=\lambda_\ell$ to get that speed. Caponnetto and De Vito (FoCM 2007) answered it for a family of priors $\mathcal P(b,c)$ described by two numbers: the decay rate $b$ of the eigenvalues of the covariance operator of the input distribution and the regularity $c$ of the target function. Their Theorem 1 gives the upper rate $\ell^{-bc/(bc+1)}$; Theorems 2 and 3 show that no algorithm does better when the output space is finite dimensional. This mission formalizes the upper rate.

Timeline. Cucker and Smale (2002) and De Vito, Caponnetto and Rosasco (2005) gave rates for RLS that did not depend on the eigenvalue decay of $\rho_X$. Zhang (2005) introduced the effective dimension $\mathcal N(\lambda)$ as the complexity measure. Caponnetto and De Vito (authors' copy dated 2006, published 2007) combined it with a source condition to obtain rates that are optimal over $\mathcal P(b,c)$, for vector-valued outputs. Steinwart, Hush and Scovel (2009) and Fischer and Steinwart (2020) later extended the analysis to other norms and to $c<1$.

Setting

The input space $X$ is a Polish space and the output space $Y$ is a real separable Hilbert space. The hypothesis space $\mathcal H$ is a real separable Hilbert space of functions $f:X\to Y$ in which evaluation at each point is continuous. For $x\in X$, $K_x:Y\to\mathcal H$ is the adjoint of evaluation at $x$, so $f(x)=K_x^*f$. Hypothesis 1 adds a measurability condition and a uniform trace bound $\operatorname{Tr}(K_x^*K_x)\le\kappa$.

A distribution $\rho$ on $Z=X\times Y$ has marginal $\rho_X$ and conditional laws $\rho(\cdot\mid x)$. The expected risk of $f\in\mathcal H$ is $\mathcal E[f]=\int\|f(x)-y\|_Y^2\,d\rho$. Hypothesis 2 asks that $\mathbb E\|y\|^2<\infty$, that $\mathcal E$ attains its infimum over $\mathcal H$ at some $f_{\mathcal H}$ (the minimizer of minimal norm is used), and that the noise $y-f_{\mathcal H}(x)$ satisfies a Bernstein moment condition with constants $M,\Sigma$.

The covariance operator $T=\int_XK_xK_x^*\,d\rho_X$ is positive and trace class, with $\langle Tf,f\rangle_{\mathcal H}=\int_X\|f(x)\|_Y^2\,d\rho_X$ and eigen-decomposition $T=\sum_nt_n\langle\cdot,e_n\rangle e_n$, $t_1\ge t_2\ge\dots>0$. The prior $\mathcal P(b,c)$, for $1<b<\infty$ and $1\le c\le2$, consists of the $\rho$ satisfying Hypothesis 2, with $f_{\mathcal H}=T^{(c-1)/2}g$ for some $\|g\|^2\le R$ (source condition), and with $\alpha\le n^bt_n\le\beta$ for all $n$ (eigenvalue decay).

The RLS estimator $f_{\mathbf z}^\lambda$ minimizes $\frac1\ell\sum_i\|f(x_i)-y_i\|_Y^2+\lambda\|f\|_{\mathcal H}^2$ over $\mathcal H$.

Formalization targets

Goal: Theorem 1, $1<b<+\infty$

With $\lambda_\ell=\ell^{-b/(bc+1)}$ and $a_\ell=\ell^{-bc/(bc+1)}$ for $c>1$, and $\lambda_\ell=a_\ell=(\log\ell/\ell)^{b/(b+1)}$ for $c=1$,

$$\lim_{\tau\to\infty}\limsup_{\ell\to\infty}\sup_{\rho\in\mathcal P(b,c)}\mathbb P_{\mathbf z\sim\rho^\ell}\Big[\mathcal E[f_{\mathbf z}^{\lambda_\ell}]-\mathcal E[f_{\mathcal H}]>\tau a_\ell\Big]=0.$$

The statement fixes the rate, not the constants: the threshold $\tau$ absorbs every constant of the prior.

Milestones

1. Proposition 1 iii)–v): the excess risk is $\|\sqrt T(f-f_{\mathcal H})\|^2$; the regularized expected and empirical risks have unique minimizers $f^\lambda=(T+\lambda)^{-1}Tf_{\mathcal H}$ and $f_{\mathbf z}^\lambda=(T_{\mathbf x}+\lambda)^{-1}g_{\mathbf z}$.
2. Proposition 2: a Bernstein inequality for means of i.i.d. Hilbert-space-valued variables.
3. Theorem 4: with probability $\ge1-\eta$,

$$\mathcal E[f_{\mathbf z}^\lambda]-\mathcal E[f_{\mathcal H}]\le3C_\eta\Big(\mathcal A(\lambda)+\frac{\kappa^2\mathcal B(\lambda)}{\ell^2\lambda}+\frac{\kappa\mathcal A(\lambda)}{\ell\lambda}+\frac{\kappa M^2}{\ell^2\lambda}+\frac{\Sigma^2\mathcal N(\lambda)}{\ell}\Big),$$

provided $\ell\ge2C_\eta\kappa\mathcal N(\lambda)/\lambda$ and $\lambda\le\|T\|$, where $C_\eta=32\log^2(6/\eta)$, $\mathcal A(\lambda)=\mathcal E[f^\lambda]-\mathcal E[f_{\mathcal H}]$, $\mathcal B(\lambda)=\|f^\lambda-f_{\mathcal H}\|^2$ and $\mathcal N(\lambda)=\operatorname{Tr}[(T+\lambda)^{-1}T]$. 4. Proposition 3: on $\mathcal P(b,c)$, $\mathcal A(\lambda)\le\lambda^c\|T^{(1-c)/2}f_{\mathcal H}\|^2$, $\mathcal B(\lambda)\le\lambda^{c-1}\|T^{(1-c)/2}f_{\mathcal H}\|^2$ and $\mathcal N(\lambda)\le\frac b{b-1}\beta^{1/b}\lambda^{-1/b}$.

Significance

The result. Theorem 1 says that RLS with $\lambda_\ell$ chosen from $(b,c)$ achieves the rate $\ell^{-bc/(bc+1)}$ uniformly over the prior, and the companion lower bounds show this is the minimax rate for $1<c\le2$ and finite-dimensional $Y$. The rate interpolates between the parametric rate $1/\ell$ (fast eigenvalue decay, smooth target) and slower nonparametric rates, and it identifies the effective dimension, rather than the dimension of $\mathcal H$, as the quantity that governs complexity. Theorem 4 is a non-asymptotic bound of independent use; it is the template for later analyses of spectral regularization, gradient descent with early stopping, and random-feature approximations of kernel methods.

The formalization. The result is proved on paper; no machine-checked proof of a kernel ridge regression rate is known to exist. A formal development requires a Bernstein inequality in Hilbert spaces, spectral calculus for a trace-class operator defined from a measure, and the operator-perturbation argument of Theorem 4. Two printed constants are corrected here: Theorem 4's proof yields $3C_\eta$, not $C_\eta$, and Proposition 3's bound on $\mathcal N(\lambda)$ has $\beta^{1/b}$ in place of $\beta$. The paper also states Theorem 1 for $b=+\infty$; that branch fails for $1\le c<2$ and is not posed.

Difficulty

The obvious argument bounds $\|f_{\mathbf z}^\lambda-f^\lambda\|_{\mathcal H}$ by uniform concentration of $T_{\mathbf x}$ around $T$ and multiplies by $\|\sqrt T\|$. That gives a variance term that ignores the eigenvalue decay of $T$, and hence a rate that does not improve with $b$. The optimal rate needs the variance measured through $\mathcal N(\lambda)$, which requires controlling $\sqrt T(T_{\mathbf x}+\lambda)^{-1}$ in operator norm with high probability. This in turn needs concentration of $(T+\lambda)^{-1/2}(T-T_{\mathbf x})$ in Hilbert–Schmidt norm, and the condition $\ell\gtrsim\mathcal N(\lambda)/\lambda$ under which the empirical operator is close enough to $T$. The noise is unbounded, so only the moment condition (9) is available, and the concentration step must use moment bounds rather than boundedness.

Formalization scope

$\mathcal H$ is Mathlib's RKHS ℝ H X Y, and $K_x$ is RKHS.kerFun H x. The trace in Hypothesis 1 is computed in a fixed Hilbert basis of $Y$. $\rho_X$ is the first marginal and $\rho(\cdot\mid x)$ is condKernel. The operator $T$ is not built as an operator-valued integral. It enters through its quadratic form $\int\langle f(x),g(x)\rangle\,d\rho_X$ and through an eigen-system $(e_n,t_n)$, indexed from $0$, so (17) reads $\alpha\le(n+1)^bt_n\le\beta$. The effective dimension is $\sum_nt_n/(t_n+\lambda)$. Samples are Fin ℓ → X × Y under the product measure, and probabilities of events are outer measures. "With probability at least $1-\eta$" is stated as "the bad event has measure at most $\eta$". The noise condition and the moments of Proposition 2 are integrals of nonnegative functions with values in $[0,\infty]$.

The hypotheses the paper uses but does not display are added: positivity of $M,\Sigma,R,\alpha,\beta,\kappa$, and integrability of the random variable in Proposition 2. The RLS estimator of the goal is any family of minimizers of (18) for $\ell\ge2$; at $\ell=1$ and $c=1$ the parameter $\lambda_1=0$ is degenerate. The goal quantifies uniformly: $L$ is chosen before $\rho$, and the estimator is fixed before $\rho$. The goal must not be replaced by a statement about $\mathcal A,\mathcal B,\mathcal N$ or by Theorem 4's event: it is the uniform rate for the estimator itself.

Reusable infrastructure: Hilbert-space Bernstein inequalities (Proposition 2 alone is a valuable target), spectral calculus for compact positive operators given by a quadratic form, and the representer/normal equation for vector-valued RLS. Contributions of proofs for any milestone, and of supporting lemmas about trace-class operators and effective dimension, are welcome.

Selected references

• A. Caponnetto, E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
• F. Cucker, S. Smale, On the mathematical foundations of learning, Bull. Amer. Math. Soc. 39 (2002) 1–49. https://doi.org/10.1090/S0273-0979-01-00923-5
• E. De Vito, A. Caponnetto, L. Rosasco, Model selection for regularized least-squares algorithm in learning theory, Found. Comput. Math. 5 (2005) 59–85. https://doi.org/10.1007/s10208-004-0134-1
• T. Zhang, Learning bounds for kernel regression using effective data dimensionality, Neural Comput. 17 (2005) 2077–2098. https://doi.org/10.1162/0899766054323008
• I. Pinelis, Optimum bounds for the distributions of martingales in Banach spaces, Ann. Probab. 22 (1994) 1679–1706. https://doi.org/10.1214/aop/1176988477
• I. Steinwart, D. Hush, C. Scovel, Optimal rates for regularized least squares regression, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/038.pdf
• S. Fischer, I. Steinwart, Sobolev norm learning rates for regularized least-squares algorithms, J. Mach. Learn. Res. 21 (2020) 1–38. https://jmlr.org/papers/v21/19-734.html