All missions

Motivation

In a scattering experiment a particle arrives from far away, interacts with a target, and leaves again. Far from the target the forces are negligible, so long before and long after the collision the particle should move like a free particle. Scattering theory makes this precise by comparing two quantum dynamics: the free evolution $\mathrm e^{-\mathrm itH_0}$ generated by the kinetic energy $H_0 = -\Delta$, and the full evolution $\mathrm e^{-\mathrm itH}$ generated by $H = H_0 + V$. The objects that compare them are the wave operators (Møller operators) $\Omega_\pm$, introduced by Møller (1945) and put on a rigorous footing by Jauch (1958) and Kato. Cook (1957) gave the first practical criterion for their existence. Kuroda, Birman, Agmon, Enß and others later developed the theory up to asymptotic completeness for short-range potentials.

This mission formalizes the abstract part of Chapter 12 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the definition and basic structure of the wave operators, Cook's criterion, and the existence of the wave operators for a square-integrable potential in three dimensions.

Setting

Let $\mathfrak H$ be a complex Hilbert space. An operator $A$ is a linear map on a subspace $\mathfrak D(A)$, its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A = A^*$. A projection-valued measure $P$ assigns to each Borel set $\Omega \subseteq \mathbb R$ an orthogonal projection $P(\Omega)$, with $P(\mathbb R) = \mathbb I$ and $P(\bigcup_n\Omega_n)\psi = \sum_n P(\Omega_n)\psi$ for disjoint $\Omega_n$. The spectral measure of $\psi$ is $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle$. By the spectral theorem every self-adjoint $A$ equals $\int\lambda\,dP(\lambda)$ for a unique $P$: $\mathfrak D(A) = \{\psi \mid \int\lambda^2\,d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\,d\mu_\psi$. The time evolution $\mathrm e^{-\mathrm itA}$ is the bounded operator with $\langle\psi, \mathrm e^{-\mathrm itA}\psi\rangle = \int\mathrm e^{-\mathrm it\lambda}\,d\mu_\psi(\lambda)$.

For two self-adjoint operators $H_0$, $H$ the wave operators are

$$\mathfrak D(\Omega_\pm) = \{\psi \in \mathfrak H \mid \exists\lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi\}, \qquad \Omega_\pm\psi = \lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi .$$

$\mathfrak D(\Omega_\pm)$ is the set of asymptotic states and $\operatorname{Ran}(\Omega_\pm) = \Omega_\pm\mathfrak D(\Omega_\pm)$ the set of states that have one. A closed subspace $\mathfrak H_1$ with projection $P_1$ reduces $A$ if $P_1\mathfrak D(A) \subseteq \mathfrak D(A)$ and $P_1A\psi = AP_1\psi$ for $\psi \in \mathfrak D(A)$.

On $L^2(\mathbb R^n)$ the free Schrödinger operator is $H_0 = -\Delta$ with domain the Sobolev space $H^2(\mathbb R^n)$: under the Fourier transform it is multiplication by $p^2$ on $\{\varphi \mid p^2\varphi \in L^2\}$. For a real potential $V$, $H = H_0 + V$ has $\mathfrak D(H) = H^2(\mathbb R^n)$ and $(H\psi)(x) = (H_0\psi)(x) + V(x)\psi(x)$.

Formalization targets

Goal: existence of the wave operators for $V \in L^2(\mathbb R^3)$ (Theorem 12.4)

Let $H_0$ be the free Schrödinger operator on $L^2(\mathbb R^3)$ and $H = H_0 + V$ with a real $V \in L^2(\mathbb R^3)$. Then

$$\mathfrak D(\Omega_+) = \mathfrak D(\Omega_-) = L^2(\mathbb R^3),$$

that is, $\lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi$ exists for every $\psi$ and both signs. Since the spectrum of $H_0$ is purely absolutely continuous, this is exactly what Teschl calls "the wave operators exist" (12.14).

Milestones

• Lemma 12.1. $\mathfrak D(\Omega_\pm)$ and $\operatorname{Ran}(\Omega_\pm)$ are closed and $\Omega_\pm : \mathfrak D(\Omega_\pm) \to \operatorname{Ran}(\Omega_\pm)$ is unitary.
• Theorem 12.2. $\mathfrak D(\Omega_\pm)$ reduces $H_0$, $\operatorname{Ran}(\Omega_\pm)$ reduces $H$, and the restricted operators are unitarily equivalent: $\Omega_\pm H_0\psi = H\Omega_\pm\psi$ for $\psi \in \mathfrak D(\Omega_\pm) \cap \mathfrak D(H_0)$.
• Lemma 12.3 (Cook). If $\mathfrak D(H) \subseteq \mathfrak D(H_0)$, $\psi \in \mathfrak D(H_0)$ and $\int_0^\infty\|(H - H_0)\exp(\mp\mathrm itH_0)\psi\|\,dt < \infty$, then $\psi \in \mathfrak D(\Omega_\pm)$ and $\|(\Omega_\pm - \mathbb I)\psi\| \le \int_0^\infty\|(H - H_0)\exp(\mp\mathrm itH_0)\psi\|\,dt$.

Significance

Existence of the wave operators is the first step of every scattering theory for Schrödinger operators: without it the scattering operator $S = \Omega_+^{-1}\Omega_-$ is not defined on a useful set of states, and the questions of completeness and asymptotic completeness (Enß's theorem, Theorem 12.12 of the same chapter) cannot be posed. Lemma 12.1 and Theorem 12.2 are the structural facts that make $\Omega_\pm$ partial isometries intertwining the two Hamiltonians; they imply that $H$ restricted to $\operatorname{Ran}(\Omega_\pm)$ has absolutely continuous spectrum whenever $H_0$ does, and that kinetic energy is conserved in scattering. Cook's criterion is the tool used in practice to prove existence for concrete potentials, including Coulomb-type and time-dependent problems.

The results are classical and proved in the literature. They are not formalized. Mathlib has neither the spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no scattering theory. The platform has no statement about wave operators; its BookProof development contains Stone's theorem for its own structure of unbounded operators, which this mission does not use.

Difficulty

The limit defining $\Omega_\pm$ involves two unitary groups whose generators do not commute, and neither group is explicit for the perturbed operator $H$. For Cook's criterion the product $\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi$ has to be differentiated in $t$, which needs control of domains: $\mathrm e^{-\mathrm itH_0}\psi$ must stay in the domain of $H - H_0$, and the derivative of a strongly continuous unitary group exists only on the domain of its generator. For the goal, the time evolution of a general $\psi \in L^2(\mathbb R^3)$ has no decay rate at all, and the potential $V \in L^2$ is unbounded and has no decay assumption beyond square integrability, so the integrability condition of Cook's criterion cannot be checked for every $\psi$ directly. The intertwining relation (12.8) concerns unbounded operators and needs the reduction of the domains, not only an identity between bounded operators.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint. Separability is not assumed.

The spectral theorem is not part of this mission. Every statement takes projection-valued measures $P_0$ and $P$ as data, with the hypotheses $H_0 = \int\lambda\,dP_0(\lambda)$ and $H = \int\lambda\,dP(\lambda)$ (domain and quadratic form as above), which is the form the spectral theorem guarantees and which determines $P_0$ and $P$. The time evolutions are $\mathrm e^{-\mathrm itH_0} = \int\mathrm e^{-\mathrm it\lambda}\,dP_0$ and $\mathrm e^{-\mathrm itH} = \int\mathrm e^{-\mathrm it\lambda}\,dP$. In the goal, the self-adjointness of $H = H_0 + V$ (Theorem 10.2 of the book) enters only through the existence of $P$. Nothing is assumed about $\Omega_\pm$.

The sign of $\Omega_\pm$ is a unit s : ℤˣ, and $t \to \pm\infty$ is written as $t \to +\infty$ in the variable $st$. $\Omega_\pm$ is Mathlib's limUnder and is used only on $\mathfrak D(\Omega_\pm)$. A formalization that set $\Omega_\pm\psi = 0$ where the limit fails and then proved only that $\Omega_\pm$ is isometric would lose the content of the goal; here the goal asserts that the limit exists for every $\psi \in L^2(\mathbb R^3)$. In Cook's lemma the finiteness of the integral is integrability on $(0,\infty)$, the bound uses the Bochner integral, and the hypothesis that $\exp(\mp\mathrm itH_0)\psi$ lies in $\mathfrak D(H)$ for $t \ge 0$, which the integrand presupposes, is explicit.

$L^2(\mathbb R^3)$ is Mathlib's Lp ℂ 2 on EuclideanSpace ℝ (Fin 3). The free Schrödinger operator is characterized through Mathlib's unitary $L^2$ Fourier transform $\mathcal F_M f(\xi) = \int\mathrm e^{-2\pi\mathrm i\langle x,\xi\rangle}f(x)\,dx$, not the book's $(2\pi)^{-n/2}\int\mathrm e^{-\mathrm ipx}f(x)\,dx$. The constants are translated: $\mathfrak D(H_0) = \{\psi \mid |\xi|^2\mathcal F_M\psi \in L^2\}$ and $\mathcal F_M(H_0\psi) = 4\pi^2|\xi|^2\mathcal F_M\psi$. $H = H_0 + V$ has $\mathfrak D(H) = \mathfrak D(H_0)$ and $H\psi = H_0\psi + V\psi$ almost everywhere.

A complete development needs a functional calculus for projection-valued measures (strong continuity and differentiability of $\mathrm e^{-\mathrm itA}$ on $\mathfrak D(A)$, Theorem 5.1), the explicit $L^1 \to L^\infty$ decay of the free Schrödinger group in $\mathbb R^3$ ((7.31) of the book), and density of $L^1 \cap H^2$ in $L^2$. These pieces are reusable for the rest of Chapter 12 (incoming and outgoing states, short-range potentials, asymptotic completeness). Proofs of any milestone and of such supporting lemmas 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. Chapter 12, pp. 247–257.
• J. M. Cook, Convergence to the Møller wave-matrix, J. Math. and Phys. 36 (1957), 82–87. doi:10.1002/sapm195736182.
• J. M. Jauch, Theory of the scattering operator, Helv. Phys. Acta 31 (1958), 127–158.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics III: Scattering Theory, Academic Press, 1979.
• V. Enß, Asymptotic completeness for quantum mechanical potential scattering. I. Short range potentials, Comm. Math. Phys. 61 (1978), 285–291. doi:10.1007/BF01940771.

Motivation

Quantum mechanics describes mixed states by density operators: positive operators $\rho$ on a Hilbert space with $\operatorname{tr}(\rho) = 1$. Expectation values are traces $\operatorname{tr}(\rho A)$, perturbation determinants and spectral shift functions are built from traces of resolvent differences, and scattering theory (the Kato–Rosenblum and Birman–Krein theorems) is phrased in terms of trace class perturbations. All of this needs a trace in infinite dimensions, and the trace $\sum_n \langle \varphi_n, K\varphi_n\rangle$ only makes sense on a restricted class of operators.

This mission formalizes Sections 6.2–6.3 of G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators (AMS Graduate Studies in Mathematics 99, 2009), the standard route from compact operators through Hilbert–Schmidt operators to the trace class. The theory goes back to von Neumann and Schatten in the 1940s (R. Schatten, Norm Ideals of Completely Continuous Operators, Springer 1960). A modern account is B. Simon, Trace Ideals and Their Applications (AMS 2005).

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 linear operators on $\mathfrak{H}$ with the operator norm $\|A\|$. An operator is of finite rank if its range is finite dimensional, and the compact operators $\mathfrak{C}(\mathfrak{H})$ are the norm closure of the finite rank operators.

For $K \in \mathfrak{L}(\mathfrak{H})$ with adjoint $K^*$, the operator $K^*K$ is positive. The singular values $s_j(K) > 0$ of a compact $K$ are the square roots of the nonzero eigenvalues of $K^*K$, each repeated according to its multiplicity $\dim\operatorname{Ker}(K^*K - \mu)$. For $p \ge 1$ the Schatten $p$-norm and Schatten $p$-class are

$$\|K\|_p = \Big(\sum_j s_j(K)^p\Big)^{1/p} \in [0,\infty], \qquad \mathcal{J}_p(\mathfrak{H}) = \{K \in \mathfrak{C}(\mathfrak{H}) \mid \|K\|_p < \infty\}.$$

A compact $K$ is Hilbert–Schmidt if $K \in \mathcal{J}_2(\mathfrak{H})$ and trace class if $K \in \mathcal{J}_1(\mathfrak{H})$. For an orthonormal basis $\{\varphi_n\}$ of $\mathfrak{H}$ the trace is

$$\operatorname{tr}(K) = \sum_n \langle \varphi_n, K\varphi_n\rangle .$$

In Lean these are compactOperators H, schattenNorm p K, schattenClass H p, IsHilbertSchmidt K, IsTraceClass K and trace K, in the namespace TeschlQM.TraceClass.

Formalization targets

Goal: the trace is well defined (Lemma 6.15)

For every trace class $K$ and every orthonormal basis $\{\varphi_n\}$ the series (6.26) converges, and for any two orthonormal bases $\{\varphi_n\}$, $\{\psi_m\}$

$$\sum_n \langle \varphi_n, K\varphi_n\rangle = \sum_m \langle \psi_m, K\psi_m\rangle = \operatorname{tr}(K).$$

Milestones

1. Theorem 6.7 (canonical form): a compact $K$ has the form $K = \sum_j s_j\langle\phi_j, \cdot\rangle\hat\phi_j$ with orthonormal $\{\phi_j\}$, $\{\hat\phi_j\}$, and the $s_j^2$ are the nonzero eigenvalues of $K^*K$ and of $KK^*$, counted with multiplicity.
2. Lemma 6.10: a compact $K$ is Hilbert–Schmidt iff $\sum_n\|K\psi_n\|^2 < \infty$ for some orthonormal basis, and then $\sum_n\|K\psi_n\|^2 = \|K\|_2^2$ for every orthonormal basis.
3. Corollary 6.11: the Hilbert–Schmidt operators form a $*$-ideal, with $\|KA\|_2, \|AK\|_2 \le \|A\|\|K\|_2$.
4. Lemma 6.12: $(\mathcal{J}_p(\mathfrak{H}), \|\cdot\|_p)$ is a Banach space, and

$$\|K\|_p = \sup\Big\{\Big(\sum_j|\langle\psi_j, K\varphi_j\rangle|^p\Big)^{1/p} \;\Big|\; \{\psi_j\}, \{\varphi_j\} \text{ orthonormal}\Big\}.$$

5. Lemma 6.13: $K$ is trace class iff $K = K_1K_2$ with $K_1, K_2$ Hilbert–Schmidt, and then $\|K\|_1 \le \|K_1\|_2\|K_2\|_2$.
6. Corollary 6.14: the trace class is a $*$-ideal, with $\|KA\|_1, \|AK\|_1 \le \|A\|\|K\|_1$.
7. Lemma 6.16 (after the goal): the trace is linear, $\operatorname{tr}(K^*) = \overline{\operatorname{tr}(K)}$, it is monotone for the operator order, and $\operatorname{tr}(AK) = \operatorname{tr}(KA)$ for bounded $A$.

Significance

The result itself. Lemma 6.15 is what turns the trace into a linear functional on $\mathcal{J}_1(\mathfrak{H})$ at all. Every later use of the trace rests on it: the normalization of density matrices, the duality $\mathcal{J}_1(\mathfrak{H})^* \cong \mathfrak{L}(\mathfrak{H})$, trace formulas and spectral shift functions, and Lidskii's theorem (the trace is the sum of the eigenvalues), which Teschl mentions right after the lemma. The ideal properties (Corollaries 6.11 and 6.14) and the factorization (Lemma 6.13) are the everyday tools for proving that a concrete operator, such as $f(x)g(-i\nabla)$ in Chapter 7, is trace class.

Formalizing it. Mathlib has compact operators (IsCompactOperator), Hilbert bases, singular values and the trace of linear maps on finite-dimensional spaces (LinearMap.singularValues, LinearMap.trace), but no infinite-dimensional singular values, Schatten classes, Hilbert–Schmidt or trace class operators, and no basis-independent trace. The Prove2Me corpus has finite-dimensional trace norms (matrices) and $L^2$ kernel operators, but no statement of this section. The results are classical and fully proved in the literature; the work is to formalize them.

Difficulty

The obvious argument for basis independence is to expand $K$ in both bases and interchange the two sums. In infinite dimensions that interchange is not justified for an arbitrary bounded $K$: for the identity on an infinite-dimensional space, or for a non-trace-class compact operator, the diagonal series diverges. The trace class hypothesis must therefore enter through a factorization, and the factorization rests on the canonical form of Theorem 6.7, which in turn needs the spectral theorem for the compact self-adjoint operator $K^*K$, including finite multiplicity of its nonzero eigenvalues. A second difficulty is bookkeeping: the singular values are a family with multiplicities that may be finite or countably infinite, and the Schatten norm, the Hilbert–Schmidt sums over a basis and the supremum formula (6.23) all have to be matched as sums in $[0,\infty]$.

Formalization scope

• Hilbert space. {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]. Separability is not assumed. Orthonormal bases are Mathlib HilbertBasis ι ℂ H with arbitrary index types, so every statement covers the book's separable case.
• Operators. Bounded operators are H →L[ℂ] H, products are compositions, adjoints are ContinuousLinearMap.adjoint, and the operator order in Lemma 6.16 is Mathlib's Loewner order ($K_1 \le K_2$ iff $K_2 - K_1$ is positive). Traces are compared with the partial order of $\mathbb{C}$.
• Compactness is the book's definition, membership in the norm closure of the finite rank operators, not Mathlib's IsCompactOperator.
• Singular values are not enumerated. $\sum_j s_j(K)^p$ is written as $\sum_{\mu > 0} \dim\operatorname{Ker}(K^*K - \mu)\,\mu^{p/2}$, with the dimension in $\{0,1,\dots\}\cup\{\infty\}$. Norms and sums live in $[0,\infty]$, so a divergent series is $\infty$, never a junk $0$. Hilbert–Schmidt and trace class are defined by $\|K\|_2 < \infty$ and $\|K\|_1 < \infty$ on compact $K$. The basis characterizations (Lemma 6.10) and the factorization (Lemma 6.13) are theorems, not definitions.
• Trace. trace K is $\sum_n\langle\varphi_n, K\varphi_n\rangle$ in one fixed, chosen Hilbert basis. The goal states summability in every Hilbert basis, not merely equality of tsum values. Since the tsum of a non-summable family is $0$ in Mathlib, a statement asserting only that all tsums agree would be trivially satisfiable by divergent series. That trivializing reading is ruled out.
• Lemma 6.12 assumes $1 \le p$ (the book's proof uses the conjugate exponent). "Banach space" is spelled out as closure under the linear operations, the norm axioms, and completeness of $\|\cdot\|_p$-Cauchy sequences.
• No projection-valued measure, no functional calculus and no Fourier transform is used, and nothing is taken as data.

Reusable infrastructure a complete development will produce includes the spectral theorem for compact self-adjoint operators with multiplicities, the singular value decomposition in infinite dimensions, and the Hilbert–Schmidt and trace class ideals. All of these are welcome as independent contributions, and any of them would fill gaps in Mathlib.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Sections 6.2–6.3. https://doi.org/10.1090/gsm/099
• R. Schatten, Norm Ideals of Completely Continuous Operators, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer, 1960 (no stable link verified).
• B. Simon, Trace Ideals and Their Applications, 2nd ed., Mathematical Surveys and Monographs 120, AMS, 2005. https://doi.org/10.1090/surv/120
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Section VI.6 (no stable link verified).

Motivation

An atom with $N$ electrons is described, with the nucleus fixed at the origin, by a Schrödinger operator on $L^2(\mathbb R^{3N})$ whose potential does not decay in all directions: moving one electron to infinity while the others stay near the nucleus leaves the remaining Coulomb attraction untouched. For this reason the standard route to the essential spectrum of a one-particle operator, showing that the potential is a relatively compact perturbation of $-\Delta$, fails for $N \ge 2$. The HVZ theorem, due to Zhislin (1960), van Winter (1964) and Hunziker (1966), gives the answer anyway: the essential spectrum of the $N$-electron atom begins exactly at the ground state energy of the ion with one electron removed. It is the basic structural result of $N$-body quantum mechanics, and the starting point for every discussion of bound states, ionization energies and the stability of atoms and molecules.

This mission follows Chapter 11 of Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which proves self-adjointness by Kato's theorem and the HVZ theorem by the localization method of Ismagilov, Morgan, Simon and Sigal.

Setting

Write $\mathbb R^n$ for Euclidean space with Lebesgue measure. The Sobolev space $H^2(\mathbb R^n)$ is the set of $\psi \in L^2(\mathbb R^n)$ with $|p|^2 \hat\psi(p) \in L^2(\mathbb R^n)$, and the free Schrödinger operator is $H_0\psi = -\Delta\psi = (|p|^2\hat\psi)^\vee$ with domain $H^2(\mathbb R^n)$ (units $\hbar = 1$, mass $1/2$). A measurable function $V$ acts as the multiplication operator $(V\psi)(x) = V(x)\psi(x)$ on its maximal domain $\{\psi \in L^2 \mid V\psi \in L^2\}$.

For an operator $A$ with domain $\mathfrak D(A)$ in a Hilbert space, the resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z$ maps $\mathfrak D(A)$ bijectively onto the space with bounded inverse $R_A(z)$, and $\sigma(A) = \mathbb C \setminus \rho(A)$ is the spectrum. The discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated points of $\sigma(A)$ and have finite-dimensional eigenspaces; the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$. $A$ is bounded from below if $\langle\psi, A\psi\rangle \ge \gamma\|\psi\|^2$ on $\mathfrak D(A)$ for some $\gamma \in \mathbb R$. $B$ is $A$ bounded if $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\|B\psi\| \le a\|A\psi\| + b\|\psi\|$; the infimum of admissible $a$ is the $A$-bound. $K$ is relatively compact with respect to $A$ if $K R_A(z)$ is compact for one $z \in \rho(A)$.

For an atom with $N$ electrons at $x = (x_1, \dots, x_N) \in \mathbb R^{3N}$, $x_j \in \mathbb R^3$, and constants $\gamma_{ne}, \gamma_{ee} > 0$, the atomic Hamiltonian is

$$H^{(N)} = -\sum_{j=1}^N \Delta_j - \sum_{j=1}^N \frac{\gamma_{ne}}{|x_j|} + \sum_{1 \le j < k \le N} \frac{\gamma_{ee}}{|x_j - x_k|}, \qquad \mathfrak D(H^{(N)}) = H^2(\mathbb R^{3N}).$$

$H^{(N-1)}$ denotes the same operator for $N - 1$ electrons with the same constants.

Formalization targets

Goal: the HVZ theorem (Theorem 11.2)

For $N \ge 1$, $H^{(N)}$ is bounded from below, and

$$\sigma_{ess}(H^{(N)}) = [\lambda^{N-1}, \infty), \qquad \lambda^{N-1} = \min \sigma(H^{(N-1)}),$$

with $\lambda^{N-1} < 0$ for $N \ge 2$. The minimum is attained and, for $N \ge 2$, negative; both are part of the claim.

Milestones

• Kato's theorem (Theorem 11.1). For real-valued $V_k \in L^\infty_\infty(\mathbb R^d) + L^2(\mathbb R^d)$, $d \le 3$, composed with the first $d$ coordinates of orthogonal transformations of $\mathbb R^{Nd}$, each $V_k(y^{(k)})$ has $H_0$-bound $0$, and $H = H_0 + \sum_k V_k(y^{(k)})$ with $\mathfrak D(H) = H^2(\mathbb R^{Nd})$ is self-adjoint with core $C_0^\infty(\mathbb R^{Nd})$.
• IMS localization formula (Lemma 11.3). If $\varphi_j \in C^\infty(\mathbb R^n)$ satisfy $\sum_j \varphi_j^2 = 1$, then for $\psi \in H^2(\mathbb R^n)$

$$\Delta\psi = \sum_{j} \big(\varphi_j\Delta(\varphi_j\psi) + |\partial\varphi_j|^2\psi\big).$$

• Localizing partition (Lemma 11.4). For $C \in (0, 1/\sqrt N)$ there are smooth $\varphi_j : \mathbb R^{3N} \to [0,1]$ with $\sum_j \varphi_j^2 = 1$, $\operatorname{supp}\varphi_j \cap \{|x| \ge 1\} \subseteq \{|x_j| \ge C|x|\}$ and $|\partial\varphi_j(x)| \to 0$ as $|x| \to \infty$.
• A compactness criterion (Lemma 11.5). A multiplication operator $V$ with $H_0$-bound $0$ and $\|\chi_{\{|x| \ge R\}} V R_{H_0}(z)\| \to 0$ as $R \to \infty$ is relatively compact with respect to $H_0$.

Significance

The result. The HVZ theorem separates the spectrum of an atom into a continuum $[\lambda^{N-1}, \infty)$, fixed by the $(N-1)$-electron ion, and a discrete part below it consisting of bound states. The ionization energy of the atom is $\lambda^N - \lambda^{N-1}$. Questions such as whether a given atom or negative ion has a bound state at all, whether it has infinitely many (Zhislin's theorem for neutral atoms and positive ions), and how many electrons a nucleus can bind are all formulated relative to the threshold the HVZ theorem identifies. The same argument, with additional notation, covers molecules with fixed nuclei and general $N$-body systems.

Formalizing it. The results are classical and proved in the standard texts (Reed–Simon IV, Cycon–Froese–Kirsch–Simon, Teschl). None is formalized. Mathlib now has the unitary Fourier transform on $L^2$, tempered distributions and Sobolev spaces defined through the Fourier transform, but no self-adjoint Schrödinger operators, no essential spectrum and no many-body Hamiltonians. This mission asks for formal proofs of Teschl's four supporting results and of the HVZ theorem, and in doing so fixes a concrete representation of $H_0$, of Coulomb-type multiplication operators and of the $N$-electron atom on which later work (bound states of atoms, scattering) can build.

Difficulty

The obvious argument for the essential spectrum of $-\Delta + V$, relative compactness of $V$ followed by Weyl's theorem, is not available: $\gamma_{ne}/|x_j|$ does not vanish as $|x| \to \infty$ in directions where $x_j$ stays bounded, and it is not relatively compact with respect to $H_0$ on $L^2(\mathbb R^{3N})$. The inclusion $\sigma_{ess}(H^{(N)}) \subseteq [\lambda^{N-1}, \infty)$ therefore requires decomposing configuration space into regions in which one specific electron is far from the nucleus, controlling the error terms of that decomposition, and comparing the localized pieces with decoupled operators whose spectrum is known; this uses self-adjointness and relative bounds for operators built from the same potentials with one electron removed. The reverse inclusion requires approximate eigenfunctions built from those of $H^{(N-1)}$ and of the free one-electron operator, and a statement that $\lambda^{N-1}$ is attained. Negativity of $\lambda^{N-1}$ needs the hydrogen-like ground state and a comparison argument across $N$.

Behind all of this sits the analytic layer: Kato's theorem requires that $1/|x|$ in three dimensions is infinitesimally bounded with respect to $-\Delta$ and that this survives the passage to $\mathbb R^{3N}$ through an orthogonal change of variables; the IMS formula requires relating the Fourier definition of $H_0$ to derivatives of products.

Formalization scope

The Hilbert space is Lp ℂ 2 volume over EuclideanSpace ℝ ι; for the atom, $\iota = \texttt{Fin N × Fin 3}$, so $|x|$ is the Euclidean norm on $\mathbb R^{3N}$ and $x_j$ is electron x j. Operators are Mathlib LinearPMaps, self-adjointness is Mathlib's IsSelfAdjoint, and sums of unbounded operators are LinearPMap sums with the intersection of the domains. $H_0$ (freeHamiltonian) is defined as $\mathcal F^{-1}\,(4\pi^2\|\xi\|^2)\,\mathcal F$ with Mathlib's unitary $L^2$ Fourier transform (kernel $e^{-2\pi i\langle x,\xi\rangle}$, no prefactor); this is the same operator $-\Delta$ on the same domain $H^2$ as Teschl's $F^{-1}|p|^2F$. Multiplication operators (mulOp) have their maximal domains. $H^{(N)}$ (atomicHamiltonian) is freeHamiltonian + mulOp V^{(N)}; the equality of its domain with $H^2(\mathbb R^{3N})$ is a claim of Theorem 11.1, not an assumption. Resolvent set, spectrum, discrete and essential spectrum are defined from the bounded two-sided inverse of $A - z$, not from Mathlib's Banach-algebra spectrum. The $A$-bound takes values in $[0, \infty]$. The IMS formula is stated in the sense of distributions, tested against $C_0^\infty$ functions, since for merely smooth $\varphi_j$ its right-hand side need not lie in $L^2$. No projection-valued measure or functional calculus is taken as data.

A trivializing formalization is ruled out: $\lambda^{N-1}$ is defined as the minimum of the spectrum of the independently constructed $(N-1)$-electron operator, never as the infimum of $\sigma_{ess}(H^{(N)})$, which would make (11.9) circular; its attainment and negativity are conclusions. The goal covers $N \ge 1$; for $N = 1$ the ion has no electrons, $\lambda^0 = 0$ is not negative, so the negativity of $\lambda^{N-1}$ is claimed for $N \ge 2$ only.

A complete development needs the $L^2$ theory of the Fourier transform and $H^2$, Hardy- or Sobolev-type bounds for $1/|x|$ in $\mathbb R^3$, the Kato–Rellich theorem, Weyl's theorem on relatively compact perturbations, a smooth partition of unity on the sphere, and the Weyl criterion for essential spectrum. The definitions of $H_0$, multiplication operators, resolvent and essential spectrum are shared with other chapters of this series and are intended for reuse; contributions of general lemmas about them are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Chapter 11. https://doi.org/10.1090/gsm/099
• G. M. Zhislin, Discussion of the spectrum of Schrödinger operators for systems of many particles, Trudy Moskovskogo Matematicheskogo Obshchestva 9 (1960), 81–120.
• C. van Winter, Theory of finite systems of particles I. The Green function, Matematisk-Fysiske Skrifter Danske Videnskabernes Selskab 2 (1964), no. 8.
• W. Hunziker, On the spectra of Schrödinger multiparticle Hamiltonians, Helvetica Physica Acta 39 (1966), 451–462.
• T. Kato, Fundamental properties of Hamiltonian operators of Schrödinger type, Transactions of the AMS 70 (1951), 195–211. https://doi.org/10.1090/S0002-9947-1951-0041010-X
• H. L. Cycon, R. G. Froese, W. Kirsch, B. Simon, Schrödinger Operators with Application to Quantum Mechanics and Global Geometry, Springer, 1987.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics IV: Analysis of Operators, Academic Press, 1978, Section XIII.5.

Motivation

Stochastic differential equations (SDEs) whose coefficients grow faster than linearly appear throughout applied probability: population and epidemic models with cubic damping, Langevin dynamics with non-quadratic potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options (Goard–Mazur 2013). Their solutions are almost never available in closed form, so they are simulated, and the method of choice is the explicit Euler–Maruyama scheme, because it is cheap and easy to implement.

For superlinearly growing coefficients the classical explicit scheme fails: its moments can diverge even when those of the true solution are finite, so it does not converge in $\mathcal L^p$. Implicit schemes repair this at a higher computational cost (Higham–Mao–Stuart 2002). A second repair is to keep the scheme explicit but modify ("tame") its coefficients by an amount that vanishes as the step size goes to zero.

Timeline.

• 2002: Higham, Mao and Stuart prove strong convergence of implicit Euler-type methods under a one-sided Lipschitz condition (MR1949404).
• 2012: Hutzenthaler, Jentzen and Kloeden introduce the tamed Euler scheme for superlinearly growing drift and globally Lipschitz diffusion (Ann. Appl. Probab. 22, MR2985171).
• 2013: Sabanis gives a short proof of convergence of tamed schemes with rate, again for superlinear drift (Electron. Commun. Probab. 18, MR3070913); Gyöngy and Sabanis prove convergence in probability of Euler approximations under local monotonicity conditions (Appl. Math. Optim. 68, MR3131501).
• 2015: Hutzenthaler and Jentzen obtain $\mathcal L^p$-convergence of explicit schemes with superlinear diffusion coefficients, in the 3/2-model only for $p<1/2$ (Mem. Amer. Math. Soc. 236, no. 1112).
• 2016: Sabanis treats superlinearly growing drift and diffusion coefficients under a local monotonicity condition, with $\mathcal L^p$-convergence for every $p<p_0$ (Ann. Appl. Probab. 26, arXiv:1308.1796). This mission formalizes that $\mathcal L^p$-convergence theorem.

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ satisfying the usual conditions, a Wiener martingale $W$ in $\mathbb R^{d_1}$ (a standard Brownian motion adapted to $\mathcal F_t$ whose future increments are independent of $\mathcal F_t$), and a horizon $T>0$. For $x\in\mathbb R^d$, $|x|$ is the Euclidean norm and $xy$ the scalar product; for a $d\times d_1$ matrix, $|A|$ is the Hilbert–Schmidt norm.

The SDE is

$$dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\tag{2.1}$$

with Borel coefficients $b(t,x)\in\mathbb R^d$, $\sigma(t,x)\in\mathbb R^{d\times d_1}$ and an $\mathcal F_0$-measurable initial value $X(0)$.

For $n\ge1$ let $\kappa_n(t)=\lfloor nt\rfloor/n$, the last grid point of mesh $1/n$ before $t$. The scheme is

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad t\in[0,T],\tag{2.2}$$

with the same initial value $X(0)$ and Borel coefficient sequences $b_n,\sigma_n$ ("varying coefficients"). Between grid points the coefficients are frozen at $X_n(\kappa_n(t))$, so the scheme is explicit.

The hypotheses, with $p_0,p_1\in[2,\infty)$: A-1 continuity of $b$ in $x$; A-2 local boundedness of $b$; A-3 local monotonicity $2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L_R|x-y|^2$ on $|x|,|y|\le R$; A-4 coercivity $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$; A-5 $\mathbb E|X(0)|^{p_0}<\infty$. For the scheme: B-1 $\int_0^T\sup_{|x|\le R}[|b_n-b|^{p_0}+|\sigma_n-\sigma|^{p_0}]\,dt\to0$ for every $R$; B-2 $|b_n|\le\min(Cn^\alpha(1+|x|),|b|)$ and $|\sigma_n|^2\le\min(Cn^\alpha(1+|x|^2),|\sigma|^2)$ for some $\alpha\in(0,1/2]$; B-3 the coercivity bound of A-4 for $b_n,\sigma_n$, uniformly in $n$.

Formalization targets

Goal: Theorem 1 (p. 5)

Under A-1–A-5 and B-1–B-3 with $\alpha\in(0,1/2]$, for every $0<p<p_0$,

$$\lim_{n\to\infty}\sup_{0\le t\le T}\mathbb E\big[|X(t)-X_n(t)|^p\big]=0.$$

No rate is claimed; the statement holds for every coefficient sequence satisfying B-1–B-3, not only for the paper's tamed Models 1 and 2.

Milestones

• Lemma 1 (p. 7): under A-5, B-2, B-3, $\sup_{n\ge1}\sup_{0\le u\le T}\mathbb E|X_n(u)|^2<\infty$.
• Lemma 2 (p. 8): under A-1–A-5, B-2, B-3, for every $p\le p_0$,

$$\sup_{0\le t\le T}\mathbb E|X(t)|^p\ \vee\ \sup_{n\ge1}\sup_{0\le t\le T}\mathbb E|X_n(t)|^p<\infty.$$

• Theorem 4 (p. 6): under A-1–A-4 and B-1, $\sup_{0\le t\le T}|X_n(t)-X(t)|\to0$ in probability.

Significance

Theorem 1 gives $\mathcal L^p$-convergence of a whole class of explicit schemes, with no global Lipschitz condition on either coefficient, for every $p$ below the coercivity order $p_0$. In the 3/2-model of the introduction ($p_1=3.5$, $p_0=6$), earlier explicit results gave $\mathcal L^p$-convergence only for $p<1/2$ (Hutzenthaler–Jentzen 2015, §4.10.3); Theorem 1 gives it for all $p<6$. The theorem is also the qualitative base on which the paper's rate results (Theorems 2 and 3, separate missions of this series) are built, and it justifies Monte Carlo estimates of moments computed with such schemes.

The result is proved in the paper. It has, to our knowledge, no machine-checked proof anywhere; Mathlib has Brownian motion but no stochastic integral, and the Itô integral used here is the relational definition published by the Ethier–Kurtz series on this platform. A formal proof needs Itô's formula for $|x|^p$, Gronwall's lemma for moment functions, the convergence in probability of Theorem 4 (which the paper cites from Gyöngy–Sabanis rather than proving), and a uniform-integrability argument. Each of these is reusable well beyond this paper.

Difficulty

The natural first idea, estimating $\mathbb E|X(t)-X_n(t)|^p$ directly by Itô's formula and Gronwall, fails: under only local monotonicity the difference of drifts cannot be bounded by $|X-X_n|$ with a constant uniform in the state, so the Gronwall constant blows up. The route through convergence in probability and uniform moment bounds is forced, and the hard step is Lemma 2: bounding $\mathbb E|X_n(t)|^{p_0}$ uniformly in $n$. The coefficients of the scheme may grow like $n^\alpha$, and the frozen argument $X_n(\kappa_n(s))$ produces a correction term $\mathbb E\int|X_n(s)|^{p_0-2}(X_n(s)-X_n(\kappa_n(s)))b_n\,ds$ whose control is exactly where the restriction $\alpha\le1/2$ enters. For fixed $n$ finiteness of moments is easy (linear growth); uniformity in $n$ is the content.

Formalization scope

States are EuclideanSpace ℝ (Fin d); diffusion values are EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. Time is ℝ≥0; coefficients are uncurried maps on ℝ≥0 × ℝ^d, assumed Borel measurable. An Itô process on $[0,T]$ is a measurable process, adapted to the filtration augmented by all $P$-null sets, with continuous paths on $[0,T]$, satisfying the integral equation almost surely simultaneously for all $t\le T$; the stochastic integral is the platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise with the integrand cut off after $T$. Nothing is required of the processes after $T$, so no existence beyond the horizon is assumed. Right-continuity of the filtration is a hypothesis; completeness is replaced by adaptedness to the augmented filtration, which is weaker, so the formal theorems are at least as strong as the paper's.

The solutions $X$ and $(X_n)_{n\ge1}$ are hypotheses, all on one probability space with one Wiener process and one initial value; the theorems do not construct them. Expectations are lower Lebesgue integrals in $[0,\infty]$ and suprema over $t$ are taken in $[0,\infty]$, so no statement can hold because an expectation or a supremum takes a default value. B-1's integrand, a supremum over an uncountable ball, is required to be a.e. measurable in $t$, as the paper's Lebesgue integral presupposes. The exponent in Theorem 1 and Lemma 2 is restricted to $p>0$, the paper's convention for $\mathcal L^p$. The dependence clauses "$C:=C(T,K,\mathbb E|X(0)|^2)$" (Lemma 1) and "$C:=C(p,T,K,\mathbb E|X(0)|^p)$" (Lemma 2) are not formalized: only finiteness, i.e. a bound independent of $n$, is stated, which is what the proofs establish. Theorem 4 is stated with exactly its printed hypotheses.

A trivializing formalization, in which the moment bounds or the limit hold because the expectation or the supremum defaults to $0$, or because the hypotheses on the solutions cannot be met, is ruled out: all quantities live in $[0,\infty]$, and a sorry-free check shows every hypothesis is satisfiable (zero coefficients, constant solutions).

Contributions welcome: Itô's formula for the platform's integral relation, Burkholder–Davis–Gundy or Doob inequalities for it, a Gronwall lemma for measurable moment functions, and the Gyöngy–Sabanis convergence-in-probability theorem.

Selected references

• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2016. https://arxiv.org/abs/1308.1796 (v4)
• I. Gyöngy, S. Sabanis, A note on Euler approximations for stochastic differential equations with delay, Appl. Math. Optim. 68, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3131501
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with non-globally Lipschitz continuous coefficients, Ann. Appl. Probab. 22, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=MR2985171
• M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236(1112), 2015. https://doi.org/10.1090/memo/1112
• S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3070913
• D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40, 2002. https://mathscinet.ams.org/mathscinet-getitem?mr=MR1949404

Motivation

In one complex variable, every smooth function $g$ on a disc is $\partial\psi/\partial\bar z$ of some smooth $\psi$, and this is what makes the Mittag-Leffler theorem work: local principal parts can be glued into a global meromorphic function. In several variables the corresponding equation is the $\bar\partial$-problem: given a differential form $\eta$ with $\bar\partial\eta = 0$, find $\omega$ with $\bar\partial\omega = \eta$. Whether it is solvable on a domain $U \subset \mathbb{C}^n$ is measured by the Dolbeault cohomology groups $H^{(p,q)}(U)$. Their vanishing characterizes domains of holomorphy, and it drives the solution of the additive Cousin I problem, the several-variable Mittag-Leffler problem.

This mission follows §4.4–4.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026). There the $\bar\partial$-problem is solved on polydiscs, from the one-variable Cauchy transform through the Dolbeault–Grothendieck lemma. The result is then applied to the Cousin I problem and to domains of holomorphy. The Dolbeault lemma goes back to P. Dolbeault (1953) and A. Grothendieck. The global theory on pseudoconvex domains is due to Hörmander (An Introduction to Complex Analysis in Several Variables, 1966) and to Cartan's Theorem B.

Setting

Write $z_k = x_k + i y_k$ for the coordinates of $\mathbb{C}^n$. The Wirtinger derivative of a function $f$ is $\partial f/\partial\bar z_k = \tfrac12(\partial f/\partial x_k + i\,\partial f/\partial y_k)$.

For strictly increasing tuples $\alpha = (\alpha_1<\dots<\alpha_p)$ and $\beta = (\beta_1<\dots<\beta_q)$ in $\{1,\dots,n\}$, write $dz_\alpha = dz_{\alpha_1}\wedge\cdots\wedge dz_{\alpha_p}$ and $d\bar z_\beta = d\bar z_{\beta_1}\wedge\cdots\wedge d\bar z_{\beta_q}$. A smooth $(p,q)$-form on an open $U\subset\mathbb{C}^n$ is

$$\eta = \sum_{\alpha,\beta}\eta_{\alpha\beta}\,dz_\alpha\wedge d\bar z_\beta,$$

where $\alpha$ and $\beta$ run over the increasing $p$- and $q$-tuples and each $\eta_{\alpha\beta}$ is $C^\infty$ on $U$. The operator

$$\bar\partial\eta = \sum_{\alpha,\beta}\sum_{k=1}^n \frac{\partial\eta_{\alpha\beta}}{\partial\bar z_k}\,d\bar z_k\wedge dz_\alpha\wedge d\bar z_\beta$$

maps $(p,q)$-forms to $(p,q+1)$-forms. A form is $\bar\partial$-closed if $\bar\partial\eta = 0$ and $\bar\partial$-exact if $\eta = \bar\partial\omega$; by convention the only exact $(p,0)$-form is $0$. The statement $H^{(p,q)}(U) = 0$ means that every smooth $\bar\partial$-closed $(p,q)$-form on $U$ is $\bar\partial$-exact.

A possibly unbounded polydisc is a product $\Delta = D_1\times\cdots\times D_n$ in which each $D_k$ is either a disc $\{|z_k - a_k|<\rho_k\}$ or all of $\mathbb{C}$; for example $\mathbb{C}^n$ itself. The finite polydisc is $\Delta_r(w) = \{z : |z_\ell - w_\ell| < r_\ell\ \forall\ell\}$.

Cousin I data on an open $U$ consist of an open covering $\{U_\iota\}_{\iota\in I}$ of $U$ and holomorphic $h_{\iota\kappa}$ on $U_\iota\cap U_\kappa$ with $h_{\iota\kappa}+h_{\kappa\iota}=0$ and $h_{\iota\kappa}+h_{\kappa\lambda}+h_{\lambda\iota}=0$ on the respective intersections. A solution is a family of holomorphic $f_\iota$ on $U_\iota$ with $h_{\iota\kappa} = f_\iota - f_\kappa$. The problem is solvable on $U$ if all Cousin I data on $U$ have solutions.

In Lean these are wirtingerBar, FormCoeffs, dbar, IsSmoothForm, DolbeaultVanishes, polydisc, IsPossiblyUnboundedPolydisc, IsCousinISolvable and IsDomainOfHolomorphy in the namespace LeblSCV.Dolbeault.

Formalization targets

Goal: Theorem 4.4.5

Let $\Delta\subset\mathbb{C}^n$ be a possibly unbounded polydisc, $p\ge0$, $q\ge1$, and $\eta$ a smooth $(p,q)$-form on $\Delta$ with $\bar\partial\eta = 0$. Then there is a smooth $(p,q-1)$-form $\omega$ on $\Delta$ with

$$\bar\partial\omega = \eta\quad\text{on }\Delta,\qquad\text{that is,}\qquad H^{(p,q)}(\Delta) = 0 \ \ (q\ge1).$$

Milestones

1. Lemma 4.4.6 (for a disc $U$). If $g$ is smooth near $\overline U$, then $\psi(z) = \frac{1}{2\pi i}\int_U \frac{g(\zeta)}{\zeta-z}\,d\zeta\wedge d\bar\zeta$ is smooth on $U$ and $\partial\psi/\partial\bar z = g$.
2. Lemma 4.4.7 (Dolbeault–Grothendieck). If $0<s_\ell<r_\ell$, every smooth $\bar\partial$-closed $(p,q)$-form on $\Delta_r(w)$, $q\ge1$, is $\bar\partial$ of a smooth $(p,q-1)$-form on $\Delta_s(w)$.
3. Lemma 4.6.4. Smooth Cousin I data on any open set have smooth solutions.
4. Theorem 4.6.5. On a domain with $H^{(0,1)}(U)=0$ the Cousin I problem is solvable.
5. Corollary 4.6.6. The Cousin I problem is solvable on every possibly unbounded polydisc.
6. Theorem 4.5.6. A domain $U\subset\mathbb{C}^n$ with $H^{(0,q)}(U)=0$ for $1\le q\le n-1$ is a domain of holomorphy.

Significance

Theorem 4.4.5 is the model case of the vanishing theorem $H^{(p,q)}(U)=0$, $q\ge1$, on domains of holomorphy. In particular it solves the $\bar\partial$-problem on all of $\mathbb{C}^n$. Through Theorem 4.6.5 it gives the Cousin I problem on polydiscs, and therefore the existence of meromorphic functions with prescribed local principal parts there. Theorem 4.5.6 is one half of the cohomological characterization of domains of holomorphy (Remark 4.5.8, item (viii)). The other half is Cartan's Theorem B, which the book states without proof as Theorem 4.4.2.

All targets are classical and fully proved in the book. As far as a search of the Prove2Me corpus and of Mathlib shows, none of them is formalized. Mathlib has real Fréchet derivatives, smooth bump functions and partitions of unity, and Lebesgue measure on $\mathbb{C}$. It has no bidegree forms, no $\bar\partial$ operator on forms, no Cauchy transform and no Dolbeault cohomology. This mission builds the $(p,q)$-form layer and the first global solvability theorem for $\bar\partial$.

Difficulty

The one-variable step needs the Cauchy–Pompeiu formula and differentiation under an integral with a weakly singular kernel. Both the smoothness of $\psi$ and the identity $\partial\psi/\partial\bar z = g$ require care near $\zeta = z$.

In several variables, the natural idea is to solve $\bar\partial\omega=\eta$ on each of an exhausting sequence of polydiscs and take a limit. It fails as stated: solutions on successive polydiscs differ by $\bar\partial$-closed forms and need not converge. For $q\ge2$ the discrepancy has to be corrected exactly, by applying the lemma again with a cutoff. For $q=1$ the discrepancies are holomorphic functions, and they have to be made small by polynomial approximation, so that the corrected solutions converge. The Dolbeault–Grothendieck lemma loses a little of the polydisc at each step, so the argument has to shrink the polydiscs at each stage.

On the formal side, $\bar\partial$ on forms carries signs from reordering wedge products. A wrong sign changes which forms are closed. So the sign convention is fixed in the definition and checked against $\bar\partial\circ\bar\partial = 0$.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ with 0-based indices. Polydiscs use the modulus in each coordinate, as in the book, so the sup norm of Fin n → ℂ agrees with them. No Euclidean ball occurs.
• A form is a coefficient family FormCoeffs n = Finset (Fin n) → Finset (Fin n) → (Fin n → ℂ) → ℂ: an increasing tuple is the set of its entries, and η A B z is the coefficient of $dz_A\wedge d\bar z_B$. IsSmoothForm U p q η requires every coefficient to be ContDiffOn ℝ ∞ on $U$ and the coefficients of the wrong bidegree to vanish on $U$. Only values on $U$ matter.
• dbar is Definition 4.4.1 written in the increasing basis. The coefficient of $dz_A\wedge d\bar z_C$ is $\sum_{k\in C}(-1)^{|A|+\#\{j\in C:j<k\}}\,\partial\eta_{A,C\setminus\{k\}}/\partial\bar z_k$. A sorry-free check confirms that this sign convention makes the mixed second derivatives cancel in $\bar\partial\bar\partial\eta$, and that $\partial\bar z_1/\partial\bar z_1 = 1$.
• $H^{(p,q)}(U)=0$ is stated as "every closed smooth $(p,q)$-form is exact"; the quotient space is not built. The solution $\omega$ is required to be smooth.
• Radii of a possibly unbounded polydisc lie in ℝ≥0∞, with $\infty$ meaning the factor $\mathbb{C}$.
• Holomorphic on an open set is DifferentiableOn ℂ. A domain is an open connected set. Cousin index types range over Type, which loses nothing.
• Restriction: Lemma 4.4.6 is stated for $U$ an open disc. The book allows any bounded open set with piecewise-$C^1$ boundary. The disc is the case that the Dolbeault–Grothendieck lemma uses. The measure $d\zeta\wedge d\bar\zeta$ is $-2i$ times Lebesgue measure.
• The goal cannot be trivialized through the form layer. A definition of $\bar\partial$ with a wrong sign, or one that drops the smoothness of $\omega$ or the $\bar\partial$-closedness of $\eta$, states a different theorem and is ruled out. Hypotheses are satisfiable: $\eta = 0$ is closed, and $\mathbb{C}^n$ is a possibly unbounded polydisc (checked sorry-free).
• Needed infrastructure: the Cauchy transform and Cauchy–Pompeiu formula, differentiation under the integral with parameters, smooth cutoffs, uniform approximation of holomorphic functions by polynomials on polydiscs, and partitions of unity. The form layer is reusable in later work on the $\bar\partial$-problem (balls, Hartogs triangle, pseudoconvex domains). Proofs of $\bar\partial^2 = 0$ for the dbar defined here, or of the one-variable lemma for general piecewise-$C^1$ domains, are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, §4.4–4.6. https://www.jirka.org/scv/
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, North-Holland Mathematical Library 7, 3rd ed., 1990.
• P. Dolbeault, Sur la cohomologie des variétés analytiques complexes, C. R. Acad. Sci. Paris 236 (1953), 175–177.