Analysis

Motivation

In quantum mechanics the energy levels of a system are the eigenvalues of a self-adjoint Hamiltonian $A$, and for almost every Hamiltonian of interest (atoms with more than one electron, molecules) they cannot be computed in closed form. What can be computed are expectation values $\langle \psi, A\psi\rangle$ of explicit trial functions $\psi$. The min-max principle turns such numbers into rigorous statements about the eigenvalues: every trial computation gives an upper bound, and the optimal choices reproduce the eigenvalues exactly. It goes back to Fischer (1905) for quadratic forms in finitely many variables and to Courant (1920) for differential operators; Temple (1928) added the matching lower bound. This mission formalizes the version for unbounded self-adjoint operators with essential spectrum, as stated in Chapter 4 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), where eigenvalues below the essential spectrum are characterized and estimated.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument. An operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$, its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A$ equals its adjoint. The resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$. For self-adjoint $A$, $\sigma(A) \subseteq \mathbb R$.

For $z \in \mathbb C$ the eigenspace is $\operatorname{Ker}(A - z) = \{\psi \in \mathfrak D(A) \mid A\psi = z\psi\}$; $z$ is an eigenvalue when it is nonzero, and its dimension is the multiplicity. The discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated points of $\sigma(A)$ and have finite multiplicity, and the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$.

Let $\Sigma = \inf \sigma_{ess}(A) \in [-\infty, +\infty]$ ($+\infty$ if $\sigma_{ess}(A)$ is empty). The numbers $E_1 \le E_2 \le E_3 \le \cdots$ are the eigenvalues of $A$ below $\Sigma$, listed in increasing order and repeated according to multiplicity; if there are only $N$ of them, $E_n = \Sigma$ for $n > N$. For vectors $\psi_1, \dots, \psi_m \in \mathfrak H$ let

$$U(\psi_1, \dots, \psi_m) = \{\psi \in \mathfrak D(A) \mid \|\psi\| = 1,\ \psi \perp \psi_1, \dots, \psi_m\}.$$

Some statements involve the spectral projections $P_A(\Omega)$ of $A$, for Borel sets $\Omega \subseteq \mathbb R$: the projection-valued measure with $A = \int \lambda\, dP_A(\lambda)$. With the spectral measures $\mu_\psi(\Omega) = \langle \psi, P_A(\Omega)\psi\rangle$, the form domain is $\mathfrak Q(A) = \{\psi \mid \int |\lambda|\, d\mu_\psi(\lambda) < \infty\}$, and on it $\langle \psi, A\psi\rangle$ means $\int \lambda\, d\mu_\psi(\lambda)$.

Formalization targets

Goal: the min-max principle (Theorem 4.10)

For self-adjoint $A$ and every $n \ge 1$,

$$E_n = \sup_{\psi_1, \dots, \psi_{n-1} \in \mathfrak H} \ \inf_{\psi \in U(\psi_1, \dots, \psi_{n-1})} \langle \psi, A\psi\rangle .$$

Both sides are extended real numbers; the infimum over an empty set is $+\infty$.

Milestones

• Theorem 2.19 (the case $n = 1$ and its mirror image): $\inf \sigma(A) = \inf_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$ and $\sup \sigma(A) = \sup_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$.
• Theorem 4.12 (i): if $\psi_1, \dots, \psi_k \in \mathfrak Q(A)$ are linearly independent and $\langle \psi, A\psi\rangle < \lambda\|\psi\|^2$ for every nonzero $\psi \in \operatorname{span}\{\psi_j\}$, then $\dim \operatorname{Ran} P_A((-\infty,\lambda)) \ge k$; with $>$, $\dim \operatorname{Ran} P_A((\lambda,\infty)) \ge k$.
• Theorem 4.12 (ii): if $\psi_1, \dots, \psi_k \in \mathfrak D(A)$ are linearly independent, $\lambda_1 < \lambda_2$, and $\|(A - \tfrac{\lambda_2+\lambda_1}{2})\psi\| < \tfrac{\lambda_2-\lambda_1}{2}\|\psi\|$ for every nonzero $\psi$ in their span, then $\dim \operatorname{Ran} P_A((\lambda_1,\lambda_2)) \ge k$.
• Corollary 4.11: if $A, B$ are self-adjoint, $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\langle \psi, (A - B)\psi\rangle \ge 0$ on $\mathfrak D(A)$, then $E_n(A) \ge E_n(B)$ for all $n \ge 1$.
• Theorem 4.13 (Temple's inequality): if $\lambda_1 < \lambda_2$, $\psi \in \mathfrak D(A)$, $\|\psi\| = 1$, $\lambda = \langle \psi, A\psi\rangle \in (\lambda_1, \lambda_2)$ and $\sigma(A) \cap (\lambda_1, \lambda_2) = \{E\}$, then

$$\lambda - \frac{\|(A-\lambda)\psi\|^2}{\lambda_2 - \lambda} \le E \le \lambda + \frac{\|(A-\lambda)\psi\|^2}{\lambda - \lambda_1}.$$

Significance

The min-max principle is the standard tool for comparing eigenvalues of different operators: Corollary 4.11 (monotonicity under operator inequalities) follows from it, and with it the stability of eigenvalues under perturbations, Dirichlet–Neumann bracketing and the Rayleigh–Ritz method used in computational quantum chemistry. Theorem 4.12 converts a finite-dimensional computation into a lower bound for the number of eigenvalues in an interval, and Temple's inequality supplies lower bounds on an eigenvalue to complement the variational upper bounds, which is what makes numerical eigenvalue enclosures rigorous.

All of these results are classical and proved in the literature. What is not available is a machine-checked version for unbounded operators: Mathlib has the Courant–Fischer characterization only for finite-dimensional or compact self-adjoint operators, and existing formal developments of Temple's inequality and min-max levels treat bounded operators. This mission formalizes the unbounded case, with the essential spectrum and the counting of eigenvalues by multiplicity made explicit, and with the edge cases (operators unbounded below, empty essential spectrum) covered by extended-real values.

Difficulty

The central difficulty is that $E_n$ is defined by spectral data (which points of the spectrum are isolated eigenvalues of finite multiplicity, and how many there are below a given level), while the right-hand side is defined by expectation values on the domain. Relating the two needs the spectral theorem for unbounded operators: for every level below $\Sigma$ the spectral subspace must be shown to be finite dimensional and spanned by eigenvectors, and for the level $\Sigma$ itself one needs infinite-dimensional spectral subspaces in every neighbourhood, which is where the essential spectrum enters. When $E_n = \Sigma$ the supremum and infimum need not be attained, so the finite-dimensional argument with eigenvectors does not transfer. For Corollary 4.11 and Temple's inequality the hypotheses concern only the operator and one vector, while the conclusions concern the spectrum.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint, which includes a dense domain. The Hilbert space is not assumed separable. The spectrum is the resolvent spectrum defined above, not Mathlib's Banach-algebra spectrum, and for self-adjoint operators it enters through its real points. Eigenspace dimensions are cardinals (Module.rank). $E_n$ is defined from the spectrum, the essential spectrum and these dimensions, as an element of EReal, indexed from $n = 1$; if $A$ is unbounded below its value is $-\infty$, and if the essential spectrum is empty and the eigenvalues run out it is $+\infty$. The min-max identity is stated in EReal, with $\langle\psi, A\psi\rangle$ entering through its real part.

A formalization that defines $E_n$ as the min-max expression itself would make the goal true by definition. This is ruled out: $E_n$ is defined only from the spectrum, the essential spectrum and the dimensions of eigenspaces.

The spectral theorem is not part of this mission. Theorem 4.12 takes a projection-valued measure $P$ on the Borel sets of $\mathbb R$ as data, together with the hypothesis that $A = \int \lambda\, dP(\lambda)$ (domain $\{\psi \mid \int \lambda^2 d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int \lambda\, d\mu_\psi$), which is the form the spectral theorem guarantees; $P_A$ is then $P$, and $\mathfrak Q(A)$ and the quadratic form are defined from it. Nothing else the book derives is taken as a hypothesis. The goal, Theorem 2.19, Corollary 4.11 and Temple's inequality use no projection-valued measure. Corollary 4.11 states the domain inclusion $\mathfrak D(A) \subseteq \mathfrak D(B)$ explicitly, as the meaning of $A - B \ge 0$.

A complete development needs the spectral theorem for unbounded self-adjoint operators (or an equivalent functional calculus), the identification of $\sigma_{ess}$ with the points where spectral projections have infinite rank, and the orthogonality of eigenspaces. These are reusable across the rest of the book. Proofs of any milestone, and of lemmas connecting the resolvent spectrum with spectral projections, are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Theorem 2.19 (p. 77), Section 4.3–4.4 (pp. 117–120), essential spectrum (p. 145).
• E. Fischer, Über quadratische Formen mit reellen Koeffizienten, Monatshefte für Mathematik und Physik 16 (1905), 234–249. doi:10.1007/BF01693781.
• R. Courant, Über die Eigenwerte bei den Differentialgleichungen der mathematischen Physik, Mathematische Zeitschrift 7 (1920), 1–57. doi:10.1007/BF01199396.
• G. Temple, The theory of Rayleigh's principle as applied to continuous systems, Proceedings of the Royal Society of London A 119 (1928), 276–293. doi:10.1098/rspa.1928.0098.

Why the endpoint behaviour of Sturm–Liouville operators matters

A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression

$$\tau f = \frac{1}{r}\big(-(pf')' + qf\big)$$

on an interval $I = (a, b)$. The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at $a$ and $b$. Whether a boundary condition is needed at all depends on the behaviour of $\tau$ near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of $\tau u = z u$ are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.

Setting

Let $-\infty \le a < b \le \infty$ and $I = (a,b)$. The coefficients satisfy: $p^{-1} \in L^1_{loc}(I)$ with $p > 0$; $q \in L^1_{loc}(I)$ real-valued; $r \in L^1_{loc}(I)$ with $r > 0$. The Hilbert space is $L^2(I, r\,dx)$ with $\langle f, g\rangle = \int_a^b f^* g\, r\,dx$.

A function $f$ is locally absolutely continuous, $f \in AC_{loc}(I)$, if it is an indefinite integral of a locally integrable function on $I$. The equation $\tau f = g$ means that $f$ and its quasi-derivative $pf'$ both lie in $AC_{loc}(I)$ and $-(pf')' + qf = rg$ almost everywhere. A solution of $(\tau - z)u = 0$, $z \in \mathbb{C}$, is a complex-valued $u$ with $\tau u = z u$ in this sense. The maximal domain is

$$\mathfrak{D}(\tau) = \{ f \in L^2(I, r\,dx) \mid f, pf' \in AC_{loc}(I),\ \tau f \in L^2(I, r\,dx) \}.$$

The modified Wronskian is $W_x(f_1, f_2) = f_1(x)(pf_2')(x) - (pf_1')(x) f_2(x)$, with no complex conjugation, and $W_a(f_1, f_2) = \lim_{x \to a} W_x(f_1, f_2)$, $W_b$ likewise.

$\tau$ is limit circle (l.c.) at $a$ if there is a $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ and $W_a(v, f) \ne 0$ for some $f \in \mathfrak{D}(\tau)$; otherwise it is limit point (l.p.) at $a$. The same holds at $b$. A function $u$ is square integrable near $a$ if $\int_a^c |u|^2 r\,dx < \infty$ for some $c \in I$.

Formalization targets

Goal: the Weyl alternative (Theorem 9.9)

For every Sturm–Liouville expression as above,

$$\tau \text{ is l.c. at } a \iff \text{for one } z_0 \in \mathbb{C}, \text{ all solutions of } (\tau - z_0)u = 0 \text{ are square integrable near } a,$$

and if $\tau$ is l.c. at $a$, then for every $z \in \mathbb{C}$ all solutions of $(\tau - z)u = 0$ are square integrable near $a$. The same two statements hold at $b$.

Milestones

1. Theorem 9.1. For $rg \in L^1_{loc}(I)$, $c \in I$, $\alpha, \beta \in \mathbb{C}$, the problem $(\tau - z) f = g$, $f(c) = \alpha$, $(pf')(c) = \beta$ has a unique solution, entire in $z$.
2. Lemma 9.2. If $u_1, u_2$ solve $(\tau - z)u = 0$ with $W(u_1, u_2) = 1$, every solution of $(\tau - z)f = g$ is given by the variation-of-constants formula (9.10).
3. Eq. (9.7). For $f, g \in \mathfrak{D}(\tau)$ the limits $W_a(g^*, f)$, $W_b(g^*, f)$ exist and $\langle g, \tau f\rangle = W_a(g^*, f) - W_b(g^*, f) + \langle \tau g, f\rangle$ (the printed $W_b - W_a$ has the wrong sign for the Wronskian (9.5)).
4. Lemma 9.5. If $v \in \mathfrak{D}(\tau)$, $W_a(v^*, v) = 0$ and $W_a(v^*, \hat f) \ne 0$ for some $\hat f \in \mathfrak{D}(\tau)$, then $W_a(v, f) = 0 \Leftrightarrow W_a(v, f^*) = 0$, and $W_a(v, f) = W_a(v, g) = 0 \Rightarrow W_a(g^*, f) = 0$.
5. Theorem 9.6. The operator $Af = \tau f$ on $\mathfrak{D}(A) = \{ f \in \mathfrak{D}(\tau) \mid W_a(v, f) = 0 \text{ if l.c. at } a,\ W_b(w, f) = 0 \text{ if l.c. at } b\}$ is self-adjoint, and the set $\mathfrak{D}_1$ of (9.21) is a core.
6. Lemma 9.7. For $z \in \rho(A)$ there are solutions $u_a$, $u_b$ of $(\tau - z)u = 0$, square integrable near $a$ resp. $b$ and satisfying the boundary condition there, and $(A - z)^{-1}$ is the integral operator with the Green function (9.28).

Significance

The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator $-d^2/dx^2 + q$ on a half-line needs a boundary condition at infinity, or whether $-\Delta + V$ with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of $z$. Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh $m$-functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.

The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.

Difficulty

The definition of limit circle refers only to $\mathfrak{D}(\tau)$ and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all $z \in \mathbb{C}$. The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for $z \in \rho(A)$, and so only for nonreal $z$ in general. Extending the conclusion to real $z$, where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.

Formalization scope

• Interval and coefficients. The structure SLData bundles $a, b \in$ EReal with $a < b$ (infinite endpoints allowed), $p, q, r : \mathbb{R} \to \mathbb{R}$, and the standing hypotheses (i)–(iii) of p. 181; $p, r > 0$ pointwise on $I$. $L^2(I, r\,dx)$ is Lp ℂ 2 for the measure $r\,dx$ on $I$.
• Regularity. $AC_{loc}(I)$ is encoded by its integral characterization. The quasi-derivative $pf'$ is the continuous function $f^{[1]} \in AC_{loc}(I)$ with $f(y) - f(x) = \int_x^y f^{[1]}/p$, chosen by Classical.choose (it is unique on $I$). $\tau f = g$ is $(pf')(y) - (pf')(x) = \int_x^y (qf - rg)$ with a local integrability clause. No smoothness of the coefficients and no $C^2$ solutions are assumed.
• Boundary Wronskians $W_a$, $W_b$ are Filter.limUnder along $x \to a$, $x \to b$ inside $I$. They are used only on $\mathfrak{D}(\tau)$, where milestone (9.7) states that the limits exist. In Lemma 9.7, where $u_a$ need not lie in $\mathfrak{D}(\tau)$, the boundary condition is stated as a convergence.
• Operators. Operators in $L^2(I, r\,dx)$ are LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph $\{(f, \tau f) \mid f \in \mathfrak{D}(A)\}$ exists (i.e. is well defined) and is self-adjoint. $\rho(A)$ and $(A - z)^{-1}$ follow Teschl (2.66): a bounded two-sided inverse of $A - z$. No projection-valued measure or functional calculus is used.
• Corrections to the printed text. Lemma 9.7 says "a solution $u_a$ of $(\tau - z)u = g$"; the proof and (9.28) need $(\tau - z)u = 0$, which is what is stated. The condition at an endpoint in (9.21) is imposed only where $\tau$ is l.c., as in (9.20). The second line of (9.10) is stated for quasi-derivatives. The boundary term of (9.7) is printed as $W_b(g^*, f) - W_a(g^*, f)$; integration by parts with (9.5) gives $W_a(g^*, f) - W_b(g^*, f)$ (check: $p = r = 1$, $q = 0$ on $(0,1)$, $f = x^2$, $g = 1$), and the corrected identity is stated.
• Ruling out trivialization. Limit circle is the Wronskian notion of p. 187, never "all solutions are square integrable", which would make the goal circular. The goal has no hypothesis beyond the standing assumptions on $p, q, r$.

A complete development needs a Carathéodory-type existence theorem for linear first-order systems with $L^1_{loc}$ coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the $L^2(I, r\,dx)$ operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Sections 9.1–9.2. https://doi.org/10.1090/gsm/099
• H. Weyl, "Über gewöhnliche Differentialgleichungen mit Singularitäten und die zugehörigen Entwicklungen willkürlicher Funktionen", Math. Ann. 68 (1910), 220–269. https://doi.org/10.1007/BF01474161
• J. Weidmann, Spectral Theory of Ordinary Differential Operators, Lecture Notes in Mathematics 1258, Springer, 1987. https://doi.org/10.1007/BFb0077960
• A. Zettl, Sturm–Liouville Theory, Mathematical Surveys and Monographs 121, AMS, 2005. https://doi.org/10.1090/surv/121

Motivation

In quantum mechanics an observable is a self-adjoint operator $A$ on a complex Hilbert space $\mathfrak H$, and the dynamics is the Schrödinger equation $i\,\tfrac{d}{dt}\psi(t) = H\psi(t)$. In finite dimensions the solution is the matrix exponential $e^{-itH}\psi(0)$, computed by diagonalizing $H$. The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to $f(A)$ for every Borel function $f$, in particular to $e^{-itA}$ and to the spectral projections $\chi_\Omega(A)$.

The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument, and let $\mathfrak L(\mathfrak H)$ be the bounded operators on it. An (unbounded) operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$; $A \subseteq B$ means $B$ extends $A$. $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A^* = A$, domains included.

The resolvent set of $A$ is the set of $z \in \mathbb{C}$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is its complement, $\sigma(A) = \mathbb{C} \setminus \rho(A)$.

A projection-valued measure assigns to every Borel set $\Omega \subseteq \mathbb{R}$ an orthogonal projection $P(\Omega) = P(\Omega)^* = P(\Omega)^2$ such that $P(\mathbb{R}) = \mathbb{I}$ and, for pairwise disjoint Borel sets $\Omega_n$, $\sum_n P(\Omega_n)\psi = P(\bigcup_n \Omega_n)\psi$ for every vector $\psi$ (strong, not norm, $\sigma$-additivity). Each $\psi$ gives the spectral measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$, a finite Borel measure of total mass $\|\psi\|^2$, and by polarization the complex measures $\mu_{\varphi,\psi}(\Omega) = \langle\varphi, P(\Omega)\psi\rangle$.

For a bounded Borel function $f$ the operator $P(f) = \int f(\lambda)\,dP(\lambda) \in \mathfrak L(\mathfrak H)$ is the bounded operator with $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for all $\psi$. For an arbitrary Borel function $f$ it is the operator with domain

$$\mathfrak D_f = \Big\{\psi \in \mathfrak H \;\Big|\; \int_{\mathbb{R}} |f(\lambda)|^2\, d\mu_\psi(\lambda) < \infty\Big\}$$

and $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for $\psi \in \mathfrak D_f$. An operator $T$ is normal if it is densely defined, $\mathfrak D(T) = \mathfrak D(T^*)$ and $\|T\psi\| = \|T^*\psi\|$ on $\mathfrak D(T)$.

Formalization targets

Goal: the spectral theorem (Theorem 3.7)

For every self-adjoint operator $A$ in $\mathfrak H$ there is a unique projection-valued measure $P_A$ with

$$A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda),$$

an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.

Milestones

• Theorem 3.1. For a projection-valued measure $P$, the map $f \mapsto P(f)$ from bounded Borel functions (sup norm) to $\mathfrak L(\mathfrak H)$ is a unital $C^*$-algebra homomorphism of norm one, $\langle P(g)\varphi, P(f)\psi\rangle = \int g^* f\, d\mu_{\varphi,\psi}$, and $P(f_n) \to P(f)$ strongly when $f_n \to f$ pointwise with $\sup_\lambda |f_n(\lambda)|$ bounded.
• Theorem 3.2. For every Borel $f$, the operator $P(f)$ with $\mathfrak D(P(f)) = \mathfrak D_f$ exists, is normal, and $P(f)^* = P(f^*)$.
• Lemma 3.5. $\alpha P(f) + \beta P(g) \subseteq P(\alpha f + \beta g)$ with domain $\mathfrak D_{|f|+|g|}$, and $P(f)P(g) \subseteq P(fg)$ with domain $\mathfrak D_g \cap \mathfrak D_{fg}$.
• Theorem 3.8. For self-adjoint $A$, $\sigma(A) = \{\lambda \in \mathbb{R} \mid P_A((\lambda-\varepsilon, \lambda+\varepsilon)) \ne 0 \text{ for all } \varepsilon > 0\}$.
• Corollary 3.9. $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R} \cap \rho(A)) = 0$.

A further supporting statement (not a milestone) records that $\mu_\psi$ is a finite measure with $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$.

Significance

The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution $e^{-itA}$, the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about $f(A)$ or $P_A(\Omega)$. Theorem 3.8 identifies the spectrum with the support of $P_A$, which is what makes spectral questions accessible to measure theory.

Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of $C^*$-algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object $f(A)$ that every later mission of this series currently has to take as data.

Difficulty

The obvious route through the bounded case fails. For bounded self-adjoint $A$ one can build $f(A)$ from polynomials by the sup norm on $\sigma(A)$ and extend by monotone limits; for unbounded $A$ there are no polynomials in $A$ defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform $(A-i)(A+i)^{-1}$, or the bounded resolvent $(A-z)^{-1}$) produce bounded normal operators whose spectral measures must then be transported back, and the domain $\mathfrak D(A)$ must be recovered exactly as $\mathfrak D_\lambda$; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections $P_A(\Omega)$ are not given by any formula in $A$ that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator $\int \lambda\, dP(\lambda)$ alone.

Formalization scope

$\mathfrak H$ is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from $\Omega \mapsto \|P(\Omega)\psi\|^2$. The spectral integral spectralIntegral P f is the operator with domain $\mathfrak D_f$ and quadratic form $\int f\,d\mu_\psi$ (the predicate IsSpectralIntegral), selected by choice; its existence for Borel $f$ is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in $\mathfrak L(\mathfrak H)$. The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, $P_A$ enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly $P_A$.

Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with $A = \int\lambda\,dP$" given as a hypothesis, and $P_A$ is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of $A$ as the only hypothesis.

Lemma 3.4 (spectral bases), Lemma 3.6 (the family $P_A(\Omega)$ built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and $L^2$ spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, $P(\Omega_1)P(\Omega_2) = P(\Omega_1 \cap \Omega_2)$, monotonicity), and of alternative proofs of the goal are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Chapter 3. https://doi.org/10.1090/gsm/099
• J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Mathematische Annalen 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
• M. H. Stone, Linear Transformations in Hilbert Space and Their Applications to Analysis, AMS Colloquium Publications 15, 1932. https://doi.org/10.1090/coll/015
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Chapters VII–VIII. https://doi.org/10.1016/B978-0-12-585050-6.X5001-4

Motivation

In one complex variable every open set is the natural domain of some holomorphic function. In several variables this fails: by the Hartogs phenomenon, every function holomorphic on some domains extends to a strictly larger one. The domains that are "natural", the domains of holomorphy, are characterised by a convexity condition on the domain. Since the work of Levi (1910), Hartogs, Oka and Cartan–Thullen (1932), the way to state that condition intrinsically has been pseudoconvexity. The tool that makes it work is the plurisubharmonic function, the complex analogue of a convex function.

This mission formalizes the part of that theory that needs no partial differential equations: harmonic, subharmonic and plurisubharmonic functions; smoothing of plurisubharmonic functions; the characterizations of Hartogs pseudoconvexity; and the Cartan–Thullen theorem. The source is §2.4–2.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), pp. 78–103.

Timeline, as the book presents it:

• Hartogs (1906) found the extension phenomenon.
• Levi (1910) found the boundary condition now called Levi pseudoconvexity.
• Cartan and Thullen (1932) proved that domains of holomorphy are exactly the holomorphically convex domains.
• Oka (1942–1953), Bremermann and Norguet (1954) solved the Levi problem: every pseudoconvex domain is a domain of holomorphy. The book states this result (its Theorem 2.6.2) but does not prove it.

Setting

Throughout, $\mathbb{C}^n$ carries the Euclidean norm $\|z\| = (|z_1|^2 + \dots + |z_n|^2)^{1/2}$. A domain is a nonempty connected open set. For $K, U \subset \mathbb{C}^n$, $K \subset\subset U$ means that $K$ is relatively compact in $U$: its closure is compact and contained in $U$.

Harmonic and subharmonic functions (one variable). A $C^2$ function $f$ on an open $U \subset \mathbb{C}$ is harmonic if $\nabla^2 f = 0$. A function $f : U \to \mathbb{R} \cup \{-\infty\}$ is subharmonic if it is upper-semicontinuous and, for every disc $B_r(a)$ with $\overline{B_r(a)} \subset U$ and every $g$ continuous on $\overline{B_r(a)}$ and harmonic inside it, $f \le g$ on $\partial B_r(a)$ implies $f \le g$ on $B_r(a)$.

Plurisubharmonic functions. For $U \subset \mathbb{C}^n$ open, $f : U \to \mathbb{R} \cup \{-\infty\}$ is plurisubharmonic if it is upper-semicontinuous and $\xi \mapsto f(a + b\xi)$ is subharmonic on $\{\xi : a + b\xi \in U\}$ for all $a, b \in \mathbb{C}^n$.

Hulls and convexity. For a class $\mathcal{F}$ of extended-real functions on $U$ and $K \subset U$, the hull is

$$\widehat{K} = \{x \in U : f(x) \le \sup_{y \in K} f(y) \text{ for all } f \in \mathcal{F}\}.$$

$U$ is convex with respect to $\mathcal{F}$ if $K \subset\subset U$ implies $\widehat{K} \subset\subset U$. For $\mathcal{F} = \{|f| : f \in \mathcal{O}(U)\}$ this is holomorphic convexity, with hull $\widehat{K}_U$.

Hartogs pseudoconvexity. $f : U \to \mathbb{R}$ is an exhaustion function if $\{z \in U : f(z) < r\} \subset\subset U$ for every $r$. A domain is Hartogs pseudoconvex if it admits a continuous plurisubharmonic exhaustion function.

Analytic discs. A closed analytic disc is a nonconstant holomorphic $\varphi : \mathbb{D} \to \mathbb{C}^n$ that extends continuously to $\overline{\mathbb{D}}$. Its image is $\Delta = \varphi(\mathbb{D})$ and its boundary is $\partial\Delta = \varphi(\partial\mathbb{D})$.

Formalization targets

Goal: Theorem 2.5.6

For a domain $U \subsetneq \mathbb{C}^n$ with $\rho(z) = \operatorname{dist}(z, \partial U)$, the following are equivalent:

$$\text{(i) } -\log\rho \text{ is plurisubharmonic};\quad \text{(ii) } U \text{ is Hartogs pseudoconvex};$$ $$\text{(iii) } U \text{ is convex w.r.t. plurisubharmonic functions on } U;\quad \text{(iv) } \textstyle\bigcup_\alpha \partial\Delta_\alpha \subset\subset U \Rightarrow \bigcup_\alpha \Delta_\alpha \subset\subset U$$

for every collection of closed analytic discs $\Delta_\alpha \subset U$.

Milestones

• Proposition 2.4.3. A continuous $f$ is harmonic iff it has the mean-value property. An upper-semicontinuous $f$ is subharmonic iff $f(a) \le \frac{1}{2\pi}\int_0^{2\pi} f(a + re^{i\theta})\,d\theta$ whenever $\overline{\Delta_r(a)} \subset U$.
• Proposition 2.4.7. Finite suprema of subharmonic functions are subharmonic, and so are arbitrary suprema that are finite and upper-semicontinuous.
• Proposition 2.4.9. A $C^2$ function is plurisubharmonic iff its complex Hessian $[\partial^2 f/\partial\bar z_k \partial z_\ell]$ is positive semidefinite.
• Theorem 2.4.10. Every plurisubharmonic $f$ is the pointwise limit of smooth plurisubharmonic $f_\epsilon \ge f$ on $U_\epsilon = \{z \in U : \operatorname{dist}(z, \partial U) > \epsilon\}$.
• Theorem 2.5.2 (Kontinuitätssatz, second version): (iii) implies (iv).
• Lemma 2.5.7. Hartogs pseudoconvexity is a local property of the boundary.
• Theorem 2.4.12 (Radó): a continuous function holomorphic off its zero set is holomorphic.
• Theorem 2.6.3 (Cartan–Thullen): for a domain $U \subsetneq \mathbb{C}^n$, being a domain of holomorphy, $\operatorname{dist}(K, \partial U) = \operatorname{dist}(\widehat{K}_U, \partial U)$ for all $K \subset\subset U$, and holomorphic convexity are equivalent.

Significance

The result. Theorem 2.5.6 makes pseudoconvexity checkable. Condition (i) involves one explicitly given function of the domain's geometry. Condition (iv) involves only families of discs. Condition (ii) is the form the Levi problem and Hörmander's $L^2$ theory need. From these equivalences one gets, for example, that intersections and increasing unions of pseudoconvex domains are pseudoconvex, that pseudoconvexity is a biholomorphic invariant, and, with Lemma 2.5.7, that it is a local boundary property. In the smooth case that local property is Levi pseudoconvexity (Theorem 2.5.8, chapter III of this series). Cartan–Thullen supplies the other half of the picture for domains of holomorphy.

Formalizing it. All of these results are classical and proved in the book, apart from routine steps left as exercises. As far as is known, none of them is formalized in any proof assistant. Mathlib has harmonic functions (InnerProductSpace.HarmonicOnNhd) and the circle average, but no subharmonic or plurisubharmonic functions, no hulls and no pseudoconvexity. The Prove2Me corpus holds a one-variable subharmonic definition based on the sub-mean-value property and the one-directional mean-value property of harmonic functions; neither is the book's definition or statement. The mission would give Lean a first library of plurisubharmonic functions in $\mathbb{C}^n$, with the definition matching the textbook.

Difficulty

The obvious route to (iv) ⇒ (i) of the goal would show $-\log\rho$ is plurisubharmonic by computing a complex Hessian (Proposition 2.4.9). That fails: $\rho$ is in general not even differentiable, so no Hessian is available. Several other steps also need measure theory with extended-real values. The sub-mean-value property requires Lebesgue integrals of upper-semicontinuous functions that may equal $-\infty$ on large sets. Smoothing requires convolution of such functions with a mollifier, and pointwise convergence in $[-\infty, \infty)$. Suprema of families lose upper semicontinuity in general, which is why Proposition 2.4.7 carries that hypothesis. In Cartan–Thullen, holomorphic convexity alone must produce a holomorphic function on $U$ that extends across no boundary point. Nothing in the hypothesis supplies such a function directly.

Formalization scope

• $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n), so balls, $\rho(z)$ = Metric.infDist z (frontier U), $U_\epsilon$ and $\operatorname{dist}(K, \partial U)$ are all Euclidean, as in the book. They are not sup-norm polydisc quantities.
• Functions with values in $\mathbb{R} \cup \{-\infty\}$ are EReal-valued with $+\infty$ excluded on $U$. Upper semicontinuity is UpperSemicontinuousOn for the order of EReal.
• Hulls take suprema in EReal, and holomorphic hulls in $[0, \infty]$, so no supremum takes a junk value. Set distances are infima in $[0, \infty]$ (Metric.infEDist).
• The circle mean in Proposition 2.4.3 (ii) is the Lebesgue integral of the positive part minus that of the negative part.
• Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there.
• A domain is IsOpen U ∧ IsConnected U. Relative compactness is compact closure contained in $U$.
• Harmonic and subharmonic functions are defined only on open subsets of $\mathbb{C} = \mathbb{R}^2$. The book defines them on $\mathbb{R}^n$, but only uses $n = 2$. This is the one restriction of scope.
• A collection of analytic discs is a set of parametrizing maps, and $\Delta_\alpha = \varphi_\alpha(\mathbb{D})$ as in Definition 1.4.5.
• Definitions 1.4.5 and 2.1.1 are restated locally in the namespace LeblSCV.Pseudoconvex.

Several trivializing formalizations are ruled out. Plurisubharmonicity is not defined through the Hessian condition, so the mission does not reduce to $C^2$ functions. Nor is it defined by the sub-mean-value property, which would make Proposition 2.4.3 (ii) a tautology. $\rho$ is not the sup-norm distance. Suprema, infima and integrals are nowhere allowed to default to $0$ on empty, unbounded or non-integrable input.

A complete development needs:

• mean values of upper-semicontinuous functions and the Poisson integral on discs (Theorem 2.4.2, not a milestone);
• convolution with a radial mollifier on $\mathbb{C}^n$;
• Cauchy estimates on polydiscs.

The subharmonic and plurisubharmonic layer is reusable beyond this mission. Chapters on the Levi problem, the $\bar\partial$-problem and Bergman kernels would all build on it. Proofs of the smaller milestones, and alternative arguments for the goal, are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026. https://www.jirka.org/scv/scv.pdf
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland Mathematical Library 7, 1990 (the book's reference [H] for the Levi problem).
• H. Cartan and P. Thullen, "Zur Theorie der Singularitäten der Funktionen mehrerer komplexen Veränderlichen: Regularitäts- und Konvergenzbereiche", Mathematische Annalen 106 (1932), 617–647.