Functional Analysis

Motivation

The quantum harmonic oscillator is the Schrödinger operator of a particle in a quadratic potential. It describes small vibrations around an equilibrium, the modes of the electromagnetic field, and phonons in a crystal. It is also one of the very few Schrödinger operators whose spectrum and eigenfunctions are known in closed form. The eigenvalues are equally spaced, and the eigenfunctions are Hermite functions. Its algebraic treatment by creation and annihilation operators goes back to Dirac (The Principles of Quantum Mechanics, 1930). That treatment became the template for second quantization and Fock space.

The same chapter of G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009, Chapter 8, AMS page) contains two further results that use commutation relations. The first is the Heisenberg uncertainty principle (Heisenberg 1927; the general form for two observables is due to Robertson, Phys. Rev. 34 (1929)). The second is an abstract statement that $A^*A$ and $AA^*$ have the same spectrum away from $0$. Physicists call this supersymmetric quantum mechanics, and Teschl uses it later for the hydrogen atom. This mission follows Teschl's Sections 8.1–8.4.

Setting

Let $\mathfrak H$ be a complex Hilbert space. A linear operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$, its domain. $A$ is symmetric if $\mathfrak D(A)$ is dense and $\langle \varphi, A\psi\rangle = \langle A\varphi, \psi\rangle$ for all $\varphi, \psi \in \mathfrak D(A)$. For a closed operator $A$ and $z \in \mathbb C$, the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $\mathfrak H$ with a bounded inverse. The resolvent set $\rho(A)$ is the set of such $z$, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$. An operator is essentially self-adjoint on its domain if its closure $\overline A$ is self-adjoint.

For $\psi \in \mathfrak D(A)$ with $\|\psi\| = 1$ (a state), the expectation is $\mathbb E_\psi(A) = \langle\psi, A\psi\rangle$ and the mean-square deviation is $\Delta_\psi(A) = \|(A - \mathbb E_\psi(A))\psi\|$. The commutator is $[A,B]\psi = AB\psi - BA\psi$ for $\psi \in \mathfrak D(AB) \cap \mathfrak D(BA)$, where $\mathfrak D(AB) = \{\psi \in \mathfrak D(B) \mid B\psi \in \mathfrak D(A)\}$.

Fix a frequency $\omega > 0$. On $\mathbb R^3$ with Lebesgue measure, let

$$\mathfrak D_\omega = \operatorname{span}\{x^\alpha e^{-\omega|x|^2/2} \mid \alpha \in \mathbb N_0^3\} \subseteq L^2(\mathbb R^3),$$

where $x^\alpha = x_1^{\alpha_1}x_2^{\alpha_2}x_3^{\alpha_3}$ and $|x|$ is the Euclidean norm. With $\Delta = \sum_j \partial^2/\partial x_j^2$ and Teschl's units ($\hbar = 1$, mass $1/2$, so the free Hamiltonian is $H_0 = -\Delta$), the harmonic oscillator is the operator

$$H = H_0 + \omega^2 x^2, \qquad (Hf)(x) = -\Delta f(x) + \omega^2|x|^2 f(x), \qquad \mathfrak D(H) = \mathfrak D_\omega.$$

In one dimension the ladder operators on $\operatorname{span}\{x^k e^{-\omega x^2/2}\}$ are

$$A_\pm = \frac{1}{\sqrt2}\Big(\sqrt\omega\,x \mp \frac{1}{\sqrt\omega}\frac{d}{dx}\Big).$$

The Hermite polynomials are $H_n(x) = (-1)^n e^{x^2}\frac{d^n}{dx^n}e^{-x^2}$. The Hermite functions are

$$\psi_n(x) = \frac{1}{\sqrt{2^n n!}}\Big(\frac\omega\pi\Big)^{1/4} H_n(\sqrt\omega\,x)\,e^{-\omega x^2/2},$$

and on $\mathbb R^3$, $\psi_{n_1,n_2,n_3}(x) = \psi_{n_1}(x_1)\psi_{n_2}(x_2)\psi_{n_3}(x_3)$.

Formalization targets

Goal: the harmonic oscillator (Theorem 8.5)

For every $\omega > 0$ the operator $H$ above exists. It is essentially self-adjoint on $\mathfrak D_\omega$, the functions $\psi_{n_1,n_2,n_3}$, $(n_1,n_2,n_3) \in \mathbb N_0^3$, form an orthonormal basis of $L^2(\mathbb R^3)$ consisting of eigenvectors of $H$, and

$$\sigma(\overline H) = \{(2n + 3)\omega \mid n \in \mathbb N_0\}.$$

Milestones

• Density (Lemma 8.3). $\operatorname{span}\{x^\alpha e^{-|x|^2/2} \mid \alpha \in \mathbb N_0^n\}$ is dense in $L^2(\mathbb R^n)$ for every $n$.
• Canonical commutation relation (Eq. (8.36)). $[A_-, A_+] = 1$ on $\operatorname{span}\{x^k e^{-\omega x^2/2}\}$.
• Factorization (Eq. (8.37)). On the same space, $-\frac{d^2}{dx^2} + \omega^2x^2 = \omega(2N + 1)$ with $N = A_+A_-$, and the space is invariant under $A_\pm$.
• Hermite functions (Eqs. (8.40)–(8.42)). $\psi_n = A_+^n\psi_0/\sqrt{n!}$ with $\psi_0(x) = (\omega/\pi)^{1/4}e^{-\omega x^2/2}$. Each $\psi_n$ is a normalized eigenfunction of $N$ for the eigenvalue $n$, and $\operatorname{span}\{\psi_n\} = \operatorname{span}\{x^k e^{-\omega x^2/2}\}$.
• Heisenberg uncertainty principle (Theorem 8.2). For symmetric $A$, $B$ and a state $\psi \in \mathfrak D(AB) \cap \mathfrak D(BA)$,

$$\Delta_\psi(A)\,\Delta_\psi(B) \ge \tfrac12\,|\mathbb E_\psi([A,B])|,$$

with equality if $(B - \mathbb E_\psi(B))\psi = i\lambda(A - \mathbb E_\psi(A))\psi$ for a real $\lambda \ne 0$, or if $\psi$ is an eigenvector of $A$ or $B$.

• Abstract commutation (Theorem 8.6). For $A$ closed and densely defined, $A^*A|_{\operatorname{Ker}(A)^\perp}$ and $AA^*|_{\operatorname{Ker}(A^*)^\perp}$ are unitarily equivalent. $A$ maps eigenvectors of $A^*A$ (eigenvalue $E$) to eigenvectors of $AA^*$ with $\|A\psi_0\| = \sqrt E\,\|\psi_0\|$. For $z \ne 0$,

$$R_{AA^*}(z) \supseteq \tfrac1z\big(A R_{A^*A}(z) A^* - 1\big), \qquad R_{A^*A}(z) \supseteq \tfrac1z\big(A^* R_{AA^*}(z) A - 1\big).$$

The last two milestones do not enter the goal. They are the chapter's other two theorems and use the same operator-theoretic layer.

Significance

Theorem 8.5 is the rigorous form of the most used exactly solvable model of quantum mechanics. Once it is available, the Hermite functions become an orthonormal basis of $L^2(\mathbb R^3)$ that diagonalizes a concrete differential operator. That basis underlies Mehler's formula and the Fourier transform's action $\mathcal F\psi_n = (-i)^n\psi_n$ (Eq. (8.46)). Perturbation arguments around the oscillator also start from it, and so does the construction of Fock space. The uncertainty principle is the basic quantitative constraint on simultaneous measurement. Theorem 8.6 gives an eigenvalue transfer mechanism that Teschl reuses to compute the hydrogen spectrum (Section 10.4).

Formally, the mission asks for a machine-checked proof about an unbounded differential operator on $L^2(\mathbb R^3)$, stated on a concrete core. Mathlib has unbounded operators (LinearPMap, closure, adjoint), $L^p$ spaces, Gaussian integrals and the probabilists' Hermite polynomials. It has no statement identifying the spectrum of a concrete Schrödinger operator. These results are proved in every textbook, but none of them has been formalized in this form.

Difficulty

The algebra of Eqs. (8.36)–(8.41) is a finite computation with polynomials times a Gaussian. The work in the goal is analytic. Essential self-adjointness is a statement about the closure of an operator on a non-closed domain. Symmetry of $H$ together with a family of eigenvectors in $\mathfrak D_\omega$ does not give it by definition, and the relevant criterion for unbounded operators is not in Mathlib. Completeness of the eigenfunctions in $L^2(\mathbb R^3)$ is a density statement about a concrete function space (Lemma 8.3), and it has to be transferred from one dimension to three. The spectrum is asked for the closure $\overline H$, not for $H$ on $\mathfrak D_\omega$: the eigenvalues $(2n+3)\omega$ are easy to exhibit, but showing that no other point of $\mathbb C$ lies in $\sigma(\overline H)$ requires control of $(\overline H - z)^{-1}$ on all of $L^2$. Finally, the Rodrigues formula (8.42) and the ladder construction (8.40) define the same functions only after an identity for all derivatives of $e^{-x^2}$.

Formalization scope

$\mathfrak H$ is a complex inner product space with CompleteSpace; separability is not assumed, and no statement needs it. Operators are Mathlib LinearPMaps H →ₗ.[ℂ] H. $A^*$ is LinearPMap.adjoint, and every statement using it assumes a dense domain. Self-adjointness is Mathlib's IsSelfAdjoint, and essential self-adjointness is IsSelfAdjoint H.closure. $\rho$ and $\sigma$ are defined in the mission for LinearPMaps (bounded two-sided inverse of $A - z$); Mathlib's Banach-algebra spectrum is not used. $L^2(\mathbb R^n)$ is Lp ℂ 2 volume on EuclideanSpace ℝ (Fin n). The Laplacian is the sum of second Fréchet derivatives along the unit vectors. Hermite polynomials are defined by the Rodrigues formula, not as Mathlib's probabilists' Polynomial.hermite. No projection-valued measure, functional calculus or Fourier transform is taken as data.

The oscillator is not defined as a construction. IsHarmonicOscillator ω H states that $\mathfrak D(H) = \mathfrak D_\omega$ and that $H$ acts on a representative $f$ as $-\Delta f + \omega^2|x|^2 f$. This determines $H$ uniquely, and the goal also asserts that such an $H$ exists. Trivializing formalization ruled out: defining $H$ as the diagonal operator $\sum_n (2|n| + 3)\omega\langle\psi_n,\cdot\rangle\psi_n$ would make the spectrum immediate. Here $H$ is the differential operator on $\mathfrak D_\omega$, and its eigenvalues must be derived.

Two choices differ from the printed text. First, Teschl's (8.34) writes the domain with $e^{-x^2/2}$, but his (8.39)–(8.41) and the conclusion $\operatorname{span}\{\psi_n\} = \mathfrak D$ use $e^{-\omega x^2/2}$. The mission uses $\mathfrak D_\omega$, which equals (8.34) for $\omega = 1$. Lemma 8.3 is stated for (8.20)'s $\mathfrak D$ itself. Second, Theorem 8.6 prints "$H_1\psi_1 = \psi_1$", and the mission states the intended $H_1\psi_1 = E\psi_1$. The uncertainty principle adds $\|\psi\| = 1$ explicitly; the book assumes it through its definition of a state.

Reusable pieces are the product of LinearPMaps, spectrum and resolvent for unbounded operators, the Gauss–polynomial core and its density, and the Hermite-function API. Contributions of general lemmas are welcome, for example "an operator with an orthonormal eigenbasis in its domain is essentially self-adjoint" and the spectrum of such an operator.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009. bookstore.ams.org/gsm-99
• H. P. Robertson, "The Uncertainty Principle", Physical Review 34 (1929), 163–164. doi:10.1103/PhysRev.34.163
• W. Heisenberg, "Über den anschaulichen Inhalt der quantentheoretischen Kinematik und Mechanik", Zeitschrift für Physik 43 (1927), 172–198. doi:10.1007/BF01397280

Motivation

Linear second-order parabolic equations such as $u_t + Lu = f$ model diffusion with advection, growth or decay, and external sources. The heat equation is the prototype. For coefficients that are only bounded and measurable, classical solutions need not exist, and the natural well-posedness theory is the $L^2$ energy theory of weak solutions. In that theory the solution is a curve $t \mapsto u(t)$ in a Sobolev space, and the equation holds in the dual space. This framework, developed by J.-L. Lions and others in the 1950s–60s (Lions–Magenes 1972), underlies the numerical analysis of parabolic problems through finite elements and spectral Galerkin methods. It also underlies the existence theory for nonlinear evolution equations such as the Navier–Stokes equations (Temam 1977).

This mission formalizes Chapter 6 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): the existence, uniqueness and energy estimate for weak solutions of the parabolic initial–boundary value problem, proved by the Galerkin method. It also formalizes the vector-valued calculus on Hilbert triples that the proof rests on, and the Ehrling and Aubin–Lions compactness results of §6.6.

Setting

Let $\Omega \subset \mathbb{R}^n$ be a bounded open set and $T > 0$. $H^1_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in the norm $\|u\|_{H^1_0}^2 = \int_\Omega (u^2 + |Du|^2)\,dx$. $H^{-1}(\Omega)$ is its dual, with pairing $\langle f, v\rangle$. Every $u \in L^2(\Omega)$ acts on $H^1_0(\Omega)$ by $v \mapsto \int_\Omega uv\,dx$.

The operator is $Lu = -\sum_{i,j}\partial_i(a^{ij}\partial_j u) + \sum_j b^j\partial_j u + cu$. Its coefficients satisfy Assumption 6.1: $a^{ij}, b^j, c \in L^\infty(\Omega\times(0,T))$, $a^{ij} = a^{ji}$, and uniform ellipticity $\sum a^{ij}\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$. The associated form is

$$a(u, v; t) = \sum_{i,j}\int_\Omega a^{ij}\partial_i u\,\partial_j v\,dx + \sum_j\int_\Omega b^j\partial_j u\,v\,dx + \int_\Omega c\,uv\,dx.$$

A function $u : [0,T] \to H^1_0(\Omega)$ has weak time derivative $u_t = w$ if $\int_0^T \phi'(t)u(t)\,dt = -\int_0^T\phi(t)w(t)\,dt$ for all $\phi \in C_c^\infty(0,T)$, with Bochner integrals in $H^{-1}(\Omega)$. Given $f \in L^2(0,T;H^{-1}(\Omega))$ and $g \in L^2(\Omega)$, $u$ is a weak solution of

$$u_t + Lu = f \ \text{in } \Omega\times(0,T), \qquad u = 0 \ \text{on } \partial\Omega, \qquad u(0) = g$$

when three conditions hold. First, $u \in L^2(0,T;H^1_0)$ and $u_t \in L^2(0,T;H^{-1})$. Second, $\langle u_t(t), v\rangle + a(u(t), v; t) = \langle f(t), v\rangle$ for every $v \in H^1_0(\Omega)$ and a.e. $t$. Third, $u(0) = g$, where the value at $0$ is that of the continuous representative in $C([0,T];L^2(\Omega))$.

The Galerkin approximations use an $L^2$-orthonormal basis $\{w_k\}$ of Dirichlet eigenfunctions and the spaces $E_N = \langle w_1, \dots, w_N\rangle$. The approximation $u_N : [0,T] \to E_N$ solves the projected equation $(u_{Nt}, v)_{L^2} + a(u_N, v; t) = \langle f, v\rangle$ for $v \in E_N$, with $u_N(0) = P_N g$.

A Hilbert triple $\mathcal{V} \hookrightarrow \mathcal{H} \hookrightarrow \mathcal{V}'$ consists of two separable Hilbert spaces $\mathcal{V}$, $\mathcal{H}$ and the dual $\mathcal{V}'$, with dense continuous injective embeddings and $\langle f, v\rangle = (f, v)_{\mathcal{H}}$ for $f \in \mathcal{H}$. The model is $H^1_0 \hookrightarrow L^2 \hookrightarrow H^{-1}$.

Formalization targets

Goal: Theorem 6.3

For every $f \in L^2(0,T;H^{-1}(\Omega))$ and $g \in L^2(\Omega)$ there is a unique weak solution $u \in C([0,T];L^2) \cap L^2(0,T;H^1_0)$ with $u_t \in L^2(0,T;H^{-1})$. There is also a constant $C = C(\Omega, T, L)$ such that

$$\|u\|_{L^\infty(0,T;L^2)} + \|u\|_{L^2(0,T;H^1_0)} + \|u_t\|_{L^2(0,T;H^{-1})} \le C\big(\|f\|_{L^2(0,T;H^{-1})} + \|g\|_{L^2}\big).$$

Milestones

• Theorem 6.41. If $u \in L^2(0,T;\mathcal{V})$ and $u_t \in L^2(0,T;\mathcal{V}')$, then $u \in C([0,T];\mathcal{H})$. Moreover $\frac{d}{dt}(u,v)_{\mathcal{H}} = \langle u_t, v\rangle$, $\frac{d}{dt}\|u\|^2_{\mathcal{H}} = 2\langle u_t, u\rangle$, and $\|u\|_{L^\infty(\mathcal{H})} \le C(\|u\|_{L^2(\mathcal{V})} + \|u_t\|_{L^2(\mathcal{V}')})$.
• Theorem 6.42. $\int_0^T\langle u_t, v\rangle\,dt = (u(T),v(T))_{\mathcal{H}} - (u(0),v(0))_{\mathcal{H}} - \int_0^T\langle u, v_t\rangle\,dt$.
• Proposition 6.5. Each Galerkin problem has a unique solution $u_N$.
• Proposition 6.6. The energy estimate above holds for $u_N$ with $C$ independent of $N$.
• Proposition 6.7. A subsequence of $u_N$ converges weakly to a weak solution satisfying the estimate.
• Lemma 6.10 (Ehrling) and Theorem 6.9 (Aubin–Lions). These are further results of the chapter, stated for Banach spaces $X \hookrightarrow Y \hookrightarrow Z$ with $X$ compactly embedded in $Y$.

Significance

Theorem 6.3 is the basic well-posedness theorem for linear parabolic equations with rough coefficients. It gives existence and uniqueness, and continuous dependence on the data through the linear estimate. The same argument gives the Galerkin convergence that justifies spectral and finite-element semi-discretizations. The Hilbert-triple calculus of Theorems 6.41–6.42 is the standard setting for linear and nonlinear evolution equations. The Aubin–Lions lemma is the compactness tool for nonlinear problems, such as the semilinear heat equation of §6.6 and the Navier–Stokes equations of §6.7.

All of these results are classical and proved in the notes, except that Theorem 6.41's proof leans on vector-valued mollification. As far as a search of the platform shows, none of them is formalized there. Mathlib has the Bochner integral, $L^p$ spaces of Banach-valued functions and Gronwall's inequality. It does not have weak derivatives of vector-valued functions, Hilbert triples, or evolution-equation existence theorems. The work here is therefore to formalize known proofs, and in doing so to build reusable infrastructure for time-dependent PDEs.

Difficulty

The main obstacle is that the natural objects are equivalence classes of vector-valued functions, not functions. The initial condition $u(0) = g$ is meaningless for an element of $L^2(0,T;H^1_0)$ until Theorem 6.41 provides a continuous representative. Its proof needs extension across the endpoints and mollification of $\mathcal{V}$-valued functions. Passing to the limit in the Galerkin scheme needs weak compactness in $L^2(0,T;H^1_0)$ and $L^2(0,T;H^{-1})$, identified with a dual Bochner space. Proposition 6.5 is a linear ODE system whose coefficients are only $L^\infty$ in time, so the Picard–Lindelöf theorem for continuous right-hand sides does not apply directly. The $H^{-1}$ bound on $u_{Nt}$ needs the projection $P_N$ to be bounded on $H^1_0$ as well as on $L^2$, which is why the basis is taken to be eigenfunctions. Uniqueness needs the energy identity (6.46) and a Gronwall argument in weak form.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. H10 n Ω is the closure of the jets $(\phi, \nabla\phi)$, $\phi \in C_c^\infty(\Omega)$, in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$, so its norm is the full $H^1$ norm. Hm1 n Ω is StrongDual ℝ (H10 n Ω). l2Embed is the embedding $H^1_0 \hookrightarrow L^2 \hookrightarrow H^{-1}$.
• $L^p(0,T;X)$ is MemLp for Lebesgue measure on $(0,T)$, and norms are eLpNorm with values in $[0,\infty]$. Constants are finite nonnegative reals. Every constant is quantified before the data it must not depend on: before $f$, $g$ in Theorem 6.3, and before the basis, $f$, $g$, $N$ in Propositions 6.6–6.7.
• The weak time derivative is (6.14) in its standard form $\int\phi' u = -\int\phi w$. The page prints $\phi$ and $\phi'$ interchanged, which is a typo.
• Weak solutions take $g \in L^2(\Omega)$ as in Assumption 6.1(3). The printed Theorem 6.3 says $g \in H^1_0(\Omega)$, a special case. $u(0) = g$ is read through a continuous representative $\tilde u \in C([0,T];L^2)$, and uniqueness means equality for a.e. $t$.
• Coefficient conditions and ellipticity hold almost everywhere on $\Omega\times(0,T)$. The Galerkin basis is a hypothesis: an orthonormal basis of $L^2(\Omega)$ of weak Dirichlet eigenfunctions.
• Proposition 6.7 states weak convergence of $u_{N_k}$ in $L^2(0,T;H^1_0)$ and of $u_{N_k t}$ in $L^2(0,T;H^{-1})$, in the explicit integral form of p. 186. This is at least as strong as the printed claim.
• Hilbert triples are structures with two continuous injective dense-range embeddings, separability, and the compatibility identity. Reflexivity in Theorem 6.9 is surjectivity of the canonical map into the bidual.
• Ruling out trivializations. Every Bochner integral in a definition has an integrable integrand under the stated $L^2$ hypotheses, so no weak-derivative or weak-solution condition holds through the integral's junk value $0$. The initial condition is imposed on a continuous representative, so it is not vacuous on a null set.
• Reusable infrastructure welcome: vector-valued mollification and extension, the Hilbert-triple calculus, and dual identification of $L^2(0,T;X)'$.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 6. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, AMS, 2010, §7.1. https://doi.org/10.1090/gsm/019
• J.-L. Lions and E. Magenes, Non-Homogeneous Boundary Value Problems and Applications I, Springer, 1972. https://doi.org/10.1007/978-3-642-65161-8
• R. Temam, Navier–Stokes Equations: Theory and Numerical Analysis, North-Holland, 1977; AMS Chelsea reprint 2001. https://doi.org/10.1090/chel/343
• J. Simon, Compact sets in the space $L^p(0,T;B)$, Ann. Mat. Pura Appl. 146 (1987), 65–96. https://doi.org/10.1007/BF01762360

Motivation

A differentiable convex function on $\mathbb{R}^n$ is determined, up to an additive constant, by its gradient, and a vector field is a gradient of a convex function exactly when it satisfies a monotonicity condition along closed cycles. Convex analysis and optimization need the same statement for nonsmooth and extended-valued functions on infinite-dimensional spaces: the subdifferential replaces the gradient, and the question becomes which multivalued maps from a Banach space to its dual arise as subdifferentials, and how much of the function they determine. The answer underlies the treatment of optimality conditions, variational inequalities and evolution equations governed by subdifferentials, where one works with the operator $\partial f$ and needs to recover $f$ from it.

Timeline.

• 1966: R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (DOI 10.2140/pjm.1966.17.497), studied cyclically monotone operators and stated the characterization of subdifferentials as the maximal cyclically monotone operators (its Theorem 3), together with the maximal monotonicity of subdifferentials (its Theorem 4).
• 1969: H. Brézis pointed out a gap in the 1966 proofs of maximality and uniqueness: a family of dual vectors $x_\varepsilon^*$ used in the argument might increase unboundedly in norm as $\varepsilon \to 0$.
• 1970: Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (DOI 10.2140/pjm.1970.33.209), repaired the argument for arbitrary real Banach spaces, proving Theorem A (maximal monotonicity of $\partial f$) and Theorem B (the characterization treated here).

Setting

Let $E$ be a real Banach space with dual $E^*$, and write $\langle x, x^* \rangle$ for the value of $x^* \in E^*$ at $x \in E$. A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$, not identically $+\infty$, with $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 (lsc) in the norm topology. Its subdifferential is the multivalued map

$$\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 a cyclically monotone operator if

$$\langle x_0 - x_1, x_0^* \rangle + \cdots + \langle x_{n-1} - x_n, x_{n-1}^* \rangle + \langle x_n - x_0, x_n^* \rangle \ge 0 \qquad\text{whenever } x_i^* \in T(x_i),\ i = 0, \dots, n,$$

and maximal cyclically monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other cyclically monotone operator. The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} (\langle x, x^* \rangle - f(x))$ on $E^*$, and $j(x) = \tfrac12\|x\|^2$. In the Lean development these are ProperConvex, subdiff, IsCyclicallyMonotone, IsMaximalCyclicallyMonotone, conj and halfSqNorm, in the namespace RockafellarMaxMono.Cyclic.

Formalization targets

Goal: Theorem B (p. 210)

For every multivalued map $T : E \to E^*$ on a real Banach space $E$,

$$\bigl(\exists f \text{ lsc proper convex with } T = \partial f\bigr) \iff T \text{ is maximal cyclically monotone},$$

and if $f$ and $g$ are lsc proper convex with $\partial f = T = \partial g$, then $g = f + c$ for a real constant $c$. Both halves are one statement.

Milestones, in attack order

1. (3.7) For a finite continuous convex function $f$ on a real Banach space, $\partial f(x)$ is nonempty and weak* compact and $f'(x;u) = \max\{\langle u, x^* \rangle \mid x^* \in \partial f(x)\}$.
2. Finite continuous case (pp. 214–215). For finite continuous convex $f, g$ on a real Banach space, $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$.
3. (3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for lsc proper convex $f$.
4. Proposition 1 $x^{**} \in \partial f^*(x^*)$ if and only if $x^{**}$ is a weak** limit of a bounded net $x_i$ with $x_i^* \in \partial f(x_i)$, $x_i^* \to x^*$ in norm.
5. (p. 213) $(f + j)^*$ is finite and continuous on $E^*$.
6. (p. 211) $f^{**}$ restricted to $E$ is $f$.
7. (3.6) For lsc proper convex $f, g$: $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$.

Significance

The result. Theorem B gives an intrinsic description of subdifferential maps: an operator is the subdifferential of a closed proper convex function if and only if it satisfies the cycle inequality and cannot be enlarged without violating it. The uniqueness clause says that a closed convex function is recovered from its subdifferential up to a constant, the nonsmooth counterpart of recovering a function from its gradient. Milestone 7 is stronger than uniqueness: a one-sided inclusion $\partial f \subseteq \partial g$ already forces $g = f + c$, and this is what gives maximality.

Formalizing it. The theorem is proved in the paper, and nothing of it is formalized on the platform. Mathlib has convex functions, continuous duals, biduals and weak-* topologies, but not extended-valued subdifferentials on Banach spaces, conjugate duality in the nonreflexive setting, or monotone operator theory. This mission produces formal statements of the paper's steps, the standard max formula for directional derivatives on a Banach space, and the Fenchel conjugate facts the argument uses, each as a separate target.

Difficulty

In a reflexive space the argument is short, because $\partial f^*$ is the inverse of $\partial f$. In a nonreflexive space it is not: $\partial f^*$ maps $E^*$ into $E^{**}$, and points of $E^{**} \setminus E$ appear. The naive route, transferring the inclusion $\partial f \subseteq \partial g$ to the conjugates by inverting the maps, breaks down there, and the 1966 argument failed at a related step, where the dual vectors in an approximation could be unbounded. Relating $\partial f^*$ to $\partial f$ without reflexivity is where the difficulty sits; the boundedness of the approximating nets in Proposition 1 is essential and cannot be dropped. The finite continuous case and the max formula (3.7) are needed on an arbitrary Banach space, including the dual $E^*$, not only on $E$.

Formalization scope

$E$ is a real Banach space (NormedAddCommGroup, NormedSpace ℝ, CompleteSpace); $E^*$ is StrongDual ℝ E with the operator norm, $E^{**}$ is StrongDual ℝ (StrongDual ℝ E), and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual. No reflexivity, inner product or finite dimension is assumed. Explicit readings:

• Values in $(-\infty, +\infty]$ are EReal with the requirement $f(x) \ne -\infty$; convexity is the paper's inequality for $0 < \lambda < 1$ in EReal arithmetic. Lower semicontinuity is in the norm topology.
• A multivalued map is E → Set (StrongDual ℝ E); $T = \partial f$ means $T(x) = \partial f(x)$ for every $x$.
• The cycle inequality quantifies over all $n \in \mathbb{N}$ and points indexed by Fin (n + 1) with wrap-around addition, so the last term is $\langle x_n - x_0, x_n^* \rangle$. Maximality is graph inclusion among cyclically monotone operators, not among monotone operators.
• The uniqueness constant is a real number, never $\pm\infty$.
• "$\supset$" in (3.6) is non-strict inclusion, and the hypothesis is one-sided.
• A net is a nonempty directed partially ordered index type with convergence along atTop; weak** convergence is pointwise convergence on $E^*$; "bounded" is a uniform norm bound.
• "Finite and continuous" for $(f+j)^*$ means equal everywhere to a continuous real-valued function. The max in (3.7) is IsGreatest, so it is attained; the directional derivative is the limit along $\lambda \to 0^+$.
• The print's "$\partial(f + j) = \partial f(x) + \partial j(x)$" in (3.1) is read as $\partial(f+j)(x)$.

A formalization that drops lower semicontinuity, allows an extended-real constant, or replaces "maximal cyclically monotone" by "maximal monotone" states a different, and in the first two cases false or trivial, theorem; the statements here keep all three.

The proof reduces Theorem B to milestone 7 through Theorem 1 of Rockafellar (1966) and its Corollary 2, which are not stated in this paper and are not milestones; formal statements of them are welcome as supporting theorems. Contributions of reusable infrastructure are welcome: extended-valued subdifferentials and conjugates on normed spaces, the Fenchel–Moreau identity on $E$, the sum rule with a continuous function, and the max formula for directional derivatives.

Selected references

• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 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 J. Math. 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
• J.-J. Moreau, Fonctionnelles convexes, mimeographed lecture notes, Collège de France, 1967.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Many linear partial differential equations of evolution type — the heat equation, the Schrödinger equation, linear wave and Klein–Gordon equations, linearized reaction–diffusion and Kuramoto–Sivashinsky equations — can be written as an ordinary differential equation

$$u_t = Au, \qquad u(0) = f,$$

in a Banach space $X$ of functions, where $A$ is a spatial differential operator. When $A$ is bounded, the solution is the operator exponential $e^{tA}f$. Differential operators are unbounded, however, and then the solution operators $f \mapsto u(t)$ are only continuous in time in the strong sense and may exist only forward in time. Semigroup theory makes this picture rigorous: it characterizes exactly which operators $A$ generate a well-posed evolution, and it is the standard route from energy estimates to existence and uniqueness for linear and semilinear evolution equations (Duhamel's formula, §5.4.5 of the notes, used for the semilinear heat equation in §5.5).

This mission formalizes §5.4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): uniformly continuous groups, strongly continuous semigroups and their generators, the Hille–Yosida theorem, the Lumer–Phillips theorem and Stone's theorem.

Timeline. The generation theorem for contraction semigroups is due independently to E. Hille (1948) and K. Yosida (1948); the general version with constants $M$, $a$ to Feller, Miyadera and Phillips (1952–53). G. Lumer and R. S. Phillips (1961) recast the contraction case in terms of dissipative operators. Stone's theorem on one-parameter unitary groups dates from 1930–32. Standard modern accounts are Pazy (1983) and Engel–Nagel (2000).

Setting

Let $X$ be a Banach space over $\mathbb{K} = \mathbb{R}$ or $\mathbb{C}$, and $\mathcal{L}(X)$ the Banach space of bounded linear operators on $X$ with the operator norm.

A uniformly continuous group is a family $\{T(t) : t \in \mathbb{R}\} \subset \mathcal{L}(X)$ with $T(0) = I$, $T(s)T(t) = T(s+t)$, and $T(h) \to I$ in operator norm as $h \to 0$. A strongly continuous (C₀) semigroup is a family $\{T(t) : t \ge 0\} \subset \mathcal{L}(X)$ with $T(0) = I$, $T(s)T(t) = T(s+t)$ for $s, t \ge 0$, and $T(h)f \to f$ as $h \to 0^+$ for every $f \in X$; it is a contraction semigroup if $\|T(t)\| \le 1$ for all $t \ge 0$. A C₀ group has the same properties for all $s, t \in \mathbb{R}$; on a complex Hilbert space it is unitary if every $T(t)$ is unitary.

An operator $A : \mathcal{D}(A) \subset X \to X$ is a linear map defined on a subspace $\mathcal{D}(A)$. The generator of a C₀ semigroup is the operator $A$ whose domain is the set of $f$ for which

$$Af = \lim_{h \to 0^+} \frac{T(h)f - f}{h}$$

exists in norm, with $Af$ this limit. $A$ is closed if its graph $\{(f, Af) : f \in \mathcal{D}(A)\}$ is closed in $X \times X$, and densely defined if $\mathcal{D}(A)$ is dense. A scalar $\lambda$ is in the resolvent set of $A$ if $\lambda I - A : \mathcal{D}(A) \to X$ is a bijection, and then $R(\lambda, A) = (\lambda I - A)^{-1}$ is the resolvent. $A$ is dissipative if $\lambda\|f\| \le \|(\lambda I - A)f\|$ for all real $\lambda > 0$ and $f \in \mathcal{D}(A)$, and m-dissipative if in addition $\lambda I - A$ is onto $X$ for some $\lambda > 0$. On a complex Hilbert space $\mathcal{H}$, $A$ is self-adjoint if $\mathcal{D}(A)$ is dense, $\mathcal{D}(A) = \mathcal{D}(A^*)$, and $(x, Ay) = (Ax, y)$ for $x, y \in \mathcal{D}(A)$.

Formalization targets

Goal: the Lumer–Phillips theorem (Theorem 5.38)

For an operator $A : \mathcal{D}(A) \subset X \to X$,

$$A \text{ generates a C₀ contraction semigroup on } X \iff A \text{ is closed, densely defined and m-dissipative.}$$

Milestones

1. Theorem 5.24. A uniformly continuous group is smooth in operator norm, $A = T'(0) \in \mathcal{L}(X)$ exists, and $T(t) = e^{tA}$ for all $t \in \mathbb{R}$.
2. Theorem 5.32. The generator of a C₀ semigroup is closed and densely defined.
3. Theorem 5.35 (Hille–Yosida). $A$ generates a C₀ semigroup if and only if, for some $M \ge 1$ and $a \in \mathbb{R}$, $A$ is closed and densely defined, $(a, \infty)$ lies in the resolvent set, and

$$\|R(\lambda, A)^n\| \le \frac{M}{(\lambda - a)^n} \qquad (\lambda > a,\ n \in \mathbb{N});$$

in that case $\|T(t)\| \le M e^{at}$ for $t \ge 0$. 4. Corollary 5.36. The contraction case: $M = 1$, $a = 0$, with $\|R(\lambda, A)\| \le 1/\lambda$. 5. Theorem 5.42 (Stone). On a complex Hilbert space, $iA$ generates a C₀ unitary group if and only if $A$ is self-adjoint.

Significance

The result itself. The Lumer–Phillips theorem is the working form of generation theory for PDEs: to show that $u_t = Au$ is well posed with $\|u(t)\| \le \|u(0)\|$, it suffices to prove an energy inequality (dissipativity) and to solve a single resolvent equation $\lambda f - Af = g$. The notes apply it to the Laplacian on $H^2(\mathbb{R}^n) \subset L^2(\mathbb{R}^n)$ and, after a shift, to the linearized Kuramoto–Sivashinsky operator; later chapters use the resulting semigroups in Duhamel's formula to construct solutions of semilinear heat and Schrödinger equations. Hille–Yosida gives the general growth bound $\|T(t)\| \le Me^{at}$, and Stone's theorem identifies unitary quantum dynamics with self-adjoint Hamiltonians.

Formalizing it. All results are classical and proved in the literature; the notes themselves state 5.32, 5.35, 5.36, 5.38 and 5.42 without proof, referring to standard texts. Mathlib currently has the operator exponential on Banach algebras, partially defined linear maps (LinearPMap) with closedness, closures and adjoints, but no theory of C₀ semigroups or their generators. A complete development would give Lean a reusable generation theory for unbounded operators, on which parabolic and dispersive PDE existence results can rest.

Difficulty

The central obstacle is the passage from resolvent information to a semigroup. Formally $T(t) = e^{tA}$, but for unbounded $A$ the exponential series is meaningless, and the necessity directions require showing that the resolvent is a Laplace transform of the semigroup, which needs integration of strongly (not norm) continuous operator-valued functions. The sufficiency directions must construct a semigroup from $A$ by an approximation of the unbounded generator and a limit that converges only strongly, and then identify the generator of the limit with $A$ — including its domain, which is where most careless arguments fail. In the Lumer–Phillips theorem, surjectivity of $\lambda I - A$ is assumed for a single $\lambda > 0$ and must be propagated to every $\lambda > 0$. In Stone's theorem both directions need domain arguments for unbounded operators on Hilbert space; symmetry of $A$ alone is not enough.

Formalization scope

• Scalars: a field 𝕜 with [RCLike 𝕜] (ℝ or ℂ), and X a Banach space over it ([NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X]). Stone's theorem is over ℂ on an InnerProductSpace ℂ H with [CompleteSpace H]. Theorem 5.24 additionally equips X with a compatible real structure ([NormedSpace ℝ X] [IsScalarTower ℝ 𝕜 X]) so that $t \mapsto T(t)$ can be differentiated; $e^{tA}$ is Mathlib's NormedSpace.exp, and $C^\infty$ is ContDiff ℝ ∞.
• Operators $A : \mathcal{D}(A) \subset X \to X$ are X →ₗ.[𝕜] X (LinearPMap); closedness is LinearPMap.IsClosed (closed graph).
• Semigroups are functions T : ℝ → X →L[𝕜] X; for semigroups only the values at $t \ge 0$ enter. Composition is multiplication in X →L[𝕜] X.
• The generator relation IsGenerator T A states, for all $f, g$: the right difference quotient $h^{-1}(T(h)f - f)$ tends to $g$ as $h \to 0^+$ if and only if $f \in \mathcal{D}(A)$ and $Af = g$. So "$A$ generates a semigroup" means that $A$ equals the generator including its domain; a formalization in which $A$ merely agrees with the limit on some subspace, or in which the generator is a restriction, would make the theorems different (and false) statements, and is ruled out.
• Resolvent norm bounds $\|R(\lambda, A)^n\| \le c$ are stated pointwise, $\|R(\lambda,A)^n g\| \le c\|g\|$ for all $g$, which is equivalent. In (5.24) $n = 0$ is included, which adds nothing because $M \ge 1$. The "in that case" clause of Theorem 5.35 is a second conjunct: for every semigroup generated by $A$ and every $M, a$ satisfying the three conditions, $\|T(t)\| \le Me^{at}$.
• Closedness and density, which the notes build into the definitions of the resolvent set and of dissipativity, are stated explicitly wherever they are used (they appear as condition (1) in every theorem).
• The generator of a C₀ group (Stone) is the generator of its forward part, as in Definition 5.30; the operator $iA$ is Complex.I • A, with the same domain as $A$. Self-adjointness is Definition 5.41 as printed, not Mathlib's IsSelfAdjoint for LinearPMap, although the two agree.
• Useful infrastructure, reusable beyond this mission: Riemann/Bochner integration of strongly continuous operator families, the Laplace-transform representation of the resolvent, Yosida approximations, and dissipativity–resolvent equivalences. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §5.4. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Springer, 1983. https://doi.org/10.1007/978-1-4612-5561-1
• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Springer GTM 194, 2000. https://doi.org/10.1007/b97696
• G. Lumer and R. S. Phillips, Dissipative operators in a Banach space, Pacific J. Math. 11 (1961), 679–698. https://doi.org/10.2140/pjm.1961.11.679
• M. H. Stone, On one-parameter unitary groups in Hilbert space, Ann. of Math. 33 (1932), 643–648. https://doi.org/10.2307/1968538
• K. Yosida, On the differentiability and the representation of one-parameter semigroup of linear operators, J. Math. Soc. Japan 1 (1948), 15–21. https://doi.org/10.2969/jmsj/00110015