Functional Analysis

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.

Why projection methods for variational inequalities

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It is the common form of convex minimization (with $F$ a gradient), of saddle-point problems (with $F$ the monotone operator of a convex–concave function), of Nash equilibria of convex games, of complementarity problems and of traffic and economic equilibria. Iterative methods that use only evaluations of $F$ and projections onto the feasible set are the methods of choice when the problem is large, because each step is cheap.

The classical such method, the projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$, does not converge for merely monotone $F$. Korpelevich's extragradient method (1976) does, at the price of two projections and two evaluations of $F$ per step, and it is known to converge R-linearly under strong monotonicity (Tseng 1995, reference [19] of the paper). Popov (1980), Tseng (2000) and Censor–Gibali–Reich (2011) reduced the number of projections or evaluations. Yu. Malitsky's projected reflected gradient method (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) uses one projection and one evaluation of $F$ per step, evaluating $F$ at the reflected point $2x_n-x_{n-1}$ instead of at $x_n$. This mission formalizes the paper's second main result: under strong monotonicity the method keeps the R-linear rate of the extragradient method.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, let $C\subseteq H$ be closed and convex, and let $F:H\to H$. The metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$. The variational inequality (1.1) is

$$\text{find } x^*\in C\ \text{ such that }\ \langle F(x^*),\,x-x^*\rangle\ \ge\ 0\quad\text{for all } x\in C,$$

with solution set $S$. The paper's standing assumptions for this result are

• (C1) $S\neq\emptyset$;
• (C2*) $F$ is strongly monotone with modulus $m>0$: $\langle F(x)-F(y),x-y\rangle\ge m\|x-y\|^2$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz with constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 chooses $x_0=y_0\in H$ and a step $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and iterates

$$x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .$$

The Lean development names these objects proj, solSet, IsStronglyMonotoneMap, IsLipschitzMap and IsPRGRun in the namespace ProjReflGrad.Linear.

Formalization targets

Goal: Theorem 3.3 (p. 6)

Under (C1), (C2*), (C3) and $0<\lambda<(\sqrt2-1)/L$, every run of Algorithm 3.1 converges to the solution $z$ of (1.1) at least R-linearly:

$$\exists\,\gamma\in(0,1),\ M>0:\qquad \|x_n-z\|\ \le\ M\gamma^n\quad\text{for all } n\ge0 .$$

The goal fixes neither $\gamma$ nor $M$; the proof produces them from $\lambda$, $L$ and $m$, but the theorem asserts only the shape of the rate.

Milestones

In attack order:

1. Uniqueness (p. 6): under (C2*) the solution set has at most one point.
2. The identity for $\|y_n-z\|^2$ (p. 6, via Lemma 2.5): $\|y_n-z\|^2=2\|x_n-z\|^2-\|x_{n-1}-z\|^2+2\|x_n-x_{n-1}\|^2\ge2\|x_n-z\|^2-\|x_{n-1}-z\|^2$.
3. (3.8) (p. 7): the strong-monotonicity estimate at $y_n$ with a free modulus $m_1\in(0,m]$.
4. (3.2) (p. 4): $\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\|x_{n+1}-x_n\|^2-2\lambda\langle F(y_n),x_{n+1}-z\rangle$.
5. (3.4) (p. 5): $2\lambda\langle F(y_{n-1}),y_n-x_{n+1}\rangle\le\|x_{n+1}-x_n\|^2-\|x_n-y_n\|^2-\|x_{n+1}-y_n\|^2$, $n\ge2$.
6. (3.5) (p. 5): the Lipschitz estimate of $2\lambda\langle F(y_n)-F(y_{n-1}),y_n-x_{n+1}\rangle$.
7. (3.9) (p. 7): the two-step recursion $a_{n+1}+b_{n+1}\le(1-2\alpha)a_n+\alpha a_{n-1}+\beta b_n$ in the iterates, with $\beta=\max\{\lambda L/(1-\sqrt2\lambda L),\tfrac12\}$.
8. Lemma 2.8 (p. 3): a nonnegative pair of sequences satisfying that recursion for all $\alpha\in(0,\alpha_0)$ has $a_n\le\gamma^nM$.

Significance

The result. Theorem 3.3 shows that halving the per-step cost of the extragradient method does not cost the linear rate under strong monotonicity. For strongly monotone problems (strongly convex minimization, strongly convex–strongly concave saddle points, strictly monotone games with a quadratic margin) the method therefore reaches accuracy $\varepsilon$ in $O(\log(1/\varepsilon))$ iterations with one projection each, which matters when projecting onto $C$ dominates the cost. The two-step recursion (3.9) and Lemma 2.8 are also a reusable template: the same mechanism gives linear rates for other methods with a memory of one past iterate.

Formalizing it. The theorem is proved in the paper; nothing here is open. No machine-checked proof of it, or of its lemmas, is on the platform. A formal proof needs the projection inequality in a general real Hilbert space, a careful account of the reflected iterate, and a rigorous version of Lemma 2.8, whose printed proof leaves the range of $n$ and the positivity of $M$ implicit. The deliverable is a checked R-linear rate for a one-projection method in infinite dimension.

Difficulty

The natural first attempt, a contraction $\|x_{n+1}-z\|\le q\|x_n-z\|$ (Q-linear convergence), is not what the paper proves and is not available: the reflected point $y_n$ depends on $x_{n-1}$, so the error at step $n+1$ is controlled only by the errors at steps $n$ and $n-1$, together with auxiliary terms $\|x_n-y_{n-1}\|^2$ and $\langle F(z),x_{n-1}-z\rangle$. Strong monotonicity is applied at $y_n$, not at $x_n$, and $\|y_n-z\|^2$ can be smaller than $\|x_n-z\|^2$; the lower bound $2\|x_n-z\|^2-\|x_{n-1}-z\|^2$ may even be negative. The step range $\lambda<(\sqrt2-1)/L$ is exactly what keeps the coefficients of the Lipschitz error terms below the gain from the projection inequality, and the resulting two-step recursion needs Lemma 2.8, with its choice of $\gamma$ and $\delta$, to yield a geometric bound.

Formalization scope

• $H$ is a general real inner product space, complete where a projection is used ([CompleteSpace H]); it is never specialized to $\mathbb R^n$.
• $P_C$ is defined by choice as a nearest point, returning its argument when none exists; every statement using it assumes $C$ closed, convex and nonempty (through $z\in C$, $C\neq\emptyset$, or (C1)), so the junk value is never reached.
• Runs of Algorithm 3.1 are infinite sequences without the stopping rule; a stopped run continues as a constant sequence. $x_0$ is any point of $H$, as in the paper, so statements that need $x_{n-1}\in C$ are stated for $n\ge2$.
• (C2*) and (C3) are required on all of $H$ with real constants $m>0$, $L>0$ (not LipschitzWith, whose $\mathbb R_{\ge0}$ constant admits $L=0$). (C1) stays in the goal: it is the paper's assumption and its only source of $C\neq\emptyset$.
• R-linear convergence means domination by $M\gamma^n$ with $0<\gamma<1$ and $M>0$; a goal allowing $\gamma=1$, $\gamma=0$ or only an $O(\cdot)$ bound would be a different and weaker (or trivially false) statement and is ruled out. The goal does not mention the auxiliary sequences $a_n,b_n$, the constants $\beta,m_1,\alpha_0$, or Lemma 2.8.
• Departures from the page are recorded in each item's Formalization Note: the ranges $n\ge1$/$n\ge2$, the range $n\ge1$ of (2.1) in Lemma 2.8, the proof's "Lemma 2.1" that means Lemma 2.8, and "$m_1$ arbitrary in $(0,m)$" where the argument uses $(0,m]$.
• The projection theorem (existence and characterization of the nearest point) is the published Proved theorem VectorSpaceOpt.min_distance_convex_set, included as a reference. Contributions welcome: proofs of the milestones in any order; Lemma 2.8 and the identity of milestone 2 are self-contained.

Selected references

• Yu. Malitsky, Projected Reflected Gradient Methods for Monotone Variational Inequalities, SIAM J. Optim. 25(1), 2015. arXiv:1502.04968v1. https://arxiv.org/abs/1502.04968 , https://doi.org/10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12, 747–756, 1976.
• P. Tseng, On linear convergence of iterative methods for the variational inequality problem, J. Comput. Appl. Math. 60, 237–252, 1995.
• L. D. Popov, A modification of the Arrow–Hurwicz method for finding saddle points, Math. Notes 28, 845–848, 1980.
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148, 318–335, 2011.

Motivation

Many problems in optimization, game theory and mechanics come down to a variational inequality: find a point of a convex set at which a given vector field points "inward" against every feasible direction. Constrained convex minimization (where the field is a gradient), saddle-point problems (where it is the gradient of a convex–concave function with one sign flipped), Nash equilibria of convex games and complementarity problems are all of this form. In large-scale and infinite-dimensional settings the methods of choice are projection methods, which use only evaluations of the field and projections onto the feasible set.

The plain projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$ does not converge for merely monotone fields: on a rotation field in the plane it spirals outward for every step size. Korpelevich's extragradient method (1976) repairs this with two field evaluations and two projections per iteration. Later methods (Tseng's forward–backward–forward method, 2000; the subgradient extragradient method of Censor, Gibali and Reich, 2011) reduce the number of projections to one, but still need two evaluations of the field.

Yu. Malitsky's paper (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which uses one projection and one field evaluation per iteration, evaluated at a "reflected" point, and proves that it converges weakly under the same assumptions as the extragradient method. This mission formalizes that convergence theorem, Theorem 3.2 of the paper.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C\subseteq H$ be closed and convex, and let $F:H\to H$ be a mapping. For $z\in H$, the metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$ (it exists when $C$ is nonempty). The variational inequality (1.1) asks for $x^*\in C$ with

$$\langle F(x^*),\,x-x^*\rangle\ \ge\ 0\qquad\text{for all }x\in C,$$

and $S$ denotes its solution set. The standing assumptions are:

• (C1) $S$ is nonempty;
• (C2) $F$ is monotone: $\langle F(x)-F(y),x-y\rangle\ge0$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz continuous with a constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 (projected reflected gradient method). Fix a step size $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and a starting point $x_0=y_0\in H$, and iterate

$$x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .$$

The point $y_{n+1}$ is the reflection of $x_n$ through $x_{n+1}$. A sequence $(x_n)$ converges weakly to $x^*$, written $x_n\rightharpoonup x^*$, if $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$.

Formalization targets

Goal: Theorem 3.2 (p. 5)

Under (C1)–(C3), for $0<\lambda<(\sqrt2-1)/L$ and every run of Algorithm 3.1 there is $x^*\in S$ with

$$x_n\rightharpoonup x^* .$$

Milestones

In the order the proof uses them:

1. Lemma 2.1 (i), p. 3: $\langle P_Mx-x,\,y-P_Mx\rangle\ge0$ for $y\in M$ (already proved on the platform, referenced).
2. Lemma 2.1 (ii), p. 3: $\|P_Mx-y\|^2\le\|x-y\|^2-\|x-P_Mx\|^2$ for $y\in M$.
3. Lemma 3.1, p. 4: for $z\in S$ and $n\ge2$,

$$\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\big(1-\lambda L(1+\sqrt2)\big)\|x_n-x_{n-1}\|^2+\lambda L\|x_n-y_{n-1}\|^2-\big(1-\sqrt2\lambda L\big)\|x_{n+1}-y_n\|^2-2\lambda\langle F(z),y_n-z\rangle .$$

4. (3.6), p. 5: the descent inequality $a_{n+1}\le a_n-b_n$ with $a_n=\|x_n-z\|^2+\lambda L\|x_n-y_{n-1}\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ and $b_n=(1-\lambda L(1+\sqrt2))\|x_n-x_{n-1}\|^2$.
5. Lemma 2.7, p. 3: nonnegative sequences with $a_{n+1}\le a_n-b_n$ have $(a_n)$ bounded and $b_n\to0$.
6. Proof of Theorem 3.2, pp. 5–6: $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$ and $\|x_{n+1}-y_n\|\to0$.
7. Lemma 2.2 (Minty), p. 3: for continuous monotone $F$, $x^*\in S$ iff $x^*\in C$ and $\langle F(y),y-x^*\rangle\ge0$ for all $y\in C$.
8. (3.7), p. 6: every weak cluster point of $(x_n)$ lies in $S$.
9. Proof of Theorem 3.2, p. 6: for each $z\in S$, $\|x_n-z\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ converges.
10. Lemma 2.3 (Opial), p. 3: if $x_n\rightharpoonup x$ and $y\ne x$, then $\liminf\|x_n-x\|<\liminf\|x_n-y\|$.

Companion items, not milestones: the defined projection is the metric projection (so runs of Algorithm 3.1 exist from every starting point), Remark 2.1 ($S$ is closed and convex), and the characterization of $S$ as the zeros of the projected residual $r(x,y)=\|y-P_C(x-\lambda F(y))\|+\|x-y\|$ (§3, p. 4).

Significance

The result. Theorem 3.2 shows that a monotone Lipschitz variational inequality in Hilbert space can be solved by an iteration costing one projection and one evaluation of $F$ per step, the minimum for a projection method, with no knowledge beyond the Lipschitz constant. This halves the cost of each iteration relative to the extragradient method when evaluating $F$ is expensive, and keeps the cost of projections at one when projecting onto $C$ is expensive. The method and its analysis became the basis for several later algorithms, including the adaptive variant in §4 of the same paper and the golden ratio algorithm of Malitsky (2020).

Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. The formal development needs, beyond the main argument, a usable library of facts about projections onto closed convex sets in Hilbert space, weak convergence of sequences (boundedness of weakly convergent sequences, weak sequential compactness of bounded sets) and Opial's property. These are reused by every weak-convergence proof for splitting and projection methods, and several companion missions of this series and of related papers rely on the same facts.

Difficulty

The naive Lyapunov function $\|x_n-z\|^2$ is not monotone along the iteration: because $F$ is evaluated at the reflected point $y_n$ rather than at $x_n$, the cross terms do not cancel as they do for the extragradient method. The quantity that does decrease (milestones 3–4) carries extra terms, and the step bound $(\sqrt2-1)/L$ is what the decrease requires. As a consequence, $\|x_n-z\|$ itself is not known to converge, so the standard Opial lemma ("if $\|x_n-z\|$ converges for every $z\in S$ and all weak cluster points lie in $S$, then $x_n$ converges weakly") does not apply directly; the uniqueness of the weak cluster point has to be argued with the perturbed quantity and Opial's inequality. In infinite dimension, the weak cluster point step also needs weak sequential compactness of bounded sets, which is not norm compactness.

Formalization scope

• $H$ is an arbitrary real inner product space with [CompleteSpace H] in every statement that needs completeness; it is never specialised to $\mathbb R^n$, where weak and norm convergence coincide.
• Weak convergence is stated elementarily: $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$. Subsequences are $x\circ\varphi$ with $\varphi$ strictly increasing.
• The projection $P_C(z)$ is defined by choice as a nearest point, with the junk value $z$ when none exists. Every statement that uses it assumes $C$ closed, convex and nonempty (directly or through $S\ne\emptyset$ or $z\in S$), and a companion item certifies that it is then the metric projection.
• (C2) and (C3) are imposed on all of $H$, as in the paper; $L$ is a real number with $L>0$, and the step range $0<\lambda<(\sqrt2-1)/L$ is strict on both sides.
• Runs of Algorithm 3.1 carry no stopping rule: a run reaching a solution $x_n=y_n\in S$ stays constant, so infinite runs subsume stopped ones. The starting point $x_0$ is any point of $H$, not necessarily in $C$; for this reason Lemma 3.1 and (3.6) are stated for $n\ge2$, which is the range the proof of Theorem 3.2 uses.
• Opial's inequality is stated with liminfs in $[0,\infty]$, where they are always defined.
• A trivializing formalization is ruled out: the goal assumes exactly (C1)–(C3), closedness and convexity of $C$ and the step range, and concludes weak convergence to a point of $S$; it does not assume boundedness of the iterates, a starting point in $C$, finite dimension, or any of the intermediate estimates.

Contributions welcome: proofs of the milestones in any order; general Hilbert-space lemmas (boundedness of weakly convergent sequences via the uniform boundedness principle, weak sequential compactness of bounded sets, Opial's inequality) are useful well beyond this mission.

Selected references

• Yu. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1) (2015), 502–520. arXiv:1502.04968, doi:10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976), 747–756.
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2) (2000), 431–446. doi:10.1137/S0363012998338806
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148 (2011), 318–335. doi:10.1007/s10957-010-9757-3
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73 (1967), 591–597. doi:10.1090/S0002-9904-1967-11761-0
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5

Motivation: the fixed point property in reflexive spaces

A map $F$ is nonexpansive if $\|F(a)-F(b)\|\le\|a-b\|$. Unlike strict contractions, nonexpansive maps need not have fixed points: on a bounded set, existence depends on the geometry of the norm. A Banach space has the fixed point property (FPP) if every nonexpansive self-map of every nonempty closed bounded convex subset has a fixed point. Since the mid-1960s, whether every reflexive Banach space has the FPP in its given norm has been one of the central open questions of metric fixed point theory. Many sufficient geometric conditions are known, but none of them covers all reflexive spaces. In fixed point theory, the question has been listed as unresolved as recently as 2026 (Nourouzi 2026).

Timeline

• 1965 — Browder and Göhde prove the FPP for uniformly convex spaces (Browder 1965; Göhde 1965). Kirk proves it for weakly compact convex sets with normal structure, in particular for closed bounded convex sets with normal structure in reflexive spaces (Kirk 1965).
• 1974–1975 — Bruck's common fixed point theorems for commuting families and compact convex semigroups (Bruck 1974; Bruck 1975).
• 1975–1976 — The Goebel–Karlovitz lemma on approximate fixed point sequences in minimal invariant sets (Goebel 1975; Karlovitz 1976). Karlovitz also shows that a norm on $\ell_2$ without normal structure still has the FPP, so normal structure is not necessary.
• 1981 — Alspach constructs a weakly compact convex subset of $L_1[0,1]$ with a fixed-point-free nonexpansive self-map, so weak compactness alone is insufficient in general Banach spaces (Alspach 1981). Maurey proves the FPP for reflexive subspaces of $L^1$ (Maurey 1981).
• 1985 — Lin proves the weak FPP for spaces with a $1$-unconditional basis (Lin 1985).
• 2006 — García-Falset, Llorens-Fuster and Mazcuñán-Navarro prove the FPP for uniformly nonsquare spaces (JFA 2006); another proof is due to Dowling, Randrianantoanina and Turett (JFA 2008).
• 2009 — Domínguez Benavides shows that every reflexive space admits an equivalent norm with the FPP (JMAA 2009). Changing the norm changes which maps are nonexpansive, so this does not settle the question for the original norm.
• 2019, 2021 — Hanebaly proposes proofs of the original-norm assertion (JP J. Fixed Point Theory Appl. 2019; preprint 2021). Later literature, such as Nourouzi (2026), still treats the question as unresolved.
• 2026 — An OpenAI preprint, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces (OpenAI Math Release, September 24, 2026), claims a proof for every real reflexive Banach space. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ be a real Banach space and $X^{**}$ its continuous bidual. The canonical map $J:X\to X^{**}$, $J(x)(\varphi)=\varphi(x)$, is always a linear isometry, and $X$ is reflexive if $J$ is surjective. A subset $C\subseteq X$ is taken nonempty, closed in the norm topology, bounded and convex. A map $F:C\to C$ is nonexpansive in the given norm of $X$, and a fixed point is a point $a\in C$ with $F(a)=a$.

In Lean, reflexivity is the definition CanonicallyReflexive X, which says that NormedSpace.inclusionInDoubleDual ℝ X is surjective.

Formalization targets

Goal: reflexive spaces have the fixed point property (Theorem 1.1)

$$X \text{ real reflexive Banach},\ C\subseteq X \text{ nonempty, closed, bounded, convex},\ \|F(a)-F(b)\|\le\|a-b\|\ \ \forall a,b\in C \ \Longrightarrow\ \exists\, a\in C:\ F(a)=a.$$

This is exactly Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the reflexive-space fixed point problem for the given norm, with no extra geometric assumption (uniform convexity, normal structure, unconditional bases, uniform nonsquareness). With Bruck's 1974 theorem it gives the source's Corollary 1.2: for every commuting family of nonexpansive self-maps of $C$, the common fixed point set is nonempty and is a nonexpansive retract of $C$. Alspach's example shows that reflexivity cannot be weakened to weak compactness of $C$ in an arbitrary Banach space.

Formalizing it. Earlier proposed proofs of the same assertion exist, and the literature has not reached a consensus, so a machine-checked proof would give unusual certainty on a disputed question. The proof relies on the minimal invariant set reduction (Zorn's lemma and weak compactness), the Goebel–Karlovitz lemma, compact semigroups of nonexpansive maps (an Ellis-type idempotent), and a tree construction with weighted telescoping estimates. Mathlib has the bidual, the weak topology, and Banach–Alaoglu, but most of the fixed-point-theoretic layer has to be built.

Difficulty

The classical route reduces a hypothetical counterexample to a minimal invariant weakly compact convex set $K$ of diameter one. By the Goebel–Karlovitz lemma, every approximate fixed point sequence in $K$ is asymptotically diametral. Normal-structure arguments then find a point whose radius is strictly below the diameter. In a general reflexive space there is no such geometric gain, and Karlovitz's example shows that normal structure is not necessary for the conclusion. Alspach's $L_1$ example shows that compactness of $C$ and nonexpansiveness alone cannot produce the contradiction: the proof has to use reflexivity of the whole space (weak compactness of the unit ball of $\overline{\operatorname{span}}(K-K)$), not just of the domain. A further obstacle is that $F$ is nonlinear, so convex combinations of approximate fixed points are not mapped to convex combinations of their images.

Formalization scope

• $X$ is any real normed space with CompleteSpace X, and reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ X (the continuous bidual). Completeness also follows from reflexivity, so including it is harmless. The scalar field is $\mathbb R$; complex spaces enter as real spaces.
• $C$ is a Set X with Nonempty, IsClosed (norm topology), Bornology.IsBounded and Convex ℝ. $F$ is a function on the subtype C → C, and nonexpansiveness is stated in the original norm of $X$, not in an equivalent norm.
• The conclusion is the existence of a fixed point ∃ a : C, F a = a. Every hypothesis is satisfiable, so the statement is not vacuous: a trivial $C$ is excluded only by nonemptiness, as in the source.
• Infrastructure needed: the minimal invariant set reduction, the Goebel–Karlovitz lemma, compact right-topological semigroups of maps and idempotents (Ellis), and weak compactness in reflexive spaces. These would serve other fixed-point formalizations, for example Kirk's and Browder–Göhde's theorems, which are not formalized in Mathlib.

Selected references

• F. E. Browder, Nonexpansive nonlinear operators in a Banach space, Proc. Natl. Acad. Sci. USA 54 (1965), 1041–1044. https://doi.org/10.1073/pnas.54.4.1041
• D. Göhde, Zum Prinzip der kontraktiven Abbildung, Math. Nachr. 30 (1965), 251–258. https://doi.org/10.1002/mana.19650300312
• W. A. Kirk, A fixed point theorem for mappings which do not increase distances, Amer. Math. Monthly 72 (1965), 1004–1006. https://doi.org/10.2307/2313345
• R. E. Bruck, Jr., A common fixed point theorem for a commuting family of nonexpansive mappings, Pacific J. Math. 53 (1974), 59–71. https://msp.org/pjm/1974/53-1/pjm-v53-n1-p05-p.pdf
• K. Goebel, On the structure of minimal invariant sets for nonexpansive mappings, Ann. Univ. Mariae Curie-Skłodowska Sect. A 29 (1975), 73–77. https://www.bc.umcs.pl/Content/31033/PDF/czas4050_29_1975_9.pdf
• L. A. Karlovitz, Existence of fixed points of nonexpansive mappings in a space without normal structure, Pacific J. Math. 66 (1976), 153–159. https://doi.org/10.2140/pjm.1976.66.153
• D. E. Alspach, A fixed point free nonexpansive map, Proc. Amer. Math. Soc. 82 (1981), 423–424. https://doi.org/10.2307/2043954
• B. Maurey, Points fixes des contractions de certains faiblement compacts de $L^1$, Séminaire d'analyse fonctionnelle (1980–1981), Exposé VIII. https://www.numdam.org/item/SAF_1980-1981____A8_0/
• P.-K. Lin, Unconditional bases and fixed points of nonexpansive mappings, Pacific J. Math. 116 (1985), 69–76. https://doi.org/10.2140/pjm.1985.116.69
• J. García-Falset, E. Llorens-Fuster and E. M. Mazcuñán-Navarro, Uniformly nonsquare Banach spaces have the fixed point property for nonexpansive mappings, J. Funct. Anal. 233 (2006), 494–514. https://doi.org/10.1016/j.jfa.2005.09.002
• T. Domínguez Benavides, A renorming of some nonseparable Banach spaces with the Fixed Point Property, J. Math. Anal. Appl. 350 (2009), 525–530. https://doi.org/10.1016/j.jmaa.2008.02.049
• K. Nourouzi, Reflexivity of Hilbert $K(H)$-modules and fixed-point property for nonexpansive mappings, J. Math. 2026, Article ID 6311273. https://doi.org/10.1155/jom/6311273
• OpenAI, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Fixed-Points-of-Nonexpansive-Maps-in-Reflexive-Banach-Spaces-September-24-2026/paper.pdf

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for all bounded operators on complex Hilbert spaces, with its sharpness, as stated in Corollary 6.3 of an OpenAI preprint dated September 23, 2026 (source), together with the preprint's structural theorems as milestones. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

For a bounded operator $A$ on a complex Hilbert space $\mathcal H\neq\{0\}$, $W(A)=\{\langle x,Ax\rangle:\|x\|=1\}$ and $K=\overline{W(A)}$; $P[A]=\sum_kA^k\otimes B_k$ acts on $\mathcal H\otimes\mathbb C^m$. A bounded open convex $\Omega\subset\mathbb C$ is admissible if its boundary is a regular real-analytic Jordan curve. For such $\Omega\supset W(A)$ ($A$ a matrix) with interior conformal map $f:\Omega\to\mathbb D$, put $T=f(A)$ and

$$\kappa^2=\min\{\tau:\ I\preceq H\preceq\tau I,\ T^*HT\preceq H\ \text{for some } H=H^*\}.$$

Formalization targets

Milestone: geometry of the numerical range (Corollary 6.3, p. 16, first assertion)

For $\mathcal H\neq\{0\}$, $K=\overline{W(A)}$ is compact and convex and contains $\operatorname{spec}(A)$.

Milestone: the zero space (Corollary 6.3, p. 16, case $\mathcal H=\{0\}$)

If $\mathcal H=\{0\}$, the numerical range is empty, every polynomial, holomorphic and rational evaluation is $0$, and the corresponding inequalities read $0\le0$ (with the supremum over the empty set taken to be $0$).

Milestone: optimal metric and common positive representation (Lemma 1.1, Theorems 1.2–1.3, p. 2)

For admissible $\Omega$ conformal coordinates exist; for every $n\ge1$ and $A\in M_n(\mathbb C)$ with $W(A)\subset\Omega$, the problem defining $\kappa^2$ is strictly feasible with attained minimum $1\le\kappa^2\le4$; for a minimizer $H$, $S=H^{1/2}$ satisfies $\|S\|\|S^{-1}\|=\kappa\le2$ and $D=Sf(A)S^{-1}$ is a contraction with $\rho(D)<1$; and one continuous $\Lambda:\mathbb T\to M_n(\mathbb C)$ with $\Lambda\succeq0$, $\int\Lambda\,d\sigma=I$ represents $v[SAS^{-1}]=\int\Lambda(t)\otimes v(G(t))\,d\sigma(t)$ for every $m$ and every $M_m$-valued $v$ holomorphic near $\overline\Omega$, giving $\|v[A]\|\le\kappa\max_{\overline\Omega}\|v\|$.

Milestone: the matrix inequality (Corollary 6.1, p. 15)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$, $B_k\in M_m(\mathbb C)$: $\|P[A]\|\le2\max_{W(A)}\|P\|$, and no smaller universal constant works.

Goal: Corollary 6.3 (p. 16)

For every complex Hilbert space $\mathcal H$ (no separability assumption) and $A\in B(\mathcal H)$: if $\mathcal H\neq\{0\}$ then $K$ is compact, convex, contains the spectrum, and for every $m\ge1$

$$\|P[A]\|\le 2\sup_{W(A)}\|P\|=2\max_K\|P\|,\qquad \|F[A]\|\le2\max_K\|F\|,\qquad \|R[A]\|\le 2\max_K\|R\|$$

for matrix polynomials $P$, matrix functions $F$ holomorphic on an open $U\supseteq K$ (holomorphic functional calculus), and matrix rational functions $R$ with poles off $K$; if $\mathcal H=\{0\}$ the degenerate statements above hold; and the constant $2$ is optimal.

Significance

The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: $\overline{W(A)}$ is a complete $2$-spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most $2$, and one positive boundary density that represents every matrix-valued analytic evaluation simultaneously. These are the objects predicted abstractly by Paulsen's and Arveson's theorems, constructed here explicitly. A companion OpenAI preprint gives an independent direct proof of the matrix inequality.

Formalizing it. Mathlib has bounded operators, the holomorphic functional calculus is only partially available, and conformal mapping of analytic Jordan domains is absent. A complete development needs the Riemann mapping theorem with boundary extension, semidefinite optimization over Hermitian matrices, Haar integration on the circle, and a finite-compression argument for nonseparable spaces.

Difficulty

Two obstacles stand out. First, the passage from the scalar to the complete inequality: scalar proofs exploit commutativity that fails for matrix coefficients, so a structure valid for every coefficient size at once is needed; here it is the optimal metric chosen before any test function. Proving $\kappa\le2$ for that metric requires an endpoint extremal pair (Proposition 2.2, p. 6) and an ordered density comparison (Lemma 5.1, p. 14). Second, the passage from matrices to arbitrary operators: the numerical range of a compression lies in $W(A)$, but one must show every vector of $\mathcal H\otimes\mathbb C^m$ and its image under $P[A]$ live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.

Formalization scope

• H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification $\mathcal H\otimes\mathbb C^m$ is the completion of the algebraic tensor product, and $A^k\otimes B_k$ is the completed TensorProduct.mapL.
• supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is $0$, matching the convention of Corollary 6.3.
• Holomorphic evaluation is defined by a contour integral over a CalculusContour around $K$ inside $U$; the goal asserts such contours exist and that the evaluation is contour-independent. Rational evaluation inverts aeval A denom; the goal asserts these denominators are units and that the rational evaluation agrees with the holomorphic one.
• SharpConstant is witnessed by a $2\times2$ matrix with $\sup_{W}|P|=1$ and $\|P[A]\|=2$.
• The structural milestone also includes, as an extra conjunct, that the open unit disk is admissible.

Two further published supporting statements are included as items but not milestones: existence of a finite-dimensional compression representing a given vector (a step in the proof of Corollary 6.3) and invertibility of rational denominators (the well-definedness part of the rational calculus).

Selected references

• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• V. I. Paulsen, Completely bounded homomorphisms of operator algebras, Proc. Amer. Math. Soc. 92 (1984), 225–228.
• W. Arveson, Subalgebras of C-algebras II*, Acta Math. 128 (1972), 271–308.
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

Formalization targets

Milestone: the inequality (Theorem 1.1, p. 1, first assertion)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$ and $B_0,\dots,B_d\in M_m(\mathbb C)$,

$$\Bigl\|\sum_{k=0}^dA^k\otimes B_k\Bigr\|\ \le\ 2\max_{z\in W(A)}\Bigl\|\sum_{k=0}^dB_kz^k\Bigr\| .$$

Milestone: sharpness (Theorem 1.1, p. 1, second assertion)

If the inequality holds with a constant $c$ in place of $2$ for all $n,m,d,A,B$, then $c\ge2$.

Goal: Theorem 1.1 (p. 1)

Both assertions together: the constant $2$ is valid and no smaller universal constant is.

Significance

The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension $n$, the coefficient size $m$ and the degree, including matrices whose numerical range is a point or a segment. The scalar case $m=1$ had recently been proved by other authors and the complete case was known only for $n\le3$; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete $2$-spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most $2$ making the conformal disk image of $A$ a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.

Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a $2\times2$ block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant-$2$ Crouzeix bound is known.

Difficulty

The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields $1+\sqrt2$. To reach $2$ in the complete setting, the argument must keep both multiplication orders $FG$ and $GF$ of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair $(x,y)$ of $F[A]$, represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of $\langle x, Ax\rangle$ over unit vectors of EuclideanSpace ℂ (Fin n).
• Coefficients are B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is $\sum_k A^k\otimes_{\mathrm{Kron}}B_k$ indexed by Fin n × Fin m, base factor first.
• rangeMaximum A B is the sSup of $\|P(z)\|$ over $W(A)$. Since $n\ge1$, $W(A)$ is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all $n,m\ge1$, all $d$, all $A$ and $B$.
• The goal OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.
• No normality, invertibility or nonempty-interior hypothesis is imposed on $A$.

Selected references

• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap $\lambda$, which controls convergence in $\ell^2(\pi)$ but loses a factor $1/\pi(x)$ when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant $\alpha$, introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.

The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate $2\alpha$, and at rate $4\alpha$ for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions act on the right, $Kf(x)=\sum_yK(x,y)f(y)$, and $\langle f,g\rangle=\sum_xf(x)g(x)\pi(x)$ is the inner product of $\ell^2(\pi)$, with norms $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$. The chain is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all $x,y$.

The continuous-time heat semigroup is

$$H_t=e^{-t(I-K)}=e^{-t}\sum_{n\ge0}\frac{t^n}{n!}K^n,$$

acting on functions by $H_tf(x)=\sum_yH_t(x,y)f(y)$ and on probability measures by $\mu H_t(y)=\sum_xH_t(x,y)\mu(x)$. The row $H_t^x=H_t(x,\cdot)$ is the law at time $t$ of the chain started at $x$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$; it is bilinear but not symmetric unless the chain is reversible. With

$$\mathcal L(f)=\sum_x|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

the log-Sobolev constant is

$$\alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

The relative entropy of a probability $\mu$ is $\mathrm{Ent}_\pi(\mu)=\sum_x\mu(x)\log\frac{\mu(x)}{\pi(x)}$, and the total variation distance is $\|\mu-\pi\|_{TV}=\sup_{A\subset\mathcal X}|\mu(A)-\pi(A)|$.

Formalization targets

Goal: Theorem 3.6 (p. 722)

For every probability measure $\mu$ on $\mathcal X$,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-2\alpha t},\qquad t>0,$$

and, if $(K,\pi)$ is reversible,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-4\alpha t},\qquad t>0.$$

Milestones

1. §2.1, Remarks (ii), p. 702: if $\mu=f\pi$ then $\mu H_t$ has density $H_t^*f$, where $H_t^*$ is the semigroup of the adjoint kernel $K^*(x,y)=K(y,x)\pi(y)/\pi(x)$.
2. Lemma 2.5, second part, p. 707: $\partial_t\,\mathrm{Ent}_\pi(H_tf)|_{t=0}=-\mathcal E(f,\log f)$.
3. Lemma 2.7, p. 708: $\mathcal E(\log f,f)\ge2\,\mathcal E(\sqrt f,\sqrt f)$, and $\ge4\,\mathcal E(\sqrt f,\sqrt f)$ for reversible chains.
4. §3.3, p. 722: for $f\ge0$ with $\|f\|_2=1$ and $\mu=f^2\pi$, $\mathcal L(f)=\mathrm{Ent}_\pi(\mu)$.
5. (2.8), p. 710: $2\|\mu-\pi\|_{TV}^2\le\mathrm{Ent}_\pi(\mu)\le\|\mu-\pi\|_{TV}+\tfrac12\|\mu/\pi-1\|_{\pi,2}^2$.

Companion: (3.3) (p. 723)

For an irreducible chain, every $x$ and $t>0$,

$$2\|H_t^x-\pi\|_{TV}^2\le\Big(\log\frac1{\pi(x)}\Big)e^{-2\alpha t},$$

with $2\alpha$ replaced by $4\alpha$ for reversible chains.

Significance

Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor $\log(1/\pi(x))$ replaces the factor $1/\pi(x)$ of the spectral bound $4\|H_t^x-\pi\|_{TV}^2\le\pi(x)^{-1}e^{-2\lambda t}$. When $\pi(x)$ is exponentially small in the size of the problem, as for random walks on large groups or product spaces, $\log(1/\pi(x))$ is polynomial where $1/\pi(x)$ is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from $\alpha$.

The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of $\mathcal E(\log f,f)$ with $\mathcal E(\sqrt f,\sqrt f)$, and Pinsker's inequality in the encoding used by the mixing-time library.

Difficulty

The statement is about measures, while the natural quantities to differentiate are densities with respect to $\pi$, and for a nonreversible chain the density of $\mu H_t$ evolves under the adjoint semigroup, not under $H_t$. The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from $2\alpha$ to $4\alpha$ holds only under reversibility.

The obvious first idea, differentiating $\mathrm{Ent}_\pi(\mu H_t)$ term by term, meets $\log 0$ wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary $t=0$ and the degenerate laws separately from the smooth interior. The constant $\alpha$ is defined as an infimum over all functions, with no claim that it is attained or positive.

Formalization scope

The state space is a Fintype with decidable equality, $K$ is a real matrix with the published predicate MarkovMixing.IsStochastic, $\pi$ satisfies MarkovMixing.IsStationary K π and $\pi(x)>0$ for all $x$, and reversibility is MarkovMixing.DetailedBalance K π. $H_t$ is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for $t>0$.

The local definitions are $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$, the norms $\|f\|_p$, $\mathcal L$, $\alpha$ as a real infimum over the ratios with $\mathcal L(f)\ne0$, $\mathrm{Ent}_\pi(\mu)$, and $\mu H_t$ as the row vector $\mu\,H_t$. Lean's Real.log 0 = 0 implements $0\log0=0$. The goal does not assume irreducibility: it is true for every stochastic $K$ with a positive invariant probability, and a reducible chain has $\alpha=0$. The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's $f\ge0$ is strengthened to $f>0$, because $\log f$ is $-\infty$ at a zero of $f$ on the page and $0$ in Lean.

Several encodings would make the goal trivially true and are ruled out. $\alpha$ is not assumed positive. $\mu$ is a probability, since for $\mu=2\pi$ the entropy is a positive constant in $t$. $\pi$ is invariant and positive, so $\mu/\pi$ is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying $H_t$ to $\mu$ as a function, $H_t\mu$, is not the same as $\mu H_t$ for a nonreversible chain.

A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property $\partial_tH_t=(K-I)H_t$; the adjoint identity for $H_t$; elementary convexity inequalities for $\log$ and $\sqrt{\cdot}$; the symmetric form of $\mathcal E$ for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6 (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
• L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97 (1975), 1061–1083. https://doi.org/10.2307/2373688
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. https://doi.org/10.1090/mbk/107