Functional Analysis

Why a nonsmooth implicit-function theorem

The classical implicit-function theorem solves an equation $F(x, y) = 0$ for $x$ as a function of a parameter $y$ near a known solution $(x_0, y_0)$, provided $F$ is (strongly) Fréchet differentiable in $x$ with an invertible partial derivative. Much of optimization does not meet that hypothesis. Optimality conditions of constrained problems, complementarity problems and variational inequalities are routinely rewritten as equations involving the projection onto a convex set, the componentwise $\min$, or the normal map of a polyhedron. These maps are Lipschitzian and piecewise smooth, but not differentiable. Sensitivity analysis asks whether the solution of such a system moves Lipschitz-continuously with the problem data, and the classical theorem cannot answer it.

Stephen M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, pp. 292–309, gives a theorem with the same shape as the classical one, in which differentiability is replaced by strong approximation by a function whose inverse is Lipschitzian. The paper's §4 applies it to parametric variational inequalities over polyhedral sets through the normal map.

Timeline. Robinson's Strongly regular generalized equations (Math. Oper. Res. 5, 1980) proved an implicit-function theorem for generalized equations under a linearization hypothesis called strong regularity. The 1991 paper reformulates that idea for single-valued nonsmooth equations: the approximating function $f$ need not be linear. Lemma 3.1 extends the Banach perturbation lemma for linear operators (Kantorovich–Akilov, Functional Analysis, Th. 4(2.V)) to Lipschitzian functions; after acceptance, A. Ioffe pointed the author to closely related results of Dmitruk, Milyutin and Osmolovskii (Lyusternik's theorem and the theory of extrema, Russian Math. Surveys, 1980, Theorems 1.2, 1.3), credited in the paper's footnote.

Setting

Let $X$, $Y$, $Z$ be real normed linear spaces, with $X$ complete. Fix $x_0 \in X$, $y_0 \in Y$, a neighborhood $\Xi$ of $x_0$ and a neighborhood $H$ of $y_0$. Let $F$ map $\Xi \times H$ to $Z$, with $F(x_0, y_0) = 0$, and let $f$ map $\Xi$ to $Z$, with $f(x_0) = 0$. $B(x, \rho)$ denotes the closed ball of radius $\rho$ about $x$.

Expansion modulus. For a map $f$ between metric spaces and a set $S$,

$$\delta(f, S) = \inf\left\{ \frac{\|f(x_1) - f(x_2)\|}{\|x_1 - x_2\|} : x_1 \ne x_2,\ x_1, x_2 \in S \right\}.$$

If $\delta(f,S) > 0$, then $f$ is one-to-one on $S$ and its inverse is Lipschitzian with modulus $\delta(f,S)^{-1}$. In Lean the mission works with lower bounds: ExpansionAtLeast f S d says $d\,\|x_1 - x_2\| \le \|f(x_1) - f(x_2)\|$ on $S$, i.e. $d \le \delta(f,S)$.

Strong approximation (Definition 2.4). $f$ strongly approximates $F$ in $x$ at $(x_0, y_0)$, written $f \approx_x F$ (Lean: StronglyApproxInX f F x₀ y₀), if for each $\varepsilon > 0$ there are neighborhoods $U$ of $x_0$ and $V$ of $y_0$ with

$$\big\|[F(x, y) - f(x)] - [F(x', y) - f(x')]\big\| \le \varepsilon \|x - x'\| \qquad (x, x' \in U,\ y \in V).$$

When $f$ is the partial derivative map $x \mapsto F_x(x_0,y_0)(x - x_0)$ this is strong partial Fréchet differentiability; in general $f$ may be piecewise linear or any map with a Lipschitzian inverse.

Formalization targets

Goal: Theorem 3.2 (p. 299)

Assume (a) $f \approx_x F$ at $(x_0, y_0)$; (b) for each $x \in \Xi$, $F(x, \cdot)$ is Lipschitzian on $H$ with modulus $\varphi$; (c) $f(\Xi)$ is a neighborhood of $0$ in $Z$; (d) $\delta(f, \Xi) =: d_0 > 0$. Then for each $\lambda > d_0^{-1}\varphi$ there are neighborhoods $U \subseteq \Xi$ of $x_0$, $V \subseteq H$ of $y_0$ and a function $x : V \to U$ with

$$x(y_0) = x_0, \qquad \|x(y_1) - x(y_2)\| \le \lambda \|y_1 - y_2\| \ (y_1, y_2 \in V), \qquad \{\xi \in U : F(\xi, y) = 0\} = \{x(y)\} \ (y \in V).$$

Every $\lambda$ strictly above $\varphi/d_0$ is claimed; $\lambda = \varphi/d_0$ is not.

Milestones

1. Lemma 3.1 (p. 298), the Lipschitz perturbation lemma: if $f$ maps $\Omega$ onto a ball $B(y_0, \alpha)$, $h$ is Lipschitzian with modulus $\eta < \delta := \delta(f, \Omega)$, $\Omega \supseteq B(x_0, \delta^{-1}\alpha)$ and $\theta := (1 - \eta\delta^{-1})\alpha - \|h(x_0)\| \ge 0$, then

$$(f + h)\big(B(x_0, \delta^{-1}\alpha)\big) \supseteq B(y_0, \theta), \qquad \delta(f + h, \Omega) \ge \delta - \eta > 0.$$

2. (3.1)–(3.2) in the proof of Theorem 3.2 (p. 300): for every $\varepsilon \in (0, d_0)$ there are $\alpha, \kappa > 0$ and a neighborhood $V \subseteq H$ of $y_0$ with $\Omega = B(x_0, d_0^{-1}\alpha) \subseteq \Xi$ such that for each $y \in V$

$$\delta(F(\cdot, y), \Omega) \ge d_0 - \varepsilon, \qquad F(\cdot, y)(\Omega) \supseteq B(0, \theta(y)) \supseteq B(0, \kappa),$$

where $\theta(y) = (1 - \varepsilon d_0^{-1})\alpha - \|F(x_0, y)\|$.

Significance

The result. Theorem 3.2 yields existence, local uniqueness and Lipschitz dependence of solutions of parametrized nonsmooth equations, with an explicit Lipschitz modulus arbitrarily close to $\varphi/d_0$. In the paper it underlies Theorem 3.3 and Corollary 3.4 (approximation and B-differentiation of the implicit function) and the sensitivity results of §4 for parametric variational inequalities over polyhedral convex sets. The same template, an equation approximated by a map with Lipschitzian inverse, is the basis of later strong-regularity and semismooth-Newton analyses in nonlinear programming and complementarity.

Formalizing it. The theorem is proved in the paper; it has not been machine-checked. The platform has the smooth implicit-function theorem (FamousTheorems.implicit_function_theorem, Rudin.ch09_implicit_function) and Mathlib has the contraction mapping principle, but there is no Lipschitz-inverse perturbation result and no notion of strong approximation. The mission produces both, together with the formal Theorem 3.2 that a follow-on mission (Theorem 3.3, Corollary 3.4, §4) would reference.

Difficulty

The obvious approach, differentiate and invert, is unavailable: $f$ need not have a derivative anywhere near $x_0$, so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of $F(\cdot, y)$ onto a ball uniformly in $y$ from information about $f$ alone. Injectivity transfers directly from $f$ through the small Lipschitz modulus of $F(\cdot, y) - f$; surjectivity does not, because $f$ carries no information about $F(\cdot, y)$ beyond the small Lipschitz modulus of the difference, and the domain ball, the image ball and the parameter neighborhood must be chosen once for all $y$. Completeness of $X$ is essential (the paper stresses this on p. 306) and is not available for $Y$ and $Z$.

Formalization scope

All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:

• Scalars are real; $X$ is a complete normed space ([CompleteSpace X]); $Y$, $Z$ are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.
• $\delta(f, S)$ via lower bounds. Every statement takes a real $d$ with ExpansionAtLeast f S d in place of "$d = \delta(f,S)$", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be $0$ on sets with fewer than two points.
• Total functions. $F$ is a curried total function F : X → Y → Z and $f : X \to Z$; hypotheses constrain them on $\Xi \times H$ only, and the conclusions keep the implicit function inside the domain: $U \subseteq \Xi$, $V \subseteq H$, $x(V) \subseteq U$. This makes explicit what the paper leaves implicit (its $F$ is only defined on $\Xi \times H$). Likewise $\Omega \subseteq \Xi$, used implicitly in the paper's proof, is a conclusion of milestone 2.
• Closed balls (Metric.closedBall), radii $\delta^{-1}\alpha$ written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.
• Lemma 3.1 keeps the paper's hypothesis that $\Omega$ is open, although Theorem 3.2's proof applies it to a closed ball.
• Milestone 2 states as an existence claim, for every $\varepsilon \in (0, d_0)$, the choices the paper makes at the start of its proof.

A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at $y = y_0$), in which $V$ may shrink to $\{y_0\}$, $\lambda$ is existential, or uniqueness is asserted outside $\Xi$, would be a different and trivial or false statement; the statements here rule these out.

Needed infrastructure: the contraction mapping principle on a closed subset of a complete space (Mathlib's ContractingWith), Lipschitz estimates on sets, and the two definitions of this mission. Lemma 3.1 is reusable for any Lipschitz-perturbation argument. Proofs of either milestone, or a direct proof of the goal, are welcome.

Selected references

• S. M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, 292–309. https://doi.org/10.1287/moor.16.2.292
• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 1980, 43–62. https://doi.org/10.1287/moor.5.1.43
• A. V. Dmitruk, A. A. Milyutin, N. P. Osmolovskii, Lyusternik's theorem and the theory of extrema, Russian Mathematical Surveys 1980, No. 6, 11–51 (as cited in Robinson 1991, p. 298).
• L. V. Kantorovich, G. P. Akilov, Functional Analysis, cited in Robinson 1991 as [17].

Motivation

A two-stage stochastic program with recourse models a decision taken in two steps: a first-stage decision is fixed before a random outcome is observed, and a second-stage (recourse) decision is chosen after the outcome is known, both subject to constraints and both incurring costs. The model is the standard framework for planning under uncertainty in operations research: capacity planning, production and inventory, energy dispatch, finance.

For linear recourse problems, duality was developed in the 1960s and early 1970s by Wets and others, partly under integrability restrictions on the random data. R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality (Pacific J. Math. 62 (1976), doi:10.2140/pjm.1976.62.173), treat the convex case, where every cost and constraint function is convex, by embedding the problem in a family of perturbed problems and applying the perturbational theory of convex duality (Rockafellar, Conjugate Duality and Optimization, SIAM 1974) together with the theory of convex integral functionals. The paper's dual variables are integrable price systems, interpreted as equilibrium prices for perturbations of the constraints; it is the starting point of a series of papers by the same authors on stochastic convex programming (relatively complete recourse, Kuhn–Tucker conditions, singular multipliers).

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. A vector $x_1\in\mathbb R^{n_1}$ is chosen subject to $x_1\in C_1$ and $f_{1i}(x_1)\le 0$ ($i=1,\dots,m_1$), at cost $f_{10}(x_1)$. Then $s\in S$ is observed and $x_2(s)\in\mathbb R^{n_2}$ is chosen subject to $x_2(s)\in C_2$ and $f_{2i}(s,x_1,x_2(s))\le 0$ ($i=1,\dots,m_2$), at cost $f_{20}(s,x_1,x_2(s))$. The aim is to minimize the expected cost

$$f_{10}(x_1)+\int_S f_{20}(s,x_1,x_2(s))\,\sigma(ds).$$

The standing assumptions are: $C_1$, $C_2$ convex, closed and nonempty; $f_{1i}$ and $f_{2i}(s,\cdot,\cdot)$ convex and finite everywhere; $s\mapsto f_{2i}(s,x_1,x_2)$ measurable, summable for $i=0$ and bounded for $i\ge 1$.

Decisions live in $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$ and perturbations in $U=\mathbb R^{m_1}\times\mathcal L^\infty_{m_2}$. The perturbation functional $F(x,u)$ is the expected cost if $x$ satisfies the constraints with right-hand sides $u_1$ and, almost surely, $u_2(s)$, and $+\infty$ otherwise. The problem $\mathbf P$ minimizes $F(x,0)$.

The space $Y=\mathbb R^{m_1}\times\mathcal L^1_{m_2}$ is paired with $U$ by $\langle u,y\rangle=u_1\cdot y_1+\int_S u_2(s)\cdot y_2(s)\,\sigma(ds)$, and $V=\mathbb R^{n_1}\times\mathcal L^1_{n_2}$ with $X$ in the same way. The Lagrangian is $L(x,y)=\inf_{u\in U}\{\langle u,y\rangle+F(x,u)\}$, the dual $\mathbf D$ maximizes $g(y)=\inf_{x\in X}L(x,y)$ over $y\in Y$, and the perturbation function is $\varphi(u)=\inf_{x\in X}F(x,u)$. Conjugates $\varphi^*$, $\varphi^{**}$ are taken with respect to the pairing of $U$ with $Y$.

Formalization targets

Goal: Theorem 3

If $C_1$ and $C_2$ are bounded, then

$$\min\mathbf P=\sup\mathbf D>-\infty,$$

and in fact $\varphi$ is a proper convex function on $U$, lower semicontinuous for the weak topology $\sigma(U,Y)$, the infimum defining $\varphi(u)$ is attained for every $u\in U$, and $\varphi^{**}=\varphi$. The goal is the theorem exactly as printed, all conclusions included.

Milestones

1. p. 174: for bounded measurable $x_1(\cdot)$, $x_2(\cdot)$, the functions $s\mapsto f_{2i}(s,x_1(s),x_2(s))$ are measurable, summable for $i=0$ and essentially bounded for $i\ge1$.
2. Proposition 3: $F$ is convex, not identically $+\infty$, and lower semicontinuous on $X\times U$ for the norm topology and for the weak topology induced by $V\times Y$.
3. (4.9): with $C_1,C_2$ bounded, $X_0=\{x: x_1\in C_1,\ x_2(s)\in C_2\text{ a.s.}\}$ is weakly compact in $X$, and $X_0'=\{x_2\in\mathcal L^\infty_{n_2}: x_2(s)\in C_2\text{ a.s.}\}$ is compact in $\sigma(\mathcal L^\infty_{n_2},\mathcal L^1_{n_2})$.
4. (4.1): $g(y)=\inf_{u}\{\langle u,y\rangle+\varphi(u)\}=-\varphi^*(-y)$.
5. (4.2): $\varphi^{**}(0)=\sup\mathbf D$.

The mission also poses the explicit form (1.8) of the Lagrangian and Corollary 1 (dual solutions are the negatives of subgradients of $\varphi$ at $0$; saddle-point characterization of primal solutions when $\partial\varphi(0)\ne\emptyset$).

Significance

Theorem 3 gives, for bounded constraint sets, the absence of a duality gap between a convex recourse problem with essentially bounded decisions and its Lagrangian dual over integrable multipliers, together with existence of an optimal decision. Through Corollary 1 it reduces the necessity of the Kuhn–Tucker (saddle-point) optimality conditions to the single question whether $\partial\varphi(0)$ is nonempty, and through the paper's later results it describes the directional derivatives of the optimal value with respect to perturbations of the constraints.

The result has been proved since 1976; it has not been machine-checked. A formal development produces the problem model on $\mathcal L^\infty$ and $\mathcal L^1$ spaces, the weak topologies of the pairings, and conjugate duality for extended-real-valued functions on such paired spaces, none of which is currently available as a ready-made Lean statement on this platform.

Difficulty

The obvious argument fails at two points. First, $\inf\mathbf P=\sup\mathbf D$ is $\varphi(0)=\varphi^{**}(0)$, and the biconjugate equals $\varphi$ only for a lower semicontinuous proper convex function in a topology compatible with the pairing. Lower semicontinuity of $\varphi$ in the norm topology of $U$ is not enough: the pairing is with $\mathcal L^1$, not with the norm dual of $\mathcal L^\infty$, so the relevant topology is the weak topology $\sigma(U,Y)$, and an infimum of lower semicontinuous functions is in general not lower semicontinuous. Second, the lower semicontinuity of $F$ itself, in the weak topology, is a statement about convex integral functionals on $\mathcal L^\infty$ that rests on measurability of the integrands in $s$ jointly with continuity in the decision variables. Boundedness of $C_1$, $C_2$ is what supplies the compactness that is otherwise missing.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ and the products $u_1\cdot y_1$, $u_2(s)\cdot y_2(s)$ are dot products. Constraint indices $i=1,\dots,m$ are Fin m.
• $\mathcal L^\infty_n$ and $\mathcal L^1_n$ are Mathlib's Lp (Fin n → ℝ) ⊤ σ and Lp (Fin n → ℝ) 1 σ, spaces of almost-everywhere classes; all second-stage conditions are stated almost surely. $\sigma$ is a probability measure (IsProbabilityMeasure).
• Values in $\mathbb R\cup\{\pm\infty\}$ are EReal; infima and suprema are lattice operations in EReal, so there are no junk values for empty or unbounded sets. Every sum has a real first summand, so no $\infty-\infty$ convention enters.
• The expected cost is a real Bochner integral; its integrand is summable for $x_2\in\mathcal L^\infty$ (milestone 1), so it is the true expected cost. No extended-real-valued function is ever integrated.
• A weak topology "induced by the pairing" is the coarsest topology making every functional of the pairing continuous; the product weak topology on $X\times U$ is the product of the two. These are passed explicitly. Replacing them by the norm topologies would make the lower semicontinuity statements strictly weaker and the compactness statement false; such a formalization does not count.
• An extended-real function is convex when its epigraph is convex, and proper when it never takes $-\infty$ and is somewhere finite.
• Boundedness of $C_1$, $C_2$ is assumed exactly where the paper assumes it: Theorem 3, (4.9) and Corollary 1.

A complete development needs the identification of $\mathcal L^\infty$ with the dual of $\mathcal L^1$ on a probability space (for weak-* compactness), lower semicontinuity of convex integral functionals, and conjugate duality on paired locally convex spaces. These are reusable well beyond this mission. Proofs of milestones, and of auxiliary lemmas of this kind as separate theorems, are welcome. The mission Stochastic Convex Programming: Basic Duality 2 formalizes the paper's other main result, on the first-stage problem and attainment of the recourse.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
• R. T. Rockafellar, Integrals which are convex functionals, II, Pacific Journal of Mathematics 39(2) (1971) 439–469. https://doi.org/10.2140/pjm.1971.39.439
• R. J.-B. Wets, Stochastic programs with fixed recourse: the equivalent deterministic program, SIAM Review 16(3) (1974) 309–339. https://doi.org/10.1137/1016053

Motivation

Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point $x$ has to satisfy $0 \in f(x) + \partial\psi_C(x)$. In applications the data $f$ depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation $f(p, x) = 0$ the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.

S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.

This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.

Setting

Let $X$ be a real normed linear space and $X'$ its topological dual, the continuous linear functionals on $X$. Let $C \subseteq X$ be closed and convex. The normal-cone operator of $C$ is

$$\partial\psi_C(x) = \begin{cases} \{y \in X' : y(c - x) \le 0 \text{ for all } c \in C\}, & x \in C, \\ \emptyset, & x \notin C. \end{cases}$$

A generalized equation is the inclusion $0 \in f(x) + \partial\psi_C(x)$, for a function $f$ from an open set $\Omega \subseteq X$ to $X'$. For $C = X$ it is the equation $f(x) = 0$. For $C$ the nonnegative orthant of $\mathbb R^n$ it is the nonlinear complementarity problem. For a general closed convex $C$ it is the variational inequality over $C$.

Let $x_0 \in \Omega$ solve the generalized equation, and let $f$ be Fréchet differentiable at $x_0$. Linearising $f$ gives the multifunction

$$T x = f(x_0) + f'(x_0)(x - x_0) + \partial\psi_C(x).$$

The generalized equation is strongly regular at $x_0$ with associated Lipschitz constant $\lambda$ if there are neighbourhoods $U$ of $0$ in $X'$ and $V$ of $x_0$ with the following property: for every $y \in U$ the inclusion $y \in Tx$ has exactly one solution $s(y)$ in $V$, and $\|s(y_1) - s(y_2)\| \le \lambda \|y_1 - y_2\|$ on $U$. The condition depends only on $f(x_0)$, $f'(x_0)$ and $C$.

In the parametric problem the function is $f(p, x)$, with $p$ in a topological space $P$ and base point $p_0$. Its partial derivative in $x$ is $f'(p, x)$.

Formalization targets

Goal: Theorem 2.1 (p. 45)

Assume that $f'$ exists on $P \times \Omega$, that $f$ and $f'$ are continuous at $(p_0, x_0)$, and that $x_0$ solves $0 \in f(p_0, x) + \partial\psi_C(x)$, strongly regularly with constant $\lambda$. Then for every $\varepsilon > 0$ there are neighbourhoods $N_\varepsilon$ of $p_0$ and $W_\varepsilon$ of $x_0$, and a function $x : N_\varepsilon \to W_\varepsilon$, with two properties. First, $x(p)$ is the unique solution in $W_\varepsilon$ of $0 \in f(p, x) + \partial\psi_C(x)$. Second,

$$\|x(p) - x(q)\| \le (\lambda + \varepsilon)\,\|f(p, x(q)) - f(q, x(q))\| \qquad (p, q \in N_\varepsilon).$$

Milestones: the steps of the proof (p. 46)

Write $L$ for the linearisation at $(p_0, x_0)$, $r(p, x) = f(p_0, x_0) + f'(p_0, x_0)(x - x_0) - f(p, x)$ for the residual, and $\Phi_p(x) = V \cap L^{-1}[r(p, x)]$. The milestones are four claims of the proof:

1. On the closed ball $V_\varepsilon$, the fixed points of $\Phi_p$ are exactly the solutions of the perturbed inclusion.
2. $\|\Phi_p(x_1) - \Phi_p(x_2)\| \le \lambda\delta \|x_1 - x_2\|$ on $V_\varepsilon$.
3. $\Phi_p$ maps $V_\varepsilon$ into itself.
4. The contraction principle on $V_\varepsilon$, with the bound $\|x(p) - x\| \le (1 - \lambda\delta)^{-1} \|\Phi_p(x) - x\|$ (2.5).

Companion results

• Corollary 2.2 (pp. 46–47). If $P$ lies in a normed space and $\|f(p, x) - f(q, x)\| \le \nu \|p - q\|$, then $x(\cdot)$ is Lipschitzian with modulus $\nu(\lambda + \varepsilon)$.
• Theorem 2.3 (p. 47). Let $\Phi_p(x_0)$ be the unique local solution of the linear generalized equation $0 \in f(p, x_0) + f'(p_0, x_0)(x - x_0) + \partial\psi_C(x)$. Then $\|x(p) - \Phi_p(x_0)\| \le \alpha_\varepsilon(p)\|p - p_0\|$, with $\alpha_\varepsilon(p) \to 0$.
• Theorem 2.4 (p. 48). This is a perturbation lemma for linear generalized equations $0 \in Ax + a + \partial\psi_C(x)$. Near $(A_0, a_0)$ the localised inverse stays single-valued, and it is Lipschitzian with modulus $\lambda(1 - \lambda\|A - A_0\|)^{-1}$.
• The case $C = X$ (remark on p. 45). There strong regularity is equivalent to $f'(x_0)$ having a continuous linear inverse.
• Strong regularity is the weakest possible condition (remark on p. 47). For the canonical perturbation $f(p,x) = f(x_0) + f'(x_0)(x - x_0) - p$, $p \in X'$, locally unique solvability with a Lipschitzian solution map $x(\cdot)$ near $p_0 = 0$ is exactly strong regularity at $x_0$.

Significance

Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at $x_0$, the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.

The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for $C^1$ maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of $X$.

Difficulty

The obvious approach is to apply the classical implicit-function theorem. It fails because $x \mapsto f(x) + \partial\psi_C(x)$ is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood $V$ and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: $\delta$ from $\varepsilon$, then $U$ and $V$, then the ball radius $\rho$, then the parameter neighbourhood. The estimate (2.4) has to come out with the constant $\lambda + \varepsilon$ and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of $X$, for example through the completeness of $X'$.

Formalization scope

• $X'$ is StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off $C$, and an inclusion $0 \in f(x) + \partial\psi_C(x)$ is written $-f(x) \in \partial\psi_C(x)$.
• Strong regularity is a predicate on $(C, f(x_0), f'(x_0), x_0, \lambda)$ with real $\lambda$. It requires existence, uniqueness in $V$ and the Lipschitz bound.
• $f$ is a total function $P \times X \to X'$ whose values off $P \times \Omega$ carry no hypothesis. The conclusion therefore asserts $W_\varepsilon \subseteq \Omega$.
• Differentiability is HasFDerivAt at every point of $\Omega$, for every $p$. Continuity of $f'$ at $(p_0, x_0)$ is joint and in operator norm.
• Uniqueness is uniqueness within $W_\varepsilon$, never global. Global uniqueness is false in general. Dropping uniqueness, or quantifying $\varepsilon$ after the neighbourhoods, would trivialize the goal, and the statements are written to exclude both.
• Theorem 2.1, Corollary 2.2 and Theorem 2.3 do not assume completeness, as printed. Theorem 2.4 assumes a Banach space, as printed.
• The contraction-principle milestone assumes completeness, under which the principle as invoked holds.
• Corollary 2.2 asks for its Lipschitz hypothesis on $N_\varepsilon \times V_\varepsilon$, sets that Theorem 2.1 produces. It is therefore stated on fixed neighbourhoods given in advance.
• Theorem 2.4 also asserts $\lambda\|A - A_0\| < 1$, which its proof secures.

A complete development needs the following:

• the mean-value inequality for Fréchet-differentiable maps on convex sets;
• the contraction principle on a closed ball;
• a fixed-point argument that obtains the fixed point through the complete space $X'$.

The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1):43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3

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

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$. Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$, and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

$$\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}$$

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$, the derivatives $G_i'(v)$, $i\in I(v)$, are linearly independent in $V^*$.

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$, and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

$$F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,$$ $$\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.$$

Milestones, in the order of the paper's proof

1. (3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$; no regularity needed).
2. (3.16): at a regular feasible point $v$, every $h$ with $\langle G_i'(v),h\rangle=0$ ($i\le p$) and $\langle G_i'(v),h\rangle\ge0$ ($i>p$, $i\in I(v)$) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$.
3. Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$.
4. Lemma 3.3: an $\varepsilon$-Farkas–Minkowski lemma in $V^*$: if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$, then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$.

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$, $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$, then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$.

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$, but that function is not differentiable at $v_\varepsilon$, so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$; closing this gap requires the regularity assumption and completeness of $V$, and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$, must be turned into an approximate multiplier representation in $V^*$, an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

• $V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
• Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$, an equality constraint iff its index is $<p$. p ≤ m is assumed in the goal.
• $C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
• No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and "$F(v)\le\inf_{\mathcal C}F+\varepsilon^2$" is "$F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$". A real infimum over an empty or unbounded set would be a junk value.
• Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ($\inf\emptyset=+\infty$) while the conclusion asks for a feasible point.
• Lemma 3.3 is stated with $\le\varepsilon$. The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$, no constraints and $w^*=\varepsilon\,\mathrm{id}$; its proof gives $\le$, and Theorem 3.1 uses $\le$.
• Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
• Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$, so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$, and a closedness result for finitely generated cones in $V^*$.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974) 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979) 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700