Analysis

Motivation

In spectral theory the resolvent of a self-adjoint operator $A$ is studied through scalar functions $F_\psi(z) = \langle \psi, (A - z)^{-1}\psi\rangle$, defined for non-real $z$. Each $F_\psi$ is holomorphic on the upper half plane and maps it into itself. The spectral theorem, in the form presented in G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), comes down to the converse: a function of this kind with the right growth is the Cauchy–Stieltjes transform of a finite measure on $\mathbb{R}$, and that measure is the spectral measure of $\psi$. In the other direction, the absolutely continuous, singularly continuous and pure point spectra of Schrödinger operators are identified by looking at the boundary values of $F_\psi$ on the real axis. This mission formalizes the appendix to Chapter 3 of Teschl's book (Section 3.4, The Herglotz theorem, pp. 106–110) and Theorem 3.10, the measure-theoretic layer that the rest of the book's spectral analysis stands on.

The representation goes back to G. Herglotz (1911) for the disc and R. Nevanlinna (1922) for the half plane. The inversion formula is due to T. J. Stieltjes (1894). The link between boundary values and the Lebesgue decomposition of the measure is classical harmonic analysis on the half plane (Fatou, de la Vallée Poussin) and is the tool behind the spectral-type results of Gilbert–Pearson subordinacy theory and Aronszajn–Donoghue rank-one perturbation theory.

Setting

Write $\mathbb{C}_+ = \{z \in \mathbb{C} \mid \operatorname{Im}(z) > 0\}$. A Herglotz function is a holomorphic map $F$ on $\mathbb{C}_+$ with $\operatorname{Im} F(z) > 0$ for every $z \in \mathbb{C}_+$ (IsHerglotz).

For a Borel measure $\mu$ on $\mathbb{R}$, its Borel transform is

$$F(z) = \int_{\mathbb{R}} \frac{d\mu(\lambda)}{\lambda - z}$$

(borelTransform μ). The spectrum of $\mu$ is its set of growth points, $\sigma(\mu) = \{\lambda \mid \mu((\lambda-\varepsilon,\lambda+\varepsilon)) > 0 \text{ for all } \varepsilon > 0\}$ (measureSpectrum).

With $B_\varepsilon(x) = (x - \varepsilon, x + \varepsilon)$ and $|\cdot|$ Lebesgue measure, the upper and lower derivatives of $\mu$ are $(\overline{D}\mu)(x) = \limsup_{\varepsilon\downarrow0} \mu(B_\varepsilon(x))/|B_\varepsilon(x)|$ and $(\underline{D}\mu)(x) = \liminf_{\varepsilon\downarrow0} \mu(B_\varepsilon(x))/|B_\varepsilon(x)|$, values in $[0,\infty]$ (upperDeriv, lowerDeriv). The derivative $(D\mu)(x)$ is the limit when it exists, possibly $\infty$ (HasMeasureDeriv μ x d).

A set $A$ is a support of $\mu$ if $\mu(\mathbb{R}\setminus A) = 0$ (IsSupport). A support $M$ is a minimal support if every Borel $M_0 \subseteq M$ with $\mu(M_0) = 0$ is Lebesgue-null (IsMinimalSupport). The Lebesgue decomposition $d\mu = d\mu_{ac} + d\mu_s$ with respect to Lebesgue measure refines to $d\mu_s = d\mu_{sc} + d\mu_{pp}$, where $\mu_{pp}$ lives on the atoms of $\mu$. The absolutely continuous part $\mu_{ac}$ and the singularly continuous part $\mu_{sc}$ are acPart μ and scPart μ.

Formalization targets

Goal: Herglotz representation (Theorem 3.20)

If $F$ is a Herglotz function and $|F(z)| \le M/\operatorname{Im}(z)$ for all $z \in \mathbb{C}_+$, then there is a Borel measure $\mu$ on $\mathbb{R}$ with $\mu(\mathbb{R}) \le M$ and

$$F(z) = \int_{\mathbb{R}} \frac{d\mu(\lambda)}{\lambda - z}, \qquad z \in \mathbb{C}_+ .$$

Milestones

1. Theorem 3.10. For a finite Borel measure $\mu$, the transform is holomorphic on $\mathbb{C}\setminus\sigma(\mu)$, is a Herglotz function when $\mu \ne 0$, and satisfies $F(z^*) = F(z)^*$ and $|F(z)| \le \mu(\mathbb{R})/\operatorname{Im}(z)$ on $\mathbb{C}_+$.
2. Theorem 3.21. $\mu$ is determined by its transform on $\mathbb{C}_+$, and for $\lambda_1 < \lambda_2$

$$\tfrac12\bigl(\mu((\lambda_1,\lambda_2)) + \mu([\lambda_1,\lambda_2])\bigr) = \lim_{\varepsilon\downarrow0}\frac1\pi\int_{\lambda_1}^{\lambda_2}\operatorname{Im}F(\lambda+i\varepsilon)\,d\lambda .$$

3. Theorem 3.22. For every $\lambda$, $(\underline D\mu)(\lambda) \le \liminf_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon) \le \limsup_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon) \le (\overline D\mu)(\lambda)$.
4. Theorem 3.23. $\lim_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon)$ exists in $[0,\infty]$ for $\mu$-a.e. and Lebesgue-a.e. $\lambda$, equals $(D\mu)(\lambda)$ wherever the latter exists; the set where it is $\infty$ supports $\mu_{sc}$, and the set where it lies in $(0,\infty)$ is a minimal support of $\mu_{ac}$.
5. Corollary 3.24. If $\limsup_{\varepsilon\downarrow0}\operatorname{Im}F(\lambda+i\varepsilon) < \infty$ for all $\lambda$ in a Borel set $I$, then $\mu|_I$ is absolutely continuous.
6. Corollary 3.25. $\lim_{\varepsilon\downarrow0}F(\lambda+i\varepsilon)$ exists (finite or $\infty$) $\mu$-a.e. and Lebesgue-a.e., and is finite Lebesgue-a.e.

Significance

Theorem 3.20 together with Theorem 3.10 is a bijection between finite Borel measures on $\mathbb{R}$ and Herglotz functions of bounded growth $\operatorname{Im}(z)|F(z)|$. In Teschl's development it produces the spectral measures $\mu_\psi$ from the resolvent, and hence the projection-valued measure of an unbounded self-adjoint operator. Theorems 3.21–3.25 turn spectral questions into boundary-value questions. The later chapters on Sturm–Liouville operators and one-dimensional Schrödinger operators decide which spectral type an operator has by reading $\operatorname{Im} F(\lambda + i0)$ for the Weyl–Titchmarsh function.

These are textbook results with complete published proofs. Mathlib has the upper half plane as a type, Lebesgue decomposition, Radon–Nikodym derivatives and Vitali-family differentiation of measures, but it has no Borel (Cauchy–Stieltjes) transform of a measure on $\mathbb{R}$, no Herglotz representation on the half plane, and no Stieltjes inversion. The remaining work is to formalize the known proofs against Mathlib's measure theory and complex analysis. No machine-checked version of these statements is known to exist on Prove2Me.

Difficulty

For the goal, the measure has to be built: nothing in the hypothesis names it. A Herglotz function gives no measure directly, only a family of absolutely continuous approximations coming from the boundary values of $\operatorname{Im} F$ slightly above the real axis. The difficulty is to pass to a limit that is only a measure (it may have atoms and singular parts), and to identify the limit's transform with $F$ itself, not just its imaginary part. The uniform bound is what makes the limit exist and keeps its mass at most $M$. Without it the general Nevanlinna representation carries an extra linear term and a non-finite measure, and the statement here fails.

For the boundary-value theorems, the pointwise behaviour of the Poisson integral has to be compared with the symmetric derivatives of $\mu$ at each point, including points where $\mu$ is singular. The almost-everywhere statements for both $\mu$ and Lebesgue measure need the differentiation theory of measures in its singular form: the derivative is infinite $\mu_s$-almost everywhere, not only finite Lebesgue-almost everywhere.

Formalization scope

Measures are MeasureTheory.Measure ℝ on the Borel σ-algebra. Every theorem assumes IsFiniteMeasure μ, except the goal, whose conclusion μ Set.univ ≤ ENNReal.ofReal M makes μ finite. Functions on the half plane are ℂ → ℂ, constrained only on {z | 0 < z.im}. The Borel transform is a Bochner integral. Every claim evaluates it where the integrand is bounded, so Mathlib's convention that a non-integrable integral is $0$ never enters.

Limits as $\varepsilon \downarrow 0$ are taken along 𝓝[>] 0. The quantities that may be infinite (derivatives of measures, boundary values of $\operatorname{Im}F$) live in ℝ≥0∞, with $\operatorname{Im}F(\lambda+i\varepsilon)$, which is nonnegative for $\varepsilon > 0$, embedded by ENNReal.ofReal. An infinite limit of $F$ itself is Tendsto … (Bornology.cobounded ℂ). The lower and upper derivatives, the supports and the parts $\mu_{ac}$, $\mu_{sc}$ are defined in the mission's namespace exactly as in the book (Sec. A.8, Sec. 3.2).

Three readings of the printed text are fixed. Theorem 3.22 is stated for $\operatorname{Im}F(\lambda+i\varepsilon)$, which is what its proof estimates. Theorem 3.23's identity takes the factor $1/\pi$ once, consistent with Theorem 3.22. Theorem 3.10's Herglotz conclusion is stated for $\mu \ne 0$: the book's Herglotz functions map into the open half plane, and the zero measure's transform is identically zero.

A Herglotz function is defined analytically (holomorphic, positive imaginary part), never as "a Borel transform"; the latter would make the goal a tautology. No object is taken as data. The chunk uses no Hilbert space, no operator, and no projection-valued measure.

Useful infrastructure: UpperHalfPlane, Cauchy's integral formula on rectangles and semicircles, weak compactness of finite measures on $\mathbb{R}$ (Helly/Prokhorov), Mathlib's VitaliFamily.ae_tendsto_rnDeriv and Measure.singularPart. A reusable Poisson-kernel library for the half plane would be a welcome by-product, as would the vague-convergence lemmas of the book's Appendix A.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Sec. 3.2, Sec. 3.4 and Sec. A.8. https://doi.org/10.1090/gsm/099
• G. Herglotz, Über Potenzreihen mit positivem, reellen Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, Math.-Phys. Klasse 63 (1911), 501–511.
• R. Nevanlinna, Asymptotische Entwicklungen beschränkter Funktionen und das Stieltjessche Momentenproblem, Annales Academiae Scientiarum Fennicae A 18 (1922).
• T. J. Stieltjes, Recherches sur les fractions continues, Annales de la Faculté des Sciences de Toulouse 8 (1894), J1–J122. https://doi.org/10.5802/afst.108
• F. Gesztesy, E. Tsekanovskii, On matrix-valued Herglotz functions, Mathematische Nachrichten 218 (2000), 61–138. https://doi.org/10.1002/1522-2616(200010)218:1<61::AID-MANA61>3.0.CO;2-D

Why self-adjoint extensions matter

In quantum mechanics an observable is a self-adjoint operator on a complex Hilbert space $\mathfrak{H}$. Physics, however, usually hands over a symmetric operator: a differential expression such as $-\mathrm{i}\,\tfrac{d}{dx}$ or $-\Delta + V$ on a convenient domain of smooth functions, on which integration by parts shows $\langle \varphi, A\psi\rangle = \langle A\varphi, \psi\rangle$. Symmetry is easy to check and self-adjointness is not. Two questions then decide whether the formal expression defines a physical theory: does $A$ have a self-adjoint extension at all, and if so, how many? Different extensions correspond to different boundary conditions and to different dynamics (via Stone's theorem), so the answer is physically meaningful.

John von Neumann answered both questions in 1929–1930 with the Cayley transform and the defect indices (von Neumann 1930). His criterion is the goal of this mission, in the form given in Chapter 2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), from which every statement of the mission is taken.

Setting

Let $\mathfrak{H}$ be a complex Hilbert space with inner product $\langle\cdot,\cdot\rangle$, conjugate-linear in the first argument. A linear operator $A$ is a linear map $A : \mathfrak{D}(A) \to \mathfrak{H}$ defined on a linear subspace $\mathfrak{D}(A)$, its domain. An operator $B$ extends $A$, written $A \subseteq B$, if $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and $B\psi = A\psi$ for $\psi \in \mathfrak{D}(A)$.

$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 densely defined $A$ the adjoint $A^*$ has domain $\{\psi \mid \exists \tilde\psi : \langle\psi, A\varphi\rangle = \langle\tilde\psi, \varphi\rangle \ \forall \varphi \in \mathfrak{D}(A)\}$ and acts by $A^*\psi = \tilde\psi$. $A$ is self-adjoint if $A = A^*$, domains included, and essentially self-adjoint if its closure $\overline{A}$ (the operator whose graph is the closure of the graph of $A$) is self-adjoint.

For $z \in \mathbb{C}$, $A + z$ is the operator $\psi \mapsto A\psi + z\psi$ on $\mathfrak{D}(A)$. The resolvent set $\rho(A)$ is the set of $z$ for which $A - z : \mathfrak{D}(A) \to \mathfrak{H}$ is a bijection with bounded inverse $R_A(z) = (A-z)^{-1}$, and the spectrum is $\sigma(A) = \mathbb{C}\setminus\rho(A)$.

For symmetric $A$ the defect spaces and defect indices are

$$K_\pm = \operatorname{Ran}(A \pm \mathrm{i})^\perp = \operatorname{Ker}(A^* \mp \mathrm{i}), \qquad d_\pm(A) = \dim K_\pm,$$

where $\dim$ is the Hilbert dimension (the cardinality of an orthonormal basis, possibly infinite). The Cayley transform of $A$ is

$$V = (A - \mathrm{i})(A + \mathrm{i})^{-1} : \operatorname{Ran}(A + \mathrm{i}) \to \operatorname{Ran}(A - \mathrm{i}).$$

Formalization targets

Goal: von Neumann's criterion (Theorem 2.26)

For every symmetric operator $A$,

$$\exists\, B \supseteq A \text{ self-adjoint} \iff d_+(A) = d_-(A).$$

Milestones

In the order of the book:

• Corollary 2.2. A self-adjoint operator has no proper symmetric extension.
• Lemma 2.3. If $A$ is symmetric and $\operatorname{Ran}(A + z) = \operatorname{Ran}(A + z^*) = \mathfrak{H}$ for one $z \in \mathbb{C}$, then $A$ is self-adjoint.
• Lemma 2.7. A symmetric $A$ is essentially self-adjoint iff $\overline{\operatorname{Ran}(A+z)} = \overline{\operatorname{Ran}(A+z^*)} = \mathfrak{H}$ for one $z \in \mathbb{C}\setminus\mathbb{R}$, iff $\operatorname{Ker}(A^*+z) = \operatorname{Ker}(A^*+z^*) = \{0\}$ for one such $z$; for nonnegative $A$, a real $z > 0$ (spectral point $-z < 0$) may be used too.
• Theorem 2.18. A symmetric $A$ is self-adjoint iff $\sigma(A) \subseteq \mathbb{R}$; it is self-adjoint with $A \ge E$ iff $\sigma(A) \subseteq [E,\infty)$; and then $\|R_A(z)\| \le |\operatorname{Im} z|^{-1}$ and $\|R_A(\lambda)\| \le |\lambda - E|^{-1}$ for $\lambda < E$.
• Theorem 2.25. The Cayley transform is a bijection from the symmetric operators onto the isometric operators $V$ with $\operatorname{Ran}(1 - V)$ dense.
• Theorem 2.26, (2.103)–(2.104). For a closed symmetric $A$ with a self-adjoint extension $A_1$ whose Cayley transform is $V_1$: $\mathfrak{D}(A_1) = \mathfrak{D}(A) + (1 - V_1)K_+$ and $A_1(\psi + \varphi_+ - V_1\varphi_+) = A\psi + \mathrm{i}\varphi_+ + \mathrm{i}V_1\varphi_+$.
• Lemma 2.27. $A$ is closed iff $\mathfrak{D}(V)$ is closed iff $\operatorname{Ran}(V)$ is closed iff $V$ is closed.
• Theorem 2.28. If a symmetric $A$ commutes with a conjugation $C$ ($C$-real), then $d_+(A) = d_-(A)$.

Significance

The criterion is the standard tool for deciding whether a formal Hamiltonian is a legitimate observable, and for classifying its realizations: by the parametrization (2.103)–(2.104), the self-adjoint extensions correspond to the unitary maps $K_+ \to K_-$. Theorem 2.28 turns the criterion into a practical test, since every real differential operator, for example a Schrödinger operator with real potential, is $C$-real for complex conjugation and therefore has self-adjoint extensions. Lemma 2.7 and Theorem 2.18 are the everyday criteria for self-adjointness and the basic spectral facts on which Chapters 3–6 of the book rest. The Friedrichs extension, Weyl's limit point/limit circle theory and the Kato–Rellich theorem all refine these statements.

All of these results are classical and proved in every text on unbounded operators (for example Schmüdgen 2012, Chapters 3 and 13). None is formalized in Mathlib, which provides the adjoint, closure and self-adjointness of a LinearPMap but no resolvent set, spectrum, Cayley transform or defect theory for unbounded operators. The platform's existing material on essential self-adjointness is stated for specific Hamiltonians on bespoke structures, not for general operators. A formal proof here supplies the unbounded-operator layer that every later mission in this series (spectral theorem, Kato–Rellich, Weyl's theorem, Sturm–Liouville theory) restates.

Difficulty

The obvious reduction, "a self-adjoint extension is a unitary extension of the Cayley transform, and a unitary $K_+ \to K_-$ exists iff the dimensions agree", hides most of the work. The correspondence between extensions of $A$ and extensions of $V$ runs through the inverse Cayley transform $A = \mathrm{i}(1+V)(1-V)^{-1}$, which requires injectivity of $1 - V$ and careful bookkeeping of partial domains. Extending an isometry to a unitary requires passing to closures of $\operatorname{Ran}(A \pm \mathrm{i})$ when $A$ is not closed. Equal Hilbert dimension must be converted into an actual unitary between the defect spaces. Theorem 2.18 needs the self-adjointness criterion of Lemma 2.7 in the direction "spectrum real implies self-adjoint", where the range conditions come from the resolvent set rather than from symmetry. Each of these steps is routine on paper and requires explicit domain management in Lean.

Formalization scope

Operators are Mathlib LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space (InnerProductSpace ℂ H, CompleteSpace H). Separability, part of the book's standing assumption, is not needed by any statement and is not assumed. Extension is the order A ≤ B. Self-adjointness is Mathlib's IsSelfAdjoint (equality with LinearPMap.adjoint), and symmetry includes density of the domain, so every adjoint in the mission is taken of a densely defined operator and is the book's $A^*$. The closure is LinearPMap.closure; closedness is LinearPMap.IsClosed.

The mission uses the series' shared definitions TeschlQM.Shared.IsSymmetric, TeschlQM.Shared.IsEssentiallySelfAdjoint and TeschlQM.Shared.IsResolventAt, resolventSet, spectrum, and defines, in the namespace TeschlQM.SelfAdjoint: addScalar, rangeAdd, kerAdd for $A + z$, $\operatorname{Ran}(A+z)$, $\operatorname{Ker}(A+z)$; IsCayleyTransform, IsIsometric, rangeOneSub; defectPlus, defectMinus, HasEqualDefectIndices; IsConjugation, IsCReal. Nothing that the book derives is taken as data: the Cayley transform is a relation that determines $V$ from $A$, and its existence and uniqueness are part of Theorem 2.25.

Conventions that matter:

• $\sigma(A)$ is defined exactly as on p. 73 of the book (bijective onto $\mathfrak{H}$ with bounded inverse), not with Mathlib's Banach-algebra spectrum. For a non-closed operator this makes $\sigma(A) = \mathbb{C}$.
• $K_\pm$ are $\operatorname{Ran}(A\pm\mathrm{i})^\perp$, and $d_+ = d_-$ is expressed as the existence of a unitary K₊ ≃ₗᵢ[ℂ] K₋, which is equivalent to equality of Hilbert dimensions. Reading "self-adjoint extension" with the order reversed, or taking $K_\pm$ as kernels of $A \mp \mathrm{i}$ (which are trivial for symmetric $A$), would make the goal trivial; neither is used.
• A conjugation satisfies $\langle C\psi, C\varphi\rangle = \langle\varphi,\psi\rangle$ (antiunitary). The book prints $\langle\psi,\varphi\rangle$ on the right, which no nonzero conjugate-linear map satisfies.
• In Lemma 2.7 the book admits "$z \in (-\infty, 0)$" for nonnegative $A$ while writing the conditions on $A + z$; the correct range in that convention, and the one its proof uses, is $z \in (0, \infty)$, which is what is stated.
• The (2.103)–(2.104) milestone assumes $A$ closed; without it (2.103) is false (a non-closed essentially self-adjoint $A$ is a counterexample).

Reusable parts: the resolvent/spectrum layer and the Cayley transform are needed throughout the rest of the book. Proofs of any milestone, and API lemmas about rangeAdd, kerAdd and adjoints (such as $\operatorname{Ker}(A^*) = \operatorname{Ran}(A)^\perp$ and the reversal $A \subseteq B \Rightarrow B^* \subseteq A^*$), are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Chapter 2. 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
• K. Schmüdgen, Unbounded Self-adjoint Operators on Hilbert Space, Graduate Texts in Mathematics 265, Springer, 2012. https://doi.org/10.1007/978-94-007-4753-1

Motivation

A closed set $F\subseteq\mathbb R^n$ is flow-invariant for a dynamical system when every trajectory that starts in $F$ stays in $F$. Invariance of sets underlies state constraints in optimal control, safety certificates for controlled systems, comparison and maximum principles for differential equations, and the positivity of solutions of kinetic and population models. The question is always the same: which infinitesimal condition at the points of $F$ is equivalent to the global statement that trajectories cannot leave $F$?

For a smooth vector field and a smooth boundary the answer is that the field must not point strictly outward. For a nonsmooth set, such as a polyhedron, the positive orthant or a set with inward cusps, "pointing inward" must be made precise through a notion of tangent vector that works at corners. Frank H. Clarke's 1975 paper introduces the generalized gradient of a Lipschitz function and derives from it a normal cone and a tangent cone for arbitrary closed sets. Its Theorem (4.4) shows that this tangent cone is exactly the right notion: for a Lipschitz differential inclusion $\dot x\in X(x)$, a closed set is flow-invariant if and only if $X(x)$ is contained in the tangent cone at each point of the set.

Timeline:

• 1942. Nagumo characterizes invariance for continuous ODEs with unique solutions by a condition on the distance function (Proc. Phys.-Math. Soc. Japan 24).
• 1969. Bony proves an invariance theorem for Lipschitz vector fields, stated through exterior normals, in the course of a maximum principle for degenerate elliptic operators (Bony 1969).
• 1970. Brezis characterizes flow-invariant closed sets of a locally Lipschitz vector field by $\lim_{\delta\downarrow0} d_F(y+\delta X(y))/\delta=0$ (Brezis 1970).
• 1972. Redheffer gives simplified proofs of the Bony and Brezis theorems under weaker "uniqueness function" hypotheses (Amer. Math. Monthly 79, 740–747).
• 1975. Clarke extends the characterization to Lipschitz multifunctions with nonempty compact values, with tangency in the sense of his new tangent cone, and recovers Bony and Brezis as corollaries (Clarke 1975, Theorem (4.4), Corollaries (4.10), (4.12)).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $\zeta\cdot v$ and norm $|\cdot|$.

Generalized gradient. For $f:\mathbb R^n\to\mathbb R$ Lipschitz on bounded sets, $\partial f(x)$ is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ with $h_i\to0$ and $f$ differentiable at each $x+h_i$ (Definition (1.1)). The generalized directional derivative is $f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}[f(x+h+\delta v)-f(x+h)]/\delta$ (Definition (1.3)).

Distance function. For a nonempty closed $E\subseteq\mathbb R^n$, $d_E(x)=\min\{|x-e|:e\in E\}$. It is Lipschitz with constant $1$. A point $e\in E$ with $|x-e|=d_E(x)$ is a closest point to $x$; it exists but need not be unique.

Normal and tangent cones. For $e\in E$, the cone of normals is

$$N_E(e)=\operatorname{cl}\{p:\ s\,p\in\partial d_E(e)\text{ for some }s>0\}\qquad\text{(Definition (3.1))},$$

and the tangent cone is its dual,

$$T_E(e)=\{\zeta:\ \zeta\cdot v\le0\text{ for all }v\in N_E(e)\}\qquad\text{(Definition (3.6))}.$$

Differential inclusions. A multifunction $X$ assigns to each $x\in\mathbb R^n$ a set $X(x)\subseteq\mathbb R^n$; standing assumption of §4: every $X(x)$ is nonempty and compact. A trajectory is an absolutely continuous $x:[0,1]\to\mathbb R^n$ with $\dot x(t)\in X(x(t))$ for almost every $t$ ((4.1)). $X$ is Lipschitz if there is $K$ such that for all $x_1,x_2$ and $v_1\in X(x_1)$ some $v_2\in X(x_2)$ has $|v_1-v_2|\le K|x_1-x_2|$ ((4.2)). A closed set $F$ is flow-invariant for $X$ if every trajectory with $x(0)\in F$ has $x(t)\in F$ for all $t\in[0,1]$ ((4.3)).

Formalization targets

Goal: Theorem (4.4)

Let $X$ be a Lipschitz multifunction with nonempty compact values and $F$ a nonempty closed subset of $\mathbb R^n$. Then

$$F\text{ is flow-invariant for }X\iff X(x)\subseteq T_F(x)\ \text{ for every }x\in F.$$

Milestones, in the order the proof uses them

1. Proposition (1.4). $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$.
2. Proposition (2.4). If $\nabla d_E(x)$ exists and is nonzero, then $x\notin E$, $x$ has a unique closest point $e$, and $\nabla d_E(x)=(x-e)/|x-e|$.
3. Corollary (2.5). For $e\in E$, $\partial d_E(e)=\operatorname{co}\{0,\lim (x_i-e_i)/|x_i-e_i|\}$ over $x_i\notin E$, $x_i\to e$, $e_i$ closest to $x_i$.
4. Proposition (3.2). $N_E(e)=\operatorname{cl}\operatorname{co}\{\lim s_i(x_i-e_i)\}$ over $s_i\ge0$, $x_i\to e$, $e_i$ closest to $x_i$.
5. Inequality (4.8). If $X(y)\subseteq T_F(y)$ on $F$ and $x$ is a trajectory, then $f(t)=d_F(x(t))$ satisfies $f'(t)\le Kf(t)$ almost everywhere.
6. Limit (4.9). If $F$ is flow-invariant, then $d_F(y+\delta v)/\delta\to0$ as $\delta\downarrow0$ for every $y\in F$ and $v\in X(y)$.
7. Proposition (3.7). $v\in T_E(e_0)$ iff $\lim_{e\to e_0,\,e\in E}\liminf_{\delta\downarrow0} d_E(e+\delta v)/\delta=0$.

Significance

The result. Theorem (4.4) turns a statement about all trajectories of a set-valued dynamical system into a pointwise geometric condition on $F$ that can be checked without solving anything. It is the prototype of the strong invariance theorems of nonsmooth control theory, later developed in viability theory and in the monograph of Clarke, Ledyaev, Stern and Wolenski, and it is the tool behind state-constrained optimal control and Lyapunov-type arguments for nonsmooth systems. Its corollaries recover the Bony and Brezis theorems for Lipschitz vector fields. The companion milestones (2.5), (3.2) and (3.7) are standalone facts of nonsmooth geometry: the Clarke normal cone is generated by limits of proximal normals, and Clarke tangency can be tested along rays from nearby points of the set.

Formalizing it. The result is proved in the paper and has been reproved in textbooks; to the best of our knowledge it has no machine-checked proof. Mathlib contains Rademacher's theorem, absolutely continuous functions on intervals and the Bouligand tangent cone, but no Clarke generalized gradient, no Clarke normal or tangent cone, and no theory of differential inclusions. A complete development supplies a first nonsmooth-analysis layer on top of Mathlib and a first existence theorem for Lipschitz differential inclusions.

Difficulty

The direction (2) $\Rightarrow$ (1) looks like a Gronwall argument for $f(t)=d_F(x(t))$, but $d_F$ is not differentiable, $x$ is only absolutely continuous, and the closest point to $x(t)$ can jump. The step that must be controlled is the comparison between $\dot x(t)$, a nearby admissible velocity at the closest point, and the normal $x(t)-y$; this is where Proposition (3.2) enters, and it is why the Clarke cone, rather than a weaker cone, is needed.

The direction (1) $\Rightarrow$ (2) needs a trajectory through an arbitrary $y\in F$ whose initial velocity is a prescribed $v\in X(y)$. For a nonconvex multifunction this is Filippov's theorem [7, Theorem 5], which the paper cites and does not prove. A solver must prove it, or an equivalent existence result for Lipschitz inclusions with compact values, from scratch in Lean. The Clarke tangent cone and the more familiar Bouligand (contingent) cone differ pointwise at nonconvex corners, so a statement written with Mathlib's tangentConeAt is a different theorem from (4.4). That the two universal conditions "$X(x)\subseteq T_F(x)$ for all $x\in F$" are equivalent for Lipschitz $X$ is a later, separate result and cannot be assumed.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $d_E$ is Metric.infDist · E; "$e$ is a closest point to $x$" is e ∈ E ∧ dist x e = infDist x E.
• $\partial f$ and $f^\circ$ follow Definitions (1.1) and (1.3). The gradient limits carry DifferentiableAt, because Mathlib's gradient is $0$ off the differentiability set. $f^\circ$ is a real limsup, and every theorem using it carries the §1 Lipschitz hypothesis.
• $N_E$ and $T_E$ are defined from $\partial d_E$ as in (3.1) and (3.6). The tangent cone is not Mathlib's tangentConeAt.
• A trajectory is x : ℝ → ℝⁿ with AbsolutelyContinuousOnInterval x 0 1 and, for almost every $t\in[0,1]$, ∃ w ∈ X (x t), HasDerivAt x w t. Values outside $[0,1]$ are irrelevant.
• Standing assumptions made explicit: $X(x)$ nonempty and compact for every $x$ (§4, p. 259); $E$, $F$ nonempty and closed and $e\in E$ (§3, p. 254); $f$ Lipschitz on bounded sets (§1, p. 247). The Lipschitz constant of (4.2) is global.
• Ruled out: dropping absolute continuity (Cantor-type curves would leave $F$), using deriv in (4.1), using a punctured filter in (3.7), which would make (3.7)(2) hold at isolated points, and assuming Filippov's theorem as a hypothesis of (4.9) or of the goal.
• Needed infrastructure: the Clarke calculus for $d_E$, a chain-rule-type estimate for $d_F\circ x$ along absolutely continuous curves, a Gronwall lemma for absolutely continuous functions (Mathlib has norm_le_gronwallBound_of_norm_deriv_right_le for the differentiable case), and Filippov's existence theorem. The generalized gradient, cones and trajectory notions are reusable by any nonsmooth-optimization or control mission. Contributions of any of these as separate lemmas are welcome.
• The §1 definitions duplicate those of the companion mission Generalized Gradients and Applications I; the two missions were drafted at the same time.

Selected references

• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
• A. F. Filippov, Classical solutions of differential equations with multivalued right-hand side, SIAM J. Control 5 (1967), 609–621. https://doi.org/10.1137/0305040
• H. Brezis, On a characterization of flow-invariant sets, Comm. Pure Appl. Math. 23 (1970), 261–263. https://doi.org/10.1002/cpa.3160230211
• J. M. Bony, Principe du maximum, inégalité de Harnack et unicité du problème de Cauchy pour les opérateurs elliptiques dégénérés, Ann. Inst. Fourier 19 (1969), 277–304. https://doi.org/10.5802/aif.319
• R. M. Redheffer, The theorems of Bony and Brezis on flow-invariant sets, Amer. Math. Monthly 79 (1972), 740–747. MR 46 #2166.
• F. H. Clarke, Yu. S. Ledyaev, R. J. Stern, P. R. Wolenski, Nonsmooth Analysis and Control Theory, Graduate Texts in Mathematics 178, Springer, 1998. https://doi.org/10.1007/b97650

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$. This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

$$\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}$$

Fix $r > 0$. For a constraint value $a$ and a multiplier $y$ put

$$\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}$$

(the two cases agree when $y + ra = 0$). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

$$L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).$$

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$. $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$, the limit of $V h'$ over $V \in \partial F(x + t h')$, $h' \to h$, $t \downarrow 0$, exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$, and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$:

$$L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,$$ $$\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.$$

All three clauses are the theorem; the last two together cover every point.

Milestones

1. $\eta \in C^1$, with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$, and $\nabla \eta$ is locally Lipschitz.
2. Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
3. Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$, $\alpha_j \to \alpha$, $t_j \downarrow 0$, then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$.
4. $\nabla\eta$ is semismooth, jointly in $(x, s)$, at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$, the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$, with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$, for all approaches $(h', \alpha') \to (h, \alpha)$, $t \downarrow 0$, including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

• $\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
• The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
• The paper's first sum prints $h(r_i, f_i(x), y_i)$; the single $r$ is used, as in the paper's definition of $h$.
• $\phi$ uses the first branch when $y + ra \ge 0$; the branches agree on the boundary. Every statement assumes $r > 0$.
• $C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
• $\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
• The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$–$\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$.
• Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$, or only the semismoothness of one term $\eta$, is not Theorem 4.1; the goal contains all three clauses for the full $L_r$. The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of equations $F(x) = 0$ with $F : \mathbb{R}^n \to \mathbb{R}^n$ that is continuous and locally Lipschitz but not differentiable. Complementarity problems rewritten through the min or Fischer–Burmeister functions, Karush–Kuhn–Tucker systems of nonlinear programs, and the gradients of augmented Lagrangians all have this form. Newton's method $x^{k+1} = x^k - F'(x^k)^{-1}F(x^k)$ cannot be applied verbatim, because $F'(x^k)$ need not exist.

Qi and Sun (Math. Programming 58 (1993) 353–367) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and proved that the resulting method converges under a condition they called semismoothness, extending Mifflin's notion (SIAM J. Control Optim. 15 (1977)) from functionals to maps. The paper has two convergence results. Theorem 3.2 is local: near a semismooth root with nonsingular generalized Jacobian the method converges superlinearly. Theorem 3.3, the target of this mission, is global in the Newton–Kantorovich sense: explicit constants on a ball $S$ around the starting point guarantee that the iteration never leaves $S$, that $F$ has exactly one zero in $S$, and that the iterates converge to it with a computable error bound. The authors describe it as "an extension of the classical Newton-Kantorovich theorem" (p. 361), which is stated for smooth maps in Ortega and Rheinboldt's monograph.

Timeline.

• 1948: Kantorovich proves semilocal convergence of Newton's method for smooth operators in Banach spaces.
• 1975–1983: Clarke introduces the generalized gradient and generalized Jacobian of a locally Lipschitz map (Optimization and Nonsmooth Analysis, Wiley 1983).
• 1977: Mifflin defines semismooth functionals.
• 1990: Pang proves convergence of a B-derivative Newton method under a strong Fréchet derivative at the solution.
• 1993: Qi and Sun (this paper) prove local and global convergence of the generalized-Jacobian Newton method for semismooth maps.

Setting

Work in $\mathbb{R}^n$ with the Euclidean norm $\|\cdot\|$; for a linear map $V$, $\|V\|$ is the induced operator norm. Let $F : \mathbb{R}^n \to \mathbb{R}^n$ be locally Lipschitz. Write $D_F$ for the set of points where $F$ is differentiable and $JF(y)$ for the derivative at $y \in D_F$.

• The generalized Jacobian of $F$ at $x$ is

$$\partial F(x) = \mathrm{co}\Big\{\lim_{i\to\infty} JF(x_i) : x_i \to x,\ x_i \in D_F\Big\}.$$

• The directional derivative is $F'(x;h) = \lim_{t\downarrow 0}\,(F(x+th)-F(x))/t$.
• $F$ is semismooth at $x$ if it is Lipschitz near $x$ and, for every $h$, $V h'$ has a limit as $V \in \partial F(x+th')$, $h' \to h$, $t \downarrow 0$. Semismoothness implies that $F'(x;h)$ exists.
• A run of the nonsmooth Newton method (3.2) from $x^0$ is a pair of sequences $(x^k)$, $(V_k)$ with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1} - x^k) = -F(x^k)$ for all $k$; any element of $\partial F(x^k)$ may be chosen.

In Lean these are NonsmoothNewton.Global.clarkeJac, dirDeriv, SemismoothAt and IsNewtonRun, over EuclideanSpace ℝ (Fin n).

Fix $x^0$, $r \ge 0$, the closed ball $S = \{x : \|x - x^0\| \le r\}$, and constants $\beta, \gamma, \delta$ with $\alpha = \beta(\gamma+\delta)$.

Formalization targets

Goal: Theorem 3.3 (global convergence)

Assume $F$ is semismooth at every point of $S$ and, for all $x, y \in S$ and $V \in \partial F(x)$: $V$ is nonsingular,

$$\|V^{-1}\| \le \beta,\qquad \|V(y-x) - F'(x;y-x)\| \le \gamma\|y-x\|,\qquad \|F(y)-F(x)-F'(x;y-x)\| \le \delta\|y-x\|,$$

with $\alpha < 1$ and $\beta\|F(x^0)\| \le r(1-\alpha)$. Then every run of (3.2) from $x^0$ stays in $S$, every $V_k$ is nonsingular, $F$ has a unique zero $x^*$ in $S$, $x^k \to x^*$, and

$$\|x^k - x^*\| \le \frac{\alpha}{1-\alpha}\,\|x^k - x^{k-1}\|,\qquad k = 1, 2, \dots \tag{3.4}$$

Milestones (steps of the proof, p. 360)

1. The first step: $\|x^1 - x^0\| \le \beta\|F(x^0)\| \le r(1-\alpha)$, so $x^1 \in S$.
2. One-step contraction: for consecutive Newton points with $x^{k-1}, x^k \in S$, $\|x^{k+1} - x^k\| \le \alpha\|x^k - x^{k-1}\|$.
3. All iterates remain in $S$, with $\|x^{k+1} - x^k\| \le r\alpha^k(1-\alpha)$.
4. A run that stays in $S$ and converges has uniformly bounded $\|V_k\|$, and its limit is a zero of $F$.
5. $F$ has at most one zero in $S$.

Significance

The theorem certifies, from data checkable on a single ball, that a solution exists, where it is, that it is unique there, and how far the current iterate is from it; (3.4) is an a-posteriori stopping criterion. It holds for every choice of $V_k \in \partial F(x^k)$, which is what implementations need, since they compute one element of $\partial F$ and not the whole set. The result underlies the global and semilocal analysis of semismooth Newton methods for complementarity problems, variational inequalities and nonsmooth KKT systems, a line that continued through the 1990s and 2000s.

The theorem is proved on paper; no machine-checked version is known. The platform has no Newton–Kantorovich theorem, smooth or nonsmooth, and no Clarke generalized Jacobian. A complete formalization would supply both, and the definitions layer here (generalized Jacobian, one-sided directional derivative, semismoothness, Newton runs) is shared with the two companion missions on Qi and Sun's local convergence theorem and on semismoothness of augmented Lagrangian gradients.

Difficulty

The Newton map is set-valued: $x^{k+1}$ depends on the choice of $V_k$, so the Banach fixed-point theorem for a single contraction does not apply directly, and the argument must hold for every sequence of choices. The contraction estimate needs both consecutive steps to start inside $S$, so containment in $S$ and the geometric decay of the steps must be established together. Identifying the limit as a zero requires a uniform bound on $\|V_k\|$, which is not a hypothesis: it has to come from local Lipschitz continuity through the structure of the generalized Jacobian. Uniqueness uses an element $V^* \in \partial F(x^*)$, whose existence rests on Rademacher's theorem. Finally, the directional derivative in the hypotheses is only meaningful because semismoothness makes it exist.

Formalization scope

The space is EuclideanSpace ℝ (Fin n), so the norm is Euclidean, as in the paper (p. 356), and $\|V^{-1}\|$ is the operator norm. Local Lipschitzness is global (LocallyLipschitz F), the standing assumption of Section 3. Conventions:

• $\partial F(x)$ is the convex hull of limits of fderiv along sequences in $D_F$; no closure is taken (the limit set is compact for locally Lipschitz $F$).
• "$V$ nonsingular, $\|V^{-1}\| \le \beta$" is the existence of a two-sided inverse $W$ with $\|W\| \le \beta$; Ring.inverse is not used.
• $F'(x;h)$ is dirDeriv, a limUnder along $t \to 0^+$, used only at points of $S$, where semismoothness makes the limit exist.
• The run is a relation, not a function; every choice of $V_k$ is covered, and nonsingularity of each $V_k$ is a conclusion.
• The radius condition $r \ge 0$ is an explicit hypothesis. Without it, $r < 0$ and $\beta < 0$ would satisfy all other hypotheses vacuously while $x^0 \notin S$.
• The paper's third inequality sits under "for any $V \in \partial F(x)$"; it is stated without $V$, which is equivalent because $\partial F(x) \ne \emptyset$.
• (3.4) is stated at index $k+1$ for $k \ge 0$, avoiding natural-number subtraction.
• The paper's statements contain no $o(\cdot)$ or $O(\cdot)$; all constants are explicit and fixed before the quantifiers over points of $S$.

The goal is the full four-part conclusion: containment, existence, uniqueness, and convergence with (3.4). A formalization that proves only that the iterates converge to some zero, or that treats $\partial F(x)$ as possibly empty so that the hypotheses become vacuous, is not the theorem. The hypotheses are satisfiable by genuinely nonsmooth maps, e.g. $F(x) = x + \tfrac{1}{10}|x| - c$ on $\mathbb{R}$ with a ball containing the kink.

A complete development needs: nonemptiness and local boundedness of the generalized Jacobian (Rademacher's theorem, available in Mathlib as LipschitzWith.ae_differentiableAt); geometric-series and Cauchy-sequence arguments in a complete space. The generalized-Jacobian facts are reusable well beyond this mission. Contributions of any of the milestones, or of these general facts as separate lemmas, are welcome.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, New York, 1983. https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061
• J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970. https://doi.org/10.1137/1.9780898719468
• J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15 (1990) 311–341. https://doi.org/10.1287/moor.15.2.311

Motivation

The Riemann mapping theorem says that every simply connected region of the complex plane other than the plane itself can be mapped one-to-one and conformally onto the open unit disk. It is the central existence theorem of geometric function theory: it reduces questions about analytic functions on an arbitrary simply connected region to questions on the disk, and it shows that, up to conformal equivalence, there are only two simply connected regions in the plane — the plane and the disk.

In L. V. Ahlfors' textbook Complex Analysis (3rd ed., McGraw-Hill, 1979) the theorem is Theorem 1 of Chapter 6, §1.1 (p. 230). Its proof draws on much of the preceding theory: the general form of Cauchy's theorem (through the existence of logarithms and roots on simply connected regions, Ch. 4, §4.4), Schwarz's lemma (Ch. 4, §3.4), Hurwitz's theorem (Ch. 5, §1.1) and the theory of normal families (Ch. 5, §5). This mission is the first of a series formalizing capstone results of the book.

Timeline (as recorded by Ahlfors, p. 229–230). The theorem was formulated by B. Riemann (1851). A related theorem from which it can be derived was proved earlier by W. F. Osgood; the first successful proof of the mapping theorem itself is credited to P. Koebe. The proof in the book is a shorter variant of Koebe's original proof.

Setting

A region is a nonempty, open, connected subset $\Omega$ of the complex plane $\mathbb C$ (Ch. 3, §1.3, Definition 4). The extended plane is $\mathbb C \cup \{\infty\}$, the one-point compactification of $\mathbb C$. A region $\Omega$ is simply connected if its complement with respect to the extended plane, $(\mathbb C\cup\{\infty\})\setminus\Omega$, is connected (Ch. 4, §4.2, Definition 1). This is Ahlfors' definition; it is not the usual "every loop is contractible" definition, although the two agree for plane regions. The point $\infty$ always lies in the complement, so, for example, a disk, a half-plane and a parallel strip are simply connected, while the punctured plane and the exterior of a circle are not.

A function $f$ is analytic in $\Omega$ if it is complex-differentiable at every point of $\Omega$ (equivalently, it has a convergent power-series expansion around every point of $\Omega$). It is univalent in $\Omega$ if it is one-to-one there. We write $\mathbb D = \{w : |w| < 1\}$ for the open unit disk.

A family $\mathfrak F$ of functions on $\Omega$ is normal in $\Omega$ if every sequence of members of $\mathfrak F$ has a subsequence which converges uniformly on every compact subset of $\Omega$ (Ch. 5, §5.1, Definition 2); the limit need not belong to $\mathfrak F$.

Formalization targets

Goal — Riemann mapping theorem (Ch. 6, Theorem 1)

Let $\Omega$ be a simply connected region with $\Omega \ne \mathbb C$ and let $z_0 \in \Omega$. Then there is an analytic function $f$ in $\Omega$ with

$$f(z_0) = 0,\qquad f'(z_0) > 0,\qquad f \text{ one-to-one on } \Omega,\qquad f(\Omega) = \mathbb D,$$

and any two functions with these properties agree on $\Omega$.

Milestones (in the order used by the proof)

1. Ch. 4, §4.4, Corollary 2 of Theorem 15. On a simply connected region, a nowhere-vanishing analytic function has single-valued analytic branches of $\log f$ and of $\sqrt[n]{f}$.
2. Ch. 4, Theorem 13 (Schwarz's lemma). If $f$ is analytic in $\mathbb D$, $|f|\le 1$ and $f(0)=0$, then $|f(z)|\le|z|$ and $|f'(0)|\le 1$, with equality only for rotations.
3. Ch. 4, §3.4, Exercise 5 (disk case). A one-to-one analytic map of a disk onto a disk is a linear fractional transformation.
4. Ch. 5, Theorem 2 (Hurwitz). A locally uniform limit of nowhere-vanishing analytic functions on a region is either identically zero or never zero.
5. Ch. 5, Theorem 15 (Montel). A family of analytic functions is normal if and only if it is uniformly bounded on every compact set.

Significance

The mapping theorem is the entry point to the conformal-mapping part of complex analysis: the uniqueness statement identifies the conformal automorphisms of a simply connected region with those of the disk, and the existence statement is the base case of the uniformization theorem for Riemann surfaces. It also yields the purely topological fact that any simply connected plane region is homeomorphic to a disk.

The theorem is classical and fully proved in the literature. What this mission adds is a machine-checked proof in Lean 4 / Mathlib, together with machine-checked versions of the supporting results listed above in the book's own formulations. Mathlib already contains related material (for example, Cauchy integral formulas and a derivative bound of Schwarz type, Complex.norm_deriv_le_div_of_mapsTo_ball); it should be reused wherever it applies.

Difficulty

The obvious approach — write down the map — is not available: for a general region there is no formula, and the map is obtained from an extremal problem (maximize $|g'(z_0)|$ over univalent maps into the disk). Three steps are delicate: showing that the competing family is nonempty (this uses the existence of a square root on $\Omega$, i.e. the general Cauchy theorem, applied with Ahlfors' complement-connectedness definition); showing that an extremal function exists and is still univalent (this needs normal families and Hurwitz's theorem, neither of which is a direct consequence of pointwise convergence); and showing that the extremal function is onto (a second square-root construction combined with a Schwarz-lemma-type estimate). Uniqueness requires the classification of the automorphisms of the disk.

Formalization scope

All statements live in the namespace AhlforsComplexAnalysis, shared by the whole book series. Functions are total maps $\mathbb C \to \mathbb C$; "analytic in $\Omega$" is Mathlib's AnalyticOnNhd ℂ f Ω (analytic at every point of $\Omega$), and values of $f$ outside $\Omega$ are unconstrained. Consequently the uniqueness part of the goal is stated as agreement on $\Omega$ (Set.EqOn f g Ω), not as equality of functions. The condition $f'(z_0) > 0$ is written as $\operatorname{Re} f'(z_0) > 0$ and $\operatorname{Im} f'(z_0) = 0$, with $f'$ the complex derivative deriv f. The extended plane is Mathlib's OnePoint ℂ; "connected" is Mathlib's IsConnected (nonempty and preconnected). Uniform convergence on compact subsets is stated literally: for each compact $K \subseteq \Omega$, uniform convergence on $K$.

The hypothesis $\Omega \neq \mathbb C$ is essential and cannot be dropped: by Liouville's theorem no nonconstant bounded analytic function on $\mathbb C$ exists. The hypotheses are satisfiable (for example by $\Omega = \mathbb D$, $z_0 = 0$), so the goal is not vacuous.

Needed infrastructure beyond Mathlib likely includes: the equivalence of Ahlfors' simple connectivity with the vanishing of winding numbers (Ch. 4, Theorem 14) and the general Cauchy theorem on such regions; Montel's theorem in the form above; Hurwitz's theorem. These pieces are reusable well beyond this mission, and contributions of any of them — as well as proofs of the milestones — are welcome.

Selected references

• L. V. Ahlfors, Complex Analysis: An Introduction to the Theory of Analytic Functions of One Complex Variable, 3rd ed., McGraw-Hill, 1979. ISBN 0-07-000657-1.
• The Mathlib Community, Mathlib4 documentation. https://leanprover-community.github.io/mathlib4_docs/