Analysis

1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

• 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
• 1962 — Radó: the busy beaver function outgrows every computable function.
• 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
• 1978 — Apéry: $\zeta(3)$ is irrational.
• 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
• 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
• 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
• 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
• 2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
• 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
• 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let

$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$

The Bateman–Horn constant is the (conditionally convergent) Euler product

$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$.

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

• Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
• The Bateman–Horn constant is the limit of the ordered partial products over $p<N$, not an unordered infinite product.
• Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
• Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
• Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
• Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$.
• The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$.
• Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at.
• Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
• Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

---

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

Motivation

Differentiation replaces a polynomial's zeros by a smaller set of critical points. Repeating it produces a sequence of finite root sets, ending at one point. The derivative-zero-chain problem asks whether a single path can visit an actual zero in every set without accumulating a length that grows with the degree. The question concerns the geometry of polynomial differentiation, rather than numerical root finding: every point of the path must satisfy the appropriate polynomial equation.

Ingo Althöfer posed the uniform-length question and the specific bound four in his derivative-chain problem announcement. Earlier work on assignments between roots and critical points is described in Konrad Kaffka's 2012 thesis. The established geometry includes the Gauss–Lucas theorem and the stochastic and convex-order refinements proved by S. M. Malamud. These results provide reusable inputs; they do not by themselves establish a degree-independent chain-length bound.

Setting

A root list is a finite list $a_1,\ldots,a_n$ of complex numbers, with repeated entries recording multiplicity and with $n\ge1$. It determines the monic polynomial

$$p_a(X)=\prod_{j=1}^{n}(X-a_j).$$

For $1\le m\le n$, define its degree-$m$ row by $P_m=D^{n-m}p_a$, where $D$ is ordinary polynomial differentiation. A complete derivative-root chain chooses one complex number $z_m$ from every row, satisfying $P_m(z_m)=0$. Its cost is the Euclidean length

$$L(z)=\sum_{m=1}^{n-1}|z_{m+1}-z_m|.$$

The order runs from the degree-one row to the original polynomial. The first point is therefore the centroid of the original root slots. Reversing the path gives the same cost. All source roots are normalized to the closed unit disk. Degree one has a single point and zero cost; no derivative row is omitted.

Formalization targets

Goal: one constant for every degree

The mission's main goal is the weakest stable uniform assertion:

$$\exists C\ge0\;\forall n\ge1\;\forall a\in\mathbb C^n,\quad \bigl(\forall j,\ |a_j|\le1\bigr)\Longrightarrow \exists z,\quad P_m(z_m)=0\ (1\le m\le n),\quad L(z)\le C.$$

The same real constant must work for all degrees and all root lists. It cannot depend on the polynomial or its degree. This target remains unproved in this development.

Stronger target and restricted classes

The stronger unrestricted milestone is the four-bound, $L\le4$. The original announcement asks for total path length at most $C$ and specifically suggests $C=4$, so this is the corresponding stated target. Additional open milestones concern real-coefficient polynomials with at most two, three or four nonreal conjugate pairs, counting multiplicity. Their proposed bounds are respectively $3$, strictly less than $7/2$, and $4$. These are explicit statements to prove or refute, not accepted consequences of a scalar estimate. Their real-coefficient hypotheses must not be transferred to the unrestricted goal.

Significance and current status

A uniform bound would control one compatible path through every nonconstant derivative row, even as the number of rows grows. It would give information beyond the containment of critical points in the convex hull of their parents. The stronger bound four specifies a quantitative target within the same problem.

The initial accepted development contained 52 proved theorem records and three definition bundles: derivative-chain foundations, root probability, and the finite Hermite model. All three bundles are now listed directly in this proposal. The six additional proved library references retain their original contributors and are separate from those initial 52 accepted proofs. They include standard mathematics, supporting lemmas, conditional constructions, overlapping formulations and restricted class results. This count is not a claim of 52 original discoveries. In particular the square-root baseline is already stated in the organizer-hosted report, while the explicit barycentric root weights and multiplicity-aware Rolle counting are available in Mathlib.

The accepted class results include the length bound $2$ for real-coefficient unit-disk polynomials with at most one nonreal conjugate pair, and the bound $(D_Q+1)R$ for real-compressed polynomials $X^rQ(X^d)$, where $d\ge2$, $0\le r<d$, $Q$ is real, and $D_Q$ is its multiplicity-counted nonreal-root deficit. The compressed ray and pair-count bounds are corollaries within that family. The accepted cubic-cube theorem gives a complete chain for $q^3$, for any monic complex cubic $q$ whose roots lie in a radius-$R$ disk, with length at most $4\sqrt2R/3$, a common monotone orthonormal coordinate frame and a repeated source-root tail. These are restricted results, not solutions of the main goal.

Reusable public proof library

The proposal also references six existing public results: the real and multivariate martingale-coupling characterizations of convex order, the absolute-deviation and integrated-tail criteria, equality of means under multivariate convex order, and finite optimal-transport attainment and its triangle inequality. These are references to the original records, not duplicate submissions or claims of new proofs by this project. The five stochastic-order proofs are credited to Nickrobbins95 and the finite-transport proof to MKPynnic; theorem submitter and proof author can differ.

• The transportation metric is an attained metric.
• Theorem 3.A.2 — the absolute-deviation characterization of the convex order.
• Theorem 3.A.4 — Strassen's martingale-coupling characterization of the convex order (corrected: finite means, random variables).
• Theorem 3.A.1 — tail-integral characterizations of the convex order.
• Eq. (7.A.5) — the multivariate convex order forces equal means.
• Theorem 7.A.1 — martingale-coupling characterization of the multivariate convex order (corrected: finite means, random vectors).

These results are supporting inputs, not proofs of the derivative-chain goal. Applying the coupling results still requires a proved convex-order statement for the actual polynomial root laws, with the correct multiplicity weights and uniform marginals. Repeated root slots yield a pseudometric, so the finite metric theorem needs distinct locations with multiplicity weights. The default norm on a real coordinate function space is not automatically the complex Euclidean norm. Neither coupling existence nor separate short edges supplies a complete uniform-length chain without a further compatible selection argument.

Verified fourth and fifth powers of complex cubics

The fourth-power theorem and fifth-power theorem now have complete Lean proofs accepted by Prove2me. For every monic complex cubic whose roots lie in a disk of radius $R\ge0$, they construct compatible chains through all twelve or fifteen ordinary derivative rows, respectively, with length at most $4\sqrt2R/3$.

Both theorems retain the cubic centroid, one common monotone orthonormal coordinate frame and a final source-root suffix of four or five entries. Repeated roots, zero radius and degenerate centered coefficients are included. Neither statement assumes a supplied prefix or continuation theorem. The accepted cubic-cube result remains a separate restricted-class theorem; these three class results do not settle either unrestricted goal or arbitrary larger powers.

The fourth-power research source, fifth-power research source and their checkpoint archive preserve the original analytic work. The linked theorem records carry the accepted formal proofs and their proved dependency chains.

The public Lean proof archive contains 193 Lean files (182 proof modules and 11 dependencies), reproduction instructions and SHA-256 manifests. This is the complete local-proof snapshot prepared before the final server submission packaging; the accepted submissions and their dependency chains on Prove2me are the authoritative server-verified artifacts. The archive README and formal-proof metadata record the accepted status of both theorems. The original research files are preserved unchanged; their earlier Open notices describe the historical research snapshot.

Difficulty

Convex containment does not control the sum of successive movements. Choosing a short edge separately at each row also need not produce a compatible path: the endpoint of one choice must be the start of the next. The known general square-root bound grows with degree, so it does not answer the uniform question. A variance bound controls squared increments and cannot simply be read as a constant bound on their unsquared sum.

Repeated roots and collisions are genuine cases, not numerical exceptions. The accepted Hermite obstruction rules out a particular local variance-increment estimate; it does not refute the unrestricted chain-length questions. Likewise, accepted scalar and conditional lemmas establish only their displayed conclusions under their stated hypotheses. A proposed polynomial application must prove those hypotheses for the same actual chain.

Formalization scope

The Lean model uses Fin n → ℂ root slots, fromRoots for the product polynomial, row a m for the ordinary derivative row, IsChain for actual root membership and chainCost for the finite sum of complex norms. Positive degree, all nonconstant rows, source normalization and multiplicity counting are explicit. No root simplicity assumption or supplied short chain is permitted in the unrestricted goal. Real-coefficient and compressed-form restrictions belong only to their named class theorems.

The accepted proofs use Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Existing declarations retain their identifiers and attribution. Generic convex-order and martingale-coupling results are reusable, but a citation to them does not prove the polynomial-specific uniform-root marginal property. Contributions are welcome on exact root-law adapters, compatible selection estimates and the listed open targets. Novelty and faithfulness to the stated problem should be assessed separately from successful Lean verification.

Selected references

• Ingo Althöfer, Math with AI — Diary, derivative-chain problem announcement, 15 August 2026. Announcement.

• A $\sqrt{n-1}$ Bound for Chains of Zeros of Successive Derivatives, organizer-hosted report. Report.

• Konrad Kaffka, Zuordnungen zwischen Nullstellen und kritischen Punkten von Polynomen, Diplomarbeit, Friedrich-Schiller-Universität Jena, 2012. Thesis.

• S. M. Malamud, Inverse spectral problem for normal matrices and a generalization of the Gauss–Lucas theorem, Transactions of the American Mathematical Society 357 (2005), 4043–4064. Preprint.

• Rajesh Pereira, Differentiators and the geometry of polynomials, Journal of Mathematical Analysis and Applications 285 (2003), 336–348. Article.

• Thorsten Theobald and Timo de Wolff, Norms of Roots of Trinomials, 2015 preprint version. Trinomial geometry.

• Public formalization reference package: 60 numbered records, including the three definitions, five open targets and 52 accepted proof sources. Statements, proofs and source conventions.

Motivation

The iteration of a rational map $f:\hat{\mathbb C}\to\hat{\mathbb C}$ of the Riemann sphere is the model problem of holomorphic dynamics. The subject was founded by Fatou and Julia around 1918–1920, who split the sphere into a region of stable behaviour and a region of chaotic behaviour, and it was revived in the 1980s by Douady, Hubbard, Sullivan and Thurston. John Milnor's textbook Dynamics in One Complex Variable (3rd ed., Princeton, 2006) is the standard graduate introduction. This mission, the first of a series on the book, formalizes the chain of results that leads from Montel's theorem on normal families to Sullivan's theorem that rational maps have no wandering domains.

Timeline of the results formalized here:

• 1912–1927, Montel. Families of holomorphic maps omitting three values are normal (Milnor, Theorem 3.7).
• 1918–1920, Fatou and Julia. Definition of the Fatou and Julia sets; the Julia set of a map of degree $d\ge2$ is nonempty and equals the closure of the repelling periodic points (Milnor, Lemma 4.8 and Theorem 14.1).
• 1920s–1942. Fatou classified the possible dynamics on an invariant Fatou component; Siegel (1942) showed that Siegel disks exist, and Herman (1979) constructed Herman rings. Together these give the four cases of Milnor's Theorem 16.1.
• 1985, Sullivan. Every Fatou component is eventually periodic (Sullivan, Quasiconformal homeomorphisms and dynamics I, Ann. of Math. 122 (1985); Milnor, Theorem 16.4).

Setting

The Riemann sphere is $\hat{\mathbb C}=\mathbb C\cup\{\infty\}$, the one-point compactification of $\mathbb C$, with the two coordinates $z$ (near finite points) and $1/z$ (near $\infty$). A rational map is $f=p/q$ with $p,q$ coprime complex polynomials, $q\neq0$; it acts on $\hat{\mathbb C}$ in the usual way, and its degree is $d=\max(\deg p,\deg q)$. Write $f^{\circ n}$ for the $n$-th iterate.

A family of maps from an open set to $\hat{\mathbb C}$ is normal if every sequence in it has a subsequence converging locally uniformly in the spherical (chordal) metric. The Fatou set $F(f)$ is the set of points having a neighbourhood on which the iterates $\{f^{\circ n}\}$ form a normal family; the Julia set is its complement $J(f)=\hat{\mathbb C}\setminus F(f)$. A Fatou component is a connected component of $F(f)$. A periodic point $z_0=f^{\circ m}(z_0)$ of minimal period $m$ has multiplier $\lambda=(f^{\circ m})'(z_0)$, computed in a local coordinate; it is repelling if $|\lambda|>1$ and attracting if $|\lambda|<1$.

A Fatou component $U$ with $f(U)=U$ is a Siegel disk (resp. Herman ring) if $f|_U$ is conformally conjugate to an irrational rotation of the unit disk (resp. of a round annulus $\{1<|w|<r\}$).

Formalization targets

Goal: no wandering domains (Theorem 16.4)

For a rational map $f$ of degree $d\ge2$ and every Fatou component $U$ there are $n\ge0$, $p\ge1$ with

$$f^{\circ p}\bigl(f^{\circ n}(U)\bigr)=f^{\circ n}(U).$$

Milestones

1. Lemma 2.5: $\hat{\mathbb C}\setminus\{0,1,\infty\}$ is covered holomorphically by the unit disk.
2. Corollary 3.3 (case $\mathbb D\to\mathbb C\setminus\{0,1\}$): holomorphic maps between hyperbolic surfaces form a normal family.
3. Lemma 3.5 (case $\mathbb C\setminus\{0,1\}\subset\hat{\mathbb C}$).
4. Theorem 3.7 (Montel): holomorphic maps from a domain to $\hat{\mathbb C}$ omitting three values form a normal family.
5. Lemma 4.3: $z\in J(f)\iff f(z)\in J(f)$.
6. Lemma 4.4: $J(f^{\circ k})=J(f)$ for $k>0$.
7. Lemma 4.8: $J(f)\neq\emptyset$ when $d\ge2$.
8. Theorem 14.1: $J(f)=\overline{\{\text{repelling periodic points}\}}$ when $d\ge2$.
9. Theorem 16.1: an invariant Fatou component is an attracting basin, a parabolic basin, a Siegel disk or a Herman ring.

Significance

The results. Montel's theorem is the engine of the Fatou–Julia theory: nonemptiness of $J$, density of iterated preimages and density of repelling cycles all rest on it. Theorem 14.1 identifies the non-normality locus with the closure of the repelling cycles, the form in which the Julia set is usually computed and pictured. Sullivan's theorem, combined with Theorem 16.1, gives a complete qualitative picture of the dynamics on the Fatou set; it is used throughout the later theory, e.g. to show that the Julia set of a postcritically finite map without superattracting cycles is the whole sphere (Milnor, Corollary 16.5).

Formalizing them. All results here are classical theorems with published proofs; none is open. A text search of Mathlib at the platform's pinned revision (0df444a) finds no Montel theorem for families of holomorphic maps, no Fatou or Julia sets and no wandering-domain results; it does contain the Schwarz lemma and the hyperbolic metric on the upper half-plane. The remaining work is to formalize the known proofs.

Difficulty

The early milestones need the uniformization-type input that $\mathbb C\setminus\{0,1\}$ is covered by the disk (via the modular function or an equivalent construction) and Schwarz–Pick-type estimates on hyperbolic surfaces; Mathlib has the Schwarz lemma and the hyperbolic metric of the upper half-plane, but not the Poincaré metric of general hyperbolic domains or covering-space uniformization. Theorem 14.1 requires a quantitative use of Montel's theorem around points of $J$ that are not critical values. Theorem 16.1 needs the Denjoy–Wolff-type classification of self-maps of hyperbolic surfaces and the Snail Lemma for parabolic points. The goal is substantially harder: Sullivan's proof uses the measurable Riemann mapping theorem (Morrey–Ahlfors–Bers) to build an infinite-dimensional family of quasiconformal deformations of $f$, contradicting the finite dimensionality of the space of rational maps of degree $d$. The theory of quasiconformal maps and Beltrami equations is absent from Mathlib, and no elementary argument avoiding it is known.

Formalization scope

All declarations live in the book-wide namespace MilnorDynamics and build on the published definition files MilnorDynamics_NormalFamilies, MilnorDynamics_RationalMaps and MilnorDynamics_PeriodicPoints; one new definition file, MilnorDynamics_FatouComponents, adds Fatou components, immediate basins, Siegel disks and Herman rings.

• $\hat{\mathbb C}$ is OnePoint ℂ; a rational map is a structure of coprime polynomials $p,q$ with $q\ne0$, acting on OnePoint ℂ via RationalMap.toFun; the degree is $\max(\deg p,\deg q)$.
• Holomorphy of a map into $\hat{\mathbb C}$ on an open $U\subseteq\mathbb C$ is continuity plus complex differentiability in the charts $z$ and $1/z$ (IsHolomorphicOn). Normality is locally uniform subconvergence in the chordal metric (IsNormalFamily); the Fatou set is defined through the standard charts of $\hat{\mathbb C}$.
• Multipliers are derivatives of $f^{\circ m}$ in the standard chart at the periodic point, $m$ the minimal period.
• Montel's theorem is stated for a domain $U\subseteq\mathbb C$ rather than an arbitrary Riemann surface (normality is local, Milnor Problem 3-e); Lemma 2.5, Corollary 3.3 and Lemma 3.5 are linked in the special cases used for Montel's theorem.
• The degree hypotheses are Milnor's: $d\ge1$ (nonconstant) in §4 Lemmas 4.3–4.4, $d\ge2$ elsewhere. Without $d\ge2$ several statements are false (e.g. $J(z\mapsto 2z)=\emptyset$), so the hypothesis must not be dropped.

Welcome contributions: the Poincaré metric and Schwarz–Pick on hyperbolic domains, the modular covering of $\mathbb C\setminus\{0,1\}$, the degree theory of rational maps, quasiconformal maps and the measurable Riemann mapping theorem. These are reusable far beyond this mission.

Selected references

• J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. https://doi.org/10.1515/9781400835539
• D. Sullivan, Quasiconformal homeomorphisms and dynamics I. Solution of the Fatou–Julia problem on wandering domains, Ann. of Math. 122 (1985), 401–418. https://doi.org/10.2307/1971308
• L. Carleson and T. W. Gamelin, Complex Dynamics, Universitext, Springer, 1993. https://doi.org/10.1007/978-1-4612-4364-9
• P. Montel, Leçons sur les familles normales de fonctions analytiques et leurs applications, Gauthier-Villars, Paris, 1927.

What the constant is

Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm:

$$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$

It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.

What is being asked

For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, neither is known. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.

The goal theorem of this mission is transcendence,

$$\gamma \notin \overline{\mathbb{Q}},$$

with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.

What is actually known

Progress has come in three forms, and the milestones below formalize each.

Conditional bounds on a putative denominator. If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go.

Disjunctive results. The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant

$$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$

Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of $\gamma$ and $\delta$ is irrational. Rivoal later strengthened this to at least one of them is transcendental. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.

Irrationality criteria. Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.

Timeline

• 1734 — Euler introduces the constant and computes it to six decimals.
• 1790s–1800s — Mascheroni computes further digits; the constant acquires its second name.
• 1873 — Hermite proves $e$ transcendental; 1882 — Lindemann does the same for $\pi$. The methods do not reach $\gamma$.
• 1980 — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$.
• 1997 — Papanikolaou: the same denominator exceeds $10^{244663}$.
• 2009 — Aptekarev: at least one of $\gamma$, $\delta$ is irrational.
• 2012 — Rivoal: at least one of $\gamma$, $\delta$ is transcendental.
• 2010s — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched.

Formalization notes

Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $q$ units before a random demand $D$ is observed, pays $b>0$ per unit of unmet demand and $h>0$ per unit left over, and minimizes the expected cost $C(q)=E[b(D-q)^+ + h(q-D)^+]$. When the distribution of $D$ is known, the optimal order is the $b/(b+h)$ quantile of $D$. In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the $b/(b+h)$ quantile of the empirical distribution.

R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is $\epsilon$-optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in $\epsilon$, the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by $\min(b,h)/(b+h)$. That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.

This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.

Setting

Fix costs $b>0$, $h>0$ and the critical ratio $\beta=b/(b+h)\in(0,1)$. A demand law is given by a probability density $f:\mathbb R\to\mathbb R$: measurable, nonnegative, with $\int f=1$. Its cdf is $F(t)=\int_{(-\infty,t]}f$, and its $\beta$ quantile is

$$q^*=\inf\{q : F(q)\ge \beta\}.$$

The absolute mean spread (AMS, Definition 1) at $t$ is the gap between the conditional means above and below $t$,

$$\Delta(t)=E(D\mid D\ge t)-E(D\mid D\le t)=\frac{\int_{[t,\infty)}x f(x)\,dx}{1-F(t)}-\frac{\int_{(-\infty,t]}x f(x)\,dx}{F(t)},$$

and the weighted mean spread (WMS, Definition 2) is $\Delta(q^*)f(q^*)$.

A density is log-concave (Definition 3) if $\log f$ is concave on its support. Equivalently, $f(x)^a f(y)^{1-a}\le f(ax+(1-a)y)$ for all $x,y$ and $a\in[0,1]$; this form allows $f$ to vanish outside an interval.

For a log-concave $f$ and a point $t$ with $f(t)>0$, the number $\gamma_1$ is a supergradient of $\log f$ at $t$, written $\gamma_1\in\partial\log f(t)$, if $\log f(x)\le\log f(t)+\gamma_1(x-t)$ for all $x$ with $f(x)>0$. The paper splits the class $\mathbb L$ of log-concave densities into the subclasses $\mathbb L_{q^*,\gamma_0,\gamma_1}$ of densities with quantile $q^*$, $f(q^*)=\gamma_0$ and $\gamma_1\in\partial\log f(q^*)$, and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density

$$\tilde f(x)=\gamma_0e^{\gamma_1(x-q^*)}\ \text{ on }[\underline x,\overline x],\qquad \underline x=q^*+\tfrac1{\gamma_1}\log\!\big(1-\tfrac{\gamma_1}{\gamma_0}\beta\big),\quad \overline x=q^*+\tfrac1{\gamma_1}\log\!\big(1+\tfrac{\gamma_1}{\gamma_0}(1-\beta)\big),$$

and zero elsewhere (display (12)), with AMS $z^*_{q^*,\gamma_0,\gamma_1}$ in closed form.

The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.

Formalization targets

Goal: Proposition 2

For every log-concave density $f$,

$$\Delta(q^*)\,f(q^*)\ \ge\ \frac{\min(b,h)}{b+h}.$$

The statement has no further hypothesis: no moment condition, no continuity, no restriction on $\gamma_0,\gamma_1$.

Milestones, in the order of the paper's proof

1. Lemma 1: at the quantile, $-\frac{b+h}{h}\le\frac{\gamma_1}{\gamma_0}\le\frac{b+h}{b}$.
2. Lemma 2: $f(x)\le\gamma_0e^{\gamma_1(x-t)}$ for every $x$.
3. Lemma 3 (Domination Lemma): a density dominated on the support of another, with the same mass left of $t$, has the larger AMS at $t$.
4. Proposition 1: $\tilde f$ belongs to $\mathbb L_{q,\gamma_0,\gamma_1}$ and minimizes the AMS there.
5. The closed form: $\Delta_{\tilde f}(q)=z^*_{q,\gamma_0,\gamma_1}=\frac{\gamma_0}{\gamma_1^2}\big[(\frac{b+h}{h}+\frac{\gamma_1}{\gamma_0})\log(1+\frac{\gamma_1}{\gamma_0}\frac{h}{b+h})+(\frac{b+h}{b}-\frac{\gamma_1}{\gamma_0})\log(1-\frac{\gamma_1}{\gamma_0}\frac{b}{b+h})\big]$.
6. Lemma 4: three elementary inequalities in $\beta\in(0,1)$ and $\eta\in(-\frac1{1-\beta},\frac1\beta)$.

Significance

The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is $\epsilon$-optimal is, asymptotically, at least $1-2\exp(-\frac14N\epsilon\,\Delta(q^*)f(q^*))$ (Theorem 3), and Proposition 2 replaces the unknown $\Delta(q^*)f(q^*)$ by $\min(b,h)/(b+h)$. A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.

The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.

Difficulty

The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of $\log f$ at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of $t$ is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around $t$, which is how Proposition 1 uses it. The case $\gamma_1=0$ (uniform minimizer) and the two boundary values of $\gamma_1/\gamma_0$ (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate $f/(1-F)$ and the reversed hazard rate $f/F$ of log-concave laws, which must be proved from log-concavity.

Formalization scope

Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of $D$ is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat $\log f$ as $0$ off the support. The quantile is an sInf; for $\beta\in(0,1)$ its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of $xf(x)$, since log-concave densities have exponential tails. The value $f(q^*)$ is taken pointwise; $q^*$ lies in the interior of the support, where a log-concave density is continuous.

Conventions and disclosed departures from the page:

• "$\gamma_1\in\partial\log f$, the set of all subgradients" is read as the superdifferential of the concave $\log f$ on $\{f>0\}$.
• Lemma 3 carries three added hypotheses: $f_2$ vanishes outside some $[l,u]\ni t$ and is positive on $(l,u)$; $0<F_1(t)<1$; and $xf_1(x)$, $xf_2(x)$ are integrable. The first repairs the printed statement; the other two are the conditions under which Definition 1 makes sense for general densities.
• Proposition 1 and the closed form of $z^*$ are stated for $\gamma_1\neq0$ and $\gamma_1/\gamma_0$ strictly inside the interval of Lemma 1, where (12) is a finite interval.
• The goal has no such restriction.

Assumption 1 of the paper (monotonicity of $f$ beyond $q^*$) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which $f(q^*)$ or $\Delta(q^*)$ takes a junk value (a non-integrable $xf(x)$, a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.

Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on $\mathbb R$ (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).

Selected references

• R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. Authors' accepted manuscript, MIT DSpace. https://doi.org/10.1287/opre.2015.1422
• R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4):821–839, 2007. https://doi.org/10.1287/moor.1070.0272

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum possible total cost. It quantifies how much selfish routing loses compared with central coordination, and it has been studied intensively since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), mostly through worst-case bounds over classes of cost functions.

Worst-case bounds say nothing about how the PoA of one particular network behaves when its data change. In transport applications both the cost functions (capacities, tolls, travel-time models) and the demands are estimated, so the PoA is only useful if small errors in the data cause small errors in the PoA. Wu and Möhring (arXiv:2007.13979, published in Mathematics of Operations Research, 2023) study this sensitivity question in a setting where cost functions and demands change simultaneously. Earlier sensitivity results changed only the demands, with the cost functions fixed: Englert, Franke and Olbrich (2010) bounded the growth of the PoA of a single-O/D network with polynomial costs of degree at most $\beta$ by a factor $(1+\epsilon)^\beta$ when the demand grows by a factor $1+\epsilon$; Takalloo and Kwon (2020) extended this to several O/D pairs whose demands are scaled together; and Cominetti, Dose and Scarsini (arXiv:1907.10101) studied differentiability of the PoA as a function of the demand of a single O/D pair. The main theorem of the paper, Theorem 9, is the subject of this mission.

Setting

A network consists of a finite set $A$ of arcs, a finite non-empty set $\mathcal K$ of origin–destination (O/D) pairs, and for every $k \in \mathcal K$ a non-empty set $\mathcal S_k$ of paths; each path is a non-empty set of arcs. From §3.1 onward the paper also assumes every arc lies on some path and every $\mathcal S_k$ has at least two paths (Condition 1).

A game $\Gamma = (\tau, d)$ on the network consists of cost functions $\tau_a : [0,\infty) \to [0,\infty)$, one per arc, that are continuous and non-decreasing, and demands $d_k \ge 0$, one per O/D pair. The total demand is $T(d) = \sum_k d_k$. The game space $\mathcal G(G,\mathcal K,\mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for all $x \in (0, T(d)]$.

A flow $f = (f_s)$ assigns a non-negative amount to every path, with $\sum_{s\in\mathcal S_k} f_s = d_k$. Its arc flows are $f_a = \sum_{s \ni a} f_s$, its path costs $\tau_s(f) = \sum_{a\in s}\tau_a(f_a)$, and its total cost

$$C(\Gamma, f) = \sum_{a\in A} f_a\,\tau_a(f_a).$$

A Wardrop equilibrium (WE) is a flow in which every used path of a pair is a cheapest path of that pair. The SO cost $\mathcal C^*(\Gamma)$ is the minimum total cost over all flows, the WE cost $\tilde{\mathcal C}(\Gamma)$ is the total cost of a WE flow (all WE flows have the same cost), and

$$\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)}.$$

Games are compared by the distance

$$\|\Gamma - \Gamma'\| = \max\Big\{\|d-d'\|_\infty,\ \max_{a\in A}\max_{x\in[0,\min\{T(d),T(d')\}]}|\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}$$

for $\Gamma = (\tau, d)$ and $\Gamma' = (\sigma, d')$. It compares cost functions only on the range of flow values both games can produce, plus the values at the respective total demands. A function $h$ is Lipschitz continuous on $[0,T]$ with constant $M$ if $|h(x) - h(y)| \le M|x-y|$ for all $x, y \in [0,T]$.

Formalization targets

Goal: Theorem 9 (p. 26)

Let $\Gamma = (\tau, d)$ be a game of the game space whose cost functions are Lipschitz continuous on $[0, T(d)]$. Then there are $\epsilon_\Gamma > 0$ and $\kappa_\Gamma > 0$, depending only on $\Gamma$, such that

$$|\rho(\Gamma) - \rho(\Gamma')| \le \kappa_\Gamma\,\|\Gamma - \Gamma'\|^{1/2}\quad\text{for every game } \Gamma' \text{ of the game space with } \|\Gamma - \Gamma'\| < \epsilon_\Gamma.$$

The goal fixes the exponent $1/2$ and leaves the radius and the constant existential, which is the form the paper claims.

Milestones

1. Lemma 1a)–c) (p. 13): properties of $\epsilon$-approximate WE flows, ending with

$$|C(\Gamma, f) - C(\Gamma, \tilde f)| \le |A|\sqrt{M\epsilon}\,T(d) + \epsilon$$

for an $\epsilon$-approximate WE flow $f$ and a WE flow $\tilde f$ when all costs are $M$-Lipschitz on $[0,T(d)]$. 2. Lemma 10a)–d) (p. 27): on a demand slice (games with a common demand vector $w$), $\mathcal C^*$ is Lipschitz, WE flows of one game are $|A|\,T(w)\,\|\Gamma_1-\Gamma_2\|$-approximate WE flows of the other, and $\tilde{\mathcal C}$ and $\rho$ are Hölder with exponent $1/2$ with explicit constants. 3. Lemma 11a)–c) (p. 31): on a cost slice (games with a common cost vector and $T(w') \le T(w)$), explicit Hölder bounds of exponent $1/2$ for $\tilde{\mathcal C}$ and $\rho$ and a Lipschitz bound for $\mathcal C^*$.

Significance

Theorem 9 is the first pointwise Hölder continuity result for the PoA on the whole game space, with demands and costs perturbed together. Its hypothesis is mild (Lipschitz costs on a compact interval, which covers polynomial, BPR-type and piecewise linear costs), and such games are dense in the game space. Together with Theorem 8 of the same paper, which shows that no uniform Hölder bound exists, it describes exactly what kind of stability the PoA has: local, with a constant depending on the game, and exponent $1/2$ in general. The explicit constants of Lemmas 10 and 11 give computable error bounds for the PoA of a network whose data are known only approximately.

The result is proved in the paper; no machine-checked proof exists. This mission formalizes the statement and the explicit slice estimates the proof rests on. Lemma 1 is a self-contained statement about approximate Wardrop equilibria that is useful well beyond this paper, for instance for analysing iterative traffic-assignment algorithms, which only ever produce approximate equilibria.

Difficulty

The obvious approach compares an equilibrium of $\Gamma$ with an equilibrium of $\Gamma'$ directly. This fails because the two games have different demand vectors, so their flows live in different polytopes: an equilibrium of one game is not even a flow of the other. The paper separates the perturbation into a change of costs at fixed demand and a change of demand at fixed costs, through an auxiliary game, and each half needs its own argument. On a demand slice an equilibrium of one game is only an approximate equilibrium of the other, and the passage from an approximate equilibrium to its cost loses a square root (Lemma 1c), which is tight by Example 2). On a cost slice the demand has to be removed path by path from an equilibrium while keeping it an equilibrium of a shifted game. Finally, the constants of the slice estimates depend on the auxiliary game, and they must be controlled uniformly near $\Gamma$.

Formalization scope

The Lean development fixes the following conventions.

• The network is a structure with $|A|$ arcs, $|\mathcal S|$ paths and $|\mathcal K|$ O/D pairs, a 0/1 arc–path incidence matrix and the map sending a path to its pair. Lemma 1 uses the §2 model assumptions: 0/1 incidence, non-empty paths, $\mathcal K \neq \emptyset$, and $|\mathcal S_k| \ge 1$. The later results add Condition 1 (every arc on a path, $|\mathcal S_k| \ge 2$), as assumed from §3.1. Paths are arbitrary non-empty 0/1 columns, not necessarily loop-free paths of a digraph; the results do not use loop-freeness.
• Cost functions are maps $\mathbb R \to \mathbb R$ required to be continuous, non-decreasing and non-negative on $[0,\infty)$ only.
• Arc flows, Wardrop equilibria (2.1) and the potential (2.6) come from the published definition KellyStochasticNetworks_Wardrop. $\epsilon$-approximate WE flows follow (2.7) in arc form. The total cost uses the arc form, which equals the path form for 0/1 incidence.
• $\mathcal C^*$ is the infimum of costs over flows, $\tilde{\mathcal C}$ the supremum of costs over WE flows, $\rho$ their quotient. The middle term of the distance is the supremum of the image of the compact set $A\times[0,\min\{T(d),T(d')\}]$, and $\|\cdot\|_\infty$ is the sup norm.
• Every statement about $\rho$, $\mathcal C^*$ or $\tilde{\mathcal C}$ quantifies over games of the game space, where $\rho$ is a genuine ratio of positive numbers. Off the game space Lean's division by zero would give $\rho = 0$, so quantifying over all pairs $(\tau, d)$ would trivialize the statements; this is ruled out. In the goal, $\epsilon_\Gamma$ and $\kappa_\Gamma$ are chosen before $\Gamma'$.
• Several printed strict inequalities are posed as non-strict, because they fail at $\Gamma' = \Gamma$ or are attained in the paper's own Example 2. In Lemma 11 the printed constants are corrected by a factor $|\mathcal K|$ that the paper's own argument needs; each item's Formalization Note quotes the printed form.

A complete development needs: existence of Wardrop equilibria and uniqueness of their cost on the game space, existence of social optima, the integral inequality (2.9) for monotone costs, positivity of $\mathcal C^*$ on the game space, and the path-by-path demand-reduction construction of Lemma 11. The existence and uniqueness results and Lemma 1 are reusable in any formalization of selfish routing. Proofs of any milestone are welcome, as are the supporting lemmas above.

The source is the arXiv preprint arXiv:2007.13979v3 (23 Aug 2021); all page and theorem numbers refer to it, not to the published version.

Selected references

• Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in non-atomic congestion games, arXiv:2007.13979v3, 2021; Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979, https://doi.org/10.1287/moor.2022.1292
• T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
• E. Koutsoupias, C. Papadimitriou, Worst-case equilibria, STACS 1999. https://doi.org/10.1007/3-540-49116-3_38
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3), 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. Englert, T. Franke, L. Olbrich, Sensitivity of Wardrop equilibria, Theory of Computing Systems 47(1):3–14, 2010.
• M. Takalloo, C. Kwon, Sensitivity of Wardrop equilibria: revisited, Optimization Letters 14(3):781–796, 2020.
• R. Cominetti, V. Dose, M. Scarsini, The price of anarchy in routing games as a function of the demand, 2020. https://arxiv.org/abs/1907.10101

Motivation

Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.

Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.

Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.

Setting

All matrices are $d\times d$ with complex entries, $d\ge 1$. A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. $A$, $\lambda_{\max}(A)$ is its largest eigenvalue and $\|A\|$ its spectral norm. Functions of s.a. matrices are defined spectrally: if $A=Q\Lambda Q^*$ then $e^{A}=Qe^{\Lambda}Q^*$, and $\log$ is defined the same way on positive-definite matrices. $A\preceq B$ is the semidefinite order: $B-A$ is positive semidefinite.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $\mathcal F_0\subset\mathcal F_1\subset\cdots\subset\mathcal F$, and write $\mathbb E_k[\,\cdot\,]=\mathbb E[\,\cdot\mid\mathcal F_k]$. The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence $X_1,\dots,X_n$ of random matrices is adapted when each $X_k$ is $\mathcal F_k$-measurable. A matrix martingale is an adapted sequence of s.a. matrices $Y_k$ with $\mathbb E\|Y_k\|<\infty$ and $\mathbb E_{k-1}Y_k=Y_{k-1}$; its difference sequence $X_k=Y_k-Y_{k-1}$ satisfies $\mathbb E_{k-1}X_k=0$.

The hypotheses of the main theorem are: $X_1,\dots,X_n$ is an adapted sequence of random s.a. matrices, and $A_1,\dots,A_n$ is a fixed (non-random) sequence of s.a. matrices, with

$$\mathbb E_{k-1}X_k = 0 \qquad\text{and}\qquad X_k^2\preceq A_k^2\ \text{ almost surely.}$$

The variance parameter is $\sigma^2 := \big\|\sum_k A_k^2\big\|$.

Formalization targets

Goal: Theorem 7.1 (Matrix Azuma), p. 27

For all $t\ge 0$,

$$\mathbb P\Big\{\lambda_{\max}\Big(\sum_{k}X_k\Big)\ge t\Big\}\le d\cdot e^{-t^2/8\sigma^2}.$$

Milestones

In the order they are used:

1. Display (2.6), Golden–Thompson: $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ for s.a. $A,H$.
2. Proposition 3.1, the Laplace transform method: $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}$.
3. Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E e^{X})$.
4. Lemma 4.3, Rademacher half: $\mathbb E e^{\varepsilon\theta A}\preceq e^{\theta^2A^2/2}$.
5. Lemma 7.6 (Symmetrization): $\mathbb E\operatorname{tr}e^{H+X}\le\mathbb E\operatorname{tr}e^{H+2\varepsilon X}$ when $\mathbb EX=0$ and $\varepsilon$ is an independent Rademacher variable.
6. Lemma 7.7 (Azuma cgf): $\log\mathbb E[e^{2\varepsilon\theta X}\mid X]\preceq2\theta^2A^2$ when $X^2\preceq A^2$.
7. Display (7.5): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(2\theta^2\sum_kA_k^2)$ under the hypotheses of the goal.

Further statements

Corollary 7.2 is the martingale form, $\mathbb P\{\lambda_{\max}(Y_n-\mathbb EY_n)\ge t\}\le d\,e^{-t^2/8\sigma^2}$. Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, $\mathbb P\{\lambda_{\max}(H(z)-\mathbb EH(z))\ge t\}\le d\,e^{-t^2/8\sigma^2}$ for a matrix-valued function $H$ of independent variables whose changes in one coordinate $k$ have squares bounded by $A_k^2$.

Significance

The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor $d$, and a variance parameter equal to the norm of the sum $\sum_kA_k^2$ rather than the sum of the norms $\sum_k\|A_k\|^2$. In the commuting case the two coincide; in general the first can be smaller by a factor of up to $n$. The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).

Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.

Difficulty

The scalar proof of Azuma's inequality multiplies conditional moment generating functions, $\mathbb E e^{\theta\sum X_k}=\mathbb E\big[e^{\theta\sum_{k<n}X_k}\,\mathbb E_{n-1}e^{\theta X_n}\big]$, and bounds each factor. For matrices this fails: $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, and $\operatorname{tr}e^{A+B+C}\le\operatorname{tr}(e^Ae^Be^C)$ is false, so the Golden–Thompson inequality cannot be iterated over $n$ terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis $X_k^2\preceq A_k^2$ bounds squares, not the matrices themselves; it does not give $X_k\preceq A_k$, so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and $\preceq$ is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. $\lambda_{\max}$ is the supremum of the real spectrum, which is why $d\ge1$ is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by $k=1,\dots,n$, so $\mathcal F_{k-1}$ is never truncated. The bound $X_k^2\preceq A_k^2$ is required almost surely. The bounds $A_k$ are deterministic matrices. The infimum over $\theta>0$ in Proposition 3.1 is posed as the bound for each $\theta>0$ at which the expectation is finite.

The hypotheses must not be made vacuous. Integrability of each $X_k$ is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is $0$ and the centring hypothesis would say nothing. The $X_k$ are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.

Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given $X$ is replaced by the expectation over $\varepsilon$ at each fixed value $x$ with $x^2\preceq A^2$; by independence these agree. Corollary 7.2 adds the hypothesis that $Y_0$ is almost surely constant, without which $Y_n-\mathbb EY_n\neq\sum_kX_k$.

A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited version arXiv:1004.4389v7 (2011). https://arxiv.org/abs/1004.4389v7
• R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
• J. A. Tropp, Freedman's inequality for matrix martingales, Electron. Commun. Probab. 16 (2011) 262–270. https://arxiv.org/abs/1101.3039
• R. I. Oliveira, Concentration of the adjacency matrix and of the Laplacian in random graphs with independent edges, arXiv:0911.0600 (2010). https://arxiv.org/abs/0911.0600
• C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer (1998) 195–248. https://doi.org/10.1007/978-3-662-12788-9_6
• R. Bhatia, Matrix Analysis, Springer GTM 169 (1997), Sec. IX.3. https://doi.org/10.1007/978-1-4612-0653-8
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X

Motivation

In quantum mechanics the spectrum of a Hamiltonian splits into two parts that behave very differently under perturbation. Isolated eigenvalues of finite multiplicity (bound states) move, split or disappear when the operator is changed even slightly; the rest of the spectrum, which carries scattering states and accumulation points of eigenvalues, is far more rigid. Weyl's theorem makes this rigidity precise: if two self-adjoint operators have resolvents that differ by a compact operator, their essential spectra coincide. It is the standard first step in locating the spectrum of a Schrödinger operator $-\Delta + V$: one shows that $V$ is a relatively compact perturbation of $-\Delta$, concludes $\sigma_{ess}(-\Delta + V) = \sigma_{ess}(-\Delta) = [0,\infty)$, and is left with the discrete eigenvalues below zero.

The result goes back to H. Weyl's 1909 work on compact perturbations of bounded self-adjoint operators; the resolvent formulation for unbounded operators is the one used in modern texts such as Reed–Simon (Vol. IV, Sec. XIII.4) and Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Section 6.4, which this mission follows.

Setting

Let $\mathfrak H$ be a complex Hilbert space and $A$ a linear operator with domain $\mathfrak D(A) \subseteq \mathfrak H$. For $z \in \mathbb C$, the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $\mathfrak H$ with a bounded inverse. The resolvent set $\rho(A)$ is the set of such $z$, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$.

The discrete spectrum $\sigma_d(A)$ is the set of eigenvalues $z$ of $A$ that are isolated points of $\sigma(A)$ and whose eigenspace $\operatorname{Ker}(A - z)$ is finite dimensional. The essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$.

A sequence $\psi_n \in \mathfrak D(A)$ with $\|\psi_n\| = 1$, $\langle \varphi, \psi_n \rangle \to 0$ for every $\varphi$ (weak convergence to zero) and $\|(A - z)\psi_n\| \to 0$ is a singular Weyl sequence for $A$ at $z$.

An operator is compact if it maps bounded sets to relatively compact sets; $\mathfrak C(\mathfrak H)$ denotes the compact operators. An operator $K$ is relatively compact with respect to $A$ if $\mathfrak D(A) \subseteq \mathfrak D(K)$ and $K R_A(z) \in \mathfrak C(\mathfrak H)$ for one $z \in \rho(A)$. $B$ is $A$ bounded if $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\|B\psi\| \le a\|A\psi\| + b\|\psi\|$ on $\mathfrak D(A)$; the infimum of admissible $a$ is the $A$-bound. A symmetric operator $A$ has defect indices $d_\pm(A) = \dim \operatorname{Ran}(A \pm i)^\perp$.

Formalization targets

Goal: Weyl's theorem (Theorem 6.19)

For self-adjoint $A$ and $B$,

$$\exists\, z \in \rho(A) \cap \rho(B):\ R_A(z) - R_B(z) \in \mathfrak C(\mathfrak H) \quad\Longrightarrow\quad \sigma_{ess}(A) = \sigma_{ess}(B).$$

Milestones

• Weyl criterion (Lemma 6.17). For self-adjoint $A$: $z \in \sigma_{ess}(A)$ if and only if a singular Weyl sequence at $z$ exists; if so, it can be chosen orthonormal.
• Compact perturbations (Lemma 6.18). For self-adjoint $A$ and compact self-adjoint $K$, $\sigma_{ess}(A + K) = \sigma_{ess}(A)$, and

$$\sigma_{ess}(A) = \bigcap_{K \in \mathfrak C(\mathfrak H),\, K^* = K} \sigma(A + K).$$

• Independence of $z$ (Lemma 6.21, first part). If $R_A(z) - R_B(z)$ is compact for one $z \in \rho(A) \cap \rho(B)$, it is compact for all such $z$.
• Self-adjoint extensions (Theorem 6.20). If $A$ is symmetric with $d_+(A) = d_-(A) < \infty$, all self-adjoint extensions of $A$ have the same essential spectrum.
• Relative compactness is infinitesimal (Lemma 6.22). For self-adjoint $A$, a relatively compact $K$ has $A$-bound $0$.
• Stability of relative compactness (Lemma 6.23). If $A$ is self-adjoint, $B$ symmetric with $A$-bound less than one, and $K$ relatively compact with respect to $A$, then $K$ is relatively compact with respect to $A + B$.

Significance

The result. Weyl's theorem reduces the determination of the essential spectrum of a perturbed operator to that of a simpler reference operator. Combined with Lemma 6.22 and the Kato–Rellich theorem, it yields $\sigma_{ess}(A + K) = \sigma_{ess}(A)$ for every relatively compact symmetric $K$; Lemma 6.23 extends this to perturbations of the form $B + K$. These are the inputs to the HVZ theorem for $N$-body systems, to the spectral analysis of one-particle Schrödinger operators with decaying potentials, and, via Theorem 6.20, to the observation that boundary conditions at a limit-circle endpoint do not affect the essential spectrum of a Sturm–Liouville operator. The Weyl criterion is independently useful: it is how points are shown to lie in $\sigma_{ess}$ in concrete examples.

Formalizing it. The results are classical and proved in every text on the subject. None of them is formalized: Mathlib has compact operators and the adjoint of a densely defined LinearPMap, but no resolvent set or spectrum for unbounded operators, no discrete or essential spectrum and no relative compactness. This mission asks for formal proofs of Teschl's statements and, with them, a reusable layer of definitions (resolvent of a LinearPMap, $\sigma_d$, $\sigma_{ess}$, singular Weyl sequences, relative compactness) on which later chapters (free Schrödinger operator, HVZ theorem) can build.

Difficulty

The obvious route to all of these statements goes through the spectral theorem: Teschl's proof of the Weyl criterion uses spectral projections $P_A((\lambda - \varepsilon, \lambda + \varepsilon))$ and spectral measures $\mu_{\psi_n}$, and his characterization (6.27)–(6.28) of $\sigma_{ess}$ by ranks of spectral projections presupposes the functional calculus. Mathlib has no spectral theorem for unbounded self-adjoint operators, so this route requires either building it or finding arguments that avoid it. The definition of $\sigma_{ess}$ used here is deliberately the PVM-free one of p. 145, which makes the statements expressible now but moves the difficulty into the proofs: showing that a point of $\sigma(A) \setminus \sigma_d(A)$ carries a singular Weyl sequence requires controlling approximate eigenvectors near a non-isolated spectral point or an eigenvalue of infinite multiplicity without projections.

A second difficulty is domain bookkeeping. $A + K$, $A + B$, $K R_A(z)$ and $R_{A+B}(z)$ all involve unbounded operators with different domains, and identities such as the second resolvent formula $K R_{A+B}(z) = K R_A(z)(\mathbb I - B R_{A+B}(z))$ must be established on the correct domains. Theorem 6.20 requires relating the resolvents of two self-adjoint extensions through the finite-dimensional defect spaces.

Formalization scope

The Hilbert space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since no statement of the section needs it. Unbounded operators are Mathlib LinearPMaps H →ₗ.[ℂ] H, self-adjointness is Mathlib's IsSelfAdjoint (which implies a dense domain), and symmetric operators are densely defined by definition, as in the book. The resolvent is the bounded two-sided inverse of $A - z$ of p. 73 (IsResolventAt), and $\rho(A)$, $\sigma(A)$ are defined from it; Mathlib's Banach-algebra spectrum is not used. "For one $z \in \rho(A) \cap \rho(B)$" is an existential over $z$ and the two resolvents. Compactness is Mathlib's IsCompactOperator, which on a Hilbert space agrees with the book's norm closure of finite rank operators. $A + K$ for bounded $K$ is K +ᵥ A (domain $\mathfrak D(A)$); $A + B$ for unbounded $B$ is the LinearPMap sum with domain $\mathfrak D(A) \cap \mathfrak D(B)$. The $A$-bound is valued in $[0,\infty]$ and is $\infty$ for an operator that is not $A$ bounded. The defect indices are "equal and finite" when both defect spaces are finite dimensional with equal finrank.

No projection-valued measure or functional calculus is taken as data, and none is needed: every statement is phrased without $f(A)$. For this reason the second half of Lemma 6.21, $f(A) - f(B) \in \mathfrak C(\mathfrak H)$ for $f \in C_\infty(\mathbb R)$, and the form-compactness results Lemma 6.26 and Corollary 6.27 of Section 6.5 are not part of the mission.

A trivializing formalization is ruled out: the discrete spectrum requires all three of "eigenvalue", "isolated in $\sigma(A)$" and "finite-dimensional eigenspace", so $\sigma_{ess}$ is neither empty nor all of $\sigma(A)$ by definition, and the resolvent hypothesis of Weyl's theorem is an existential over genuine resolvents, never a junk value outside $\rho(A)$.

A complete development needs the resolvent identities for LinearPMaps, the relation between self-adjointness and real spectrum, weak convergence of bounded sequences, and the fact that compact operators map weakly null sequences to norm-null ones. The definitions of resolvent, $\sigma_{ess}$, relative compactness and $A$-bound are shared with other chapters of this series and are intended for reuse. Contributions of general lemmas on LinearPMap resolvents are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Section 6.4. https://doi.org/10.1090/gsm/099
• H. Weyl, Über beschränkte quadratische Formen, deren Differenz vollstetig ist, Rendiconti del Circolo Matematico di Palermo 27 (1909), 373–392. https://doi.org/10.1007/BF03019655
• M. Reed and B. Simon, Methods of Modern Mathematical Physics IV: Analysis of Operators, Academic Press, 1978, Section XIII.4.
• T. Kato, Perturbation Theory for Linear Operators, 2nd ed., Springer, 1980, Section IV.5. https://doi.org/10.1007/978-3-642-66282-9