Functional Analysis

Motivation

Monotone operators from a Banach space $E$ to its dual $E^*$ are the abstract framework for nonlinear equations, variational inequalities and evolution equations, and for the convergence theory of proximal-point and splitting algorithms in infinite dimensions. Within that framework, the class that behaves well — for surjectivity results, for resolvents, for sums — is the class of maximal monotone operators. The most important source of such operators is convex analysis: the subdifferential of a convex function. Whether every subdifferential of a closed proper convex function is maximal monotone, in an arbitrary Banach space, is therefore a basic question for convex optimization in function spaces.

Timeline:

• 1964. G. J. Minty proves maximality of the subdifferential for convex functions that are finite and continuous everywhere (Minty, Pacific J. Math. 14 (1964)).
• 1965. A. Brøndsted and R. T. Rockafellar show that subgradients exist on a dense set and approximate ε-subgradients (Brøndsted–Rockafellar, Proc. AMS 16 (1965)). J.-J. Moreau develops proximal maps and conjugate duality for convex functions in Hilbert space (Moreau, Bull. SMF 93 (1965)); his later lecture notes Fonctionnelles convexes (Collège de France, 1967) are the paper's reference for conjugates in locally convex spaces.
• 1966. R. T. Rockafellar announces the general Banach-space result, for every lower semicontinuous proper convex function (Rockafellar, Pacific J. Math. 17 (1966)). H. Brézis later points out a gap in that proof: a subgradient chosen in the argument may grow without bound.
• 1970. Rockafellar gives a complete proof by a different route, valid in nonreflexive spaces, in the paper formalized here (Rockafellar, Pacific J. Math. 33 (1970)).

Setting

Let $E$ be a real Banach space with dual $E^*$ and bidual $E^{**}$, and write $\langle x, x^*\rangle = x^*(x)$. $E$ sits in $E^{**}$ through the canonical embedding.

A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$, not identically $+\infty$, such that $f((1-\lambda)x + \lambda y) \le (1-\lambda) f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$. It is lower semicontinuous for the norm topology.

The subdifferential of $f$ is the multivalued map $\partial f : E \to E^*$,

$$\partial f(x) = \{\, x^* \in E^* \mid f(y) \ge f(x) + \langle y - x, x^* \rangle \ \ \forall y \in E \,\}.$$

A multivalued map $T : E \to E^*$ is monotone if $\langle x_0 - x_1, x_0^* - x_1^* \rangle \ge 0$ whenever $x_0^* \in T(x_0)$ and $x_1^* \in T(x_1)$. It is maximal monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other monotone map $T' : E \to E^*$.

The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} \{\langle x, x^*\rangle - f(x)\}$, a function on $E^*$; its subdifferential $\partial f^*$ maps $E^*$ into $E^{**}$. Finally $j(x) = \tfrac12 \|x\|^2$.

In Lean these are ProperConvex f, subdiff f, IsMonotoneOp T, IsMaximalMonotone T, conj f and halfSqNorm, all stated over an arbitrary real normed space V so that they apply equally to $E$ and to $E^*$.

Formalization targets

Goal: Theorem A (p. 210)

$$f \text{ lower semicontinuous proper convex on } E \quad\Longrightarrow\quad \partial f : E \to E^* \text{ is maximal monotone.}$$

No reflexivity, inner product or finite dimension is assumed.

Milestones, in attack order

1. (2.2) Fenchel–Young: $f(x) + f^*(x^*) \ge \langle x, x^* \rangle$, with equality iff $x^* \in \partial f(x)$.
2. §2, p. 210. $f^*$ is a weak* lower semicontinuous (hence strongly lower semicontinuous) proper convex function on $E^*$.
3. §2, p. 211. The restriction of $f^{**}$ to $E$ is $f$.
4. Proposition 1. $x^{**} \in \partial f^*(x^*)$ iff there are a net $x_i^* \to x^*$ in norm and a bounded net $x_i \to x^{**}$ weak**, on one directed index set, with $x_i^* \in \partial f(x_i)$.
5. (3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for all $x \in E$.
6. §3, p. 213. $(f + j)^*$ is finite and continuous throughout $E^*$.
7. §3, p. 213 (Minty). On any real Banach space, a convex function that is finite and continuous everywhere has a maximal monotone subdifferential.

Significance

Theorem A places every closed proper convex function in the maximal monotone class, in every real Banach space. Downstream, it is what allows convex minimization problems to be treated by the general theory: surjectivity of $\partial f + \lambda J$ (with $J$ the duality map) in reflexive spaces, existence for evolution equations governed by subdifferentials, the definition of resolvents and proximal maps, and the convergence of proximal-point and splitting methods for convex problems. Proposition 1 is of independent interest: in a nonreflexive space $\partial f^*$ is not the inverse of $\partial f$, but it is still completely determined by $\partial f$ through bounded weak** nets.

The theorem is classical and fully proved in the literature. What this mission adds is a machine-checked proof of the nonreflexive Banach-space statement, together with the infrastructure it needs: extended-real-valued proper convex functions, the subdifferential and the conjugate on a normed space and its dual, monotone and maximal monotone operators, and the Fenchel–Moreau identity $f^{**}|_E = f$. None of these exists in Mathlib at the pinned revision, and Mathlib contains no statement of Theorem A, in Hilbert or in Banach spaces.

Difficulty

Monotonicity of $\partial f$ follows in two lines from the definition; the whole difficulty is maximality. In a Hilbert space the standard argument solves $x + \partial f(x) \ni y$ by minimizing $f + \tfrac12\|\cdot - y\|^2$ and uses the identification of $E$ with $E^*$; in a general Banach space there is no such identification, and minimizers need not exist without reflexivity. The 1966 argument tried to approximate subgradients of $f$ at nearby points, and it failed because those subgradients could become unbounded as the approximation was refined. Any argument that passes through the dual meets a second obstacle: $\partial f^*$ takes values in the bidual $E^{**}$, which is strictly larger than $E$ when $E$ is not reflexive, so $\partial f^*$ is not the inverse of $\partial f$. Relating the two is the content of Proposition 1, and its necessity half requires approximation results well beyond the definitions.

Formalization scope

Lean representation and committed conventions:

• $E$ is a real Banach space: NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E. $E^*$ is StrongDual ℝ E with the operator norm; the pairing $\langle x, x^*\rangle$ is x' x; $E^{**}$ is StrongDual ℝ (StrongDual ℝ E) and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual ℝ E.
• The value set $(-\infty,+\infty]$ is EReal with the clause "never $\bot$". Properness also requires some value $\ne \top$. Convexity is the paper's inequality for $0 < \lambda < 1$, computed in EReal.
• Multivalued maps are V → Set (StrongDual ℝ V). Maximality is graph inclusion, quantified over every monotone T', not only over subdifferentials.
• The conjugate is an EReal supremum over all of $V$; the biconjugate is conj (conj f) on the bidual.
• (2.2) is stated as $\langle x, x^*\rangle \le f(x) + f^*(x^*)$ with the equality case, avoiding EReal subtraction.
• Weak* lower semicontinuity of $f^*$ is lower semicontinuity on WeakDual ℝ E.
• In Proposition 1 a net is a map from a nonempty, directed, partially ordered index type (in the universe of $E$), with convergence along atTop. Weak** convergence is pointwise convergence on $E^*$ of the canonical images, which is convergence in the weak topology induced on $E^{**}$ by $E^*$. Boundedness is a uniform norm bound.
• (3.1) reads the printed $\partial(f+j)$ as $\partial(f+j)(x)$; the right side is the pointwise (Minkowski) set sum.
• "Finite and continuous" for $(f+j)^*$ is the existence of a continuous real-valued $h$ on $E^*$ equal to it everywhere.
• Minty's case is stated for an arbitrary real Banach space $V$, because the proof applies it on $E^*$.

A trivializing formalization is ruled out: properness excludes $f \equiv +\infty$ (whose empty subdifferential is monotone but not maximal) and $-\infty$ values, maximality ranges over all monotone operators, and the index set in Proposition 1 is nonempty and directed so that no convergence statement holds vacuously.

Infrastructure needed and reusable beyond this mission: extended-real convex analysis on normed spaces (conjugates, the Fenchel–Moreau theorem via Hahn–Banach separation, lower semicontinuity in the weak and weak* topologies), subdifferential calculus for a sum with a continuous function, nets and weak** approximation in the bidual (Goldstine-type arguments), and the Brøndsted–Rockafellar approximation of ε-subgradients. Contributions are welcome at every milestone; the definitions layer and milestones 1–3 are the natural starting points.

Selected references

• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific Journal of Mathematics 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific Journal of Mathematics 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
• G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific Journal of Mathematics 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• A. Brøndsted and R. T. Rockafellar, On the subdifferentiability of convex functions, Proceedings of the American Mathematical Society 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8

Motivation

Many problems in signal processing, statistics and operations research ask to minimize a sum $\Theta = \Phi + \Psi$ of a nonsmooth convex term $\Phi$ (a constraint indicator, an $\ell^1$ penalty) and a smooth term $\Psi$. The standard method is the forward-backward (proximal-gradient) algorithm: an explicit gradient step on $\Psi$ followed by a proximal step on $\Phi$. Its classical convergence theory requires $\Psi$ to be convex and the step size to stay below $2/L_\Psi$, where $L_\Psi$ is the Lipschitz constant of $\nabla\Psi$.

Attouch, Peypouquet and Redont (authors' manuscript of SIAM J. Optim. 24 (2014)) derive an inertial forward-backward algorithm (IFB) as a time discretization of a second-order dissipative dynamical system with Hessian-driven damping. The added inertial terms cost essentially nothing to compute, yet they allow step sizes beyond $2/L_\Psi$ and a smooth part $\Psi$ that is not convex, provided the sum $\Theta$ is.

Timeline of the relevant results:

• Heavy-ball-with-friction methods, the inertial discretizations of $\ddot u + \alpha\dot u + \nabla\Phi(u) = 0$, were introduced by Polyak (1964) and developed by Alvarez and Attouch (2001) for proximal schemes.
• Hessian-driven damping for one potential: Alvarez, Attouch, Bolte and Redont (2002); for a nonsmooth potential plus a smooth one, the continuous dynamics underlying (IFB): Attouch, Maingé and Redont (2012).
• The discrete algorithm (IFB) and its weak convergence in Hilbert spaces: Attouch, Peypouquet and Redont (2014), the paper of this mission.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. Let $\Phi : H \to \mathbb R\cup\{+\infty\}$ and $\Psi : H \to \mathbb R$, and write $\Theta = \Phi + \Psi$ and $\mathcal S = \operatorname{Argmin}\Theta$. A vector $g$ is a subgradient of $\Phi$ at $u$, written $g \in \partial\Phi(u)$, if $\Phi(u) < +\infty$ and $\Phi(u) + \langle g, v - u\rangle \le \Phi(v)$ for all $v$.

Hypothesis H fixes positive constants $L_\Psi$, $a$, $b$ and a step size $\lambda$ with:

• $H_\Phi$: $\Phi$ is proper, lower semicontinuous and convex;
• $H_\Psi$: $\Psi$ is differentiable and $\nabla\Psi$ is $L_\Psi$-Lipschitz;
• $H_\lambda$: $0 < \lambda < \Lambda = \min\{1/a,\ 2(a+b)/(bL_\Psi)\}$;
• $H_\Theta$: $\Theta$ is convex and bounded from below.

Algorithm (IFB). From any $(u_0, y_0) \in H \times H$, compute for $k \ge 0$

$$0 \in \frac{u_{k+1}-u_k}{\lambda} + \partial\Phi(u_{k+1}) + a u_k - b y_k, \qquad 0 = \frac{y_{k+1}-y_k}{\lambda} + \nabla\Psi(u_{k+1}) - a u_{k+1} + b y_{k+1}.$$

A sequence $u_k$ converges weakly to $p$, written $u_k \rightharpoonup p$, if $\langle u_k, v\rangle \to \langle p, v\rangle$ for every $v \in H$. The analysis uses the velocity $\xi_k = u_k - u_{k-1}$, the energy $E_k = \Theta(u_k) + \gamma\|\xi_k\|^2$ with $\gamma = (1-a\lambda)/(2b\lambda^2)$, and two auxiliary real sequences $G_k(q)$ and $F_k(q)$, defined from $u$, $y$ and a reference point $q$ by (17) and (18) of the paper.

Formalization targets

Goal: Theorem 1

Under Hypothesis H, for every sequence generated by (IFB),

$$\lim_{k\to\infty}\Theta(u_k) = \inf\Theta;$$

if $\mathcal S \ne \emptyset$ and one of (i) $\mathcal S$ is a singleton, (ii) $\Phi$ is differentiable with weak-to-weak sequentially continuous gradient, (iii) $\nabla\Psi$ is weak-to-weak sequentially continuous, (iv) $\Psi$ is convex, holds, then

$$u_k \rightharpoonup p \quad\text{for some } p \in \mathcal S;$$

and if $\mathcal S = \emptyset$, then $\|u_k\| \to +\infty$.

Milestones

In the order of the paper's argument: Proposition 2 (energy decrease, $\sum\|\xi_k\|^2 < \infty$); Proposition 3 (the identity and inequality (19) for $F_k(q)$); Proposition 4 ($G_k(q)$ is bounded above for $q\in\operatorname{dom}\Phi$); the lower bound (28) on $F_k(q)$; Lemma 5 (a real-sequence lemma); Proposition 6 ($\Theta(u_k)\to\inf\Theta$, weak cluster points lie in $\mathcal S$); Lemma 7 (a boundedness lemma); Proposition 8 (boundedness of $(u_k)$ and convergence of $F_k(q)$ when $\mathcal S \ne\emptyset$).

Significance

The result gives convergence of a forward-backward type method under a step-size bound $\Lambda$ that can be made arbitrarily large by choosing $a$ small, and for a smooth term $\Psi$ that need not be convex. The special case $\Phi = \delta_C$ (indicator of a closed convex set) yields an inertial gradient-projection method, and the paper applies the theorem to feasibility problems, the CQ algorithm, Pareto fronts and $\ell^1$ signal recovery.

The theorem is proved in the paper; to our knowledge it is not formalized anywhere. A complete formalization would provide a machine-checked Liapunov analysis of an inertial proximal method in an infinite-dimensional Hilbert space, including the passage from a minimizing sequence to weak convergence. The milestones Proposition 2, 3 and 8 are energy estimates that also underlie other inertial and proximal schemes.

Difficulty

The energy $E_k$ controls the values $\Theta(u_k)$ and the velocities $\xi_k$, but not the iterates themselves. The first idea, proving that $\|u_k - q\|$ is nonincreasing for every $q \in \mathcal S$ (Fejér monotonicity, the standard route for the classical forward-backward method), does not come out of the energy estimates for (IFB): the inertial variable $y_k$ couples consecutive steps, and the distance to a minimizer is not a Liapunov function. The paper's replacement, the sequence $F_k(q)$, carries the auxiliary sum $G_k(q)$, whose upper bound already requires the full Hypothesis H. Because $H$ is infinite-dimensional, bounded sequences have only weakly convergent subsequences, so the minimizing property has to pass through weak lower semicontinuity of $\Theta$, and the final step, uniqueness of the weak cluster point, needs a separate argument in each of the cases (i)–(iv) together with Opial's lemma, which is not in Mathlib.

Formalization scope

• $H$ is a general real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); nothing is specialized to finite dimension.
• $\Phi$ and $\Theta$ take values in EReal. Properness excludes $-\infty$. Convexity of an extended-valued function is convexity of its epigraph in $H\times\mathbb R$, because Mathlib's ConvexOn needs a scalar action that EReal lacks. The subgradient predicate requires $\Phi(u) < +\infty$, so $\partial\Phi(u) = \emptyset$ off $\operatorname{dom}\Phi$.
• (IFB) is encoded as the subgradient inclusion, not through the proximity operator. Weak convergence is convergence of all inner products $\langle u_k, v\rangle$; weak cluster points are weak limits along strictly increasing subsequences.
• $L_\Psi > 0$ is assumed (harmless: a Lipschitz gradient is Lipschitz with every larger constant). The step size $\lambda$ is written lam.
• $\xi_k$, $z_k$, $E_k$, $G_k$, $F_k$ are defined on all natural indices, and each statement quantifies $k \ge 1$ (or $k \ge 2$ for $G_k$) as the paper does. Energies and values are never truncated to real numbers, so no statement becomes true through the convention EReal.toReal ⊤ = 0.
• Deviation from the printed text: Proposition 4 is printed under $H_\Phi$ and $H_\Psi$ only, but its proof invokes Proposition 2, which needs all of Hypothesis H, and the printed statement is false for step sizes above $\Lambda$ (e.g. $H=\mathbb R$, $\Phi = x^2/2$, $\Psi = 3x^2/2$, $a=2$, $b=0.02$, $\lambda = 10$). The milestone is stated under the full Hypothesis H.
• A formalization in which $\partial\Phi(u)$ is nonempty at points of infinite value, in which the energy is converted to a real number, or in which Hypothesis H cannot be satisfied, would make these statements trivial or vacuous, and is ruled out by the definitions above.

A complete development needs Opial's lemma, weak sequential compactness of bounded sets in Hilbert space, weak lower semicontinuity of lower semicontinuous convex functions, the descent lemma for functions with Lipschitz gradient, and monotonicity of the subdifferential. These are reusable well beyond this mission; contributions of any of them, and of the milestones in any order, are welcome.

Selected references

• H. Attouch, J. Peypouquet, P. Redont, A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization, SIAM J. Optim. 24(1), 2014 (statements cited from the authors' manuscript of Aug 2013). https://doi.org/10.1137/130910294
• H. Attouch, P.-E. Maingé, P. Redont, A second-order differential system with Hessian-driven damping; application to non-elastic shock laws, Differential Equations and Applications 4(1), 2012. https://doi.org/10.7153/dea-04-02
• F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Analysis 9, 2001. https://doi.org/10.1023/A:1011253113155
• F. Alvarez, H. Attouch, J. Bolte, P. Redont, A second-order gradient-like dissipative dynamical system with Hessian-driven damping, J. Math. Pures Appl. 81(8), 2002. https://doi.org/10.1016/S0021-7824(01)01253-3
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0

Motivation

Many problems in convex optimization, variational inequalities and signal processing reduce to finding a zero of a sum of three monotone operators, one of which is single-valued and smooth. Davis and Yin (Set-Valued Var. Anal. 25, 2017) introduced a splitting scheme that evaluates each of the three operators separately: the two set-valued ones through their resolvents, the single-valued one through a forward step. With a fixed stepsize, their Algorithm 1 converges weakly but can be slow: the paper's Section 3.4 constructs examples where the squared distance of the iterates to the solution decays no faster than $(k+1)^{-(1+\epsilon)}$ for every $\epsilon > 0$.

When one of the operators is strongly monotone (for example the subdifferential of a strongly convex function), first-order splitting methods can be accelerated by letting the stepsize shrink like $1/k$; the paper relates its stepsizes to those of Chambolle and Pock's accelerated primal–dual method (J. Math. Imaging Vis. 40, 2011, Algorithm 2) and of Boţ, Csetnek, Heinrich and Hendrich (Math. Program. 150, 2015, Algorithm 5). Section 3.3 of Davis–Yin carries this device over to three-operator splitting and obtains an $O(1/(k+1)^2)$ rate for the squared distance. This mission formalizes that result.

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A : H \to 2^H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ for all $u \in Ax$, $v \in Ay$, and maximal monotone if its graph is not properly contained in the graph of another monotone operator. It is $\mu$-strongly monotone if $\langle x - y, u - v\rangle \ge \mu\|x-y\|^2$ for all such pairs. A single-valued $C : H \to H$ is $\beta$-cocoercive if $\beta\|Cx - Cy\|^2 \le \langle Cx - Cy, x - y\rangle$, and $L_C$-Lipschitz if $\|Cx - Cy\| \le L_C\|x - y\|$.

The problem is to find $x^* \in \operatorname{zer}(A + B + C)$, that is, $0 \in Ax^* + Bx^* + Cx^*$, where $A$, $B$ are maximal monotone and $C$ is monotone and single-valued. For $\gamma > 0$ the resolvent $J_{\gamma A} = (I + \gamma A)^{-1}$ is the map with $x \in J_{\gamma A}x + \gamma A(J_{\gamma A}x)$.

Algorithm 3 fixes stepsizes $(\gamma_k)_{k\ge 0} \subseteq (0,\infty)$ and an initial point $x_A^0 \in H$, sets $x_B^0 = J_{\gamma_0 B}(x_A^0)$, $u_B^0 = \gamma_0^{-1}(x_A^0 - x_B^0)$, and iterates for $k \ge 0$

$$x_B^{k+1} = J_{\gamma_k B}(x_A^k + \gamma_k u_B^k),\quad u_B^{k+1} = \tfrac{1}{\gamma_k}(x_A^k + \gamma_k u_B^k - x_B^{k+1}),\quad x_A^{k+1} = J_{\gamma_{k+1}A}(x_B^{k+1} - \gamma_{k+1}u_B^{k+1} - \gamma_{k+1}Cx_B^{k+1}).$$

The stepsize changes in the middle of an iteration. Two stepsize rules are considered, each defined recursively from $\gamma_0$:

$$\text{(3.6)}\quad \gamma_{k+1} = \frac{-2\gamma_k^2\mu_C\eta + \sqrt{(2\gamma_k^2\mu_C\eta)^2 + 4(1+2\gamma_k\mu_B)\gamma_k^2}}{2(1+2\gamma_k\mu_B)}, \qquad \text{(3.7)}\quad \gamma_{k+1} = \frac{\gamma_k}{\sqrt{1 + 2\gamma_k(\mu_B - \gamma_kL_C^2/2)}}.$$

Formalization targets

Goal: Theorem 3.3, both parts

Let $B$ be $\mu_B$-strongly monotone with $\mu_B \ge 0$.

1. If $C$ is $\beta$-cocoercive and $\mu_C$-strongly monotone ($\mu_C > 0$), $\eta \in (0,1)$, $\gamma_0 \in (0, 2\beta(1-\eta))$ and the stepsizes follow (3.6), then for every $x^* \in \operatorname{zer}(A+B+C)$

$$\exists K\ \forall k \ge 0:\quad \|x_B^k - x^*\|^2 \le \frac{K}{(k+1)^2}.$$

2. If $C$ is $L_C$-Lipschitz, $\mu_B > 0$, $\gamma_0 \in (0, 2\mu_B/L_C^2)$ and the stepsizes follow (3.7), the same conclusion holds.

The goal asserts the shape of the rate only; the constant $K$ is not fixed.

Milestones

• Proposition 3.1, Parts 1 and 2: the one-step inequalities (3.9) and (3.10) for Algorithm 3 with arbitrary admissible stepsizes.
• Stepsize facts from the proof of Theorem 3.3: the identities that make (3.9) and (3.10) telescope, the monotonicity of the stepsizes (3.6), and the limits $(k+1)\gamma_k \to 1/(\mu_C\eta + \mu_B)$ for (3.6) and $(k+1)\gamma_k \to 1/\mu_B$ for (3.7).

Significance

The theorem shows that strong monotonicity of $B$ or $C$ can be converted into a quadratically decaying distance bound without knowledge of the solution, with stepsizes that are computable from the strong monotonicity and cocoercivity (or Lipschitz) constants alone. Since the rate is established for $x_B^k$, it applies directly to splitting schemes for strongly convex composite problems $\min f + g + h$ with $h$ smooth, where $x_B^k$ is the proximal point of $g$.

The result is proved in the paper; no machine-checked version is known. The formalization adds a precise statement of the admissible parameter ranges, a check of the index conventions of a scheme whose stepsize changes mid-iteration, and a correction of the one-step inequalities at the first iteration (see Formalization scope). The stepsize limits are statements about explicit real recursions and are of independent use for other accelerated schemes.

Difficulty

The one-step inequalities (3.9) and (3.10) are long but elementary chains of inner-product identities and Young's inequality; the work lies in bookkeeping two stepsizes per iteration. The rate itself does not follow from the one-step inequality alone: telescoping gives a bound of the form $\|x_B^{k}-x^*\|^2 \lesssim \gamma_k^2$, and one must then show $\gamma_k$ decays exactly like $1/k$. The rules (3.6) and (3.7) are nonlinear recursions without closed form, so their asymptotics require a Stolz–Cesàro type argument, which is not available in Mathlib under that name. Choosing a stepsize sequence of the form $c/k$ instead is a different algorithm and not covered by the theorem.

Formalization scope

• $H$ is an arbitrary real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not a Euclidean space.
• Resolvents are not constructed. They are families JA JB : ℝ → H → H required to satisfy the resolvent inclusion $\gamma^{-1}(x - J(\gamma)x) \in A(J(\gamma)x)$ for every $\gamma > 0$; for maximal monotone operators such maps exist and are unique, so nothing is lost.
• Algorithm 3 is a single recursive definition of the triple $(x_A^k, x_B^k, u_B^k)$ from $x_A^0$, the stepsizes, the resolvent families and $C$; the paper's loop index $k = 1, 2, \dots$ matches recursion (3.8) shifted by one.
• The stepsize rules (3.6) and (3.7) are recursive real sequences, used verbatim; each theorem assumes the paper's parameter ranges.
• $O(1/(k+1)^2)$ is rendered as $\exists K\,\forall k,\ \|x_B^k - x^*\|^2 \le K/(k+1)^2$, with $K$ chosen after all data (initial point, operators, constants, $\gamma_0$, $x^*$) and before $k$. No explicit constant is stated.
• Strong monotonicity of $C$ means $\mu_C > 0$; only $\mu_B = 0$ is allowed, as on the page. With $\mu_B = \mu_C = 0$ rule (3.6) keeps $\gamma_k$ constant and the rate fails, so a formalization allowing $\mu_C = 0$ would be false. In Part 2, $L_C > 0$ is assumed so that the stepsize interval is meaningful, and $C$ is assumed monotone, as in problem (1.1) and as used in the paper's proof of (3.10).
• The paper states (3.9) and (3.10) for all $k \ge 0$; at $k = 0$ the initial point $x_A^0$ is not a resolvent output, and both inequalities fail in general. The milestones state them for $k \ge 1$. Theorem 3.3 is unaffected, since finitely many initial terms do not change an $O(\cdot)$ bound.
• The display $\gamma_k^2 - \gamma_{k+1}^2 = \gamma_k\gamma_{k+1}(2\gamma_k\mu_B + 2\gamma_{k+1}\mu_C\eta)$ on p. 845 has $\gamma_k$ and $\gamma_{k+1}$ swapped inside the bracket; the milestone states the corrected identity $\gamma_k\gamma_{k+1}(2\gamma_{k+1}\mu_B + 2\gamma_k\mu_C\eta)$.
• A trivializing formalization, such as one in which the resolvent hypothesis is unsatisfiable, the stepsize interval is empty, or the rate constant may depend on $k$, is ruled out: the hypotheses are met by $A = 0$, $B = \mu_B I$ (with resolvents $J_{\gamma A} = I$, $J_{\gamma B} = (1+\gamma\mu_B)^{-1}I$) and $C = cI$ with $c > 0$, and $K$ is quantified before $k$.

Contributions are welcome at every level: proofs of the real-sequence milestones (a general Stolz–Cesàro lemma would be reusable well beyond this mission), of the two one-step inequalities, and of the telescoping argument that assembles the goal.

Selected references

• D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017), 829–858. https://doi.org/10.1007/s11228-017-0421-z (preprint: https://arxiv.org/abs/1504.01032)
• R. I. Boţ, E. R. Csetnek, A. Heinrich and C. Hendrich, On the convergence rate improvement of a primal-dual splitting algorithm for solving monotone inclusion problems, Mathematical Programming 150 (2015), 251–279. https://doi.org/10.1007/s10107-014-0766-0
• A. Chambolle and T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, Journal of Mathematical Imaging and Vision 40 (2011), 120–145. https://doi.org/10.1007/s10851-010-0251-1
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

Support vector machines (SVMs) are trained by solving a regularized empirical risk minimization problem over a reproducing kernel Hilbert space (RKHS) — a space that is typically infinite-dimensional. On its face, this looks computationally hopeless: how can a computer search an infinite-dimensional space for a minimizer? The representer theorem is the result that makes SVM training tractable at all: it shows that no matter how large the RKHS is, the minimizer of the SVM objective for a sample of size $n$ always lies in the $n$-dimensional subspace spanned by the kernel evaluated at the $n$ sample points. This turns an infinite- dimensional optimization problem into a finite-dimensional one before a single line of an optimization algorithm is written, and it is the reason every practical SVM solver (from the original sequential minimal optimization algorithm onward) searches only over $n$ coefficients rather than over an abstract function space.

The theorem in this mission — Theorem 5.5 of Steinwart and Christmann, Support Vector Machines (Springer, 2008) — is stated for general convex losses and general kernels, subsuming the classification-SVM and regression-SVM special cases that appear throughout the machine learning literature. Its lineage traces to Kimeldorf and Wahba's 1971 representer theorem for spline-smoothing problems; the book's own version (attributed to a 1971 result, generalized here to arbitrary convex losses and RKHSs) is the general form used throughout the rest of the book.

Setting

Fix a nonempty set $X$ (the input space) and a loss function $L : X \times \mathbb R \times \mathbb R \to [0,\infty)$: a measurable map where $L(x,y,t)$ is the cost of predicting label $y$ by value $t$ when the input is $x$. $L$ is convex if $L(x,y,\cdot)$ is convex for every fixed $x,y$.

A reproducing kernel Hilbert space (RKHS) over $X$ is a real Hilbert space $H$ of real-valued functions on $X$ that carries a kernel $k : X \times X \to \mathbb R$ with two properties: $k(\cdot,x) \in H$ for every $x \in X$, and the reproducing property $f(x) = \langle f, k(\cdot,x)\rangle_H$ holds for every $f \in H$ and $x \in X$. Intuitively, $k$ lets you evaluate any $f \in H$ at a point $x$ by taking an inner product with the fixed function $k(\cdot,x)$ — this is what makes $H$ a space of genuine, pointwise-evaluable functions rather than an abstract Hilbert space.

Given a finite sample $D := ((x_1,y_1),\dots,(x_n,y_n)) \in (X \times \mathbb R)^n$, the empirical $L$-risk of $f : X \to \mathbb R$ is $R_{L,D}(f) := \tfrac1n\sum_{i=1}^n L(x_i,y_i,f(x_i))$. For a regularization parameter $\lambda > 0$, the SVM training problem asks for a minimizer of the regularized empirical risk

$$f \mapsto \lambda\|f\|_H^2 + R_{L,D}(f)$$

over all of $H$. A minimizer of this objective is called an empirical SVM solution $f_{D,\lambda}$.

Formalization targets

Goal — Theorem 5.5 (Representer theorem)

$$\exists! \, f_{D,\lambda} \in H : \quad \lambda\|f_{D,\lambda}\|_H^2 + R_{L,D}(f_{D,\lambda}) = \min_{f \in H} \Bigl(\lambda\|f\|_H^2 + R_{L,D}(f)\Bigr), \qquad f_{D,\lambda}(x) = \sum_{i=1}^n \alpha_i\, k(x,x_i) \; \text{ for some } \alpha_1,\dots,\alpha_n \in \mathbb R.$$

The theorem asserts both halves at once: the regularized empirical risk has a unique minimizer over the (possibly infinite-dimensional) $H$, and that unique minimizer is representable as a finite linear combination of the kernel functions at the sample points. Neither the coefficients $\alpha_i$ nor the finite-dimensional subspace they live in are fixed in advance by the statement; only their existence is asserted, so a stronger claim (e.g. uniqueness or an explicit formula for the $\alpha_i$) would be a different, harder theorem not proved here.

Supporting milestones (the general, population-level analogue)

The book develops the representer theorem's existence-and-uniqueness clause by first proving it for the corresponding population problem — minimizing $f \mapsto \lambda\|f\|_H^2 + R_{L,P}(f)$ over a distribution $P$ rather than a finite sample — and then adapting the same two arguments to the empirical case:

• Lemma 5.1 (uniqueness): for a convex loss and an RKHS $H$ with $R_{L,P}(f) < \infty$ for some $f \in H$, the regularized population risk has at most one minimizer over $H$, for every $\lambda > 0$.
• Theorem 5.2 (existence): for a convex, $P$-integrable Nemitski loss and the RKHS of a bounded kernel, the regularized population risk has at least one minimizer, for every $\lambda > 0$.
• Theorem 5.6 (non-triviality): under the same hypotheses as Theorem 5.2, if $H$ can beat the risk of the zero function ($\inf_{f \in H} R_{L,P}(f) < R_{L,P}(0)$), then every minimizer is nonzero, for every $\lambda > 0$.

Significance

The representer theorem is the single fact that turns kernel-based learning from a theoretical curiosity into a practical algorithm family: every popular SVM solver (SMO, coordinate descent, interior-point methods for the dual) is, at bottom, a method for finding the $n$ coefficients $\alpha_1,\dots,\alpha_n$ the theorem guarantees exist, not for searching $H$ directly. The representation also underlies the "kernel trick": since the objective and the solution both depend on $H$ only through inner products $\langle k(\cdot,x_i), k(\cdot,x_j)\rangle_H = k(x_i,x_j)$, an SVM can be trained and evaluated without ever computing with elements of $H$ explicitly, using only the $n \times n$ Gram matrix of kernel values.

Formalizing this theorem means formalizing the existence-and-uniqueness argument (Lemma 5.1's strict-convexity computation for the midpoint of two hypothetical minimizers, together with the weak-compactness argument used for existence) and the orthogonal-projection argument for the representation clause (projecting any candidate minimizer onto the finite-dimensional span of the kernel functions at the sample points strictly improves — or leaves unchanged — both the norm term and the risk term, so an optimal solution can always be chosen inside that span). No part of this argument has a machine-checked Lean proof in Mathlib or elsewhere at the time of writing; only the underlying general-purpose tools (Hilbert-space projections, convexity of norms) are already in Mathlib.

Difficulty

The natural first idea for the representation clause is to try to exhibit the coefficients $\alpha_i$ directly, e.g. by writing down the dual optimization problem and reading off its KKT multipliers. This is exactly backwards: the book's proof (and any faithful one) derives the representation before knowing anything about a dual problem, purely from the orthogonal decomposition $H = H|_{X'} \oplus H|_{X'}^\perp$ of $H$ into the span $H|_{X'}$ of the sample's kernel functions and its orthogonal complement. The key insight — one that a solver who reaches for duality first will miss — is that projecting any $f \in H$ onto $H|_{X'}$ leaves the empirical risk exactly unchanged (since $R_{L,D}$ only sees $f$'s values at the sample points, and the reproducing property shows those values are unaffected by throwing away the $H|_{X'}^\perp$ component) while weakly decreasing the norm term, so the infimum over all of $H$ is already attained inside the finite-dimensional $H|_{X'}$.

For the existence-and-uniqueness clause, the difficulty is genuinely functional-analytic rather than algorithmic: existence needs a compactness argument in a space with no compact balls (Theorem 5.2 gets around this via lower semicontinuity and boundedness of the sublevel set, not via any finite-dimensional trick), and uniqueness needs the parallelogram-law strict convexity of the Hilbert norm, not merely convexity of the loss.

Formalization scope

$H$ is represented as an arbitrary real Hilbert space together with an injective linear evaluation map into $X \to \mathbb R$ (so that $H$ is genuinely realized as a space of functions, not an abstract Hilbert space with no relation to $X$), and a kernel $k$ satisfying the reproducing property with respect to that evaluation map (IsRKHSOfKernel). This is an equivalent, operative rendering of "$H$ is the RKHS of the kernel $k$" (Definition 4.18 together with Lemma 4.19 of the book), chosen because it is exactly the form the chapter's own proofs use; it is restated inside this chunk's own InfiniteSample sub-namespace rather than imported from the Kernels chapter's mission, since drafts in this series cannot import one another.

The population risk $R_{L,P}$ is formalized as a lower Lebesgue integral into $[0,\infty]$ (ENNReal), which is always well-defined for a nonnegative integrand with no integrability hypothesis — matching the book's own remark that "the integral always exists, although it is not necessarily finite." The empirical risk $R_{L,D}$, by contrast, is a manifestly finite average over the $n$ sample points and is formalized as an ordinary real number. The sample size $n$ is required positive ($n \ge 1$), matching the book's implicit convention that the empirical measure $\bar D := \tfrac1n\sum_i \delta_{(x_i,y_i)}$ presupposes a nonempty sample.

A trivializing formalization of the representer theorem would state only the representation clause $f_{D,\lambda}(x) = \sum_i \alpha_i k(x,x_i)$ while assuming the existence of "the" solution $f_{D,\lambda}$ as a hypothesis; this begs the question, since the book's own proof establishes existence and uniqueness as part of the theorem, not as a standing assumption. This mission's goal keeps both clauses bundled into one ∃! statement for exactly this reason.

The infrastructure needed — a general convex loss, a Nemitski-loss integrability condition, and the RKHS/reproducing-kernel bundle — is restated locally here and is reusable, with the same caveat about not being importable across this series' independently drafted chapters, by any later mission (e.g. this book's own Chapters 6, 8 and 9) that needs the same objects. Contributed proofs are welcome for either the existence/uniqueness argument (Lemma 5.1/Theorem 5.2's techniques) or the orthogonal-projection representation argument; the two are largely independent and could be solved separately.

Selected references

• I. Steinwart and A. Christmann, Support Vector Machines, Springer Series in Information Science and Statistics, Springer, 2008. https://doi.org/10.1007/978-0-387-77242-4
• G. Kimeldorf and G. Wahba, "Some results on Tchebycheffian spline functions," Journal of Mathematical Analysis and Applications, 33(1):82–95, 1971. https://doi.org/10.1016/0022-247X(71)90184-3
• B. Schölkopf, R. Herbrich, and A. J. Smola, "A generalized representer theorem," in Computational Learning Theory (COLT 2001), Lecture Notes in Computer Science, vol. 2111, Springer, 2001, pp. 416–426. https://doi.org/10.1007/3-540-44581-1_27

Motivation

Quantum field theory begins, mathematically, with a question that has a completely precise answer: what is the state space of a single relativistic particle? Non-relativistic quantum mechanics answers $L^2(\mathbb{R}^3)$ and moves on. Relativity does not allow that answer, because the state space must carry an action of the symmetry group of Minkowski spacetime — the Poincaré group — and the choice of Hilbert space is dictated by which such action one wants. The construction that results is the foundation on which Fock space, creation and annihilation operators, free fields and eventually interacting theories are built, and it is where the objects that reappear everywhere in the subject are introduced: the mass shell, the Lorentz-invariant measure on it, and the double cover $SL(2,\mathbb{C}) \to SO^{\uparrow}(1,3)$ that is responsible for spin.

This mission formalizes that construction as it is presented in S. Chatterjee's Lectures on Quantum Field Theory (Stanford, 2018–19), Lectures 9–11 and Lecture 25: the one-particle space of a massive scalar boson, the one-particle space of an electron, and the statement that both carry inner products invariant under the Poincaré action.

Setting

Minkowski spacetime is $\mathbb{R}^{1,3}$ with the bilinear form

$$(x, y) \;=\; x^0 y^0 - \big(x^1y^1 + x^2y^2 + x^3y^3\big), \qquad x^2 := (x,x).$$

A Lorentz transformation is a linear map $L$ with $(Lx, Ly) = (x,y)$; the restricted Lorentz group $SO^{\uparrow}(1,3)$ consists of those with $\det L = 1$ and $L^0{}_0 > 0$. The Poincaré group is $\mathcal{P} = \mathbb{R}^{1,3} \rtimes SO^{\uparrow}(1,3)$ with the group law $(a,A)(b,B) = (a + Ab,\, AB)$.

For a mass $m > 0$, the four-momentum of a particle satisfies $p^2 = m^2$ and $p^0 \ge 0$, so it lies on the mass shell

$$X_m \;=\; \{\, p \in \mathbb{R}^{1,3} : p^2 = m^2,\ p^0 \ge 0 \,\},$$

a three-dimensional manifold parametrised by the spatial momentum $q \in \mathbb{R}^3$ through $q \mapsto (\omega_q, q)$ with $\omega_q = \sqrt{m^2 + |q|^2}$. On $X_m$ there is, up to a multiplicative constant, exactly one measure invariant under $SO^{\uparrow}(1,3)$; with the normalisation used in the lectures it is the measure $\lambda_m$ determined by

$$\int_{X_m} f \, d\lambda_m \;=\; \int_{\mathbb{R}^3} \frac{d^3q}{(2\pi)^3\, 2\omega_q}\, f(\omega_q, q).$$

The state space of a massive scalar boson is $\mathcal{H} = L^2(X_m, d\lambda_m)$, acted on by $(U(a,L)\psi)(p) = e^{i(a,p)}\psi(L^{-1}p)$.

For an electron the wave function takes values in $\mathbb{C}^2$ and the group acts through the double cover. To each four-vector $x$ one attaches the Hermitian matrix

$$M(x) = \begin{pmatrix} x^0+x^3 & x^1 - ix^2\\ x^1+ix^2 & x^0-x^3\end{pmatrix}, \qquad \det M(x) = (x,x),$$

and for $A \in SL(2,\mathbb{C})$ the transformation $\kappa(A)$ of $\mathbb{R}^{1,3}$ is defined by $M(\kappa(A)x) = A M(x) A^{\dagger}$; the map $\kappa$ is a surjective two-to-one homomorphism onto $SO^{\uparrow}(1,3)$. Writing $p^* = (m,0,0,0)$, each $p \in X_m$ is reached from $p^*$ by a unique positive-definite $V_p \in SL(2,\mathbb{C})$, the pure boost, and the electron inner product is the $V_p^{-2}$-weighted one,

$$(\psi, \varphi) \;=\; \int_{X_m} d\lambda_m(p)\; \psi(p)^{\dagger} V_p^{-2} \varphi(p),$$

with the group acting by $(U(a,A)\psi)(p) = e^{i(a,p)} A\, \psi(\kappa(A)^{-1}p)$.

Formalization targets

Goal — both one-particle inner products are Poincaré invariant

For $m > 0$, $a \in \mathbb{R}^{1,3}$, $A \in SL(2,\mathbb{C})$ and $L = \kappa(A)$:

$$\int_{X_m} \overline{(U(a,L)\psi)}\,(U(a,L)\varphi)\, d\lambda_m \;=\; \int_{X_m} \overline{\psi}\,\varphi\, d\lambda_m \qquad (\psi,\varphi \in L^2(X_m, d\lambda_m)),$$ $$\int_{X_m} (U(a,A)\psi)^{\dagger}\,V_p^{-2}\,(U(a,A)\varphi)\, d\lambda_m \;=\; \int_{X_m} \psi^{\dagger}\,V_p^{-2}\,\varphi\, d\lambda_m$$

for $\psi, \varphi$ in the weighted $L^2$ space of $\mathbb{C}^2$-valued functions. The goal fixes no constants beyond the normalisation of $\lambda_m$, and it is the statement that the spaces defined in the mission really are the one-particle spaces of the theory: a Hilbert space together with a Poincaré action by isometries.

Supporting targets

The milestone list follows the lectures: the parametrisation of $X_m$; invariance of $X_m$ under $SO^{\uparrow}(1,3)$; the integration formula for $\lambda_m$ (eq. (10.1)); invariance of $\lambda_m$; uniqueness of the invariant measure up to a constant; the composition law and unitarity of the scalar representation; $\det M(x) = (x,x)$ and bijectivity of $M$ onto Hermitian matrices; $\kappa$ as a multiplicative map into $SO^{\uparrow}(1,3)$; surjectivity of $\kappa$ with fibres $\{\pm A\}$; existence and uniqueness of the pure boost $V_p$; Lemma 25.1; and the identification of the weighted electron space with the plain $\mathbb{C}^2$-valued $L^2$ space via $\psi \mapsto V_\cdot^{-1}\psi$.

Significance

The objects here are used unchanged for the rest of a QFT course: the bosonic and fermionic Fock spaces are built on these one-particle spaces, and the free scalar and Dirac fields are operator-valued distributions written as integrals against $d\lambda_m$ on $X_m$. Formalizing them fixes, once and for all, the conventions later work must match — the normalisation of $\lambda_m$, the sign convention of the metric, which of the two elements $\pm A$ of $SL(2,\mathbb{C})$ acts, and the weight in the electron inner product.

What this mission adds beyond the lectures is a machine-checked development of material usually treated as routine but rarely written out: the uniqueness of the invariant measure, the covering map and its fibres, and the existence-uniqueness of the pure boost are all stated in the source either without proof or as exercises. Mathlib has the general theory of $L^2$ spaces, push-forward measures, Hermitian and positive-definite matrices, and $SL_2$, but it has no mass shell, no invariant measure on it, and no covering map onto the restricted Lorentz group; all of that is constructed here and is reusable by any later mission on free fields or Fock spaces.

Difficulty

The obvious route to the invariant measure — "restrict Lebesgue measure to the submanifold $X_m$" — does not work: the induced Riemannian volume of the hyperboloid in the Euclidean metric is not Lorentz invariant. The lectures instead take a scaling limit of Lebesgue measure on the invariant annuli $\{m^2 < p^2 < (m+\varepsilon)^2\}$; the formalization takes the resulting formula (10.1) as the definition and must then prove invariance, which amounts to a change-of-variables computation whose Jacobian is exactly $\omega_{q}$-dependent. Uniqueness is harder: it is a statement about invariant measures on a homogeneous space of a non-compact group, with no finiteness available.

On the spinor side, the central difficulty is that the weight $V_p^{-2}$ is unbounded on $X_m$, so the electron space is not the naive $\mathbb{C}^2$-valued $L^2(X_m, d\lambda_m)$ — the two spaces consist of different functions, and are related only through the measurable field of isomorphisms $\psi \mapsto V_p^{-1}\psi$. A formalization that silently uses the unweighted space would prove a different, and false, unitarity statement.

Formalization scope

Four-vectors are functions $\mathbb{R}^{1,3} = (\text{four-element index}) \to \mathbb{R}$, with the metric signature $(+,-,-,-)$; Lorentz transformations are real $4\times4$ matrices, and membership in $SO^{\uparrow}(1,3)$ is the predicate ($\det = 1$, $L^0{}_0 > 0$, form preserved). $\lambda_m$ is a Borel measure on all of $\mathbb{R}^{1,3}$ carried by $X_m$, defined as the push-forward of $(2\pi)^{-3}(2\omega_q)^{-1}\,d^3q$; the boson space is the library $L^2$ space of that measure. The pure boost is given by the closed formula $V_p = (M(p)/m + I)/\sqrt{2 + 2p^0/m}$ — the positive-definite square root of $M(p)/m$ — rather than by a choice function, and a milestone certifies that it is the unique positive-definite element of $SL(2,\mathbb{C})$ carrying $p^*$ to $p$. The electron space is the set of $\mathbb{C}^2$-valued measurable functions of finite weighted norm, with the weighted pairing given explicitly; the milestone identifying it with the plain $L^2$ space via the inverse boost is what supplies its Hilbert-space structure.

The unitarity statements are formalized as equalities of integrals over pairs of wave functions rather than as statements about abstract operators, so that no trivializing reading is available: in particular the electron clause is stated for the weighted pairing, which is not the standard $L^2$ inner product, and the hypotheses ($m > 0$, $\det A = 1$, $\psi,\varphi$ in the respective spaces) are satisfiable, so no clause holds vacuously. Total-function conventions of the library (inverse of a singular matrix is $0$; integral of a non-integrable function is $0$) are visible in the statements and are recorded in each item's read-back.

Contributions of any of the milestones are welcome; the measure-theoretic milestones (invariance and uniqueness) and the $SL(2,\mathbb{C})$ covering milestones are independent of each other and can be attacked in parallel.

Selected references

• S. Chatterjee, Lectures on Quantum Field Theory, Stanford University, 2018–19 (scribed lecture notes). https://souravchatterjee.su.domains/qft-lectures-combined.pdf
• E. P. Wigner, On unitary representations of the inhomogeneous Lorentz group, Annals of Mathematics 40 (1939), 149–204. https://doi.org/10.2307/1968551

Motivation

Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).

This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.

Setting

Let $X$ be a real normed space and $K\subseteq X$ a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.

When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets

$$\{x:g_K(x)\le 1\}=\overline K, \qquad \{x:g_K(x)<1\}=\operatorname{int}K.$$

These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).

For two convex sets $K_1,K_2$, Eidelheit separation means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.

Formalization targets

Gauge and geometric Hahn--Banach milestones

Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that

$$f(v)=c\quad(v\in V), \qquad f(k)<c\quad(k\in\operatorname{int}K).$$

This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).

Supporting hyperplanes and convex-set separation

For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:

$$f(x)\le c\le f(y) \quad\text{for all }x\in K_1,\ y\in K_2.$$

These are Theorems 2 and 3 of §5.12 (pp. 133--134).

Convex minimum-distance duality

Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and

$$f(x_1)-c=d.$$

Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).

Significance

The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.

Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.

Difficulty

A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.

Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.

Formalization scope

The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.

The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. Public scan.